An Algebra of Transformers

1 Introduction

• The motivation situates this work alongside theoretical analyses of transformer computability, parallelizability, and bounded-precision limitations.The passage notes transformers’ growing use in large language models, citing their parallelizability [1].Source: §1 · p. 4
• The paper introduces an algebra for reasoning about transformers based on their functional decomposition [5].The decomposition divides a transformer into atomic constructions operating on vectors or matrices.Source: §1 · p. 4
• The decomposition distinguishes atomic actions from guards, with truth values interpreted as 1 or 0 for Boolean functions and I or 0 for general vector or matrix operations.The actions and guards are denoted Act and Grd, respectively.Source: §1 · p. 5

2.1 Multiset

• Pomsets are equivalence classes of labelled posets, with sequential and parallel compositions that each admit unique factorizations.A multiset retains repeated elements, distinguishing {∣a,b,b∣} from {∣a,b∣}.Source: §2.1 · p. 6

2.2 Equational Logic

• Equational axioms generate equality through substitution, equivalence, and contexts, while term rewriting systems specify rules and their induced reductions.Terms may be open or closed, and rewriting is closed under substitution and contexts.Source: §2.2 · p. 7
• A terminating, weakly confluent term rewriting system reduces each term to a unique normal form; weak confluence is equivalent to convergence of all critical pairs.Knuth-Bendix completion adds rules to join right-hand sides arising from overlaps in rewrite-rule left-hand sides.Source: §2.2 · pp. 7–8

2.3 Pomset Labelled Transition System

• A pomset-labelled transition system models a state change by a pomset, with traditional single-action transitions as the primitive-pomset special case.A state may also satisfy or fail predicates.Source: §2.3 · pp. 8–9
• PLTSs are classified as finitely branching, regular, or finite by their outgoing transitions, reachable states, and infinite transition sequences.Regular systems are finitely branching and have finitely many reachable states per state; finite systems are finitely branching and have no infinite transition sequence.Source: §2.3 · p. 9
• Pomset transition system specifications are collections of inductive rules for deriving transitions, and pomset bisimulation relates processes that match each other's transitions.Positive specifications contain no negative premises.Source: §2.3 · p. 9

3 Basic Algebra for Transformers

• BAT combines pomsets, guards, deadlock 0, identity I, serial composition ○, and alternative composition +.Deadlock represents incomposable serial actions, which can result from vector or matrix dimension mismatches.Source: §3 · p. 11, §3.1 · p. 11

3.1 Axiomatic System

• The axiomatic system uses test(ϕ,s) to express guard truth, defines weakest-precondition predicates, and extends guards with basic-guard formation rules.The text states that test(I,s) holds while test(0,s) does not.Source: §3.1 · p. 11
• Every closed BAT term is provably equal to a basic BAT term.The proof uses a strongly normalizing rewrite system and shows that normal forms of closed terms are basic.Source: §3.1 · pp. 12–13

3.2 Operational Semantics

• The operational rules cover identity, atomic actions, pomsets, guards, serial composition, and alternative composition; U's successful termination is represented separately.The transition rules are given in Table 4.Source: §3.2 · p. 14, Table 4 · p. 14
• Pomset bisimulation equivalence is a congruence with respect to BAT, so equivalent terms remain equivalent under its operators.The stated proof basis is that BAT's transition system is positive after reduction and in panth format.Source: §3.2 · p. 14

3.3 Soundness and Completeness

• The axiomatization is sound and complete modulo pomset bisimulation: derivable equalities imply bisimilarity, and bisimilar closed terms are equal.Completeness reduces closed terms to basic terms and compares normal forms modulo associativity and commutativity of alternative composition.Source: §3.3 · pp. 14–15
• The section proves soundness by checking that each BAT axiom is sound modulo pomset bisimulation equivalence.The proof relies on bisimulation being both an equivalence and a congruent relation.Source: §3.3 · p. 14

4.1 Operational Semantics

• Pomset bisimulation equivalence is a congruence with respect to APT's parallel composition.The section introduces transition rules and axioms for parallelism.Source: §4.1 · p. 16, §4.2 · p. 16

4.2 Axiomatic System

• Every closed APT term is provably equal to a basic APT term, giving the algebra an elimination property.The proof uses a strongly normalizing rewriting system and establishes that closed-term normal forms are basic terms.Source: §4.2 · pp. 17–18

4.3 Soundness and Completeness

• APT is a generalization of BAT, and the section proves its axiomatization sound and complete modulo pomset bisimulation equivalence.For closed terms, bisimilarity implies equality; axiomatic equality implies bisimilarity for APT terms.Source: §4.3 · p. 19
• The completeness argument shows that bisimilar normal forms are equal modulo associativity and commutativity of conflict.It compares their summands and uses induction on the sizes of the normal forms.Source: §4.3 · p. 20

5 Recursion

• Recursion captures infinite computations through finite sets of recursive equations whose right-hand sides are process terms.The section distinguishes guarded and linear recursive specifications.Source: §5 · p. 21

5.1 Operational Semantics

• APT with guarded recursion is a conservative extension of APT, and pomset bisimulation equivalence remains a congruence.The transition rules for guarded recursion contain only a fresh constant in their source.Source: §5.1 · p. 22

5.2 Axiomatic System

• The recursive definition and specification principles follow from matching initial transitions and the uniqueness of solutions for guarded specifications.RDP follows from the transition rules; RSP follows from guarded specifications having only one solution.Source: §5.2 · pp. 22–23

5.3 Soundness and Completeness

• For closed APT terms with linear recursion, pomset bisimilarity implies equality.The completeness proof constructs a specification relating the recursive equations of the two processes.Source: §5.3 · p. 23

6 Abstraction

• The silent step τ and abstraction operator τI, for I ⊆ Act ∪ Grd, abstract internal transformer implementations so external behavior can be verified.I denotes internal events or guards.Source: §6 · p. 24

6.1 Silent Step

• The silent step τ represents internal actions, and τ steps can be removed when considering a process's external behavior.τ changes only the state of the internal data environment.Source: §6.1 · p. 24

6.1.1 Operational Semantics

• Guarded linear recursion excludes infinite sequences of internal I-transitions and τ-transitions, addressing the τ-loops possible under X = τX.The section identifies those loops as causing unfairness.Source: §6.1.1 · p. 25
• APT with silent step and guarded linear recursion is a conservative extension of APT with linear recursion.The added silent-step transition rules contain only a fresh constant τ in their source.Source: §6.1.1 · p. 25

6.1.3 Soundness and Completeness

• Rooted branching pomset bisimulation is a congruence, and the axiomatization is sound; for closed terms, bisimilarity implies equality.The axioms for the silent step are presented in Table 11.Source: §6.1.1 · p. 26, §6.1.3 · p. 26, §6.1.2 · p. 26

6.2 Abstraction

• The abstraction operator τI renames atomic events in I to τ, hiding internal actions when reasoning about external behavior.The section introduces axioms for τI and gives its transition rules.Source: §6.2 · p. 27, §6.2.1 · p. 28, §6.2.2 · p. 28

6.2.1 Operational Semantics

• APTτ with guarded linear recursion is a conservative extension of APT with silent step and guarded linear recursion.The abstraction rules add a fresh operator to their sources, preserving the existing transition rules.Source: §6.2.1 · p. 28
• Rooted branching pomset bisimulation equivalence is a congruence for APTτ with guarded linear recursion.The paper attributes this result to the reduced transition system being positive and in RBB cool format.Source: §6.2.1 · p. 28

6.2.3 Soundness and Completeness

• The axiomatic system is sound, and closed terms with CFAR that are rooted branching pomset bisimilar are equal.CFAR is sound modulo rooted branching pomset bisimulation; the completeness theorem applies to closed terms with guarded linear recursion and CFAR.Source: §6.2.3 · pp. 29–30
• Clusters group recursive variables connected through actions in I or τ, and CFAR supports fair abstraction when such clusters have exits.The paper introduces clusters and CFAR to address τ-loops that can be constructed using abstraction.Source: §6.2.3 · pp. 29–30

• The chapter applies APT to Most-Recent Induction, Dyck-1 recognition, and Dyck-1-2 recognition, establishing functional specifications and deriving external behavior by abstraction.It represents components using existing atomic constructions and establishes functional correctness from concrete computation before hiding internal actions.Source: §7 · p. 32

7.1.1 A Transformer Construction of the Most-Recent Induction

• The construction predicts the symbol following the most recent earlier occurrence of the current symbol, or the current symbol when no earlier occurrence exists.Rightmost selection chooses the largest matching candidate index.Source: §7.1 · p. 32, §7.1.1 · p. 33

7.1.2 Algebraic Representation

• The algebraic representation composes embedding, predecessor retrieval, induction retrieval, and unembedding actions to implement the prediction computation.The second layer uses content matching and rightmost selection; when there is no match, it returns the current-symbol embedding.Source: §7.1.2 · pp. 33–34

7.1.3 Verification of the Most-Recent Induction Transformer

• Abstraction hides configured internal actions while leaving input and output visible, yielding the required external behavior equation.The proof reduces seven sequential silent actions between input and output.Source: §7.1.3 · pp. 35–36
• For every input sequence, the transformer emits the Most-Recent Induction prediction sequence and returns to the input-waiting state.The prediction at each position is supported by predecessor and retrieval computations, including the no-match case.Source: §7.1.3 · p. 35

7.2 Verification of a Transformer for Dyck-1

• The construction is uniform, with parameters independent of input length, and computes recognition quantities rather than an internal binary acceptance bit.It is stated for nonempty inputs because it inspects the final-position representation; the empty string may be accepted separately by convention.Source: §7.2 · p. 36, §7.2.1 · p. 36

7.2.1 A Transformer Construction for Dyck-1

• The cited passage states an exact equivalence: a string belongs to Dyck-1 if and only if its numerical output, denoted oD, is the ordered pair (0,0).Source: §7.2.1 · p. 38
• The equality test on the emitted numerical result is external; the construction does not perform an internal comparison or Boolean classification.The output action emits a two-dimensional numerical result without performing the acceptance test.Source: §7.2.1 · p. 38, §7.2.2 · p. 40

7.2.2 Algebraic Representation

• The algebraic representation uses causal uniform averaging, residual connections, and a four-dimensional residual workspace, without positional embeddings or layer normalization.The first attention component computes prefix balance; the feed-forward component computes prefix error, and the second attention component computes its causal prefix average.Source: §7.2.2 · pp. 38–40

7.2.3 Verification of the Dyck-1 Transformer

• For a nonempty input string, the construction computes and emits its numerical result, then returns to the input-waiting state.The external behavior is derived after abstraction hides configured internal actions while preserving the input and output interfaces.Source: §7.2.3 · pp. 40–41

7.3 Verification of a Transformer for Dyck-1-2

• The section applies APT to a depth-two bracket-matching Transformer that maintains an active bit at every position and performs two rounds of nearest-neighbor matching.Its components are represented with existing APT atomic constructions before recursive process equations are abstracted.Source: §7.3 · p. 41

7.3.1 A Transformer Construction of Dyck-1-2

• For well-nested strings with one bracket type and maximum depth two, adjacent pairs are matched first, then nearest unmatched brackets; acceptance requires all active bits to be zero.The first round matches adjacent opening–closing pairs; the second searches for the nearest unmatched bracket on each side.Source: §7.3.1 · pp. 41–43

7.3.2 Algebraic Representation

• The algebraic representation initializes bracket, active-bit, and positional coordinates, retrieves neighboring brackets with attention, and uses feed-forward components to update active bits.The representation also includes an output action that emits the final active-bit sequence.Source: §7.3.2 · pp. 44, 46

7.3.3 Verification of the Dyck-1-2 Transformer

• The construction receives an input, emits its computed final active-bit sequence, and returns to its input-waiting process under abstraction.The theorem states the external behavior after internal actions are hidden.Source: §7.3.3 · pp. 47–48