42  x ∈ P(y)  ↔  y ∈ inv(P)(x)

42 — Related Work

Where 42 comes from and where it sits. It is the second instantiation of 4₂, specified in a 1993 thesis; this page traces what was already there, what it shares with Inv, PisoLang and the Π branch, what in it is new, and what the others have that it does not.

Where 42 sits in the literature on reversible programming, and what in it is actually new.

#0. The 1993 original

42 is not a new design. It is the second instantiation of a language first defined in 1991 and specified in a thesis two years later, and enough of the present one is already in that document that the comparisons below cannot be dated without it.

The source. P. G. M. Jansen, Reversible Programming in 4₂, Master's thesis, University of Amsterdam (study group Robotics and Artificial Intelligence), 1993; the research carried out at Philips Natuurkundig Laboratorium and IPO (Institute for Perception Research), Eindhoven. The language is called 4₂, and the preface credits it to two people:

The result was 4₂ (pronounce: forty-two), an imperative reversible programming language created by Joep Rous and Paul Jansen.

The dates. Two of them, and they are not the same. The language was first defined in 1991, inside Rosetta, and became a thesis topic afterwards; the thesis is from 1993 and is the only surviving document. The earlier date is Joep Rous's own recollection and is recorded here as that, not as something the thesis establishes. Where this page says "1993" it means the document, which is what every comparison below is actually dated against.

Where it came from. The motivation was machine translation, not reversible computing: the Rosetta project at Philips, and a formalism of "M-rules" for writing natural-language grammars that had to run in both directions: parse one way, generate the other. When Rosetta closed the language was generalised rather than abandoned. Bidirectionality was the requirement first, and reversible computation the frame applied afterwards.

That is about motivation only. The thesis was not working in ignorance of reversible computing: its bibliography cites Landauer (1961) and Bennett (1973) directly, alongside the program-inversion literature: Dijkstra's EWD671 (1978), Gries (1981), Gries & van de Snepscheut (1989), Chen & Udding (1990). §0.4 lists what was in view.

The name. From Douglas Adams. Deep Thought computes the answer, forty-two, and the question is lost; a successor machine has to be built to recover it.

The rationale of the name 4₂ then is: if Deep Thought would have made use of 4₂ it should have been able to compute the original question: besides generating the normal interpretation of a program, the 4₂ compiler generates automatically the inverse of a program as well.

#0.1 What is already there

The defining law, as numbered equation (2.2) of chapter 2:

∀s₁ ∈ S_left, s₂ ∈ S_right :  s₂ ∈ Π(s₁)  ⟺  s₁ ∈ Π⁻¹(s₂)

This formula says that every end state which is the result of a program execution in one direction, results in a set of states containing the original start state if it is executed in the other direction.

In 42 that same law is written x ∈ P(y) ⟺ y ∈ inv(P)(x), and glossed the same way: running forward and then backward returns a set containing where you started. Both the statement and the gloss are already 1993's.

The contravariance of inversion, as a definition rather than an implementation detail. An operator ⊙ is called syntactically reversible when

∀(R₁,…,Rₙ) ∈ D_⊙ :  (⊙(R₁,…,Rₙ))⁻¹ = ⊙(Rₙ⁻¹,…,R₁⁻¹)

A simple example of a syntactically reversible operator is the sequence operator ";". The inverse interpretation of the construct "R₁ ; R₂" is "R₂⁻¹ ; R₁⁻¹" which is exactly the same as reading the construct from right to left.

which is case Seq(s, u): return Seq(dagger(u), dagger(s)) in rel42/core.py.

Nondeterminism, accepted rather than excluded. From §3.1, on inverting a function applied to an uninstantiated argument:

The fact that the inverse function is a set containing possibly more than one value makes the whole process indeterministic.

and failure is emptiness, not error:

Failure of a transformer implies more or less that the environment of the transformer will produce an empty set of output states.

The operators. Sequence, union |, intersection &, repetition {R}, test R?, relation call, with the lineage named:

This enumeration defines the so called class of regular relations extended with an intersection operator and a possibility to do tests. In modal logic it resembles the system of Pratt as described in [Pratt80] and [Harel84].

So 42's ;, | and ^ are all 1993, | down to the character, and repetition is already reflexive-transitive closure — "the set of output states contains all states generated in between, including the original input state", with the backward asymmetry of pred^ versus succ^ noted in the same paragraph.

Decidable atoms and no complement. Atomic relations are defined by a formula of a decidable language (§2.2), and complement is deliberately absent:

the complement operator which corresponds with the logical negation at the level of complex relations is not implemented. The reason for this is the requirement of finiteness of result

Those are the two ingredients of the expressiveness theorem's soundness proof: decidable primitives, and only positive operators over them. The 1993 reason is not the 2026 reason: theirs is that a complement in an infinite universe is not finitely presentable, mine is that it leaves Σ⁰₁. Convergent instinct, different argument.

#0.2 What is not there

The point-free core. 4₂ is imperative, and says so. It has variables (topics, state variables, match variables) and its atomic construct is assignment-shaped, topic := t₁ ! t₂, with the two terms read in opposite orders depending on direction. There are no 0, 1, +, × primitives, no semiring isomorphisms, and nothing resembling a rig groupoid. §6's claim that 42's primitives are forced rather than chosen is therefore a claim about the second instantiation only, and must not be back-dated.

The ! did survive, but with a changed job: in 4₂ it separates the preterm from the postterm, marking where the two readings meet. In 42 it is the operator that swaps them.

#0.3 The open problem, and what 42 does with it

Having defined syntactic reversibility, the thesis finds its own constructs failing it. Of the conditional:

It is easy to see that the "IF-THEN" construct we described above is not syntactically reversible.

and of the boolean test, which is implemented by copying the state, evaluating, and returning the copy on success:

An awkward consequence of this particular evaluation is the loss of syntactical reversibility … The boolean operator "?" could be made syntactically reversible by allowing only the subclass of symmetrical programs of 4₂ in boolean tests. Whether we loose expressiveness by restricting boolean tests to symmetrical programs is still an open question.

42 is the language in which every operator is syntactically reversible, and that is what going point-free buys. There is no conditional to fail the property, because branching is +; and there is no test operator, because filtering is the composite copy ; (test * id) ; unitprod. That is the theorem's Lemma 7, and it is its own dagger for any test, with no restriction to symmetrical programs:

$ 42 theorem keep "R ()"
keep(R ()) =
  R ()
  -- 1 result
$ 42 theorem keepd "R ()"
keepd(R ()) =
  R ()
  -- 1 result

The expressiveness half of the 1993 question is settled by the theorem's Theorem 12: filters of exactly this shape reach every r.e. subset, so nothing is lost by having no primitive test at all. Intersection goes the same way: 4₂'s & is copy ; (f * g) ; copy!, running both and insisting the answers agree, so the operator was absorbed rather than dropped.

Because dagger is total on every construct, ! can be eliminated at parse time, which is the syntactic form of the 1993 property:

parse("(copy ; join)!")  ==  parse("join! ; copy!")

#0.4 What was in view in 1993

The thesis's bibliography answers a question this document would otherwise have to guess at: what a designer in 1993 could see. Five groups.

Notably absent: Lutz & Derby's Janus (1986). It was invisible until Yokoyama & Glück revived it in 2007, and its absence here is direct evidence of that.

And one entry that is not a source but a plan, the last one alphabetically before Schmidt:

Rous, J. and Jansen, P.G.M., Reversible Programming in 4₂, forthcoming.

That is the thesis's own title, under two names instead of one. The bibliography contains a forward reference to the paper the thesis was meant to become: same work, joint authorship, submitted nowhere. It did not appear.

#0.5 A note on citing this

The thesis exists on paper only. Every other quotation in this document is checked against a machine-readable copy of its source; the ones in §0 cannot be, because there is no such copy. They were transcribed by hand from page images, and should be treated as hand-transcribed.

What has been read is the preface, chapters 2 and 3.1–3.5, and the bibliography. Chapters 4 and 5, which carry the formal syntax and semantics, have not.

#1. The axis everything sits on

Every language here can be placed by how many answers running backwards may give:

Setting|P(y)|Languages
Groupoid — total bijectionsexactly 1Π; Q42 (unitaries)
PInj — partial injections≤ 1Janus, Theseus, RFUN, Inv, Chardonnet et al., PisoLang
Rel — relationsarbitrary42

The middle row holds almost every language in the field. Reversible languages are, with near-unanimity, injective languages; they differ in surface syntax and in how injectivity is enforced rather than in what they denote.

42's position is the bottom row, and its thesis is that the bottom row has the simpler metatheory. Q42 is the top row, and reaches it by changing the semiring rather than by adding restrictions.

#2. Inv — the nearest relative

Mu, Hu & Takeichi, An Injective Language for Reversible Computation, MPC 2004.

Inv is 42's closest predecessor. PisoLang's related-work section describes it as follows:

Mu et al. present Inv, an injective language for reversible computation formulated in a point-free, combinator-style functional setting with a relational semantics.

Which is 42's design space, described by someone else, in 2004. Inv is a point-free functional language with a relational semantics in which only injective functions are definable; non-injective computations are accommodated by returning a history, and it is computationally equivalent to Bennett's reversible Turing machines.

The defining law is the same equation. Inv, §2:

The converse of a relation R, written R°, is obtained by swapping the pairs in R. That is, (b, a) ∈ R° ≡ (a, b) ∈ R.

42:

x ∈ P(y) ⟺ y ∈ inv(P)(x)

These are the same statement. 42's law is a restatement of the converse of a relation, not a new formulation.

The inversion rules are the same rules. Inv gives:

(f ; g)° = g° ; f°        (f × g)° = f° × g°
(f ∪ g)° = f° ∪ g°        (µF)°    = µ(° ; F ; °)

and 42's dagger is, line for line:

case Seq(s, u):   return Seq(dagger(u), dagger(s))
case Prod(s, u):  return Prod(dagger(s), dagger(u))
case Union(s, u): return Union(dagger(s), dagger(u))
case Ref(n, i):   return Ref(n, not i)

copy/copy! is dup/eq, and the observation about them is the same observation. Inv, §2:

dup° = fst ∩ snd. Given a pair, fst extracts its first component, while snd extracts the second. The intersection means that the results have to be equal. That is, dup° takes a pair and lets it go through only if the two components are equal. That explains the observation that to "undo" a duplication, we have to perform an equality test.

42's primitive table: "copy, the diagonal a → a×a; its converse is the partial 'these agree'." The fact and its framing are Inv's, from 2004.

Three languages solve it three ways, and the third is the most ingenious. Inv has dup and eq as separate constructs with eq = dup°. 42 has one primitive copy whose dagger is partial. RFUN has one operator ⌊·⌋ that is total and self-inverse, because it answers the equality question in the arity of its result:

⌊⟨x⟩⌋    =  ⟨x, x⟩
⌊⟨x, y⟩⌋ =  ⟨x⟩      if x = y
            ⟨x, y⟩   if x ≠ y

Thus, if the input is a binary tuple we can discern from the arity of the result tuple whether the arguments were equal or not; and if the input is a unary tuple, the result is a duplication of the value.

RFUN pays no partiality at all here, where 42 pays it in copy! and Inv in eq. That is worth recording as a case where the injective setting produces the neater construct rather than the clumsier one.

Where 42 differs from Inv. Three differences. The first two are trade-offs in expressiveness; the third is the one §6 claims as new.

  1. Inv restricts to injective functions; 42 does not. Inv's whole discipline is "injectivity by construction": the problematic constructs of its ambient language Fun (constant functions, fst, snd, the split) are replaced by more structured ones. 42 admits the whole of Rel and takes the many-valued dagger as a feature.
  2. Inv's dup/eq are parameterised families; 42's copy is one primitive. Inv's dup :: (Fa → a) → Fa → (Fa × a) takes a selector argument, and Inv also has a primitive neq. In 42 selection is done by composition and there is no inequality test at all, which is simpler and less expressive.
  3. Inv's primitive set is chosen; 42's is forced. Inv has swap, assocr,

dup, eq, neq, and constructors succ | cons; assocl is derived rather than primitive. Its core carries no coproduct, no dist and no unit isomorphisms. Sum types arrive only in §6, as inl/inr/unit/in introduced for the history-logging translation, with the core deferring them ("some more operators will be introduced in sections to come to deal with the sum type, trees, etc."). 42's primitives are exactly the isomorphisms witnessing the commutative-semiring structure of (0, 1, +, ×), which is to say a rig groupoid presentation, which is to say Π. That is what makes the primitive table forced rather than curated, and it is what makes the Q42 extension of §5 possible: Inv cannot be taken to ℂ by the same route, because the rig structure the two new generators attach to is not present in its core.

#3. The disjointness condition, six ways

The same condition appears in six languages here and is discharged six different ways, which locates 42 more precisely than any other single comparison.

Inv, §4 — assumed, and flagged as unexplored:

An extra restriction needs to be imposed on union. To preserve reversibility, in f ∪ g we require not only the domains, but the ranges of f and g, to be disjoint. The disjointness may be checked by a type system, but we have not explored this possibility.

The condition costs Inv a primitive. Its inequality test neq p₁ p₂ is a partial function that lets (x, y) through only when p₁ x ≠ p₂ y, and its stated purpose is that "it is sometimes necessary for ensuring the disjointness of the two branches of a union." So one of Inv's twelve constructs exists to discharge a proviso 42 does not have.

PisoLang, I-Case — the same condition, now statically checked. Its typing rule for a case-expression carries two premises beyond the types:

∀i ≠ j,  pᵢ ⊥ pⱼ        (the patterns do not overlap)
∀i ≠ j,  eᵢ ⊥ eⱼ        (the output expressions do not overlap either)

with orthogonality defined as p₁ ⊥ p₂ ⇔ σ(p₁) ≠ σ(p₂) for every substitution σ, decided by unification: the type system Mu et al. left unexplored.

Theseus — the same condition, on both sides, as the language's only rule. §3.1 states it as the single constraint a programmer must maintain:

Non-overlapping and exhaustive coverage in pattern clauses. The collections of patterns in the left-hand side (LHS) of each clause must be a complete non-overlapping covering of the input type. Similarly, the collections of patterns in the right-hand side (RHS) of each clause must also be a complete non-overlapping covering of the return type.

Chardonnet, Lemonnier & Valiron — the same condition again, with exhaustivity dropped. Non-overlap is kept and made formal as an orthogonality relation v₁ ⊥ v₂ decided structurally, appearing as two premises ∀i ≠ j, vᵢ ⊥ vⱼ and ∀i ≠ j, eᵢ ⊥ eⱼ in the typing rule for an iso; exhaustivity goes, deliberately, "in order to allow non-terminating behaviour". So within one lineage the condition survives on both sides while totality is given up, which is a useful data point for how load-bearing each half is.

RFUN — the same condition, relaxed into an ordering. Thomsen & Axelsen name it as one of the two ways irreversibility enters their irreversible source language:

Non-orthogonality of case-branches. Slightly more subtle is the issue that case branches may be non-orthogonal: the result might conceivable have come from several branches, i.e., match several of the left-expressions terminating the case branches. This is the functional variant of the problem of the general irreversibility of if-then-else constructs.

and RFUN's answer is not to forbid overlap but to order it:

A first match policy for case branches. The result of a case-expression branch may match several terminating left-expressions, but it must never match a branch that textually precedes it.

which is a third option: neither assumed nor statically decided, but made harmless by fixing which branch wins. Note the connection RFUN draws and Theseus draws independently: this is if-then-else, and it is the same construct the 1993 thesis found violating its own definition of syntactic reversibility (§0.3). Four languages, one conditional.

Janus — the same condition, discharged by the programmer. Yokoyama & Glück formalise the language and are exact about the mechanism:

A reversible conditional has two predicates: the predicate after if is the test, and that after fi is the assertion. If the test is true, the then-branch is executed and afterward the assertion must be true; if it is false, the conditional is undefined. … The assertion makes the conditional reversible.

The loop is symmetric, and the cost is stated as plainly: "If the assertion does not have the required value, execution of the loop is undefined." So Janus does not decide the condition, nor assume it, nor order it. It obliges the programmer to supply a predicate that makes backward flow deterministic, and undefines the program when the predicate is wrong.

One further point is sharper than the usual summary of Janus allows, and it bears directly on §6. Janus does not require its operations to be injective:

The evaluation of expressions is not backward deterministic because function [[⊙]] is not injective, and thus there exists no inverse. As we shall see, this does not harm the backward and forward determinism of Janus statements.

Injectivity is demanded of statements, not of the arithmetic, and the syntactic restriction that x may not occur in the right-hand side of x ⊕= e is what buys it. Janus and 42 therefore agree that non-injective operations are admissible and disagree about where to pay for them: Janus pays in a restriction on assignment plus an assertion per conditional, 42 pays in the ∈.

42 has no such condition. join! keeps both branches, so nothing needs to be disjoint, and dagger is total with no side conditions, no well-formedness checks, and no proof obligations. The price is paid in exactly one place: the ∈ in the defining law, which is to say that forward-then-backward returns a set containing where you started rather than where you started.

Stated as a progression, and now datable: dropped (4₂, 1993) → assumed (Inv, 2004) → made the only rule (Theseus, 2014) → kept but shorn of exhaustivity (Chardonnet et al., 2024) → checked statically (PisoLang, 2026). That is not the order of a fix being found; it is three different answers, and the earliest is the one that declines the question. §0 gives the 1993 evidence: the defining law is stated there with the ∈ already in it, and nondeterminism is called a consequence to be accepted rather than a condition to be excluded.

This is a claim about the design space, not a claim of superiority. Inv and PisoLang want injectivity and must therefore pay for it; 4₂ and 42 want something weaker and do not.

#4. PisoLang

Onodera, Nakano, Asada & Kikuchi, PisoLang: a User-Friendly Reversible Programming Language with Inductive Types, RC 2026. Implementation: github.com/42067/reversible_lang.

An ML-style surface language over the reversible core calculus of Chardonnet, Lemonnier & Valiron, itself descended from Theseus. Its goal is usability, and the surface language supplies it: algebraic data types with user-defined constructors, OCaml-style pattern matching, Hindley–Milner inference so functions are polymorphic by default, higher-order functions over isos, nested patterns and nested applications elaborated to an invertible let-normal form.

Its add is 42's padding trick, arrived at independently:

The function add … takes two natural numbers m and n and returns a pair (m + n, n) in order to make the function injective.

42 makes the same trade in mul : (m, n) → (n, m×n), where keeping the multiplier costs one component and buys injectivity. Same move, same reason.

Where 42's generality earns something. Beyond the disjointness condition of §3:

(case True ↔ ()) False is well-typed but stuck, so progress does not hold. In 42 that term denotes ∅, a legitimate morphism of Rel, and there is no theorem to weaken. In 42, partiality is not failure, which is the same point.

Where PisoLang is more expressive.

42 closes part of this with parameterised definitions: def ctrl m = mat ; (id + m) ; mat! is inferred as (a <-> a) -> (qubit x a <-> qubit x a) with no annotation. Two differences remain. 42's is deliberately second-order: a parameter denotes a relation, never another combinator, where PisoLang's T₁ → T₂ nests freely. And 42's inversion convention differs: PisoLang fixes variables under inversion (ϕ⁻¹ := ϕ) and inverts an application's argument, while 42 flips the variable and leaves the argument alone. Either way it is a matched pair, but 42 needs its version because ! is eliminated at parse time, so a variable without its own flag would make m! and m parse identically.

On map, this document was wrong, and the truth is more specific. It is not that a parameter cannot be applied to a list. map is writable and well-typed in 42: a list is already a sum, so the sum functor does the case split with no plumbing at all:

def map f = id + (f * map f)

inferred as (a <-> b) -> (mu X. c + a x X <-> mu Y. c + b x Y), which is (a <-> b) -> (list a <-> list b), the very scheme PisoLang's map has. Its dagger is computed correctly too: 42 show prints map! not for the inverse of map not.

What fails is evaluation, and for a reason that is about the elimination strategy rather than about types or arity. Parameterised definitions are removed by substitution before evaluation, which is what expand does and why neither evaluator has a case for an application, and a recursive combinator has no finite expansion. Running map not reports application depth exhausted; is a combinator recursive?, and raising the limit does not help, because the divergence is in the expansion and so independent of the input.

So the honest statement of the gap: 42 admits recursive combinators in its type system and rejects them in its reduction strategy. Interpreting App rather than expanding it away would close this, and nothing in the type system stands in the way.

type 'a list = Nil | Cons of 'a * 'a list. Because Z and Nil are different constructors, the ambiguity that 42 addresses with type-directed printing cannot arise.

The type systems, side by side. 42's checker is close enough in kind to invite direct comparison:

PisoLang42
Algorithmalgorithm W, constraints + unificationthe same
Recursive typesnominal, user-declared, standard occurs checkinferred equirecursive, no occurs check
Inversionan Inverted type former, normalised during unificationScheme.swap() at the point of use
Annotationsnone required, but types are declarednothing is written at all
Verifiedno — "the algorithm for type inference needs to be verified"no

The inversion row records a simplification specific to the point-free setting. PisoLang's unify_type must handle cases like Inverted i, BiArrow{a,b} → (i, BiArrow{b,a}), because inv ω is a term whose type must be deferred. In 42, ! is eliminated at parse time, so inversion never enters the type language.

The recursion row is the conventional choice against an unconventional one and neither is better. Theirs means the programmer writes type nat = Z | S of nat; 42's means nobody writes anything and μX. 1 + X appears because unification closed a loop.

#5. The Π branch, and Q42

#5.0 Π, exactly

A second line descends from Theseus. James & Sabry's Π is a reversible language whose terms are the isomorphisms witnessing a commutative-semiring structure, which is 42's primitive table, arrived at independently. Two things need saying precisely, because the loose version of this claim is wrong.

Which Π. Information Effects (POPL 2012) gives Π with

value types, b ::= 1 | b + b | b × b

— no 0, and six isomorphism pairs: swap+, assocl+/assocr+, unite/uniti, swap×, assocl×/assocr×, distrib/factor. The zero arrives with Πo, whose table is given in full in Theseus §2: types 0 | 1 | b + b | b ∗ b | x | µx.b, and additionally zeroe/zeroi : 0 + b ↔ b, distrib0/factor0 : 0 ∗ b ↔ 0, and fold/unfold. Of that presentation Theseus says exactly what this document has been saying of 42:

Collectively the isomorphisms state that the structure (b, +, 0, ∗, 1) is a commutative semiring.

The correspondence, term by term. Against Πo:

Πo42
zeroe/zeroi, swap+, assocl+/assocr+unitsum, swapsum, assocsum
unite/uniti, swap∗, assocl∗/assocr∗unitprod, swapprod, assocprod
distrib/factordist
distrib0/factor0 : 0 ∗ b ↔ 0absent — 0 × a is uninhabited, so it is extensionally zero
fold/unfoldabsent — types are equirecursive, so there is nothing to write
id, sym, #, +, ∗id, !, ;, +, *
trace—
—zero, inl, inr, copy, join, |, ^

Two rows are the whole difference. fold/unfold are the isorecursive tax 42 does not pay. And the last row is 42 leaving the groupoid.

The last row is not arbitrary. Information Effects §3.1, having listed the isomorphisms, names the two identities that are not among them:

b × b            ↮   b
b1 + (b2 × b3)   ↮   (b1 + b2) × (b1 + b3)

and 42's two extra primitives are witnesses for precisely the first of these and its dual: copy : a ↔ a × a and join : a + a ↔ a. What is more, Π does recover both, but only in the arrow metalanguage MLΠ, as information effects built from create and erase. clone is Lemma 7.2 there; join is defined as

We define an operator join : b + b ⇝ b that takes a value of type b tagged by either left and right and removes the tag. The definition converts the input b + b to (1 + 1) × b and then erases the first component.

So the position is sharp, and it is the same one §3 reaches from the other direction: what Π must treat as an effect, requiring a type-and-effect system and a metalanguage, 42 has as a primitive, because in Rel those two morphisms are morphisms, and the price is paid once, in the ∈ of the defining law, rather than per-use in an effect system.

#5.1 √Π and the quantum branch

Carette, Heunen, Kaarsgaard & Sabry, √Π (POPL 2024), prove that a rig groupoid extended with two maps and three equations is computationally universal for quantum computing, and equationally sound and complete for Clifford, ≤2-qubit Clifford+T, and Gaussian Clifford+T. The maps are an 8th root of the identity on the unit and a square root of the symmetry on 1 + 1. Q42 is 42 taken to ℂ along exactly this route, and q42/ implements it.

#5.2 Two routes from a rig groupoid to quantum

The Quantum Effect is the other half of this branch, by overlapping authors, and it reaches universal quantum computation from Π by a completely different road than √Π does. Setting the two side by side is the sharpest thing this document can say about where Q42 sits.

QuantumΠ layers effects. It takes two copies of Π, Π_Z and Π_φ, rotated with respect to each other, amalgamates them with an arrow so their expressions interleave, layers a second arrow introducing a state zero and an effect assertZero, and then imposes the complementarity equation. The payoff is their canonicity theorem: satisfying the classical-structure laws, the execution laws and complementarity is enough to force computational universality. The The argument is short: arr_φ swap+ must be involutive, being the lifting of a symmetry, which rules out SH and leaves Hadamard.

Q42 changes the semiring. One copy, no arrows, no imposed equation: reinterpret the same terms over ℂ instead of 𝔹 and adjoin √Π's two generators.

Three consequences of the difference are worth recording.

One item of their future work is directly Q42's territory: extending QuantumΠ from finite Π to Πo with a trace operator, which they judge "would require answering fundamental open questions about the nature of infinite-dimensional quantum computation". Q42 meets the same wall from the other side and gets a sharper, more elementary statement of it: closure is a least fixed point wanting 1 + 1 = 1, so it cannot survive the move to ℂ at all.

#5.3 Control and the rig structure are the same thing

One rig to control them all answers a question this document had been posing loosely, whether Q42's ctrl should be primitive or derived, and the answer is that the question dissolves. Heunen, Kaarsgaard and Lemonnier give seven equations for control (not eight, as this document previously said from its abstract), and prove that adding them to a prop of base circuits constructs the free rig category on that prop. Their title claim, stated in the introduction:

These results also substantiate the claim in the title, that rig structure encapsulates controlled computation, and only controlled computation. Thus rig categories form the bare minimum model of computation: the ability to compose instructions sequentially (with ∘), to consider data in parallel (with ⊗), and to use one piece of data to condition computations on another (using ⊕).

So control and rig structure are interderivable, and 42 and their construction are the two directions of one correspondence. 42 takes the rig structure as primitive, which is what its primitive table is, and derives ctrl from dist in one parameterised definition. They take control as the added theory and derive the rig. Neither is more fundamental; what differs is which end you build from.

Two consequences are worth carrying into Q42's paper.

Their Theorem 27 is about Q42's generators. Taking the prop generated by ω : 0 → 0, V : 1 → 1 and S : 1 → 1 with ω⁸ = id, V⁴ = id and SVS = VSV, forming its controlled prop and quotienting by S = ω², they obtain soundness and completeness for Clifford, ≤2-qubit Clifford+T and Gaussian Clifford+T: the same three fragments √Π covers, and the same generators q42/ implements. Their proof notes that √Π's results needed only ω⁸ = id, V² = γ₁,₁ and SVS = VSV, "as well as the axioms of rig categories, which are implied by the control equations". Q42 has those axioms as primitives, so it sits on the other side of that implication.

There is a no-go theorem, and 42's parameters step around it. They note that "there is no quantum circuit implementation of a controlled unitary where the unitary is a black box input", and that physical implementations bypass it by identifying subspaces with auxiliary dimensions. Q42's ctrl is not troubled by this, and the reason is a design decision made for unrelated motives: a parameter in 42 denotes a term, not a value, and applications are eliminated by substitution before evaluation (§4). ctrl m never receives a black box; it receives syntax, and expands. The second-order restriction that §7 records as a limitation is what keeps ctrl on the right side of a no-go theorem.

Their future work also touches Q42's: the control equations "implicitly assume only two possibilities on each wire" and they ask about qutrits, which is QMANUAL §9.4's register-width question from the other direction, since 1 + (1 + 1) is a perfectly good Q42 type and a perfectly bad qubit register.

Note that Lemonnier appears on both branches, as an author of PisoLang's semantic basis and of One rig, so the two lines are not as separate as their citation graphs suggest.

PisoLang has no quantum content, so §4's comparison and this section concern disjoint parts of the design space.

#6. What is actually new in 42

§2 and §3 establish that much of 42 is not new. This section separates the remainder.

Not new. The point-free relational setting; the defining law x ∈ P(y) ⟺ y ∈ inv(P)(x); the contravariant inversion rules; the observation that undoing duplication is an equality test; the padding trick for injectivity. All of this is Inv (2004), and some is older.

New, or at least not found elsewhere:

  1. Making every operator syntactically reversible, so that the metatheory is simpler rather than more complicated: dagger is total, needs no side conditions, and satisfies dagger(dagger(t)) == t syntactically. Be careful what is being claimed. Dropping the disjointness condition is 1993, not new here, and neither is the property itself, which has been named independently at least three times:
nameformulation
4₂, 1993syntactic reversibility(⊙(R₁,…,Rₙ))⁻¹ = ⊙(Rₙ⁻¹,…,R₁⁻¹)
Janus, 2007local invertibility"for any given program unit the inversion can always produce an inverse unit"
Theseus, 2014syntactic reversibilitythe inverse reading coincides with the inverse meaning

All three give sequential composition as the worked example and all three get the contravariant law: Janus as (s₁ s₂)˘ ∼ s̆₂ s̆₁, 4₂ and Theseus as the displayed equation. Where they differ is what it costs to hold it everywhere. Janus holds it, and pays with a programmer-supplied assertion on every conditional, undefining the program when the assertion is wrong. Theseus does not hold it: its own conditional and its own boolean test fail, and the repair is left open. 4₂ does not hold it either, for the same reason. What is new is holding the property everywhere without either price: no assertion for the programmer to discharge, and no construct excluded. Going point-free is the repair. There is no conditional, because branching is +, and there is no test operator, because filtering is a composite of copy. The README states the consequence as "dropping restrictions is what buys the elegance here". The claim is about metatheory, not expressive power.

  1. A primitive set that is forced rather than chosen. Inv's primitives are curated; 42's are the semiring isomorphisms and nothing else, with copy and

join named as precisely the two morphisms that make the setting Rel rather than a groupoid. The generating set coinciding with Π's is evidence it is the right one. Unlike (1) this cannot be back-dated: 4₂ is imperative and has no such primitives (§0.2).

  1. Equirecursive types inferred rather than declared, with the occurs-check failure read as a diagnosis: μX. F(X) is admitted when F(0) is inhabited and rejected when it is not. (inr!)^ is therefore accepted at

mu X. a + X, which is nat when a = 1, while copy^ is rejected, with the occurs check reported as the reason: X would have to equal X x X. No language here does this; all of them declare their inductive types.

  1. The quantum extension being a semiring change rather than a new language.

q42/ shares Value, Term, dagger, the parser and the entire type-inference engine with rel42/; only the primitive table and the evaluator differ. q42/classical.42 runs under both interpreters unmodified. This is a consequence of (2): the rig structure is what the two generators attach to.

Caveat on (1). Inv, PisoLang, Theseus and RFUN all want injectivity, and pay for it deliberately. 42 wants something weaker, so it is not paying a cost they failed to avoid. The right claim is that the weaker setting is underexplored and better behaved, not that the others made a mistake.

#7. What 42 lacks that the others have

Theseus does not, and this document said otherwise until the paper was read. Its parametrised maps look higher-order and are not:

This parametrization should be thought of as a macro or a meta-language construction. Theseus does not have high-order maps in the formal sense. In other words, the final type of a Theseus program must be of the form a ↔ b and every occurrence of an arrow type → must be instantiated at compile time.

While parametrized maps add tremendous programming convenience to Theseus, they don't change the expressive power of the language. All programs expressible with parametrized maps, can be expressed without them by fully inlining the actual parameters.

RFUN does not either, and says so in the same words. Its functional parameters are described as "not enough to make functions first class citizens", yet "sufficient to implement certain very useful higher-order functions such as (reversible) map".

So three languages, Theseus, RFUN and 42, independently chose second-order parameters and independently described them as not-first-class. The gap in this row is against PisoLang and Chardonnet et al. only. What separates 42 from the other two is narrower and is stated in §4: all three admit map, but 42 eliminates parameters by substitution and so cannot run a recursive combinator, while RFUN and Theseus interpret theirs.

drop : C <-> 1 is definable in 42, at every type, though it is not a primitive. Theseus lists exactly that program as ill-formed. Its §3.1 gives drop_var, in which a bound n is not used on the other side, as one of four examples of invalid expressions, alongside dup_var, which uses one twice. Both are enforced by its second rule, that each variable "must appear exactly once on the other side and with the same type". 42 has no variables and so no such rule, and gets copy and drop as ordinary morphisms. Whether that is a gap or a feature is the whole argument of §6, but it is certainly a difference in what the language will refuse to accept.

type list a = mu X. 1 + (a x X), are abbreviations over those structural types rather than new types. The difference is not only notational: because Z and Nil are distinct constructors in PisoLang, the 0/[] ambiguity that 42 handles by type-directed printing does not arise there at all.

.GT., .GE., .LE. and a negation available inside boolean tests; 42 has only copy!, to filter on two values agreeing, and no way to filter on their differing. This one is less of a gap than it looks, since neq is there largely to establish the disjointness 42 does not require (§3), but the expressiveness difference is real and worth checking rather than assuming away.

A note on which completeness theorem applies. The result the neighbouring languages prove is Axelsen & Glück's: reversible Turing machines compute exactly the injective computable functions. That is the right statement for a language whose terms denote injections, and it is the wrong shape for 42, whose terms denote relations. The statement proved in the expressiveness theorem is a characterisation rather than a lower bound:

a relation R ⊆ A × B is denotable in 42 iff R is recursively enumerable

with ordinary Turing completeness as the single-valued case. Two things about it bear on this document's comparisons.

The soundness half is an induction over terms: the r.e. relations are closed under composition, union, product, sum, converse and reflexive-transitive closure, which is the whole of 42's syntax, and nothing in the language forms a complement, so the denotations cannot leave Σ⁰₁. The converse clause, which an injective language has to argue for, is free here: 42's total dagger and the class of r.e. relations have the same closure properties. That correspondence is the same fact §2 and §3 keep circling: dropping the disjointness condition is what lets the semantic class be one that is already closed under the operation the language is built around.

That shape is not hypothetical: Chardonnet, Lemonnier & Valiron prove exactly the injective version, and say so in those words:

we showed that for any computable function f from PInj, there exists an iso whose semantics is f, thus our language fully characterises all of the computable morphisms in PInj.

Read side by side, their theorem and Theorem 14 here are the same statement in two different categories: every computable morphism of the ambient category is denotable, with PInj there and Rel here. That is the cleanest way to put what 42 changes: not the theorem, the category.

The completeness half is where 42's extra generality is visibly cheaper than the neighbours'. The proof guesses the output and checks it, and both halves of that come from constructions the language already had rather than from anything added for the proof: the guess is drop_A ; drop_B!, and the check is copy. An injective language cannot write the guess at all.

#8. The backend axis

Every section above compares semantics. This one compares what happens after the semantics: whether a language reaches a machine. Two of the languages here were designed with a compilation target in view, so the axis is a real one, and it is where 42 is furthest behind.

None of these papers was read for this document; the descriptions come from general knowledge of the field and must be checked before any of it is repeated in print. The claims made here concern only shape: which layers exist, and which systems occupy them.

#8.1 Reversible classical: a complete stack, since 2011

The Janus lineage goes all the way to silicon:

  Janus  ->  RIL / RSSA  ->  PISA  ->  Pendulum
  (1986)     (Axelsen)      (ISA)     (a reversible processor)

Janus (Lutz & Derby 1986; semantics and inverter by Yokoyama & Glück, PEPM 2007) compiles through Axelsen's reversible intermediate languages to PISA, the Pendulum Instruction Set Architecture, and PISA was implemented in Vieri's adiabatic reversible processor at MIT (1999). ROOPL (Haulund) reaches PISA from a reversible object-oriented language; Hermes (Mogensen) compiles a reversible language for cryptographic primitives down to C.

The paper to read first, if 42 ever grows a compiler, is Axelsen's Clean Translation of an Imperative Reversible Programming Language (CC 2011). Its subject is the obligation that makes reversible compilation different from ordinary compilation: each translation step must itself be reversible, or the compiler destroys the property it exists to preserve. That constraint applies to 42 exactly as written, and it is not a constraint 42's design has yet been tested against.

PISA is a classical reversible ISA, valued in 𝔹, the semiring in which 42 is interpreted (§1). The natural compilation target for 42, as distinct from Q42, is therefore this branch rather than quantum hardware.

#8.2 Quantum: the stack is standardised, but the front ends are not languages

layerwhat occupies it
front endQiskit, Cirq, pyQuil, Q#, Guppy
IROpenQASM 3, QIR (LLVM-based)
optimiser / routertket, Qiskit's transpiler, VOQC (formally verified)
devicesuperconducting and trapped-ion hardware

The asymmetry is the point. The lower three layers are mature, shared and vendor-neutral; anything that can produce OpenQASM 3 or QIR inherits routing and gate synthesis for free. The top layer is mostly circuit-assembly libraries embedded in Python rather than languages with a semantics. Q# is the clearest exception, and reaches hardware through QIR.

Two front ends are relevant here for opposite reasons. Quipper (Green, Lumsdaine, Ross, Selinger, Valiron, PLDI 2013) is a real circuit-generating toolchain, aimed at resource estimation more than at a chip. Guppy (Quantinuum) exists to expose precisely what Q42 declines to have: mid-circuit measurement with real-time classical feedback. It is the shape of language you get when the hardware's capabilities, rather than a semantics, set the design.

#8.3 The Π lineage has no backend at all

Π, √Π, Theseus, RFUN, PisoLang, Inv: none emits anything executable on hardware. They are calculi with interpreters and, in the best cases, mechanised proofs. √Π's relation to Clifford+T is a completeness theorem, not a code generator.

The nearest thing to a bridge is Qunity (Voichick, Li, Rand & Hicks, POPL 2023), which is close to Q42 in spirit, being a unified quantum/classical language built on sums and products, and which describes a compilation procedure down to circuits — which is the closest any of them comes. Silq (Bichsel, Baader, Gehr & Vechev, PLDI 2020) is aimed elsewhere. Its contribution is what it says it is:

the first quantum language that addresses this challenge by supporting safe, automatic uncomputation

which is a language-design result, not a path to a device.

So the position 42 and Q42 are in is the normal position for this family, not an unusual deficit. What is unusual is how little would close it.

#8.4 What closing it would take

For Q42, an emitter rather than a backend: lower a term to OpenQASM 3 or QIR and let an existing compiler route it. Routing and rotation synthesis, the two two costly parts, are commodity. Specific to Q42 are wire assignment (the width rule of QMANUAL §9.4 read constructively) and unrolling recursive definitions to a fixed depth.

One component has no existing counterpart. Q42 defers every measurement, by construction (QMANUAL §9.2), and on hardware deferral costs coherence time and prevents qubit reuse. A lowering would therefore want to apply the principle of deferred measurement in reverse: recognise a ctrl whose control qubit is not used again, and emit measure-and-branch where the term specifies quantum control. No prior language requires such a pass, because none is structurally obliged to defer.

For 42, the target is §8.1's, not §8.2's: a reversible classical ISA. That is a much less fashionable direction and a much better fit, and Axelsen's reversibility-preserving translation discipline is the thing to read before attempting it.

#9. Bidirectional transformation

Every other section here compares 42 to a reversible language. This one compares it to the field that took the same problem down a different road, and it is the only section in which 42 is the late arrival rather than the survivor.

§0 records that bidirectionality was the requirement first: Rosetta's M-rules had to parse one way and generate the other, and reversible computation was the frame applied afterwards. That requirement did not go away when Rosetta closed. It became a field.

#9.1 What a lens asks of you

A lens between a source type S and a view type V is a pair of functions

    get : S -> V
    put : V x S -> S

subject to two laws, which Foster, Greenwald, Moore, Pierce & Schmitt (TOPLAS 2007) name GetPut and PutGet:

    GetPut:   put (get s) s  =  s
    PutGet:   get (put v s)  =  v

Note put's second argument. Going backwards is ambiguous, and the original source is what resolves the ambiguity: it is the state you edit towards, not merely a value you reconstruct. PutGet is what forces the edit to take:

the putback function must capture all of the information contained in the abstract view

You write both directions, and the laws are obligations on the pair.

#9.2 A lens is the dagger plus a choice

Read the two laws in §1's vocabulary and they say something exact. Take get as a 42 program.

PutGet says put selects from the dagger. get (put v s) = v means put v s is a source whose view is v — that is, put v s ∈ ⟦get!⟧(v).

GetPut says the selection fixes the source it was given. put (get s) s = s picks s out of ⟦get!⟧(get s), which contains s by the defining law.

So a lens is not an alternative to what 42 computes. It is what 42 computes plus a choice function, and its two laws are precisely the statements that the choice is a choice from the converse and that it is reflexive.

That is not a reading imposed from outside. The lens paper says the same thing when it explains why a language was needed at all:

there are many ways to equip a given get function with a putback function to form a well-behaved and total lens; we need some means of specifying which putback is intended

A get underdetermines its put. What it determines is the set, and the set is ⟦get!⟧. Their linguistic approach is a way of writing down which element of it you meant.

#9.3 The half 42 does not do

42 gets that set for free, totally, with no obligation to discharge, because §1's class is closed under converse. What it does not get is the choice.

For most of what bidirectional transformation is used for — view update, model synchronisation, data migration — you must produce a source, not a set of candidates. append! gives four ways to split [1, 2, 3]; a lens must return one. 42 hands over all four and has nothing to say about which.

The two fields therefore paid opposite prices for the same difficulty. The lens design goal was a language in which the choice could be stated without cost:

does not involve onerous proof obligations or checking of side conditions

42 removes exactly those obligations from the converse, and says nothing about the choice. Whether the two can be separated — the relation derived, the choice supplied on top — is the obvious question from here, and this document does not know the answer.

#9.4 Where the set is the answer

The mismatch above is with these applications, not a deficiency in general. There is a domain in which the set is what you want, and 42 came out of it.

A sentence in a natural language is ambiguous. I saw the man with the telescope has two readings, and that is a fact about the sentence rather than a defect in whatever parsed it. Generation is many-valued in the same way: one meaning admits many surface forms. So both directions are many-valued at once, which is §1's bottom row and nothing above it. An injective language can of course return a list of readings — but then the alternatives are a data structure the programmer threads by hand, and every later stage has to be written to consume a list. In 42 they are the denotation: composition unions over them, and ! still applies. Rosetta's M-rules had to work in exactly that setting (§0), and it is the requirement 4₂ was answering. The choice is not the grammar's to make; it belongs downstream, where there is context to make it well.

This also explains the shape of §9.3's complaint. A lens must decide early, because a calendar synchroniser has to write one calendar. A grammar must decide late, or not at all. The two requirements pull in opposite directions, and 42 was built to the second while the field standardised on the first.

It is not a live application, though. Machine translation left that road entirely — statistical, then neural, then large language models — and none of them keeps a grammar to run backwards. Ambiguity is resolved inside continuous representations rather than surfaced as a set of readings, and the bidirectional grammar is not a component of any current system. So 42 has no more of a foothold in machine translation than the lens does. The requirement that shaped it in 1991 is not how the problem is approached now.

What survives is the distinction rather than the domain: some problems want a chosen source, and some want the preimage. The lens literature is built for the first. 42 is the only entry in §1's table whose semantics is the second.

#9.5 The complement, which 42 carries structurally

The sharper connection is older than lenses. Bancilhon & Spyratos (1981) answered view update by pairing the user's view with a second one:

Together with the user-defined view, we define a "complementary" view such that the database could be computed from the view and its complement

Hold that complement fixed and the backward direction is determined — translation under constant complement. Their main result is that this is not one technique among several:

translation under constant complement is the only method of translation

The complement itself, however, is not unique, and settling on one is a design act rather than a derivation:

a view can have many different complements and that the choice of a complement determines an update policy

That is §9.2's choice again, stated at the origin of the subject and a quarter of a century before lenses. It recurs: §9.2 has the lens paper saying it of put, and §9.6 has the putback line saying it once more. Going backwards leaves a set, and the work is in choosing from it.

Matsuda, Hu, Nakano, Hamana & Takeichi (ICFP 2007) give the same device in functional form:

a view complement function of f is a function from the source to another view (called a complement view) g : S -> V' such that the tupled function (f △ g) : S -> (V × V') is injective

That condition is 42's mul. MANUAL §11.3 explains that mul : (m, n) -> m x n is not writable, because the base case 0 x n = 0 discards n and cannot even recover it as a set. What is written instead is

    mul : (m, n) -> (n, m x n)

which is the tupled function ⟨complement, view⟩, injective by construction — and mul! is the inverse of it that the method needs. Matsuda et al. derive a complement per view function and then invert the tupling. 42 cannot express the un-tupled version at all, so every program is already in that form, and ! is the inversion.

What that literature derives per transformation, 42 makes a precondition of writing the transformation. The cost is that a genuinely discarding program is not usefully writable. The return is that no complement has to be inferred and the backward direction is exact rather than derived: divexact is mul!, and arith.42 contains no division algorithm.

Foster et al. place the same idea in the lens lineage, as one of the ancestors their own laws generalise — "update translation under a constant complement".

#9.6 The fork, and who took which branch

Worth recording, because §2 has already named them. Inv — Mu, Hu & Takeichi, MPC 2004 — is called 42's nearest relative there. Hu and Takeichi are also central to bidirectional transformation, including the ICFP 2007 bidirectionalization above and the later putback-based line, whose rationale Ko, Zan & Hu (PEPM 2016) state directly:

the put component of a bidirectional transformation uniquely determines its get component

That is §9.2 from the other side. put carries a choice that get! does not, so put is the more informative of the two, and a language may reasonably ask you to write it and derive get. BiGUL is that language, and the cost shows up where the asymmetry predicts — not every put is one, so the work becomes

ensuring the well-behavedness of a put

42 answers "write either and get the other", which is true of the relation and silent about the choice. That silence is the same gap §9.3 declines to close, and it is why 42 is not a lens language and does not become one by rearrangement.

#10. Logic and relational programming

Every section up to §9 compares 42 to a language built for reversibility. This one compares it to the family that agrees with 42 about the semantics — programs denote relations, and running one backwards is an ordinary thing to ask — and disagrees about nearly everything else. It is the comparison a reader who has written Prolog will reach for first, and §6 already concedes half of it: the relational setting is not what is new here.

#10.1 The same demonstration, forty years earlier

This document and the manual both lead with append run backwards: one list in, every way of splitting it out. Körner, Barbosa et al.'s survey of fifty years of Prolog uses the same program as its membership test for the whole language family:

one can check if a logic solver can be considered as a Prolog system or not via the following test

The test is that append/3 — Prolog names a predicate by its arity as well as its name, so this is the three-argument one — can be written in two clauses and then

deconstruct a list as in: append(A, B, [1, 2])

which is append!([1, 2]), with A and B the arguments left unbound for the query to solve. Prolog has done it since 1972. It is worth being plain about this. 42's flagship demonstration is not a new capability; it is a familiar one reached by a different route, and a reader who knows Prolog will not be impressed by the demonstration alone. What is different is everything about how it is obtained.

#10.2 Search at run time, or a term at parse time

Prolog and miniKanren get their multi-directionality from unification and backtracking, at the moment a query is asked. Nothing in the program text distinguishes the forward reading from the backward one, because there is no backward reading — there is one relation and many ways to query it.

42 has no unification, no logic variables, and no search. ! is a syntactic transformation of the term, applied by the parser (README):

parse("(copy ; join)!")  ==  parse("join! ; copy!")

The consequences are the whole difference. P! is a term: 42 show prints it, the checker types it, and THEOREM.md §2.5's proposition says the type is P's with the sides swapped. It composes with other terms. dagger(dagger(t)) = t holds on the nose, syntactically, which is not a statement one can make about a query strategy. And the cost of the backward direction is the cost of running a program, not of a search whose shape depends on which arguments were bound.

#10.3 Two directions, not one per argument

The honest side of that trade. The survey's test asks for append/3 to work

with any arbitrary instantiation of the arguments

which is one mode per subset of the arguments, chosen at the query. A 42 program P : A <-> B has exactly two directions, fixed when it is written. The arguments are packed into one value (MANUAL §4), so there is no notion of binding some of them and leaving others free: to ask 42 what add does given the first summand and the total, you run add! and filter, which enumerates where Prolog would constrain.

That is a real expressive gap in querying, and it is not closed by anything in §1's setting. It is the price of having the inverse be a program rather than a search.

#10.4 A property of some predicates, or of every term

Prolog's reversibility is a property a predicate may or may not have. append/3 has it; a predicate using arithmetic, cut, or I/O does not, and the survey notes that coroutining exists partly to recover it —

allowing programmers to write truly reversible predicates

— which is the same repair, made per predicate, that §3 records the reversible languages making per construct. In 42 there is nothing to recover, because dagger is total on the syntax (THEOREM.md §2.3) and there is no construct it can fail on. That is the property §6 claims as new, and it is new against this family too: not that programs can run backwards, but that every program can, without the programmer arranging it.

#10.5 The relational interpreter, done there first

§7 of THEOREM.md interprets 42 in 42 and runs the interpreter backwards. That idea is not new either, and the prior art is precise. Byrd, Holk & Friedman (Scheme Workshop 2012):

We present relational interpreters for several subsets of Scheme, written in the pure logic programming language miniKanren. We demonstrate these interpreters running "backwards" — that is, generating programs that evaluate to a specified value

and they use it to

trivially generate quines

Two differences, and the first favours them. Their interpreter leaves the program slot free and searches for programs; THEOREM.md §7's eval fixes the encoded term and inverts only the value, so it runs a given program backwards rather than synthesising one. 42 can state the stronger relation — §7.1's encoding with the term dropped — and it does not run. Theirs does.

The second difference is the one this document is about. Their backward direction is the search strategy applied to a relation; 42's is eval!, the dagger of a term, which is why THEOREM.md §7.4's Theorem 19 is sayable at all: there are two syntactic objects to compare, eval! and dag, and the theorem is that they agree. There is no corresponding statement to make about a miniKanren program, because there is no second object.

#10.6 What is left

Set the two families side by side.

semanticshow the other direction is obtained
Janus, RFUN, Theseus, Inv, PisoLang (§§2–4)injectivesyntactic, with side conditions
Prolog, miniKanren, Curryrelationalsearch, at query time
42relationalsyntactic, without side conditions

The reversible family takes the mechanism 42 takes and pays for it by giving up many-valuedness. The logic family keeps many-valuedness and pays for it by giving up the mechanism. The claim of this document is the third row, and §1's observation is why it is available: the class of r.e. relations is closed under converse, so a language that denotes exactly that class can inherit a total dagger without restricting anything.

What 42 gives up to occupy it is in §10.3, and it is not small.

#11. The equational axis

Every section so far compares 42 or Q42 to another language. This one compares the three equations of QMANUAL §6 to the other thing in the literature that does what they do: settle when two quantum programs are the same. That axis has an established occupant, the ZX-calculus, and setting Q42 beside it is the sharpest way to say what §6 is for — and, more usefully, what it does not yet do.

#11.1 What the completeness theorem actually says

Two claims get run together and should not be. §5.1 states the theorem precisely: a rig groupoid with √Π's two maps and three equations is computationally universal for quantum computing, and sound and complete for Clifford, for ≤2-qubit Clifford+T, and for Gaussian Clifford+T.

Universality and completeness are different properties, and here they have different scopes. Universality is unrestricted: every Clifford+T circuit, at any arity, is expressible. Completeness is not: it holds in the three named fragments. Outside them — three qubits and a t, which is ccz, an entirely ordinary program — two Q42 terms can denote the same matrix without the equations of §6 proving that they do.

So "Q42 has an equational theory" is true in the sense that the equations are sound and pin the model down, and false in the sense a reader coming from the axiomatisation literature will hear it. §6 says which.

#11.2 Q42's answer to the gap is not an equation

Where an axiomatisation proves two terms equal by rewriting one into the other, Q42 decides it by evaluating both: 42q matrix computes the matrix of a term, and two terms are equal exactly when their matrices are. That is a decision procedure, and it is one because the generators are discrete. Every amplitude a Q42 program can produce is built from 0, 1, omega and v, so every amplitude lies in Z[1/√2, i], a countable ring with decidable equality — and q42/exact.py evaluates in that ring rather than in floating point. An amplitude is (a + bω + cω² + dω³)/√2^k over the integers; reduced, that quadruple is unique, because ω has minimal polynomial x⁴ + 1 and the four powers are therefore independent. So omega^8 = id and h ; h = id are not observed to twelve decimal places. The cancelled amplitude is absent.

Backens states plainly the disadvantage of circuit notation that ZX was built to remove:

The only way to simplify or compare quantum circuit diagrams is by translating them back into matrices, thereby losing the advantages of the graphical notation.

Q42 does exactly that, deliberately, and the ring is what stops it costing any precision. What it costs instead is time: the matrix is 2ⁿ × 2ⁿ, so the decision is exponential, which QMANUAL §9.3 concedes for simulation and which applies here for the same reason. The alternative is not obviously cheaper — deciding the equality of two ZX diagrams by rewriting is not a polynomial procedure either — but the difference between them is real, and it is not about cost. One method yields a proof and the other yields a computation, and only the first produces an argument a reader can check by hand.

It costs exponential time and memory in the number of qubits, which QMANUAL §9.3 concedes for simulation and which applies here for the same reason. What is worth noticing is that the alternative is not obviously cheaper: deciding equality of two ZX diagrams by rewriting is not a polynomial procedure either. The difference is not cost. It is that one method yields a proof and the other yields a computation, and only the first produces an argument a reader can check by hand.

#11.3 ZX, and the opposite bet

The ZX-calculus began as Coecke & Duncan's

intuitive and universal graphical calculus for multi-qubit systems

which writes a circuit as a diagram of two families of nodes carrying phase angles, and reasons by rewriting one diagram into another. Its completeness results are the ones §11.1's should be measured against. Backens (2014) proved the stabiliser fragment complete, in the sense that

any equality that can be derived using matrices can also be derived pictorially

and Jeandel, Perdrix & Vilmart (LICS 2018) settled what they call

one of the main open questions in categorical quantum mechanics

by making the language

complete for the so-called Clifford+T quantum mechanics by adding two new axioms to the language

which gives, in their own description, the first complete and approximatively universal diagrammatic language for quantum mechanics. Ng & Wang (2017) then gave

a universal completion of the ZX-calculus for the whole of pure qubit quantum mechanics

and Hadzihasanovic, Ng & Wang (LICS 2018) extended both ZW and ZX and did the same, in their words to

show their completeness for pure-state qubit theory

which each paper describes as settling a long-standing open problem of the field. The consequence, as van de Wetering's survey states it, is that

in principle all reasoning about quantum computation can be done inside the ZX-calculus.

That is a real concession and this document should make it plainly: on the axis §6 sits on, ZX is ahead. ZX has a complete axiomatisation of the whole of Clifford+T; √Π has one for three fragments of it, and whether its three equations extend to a complete presentation at every arity is open.

The two are making opposite bets, and it is the trade QMANUAL §9.4 ends on, seen from the other side.

The main drawbacks were that the axioms that were added to achieve completeness were numerous, tedious to manipulate and lacked a physical interpretation.

His near-minimal axiomatisations (LICS 2019) answer exactly that, and are offered as optimal in the sense that

all their equations are necessary

That bet has a name, and it is a single invariant. Coecke & Duncan attach to each observable the group of phases available to it — the phase group (their §7.4) — and compute it for the qubit: the phase shifts are diag(1, e^{iα}), so the group

is therefore isomorphic to the circle

with the group operation being addition of angles modulo 2π. ZX's spiders carry exactly those angles. Q42's omega has order eight, so its phase group is Z₈, the eight-element subgroup of that same circle (QMANUAL §6.2, where z, s and t come out as its subgroup chain). The two bullets above are that one difference worked out: a continuous phase group cannot be decided by evaluating, and needs a rule set; a finite one can be, and does not.

Which makes the fragment Jeandel, Perdrix & Vilmart proved complete the interesting one to name. They call it the π/4-fragment — ZX with every angle a multiple of π/4, which is ZX with Z₈ for a phase group, which is ZX cut down to precisely Q42's phases. Q42 sits on that fragment, not merely near it. Their statement of its reach,

represents exactly all the matrices over some finite dimensional extension of the ring of dyadic rationals

is then no coincidence beside §11.2's Z[1/√2, i], but the same fact reached twice: two calculi with the same phase group have the same reach, and both papers report that reach as a ring.

The invariant is sharp enough to be worth borrowing. Coecke & Duncan use it to separate theories that otherwise look alike: the qubit stabiliser category and Spekkens' toy model have, in their Example 7.23, the cyclic group of order four and the Klein four group respectively, and that difference is where the non-locality of the GHZ state sits. Read on the same scale, Q42 is one rung above the stabiliser theory and ZX is not on the scale at all, having all of it.

#11.4 The generators, side by side

§2 of Coecke & Duncan presents the calculus in the same shape QMANUAL §6 uses — a handful of generators, a set of equations, an interpretation into matrices, and a universality claim — and the two agree far enough to be worth laying out before saying where they part. What follows compares that section's simplified calculus, not the general theory the rest of their paper develops.

Their generators are wires, wire crossings, cups and caps, and four kinds of vertex: Z and X spiders labelled by a phase α ∈ [0, 2π), which

can have any number of inputs or outputs (including none)

an H box with exactly one of each, and a black diamond with neither.

ZX §2Q42 §6
a wireid
a wire crossingswapprod
a Z spider with phase α, at arity 1 → 1id + <phase>, the sum functor (§6.2)
the H boxh, derived rather than given (§6.3)
the black diamond, a scalaromega, "a number rather than a gate"
the colour-change rule (C)(E3), the Euler decomposition
spider fusion: phases addomega ; omega
a Z spider at any other aritycopy, join — dropped (§5.2)
cups, caps, and the topology rulenothing
the bialgebra and π-copy rulesnothing; + does that work

The third row is an identity and not an analogy: their Z¹₁(α) is diag(1, e^{iα}), which is what §6.2 writes as id + <phase>, so a spider at π/4 is t. It is also the row on which §11.3's whole comparison turns, that generator carrying the phase group of each calculus — the circle there, Z₈ here. The fifth is a smaller agreement worth noticing — both calculi found they needed a generator at the unit, and both did so in order to keep their equations exact rather than true up to a scalar. Coecke & Duncan say why they cannot do without theirs:

The points in the calculus are not normalized. This is required for reasons of simplicity; if we were to normalize σ_Q and η_Q, then the (T1) rule would require additional scalar multipliers

which is QMANUAL §6.3's decision to track the global phase of h exactly, made for the same reason and paid for in the same coin.

The sixth row is the sharpest agreement of all. Both calculi need the fact that a rotation about one axis decomposes into rotations about the other; ZX states it as the rule that lets H commute past a coloured dot and change its colour, Q42 states it as (E3), and in both it is the axiom that does the work.

The break is in the arity, and it is exact. A spider is not one generator but a family indexed by its inputs and outputs, and Q42 keeps precisely the square members of it. Coecke & Duncan name the others as they introduce them: arity 1 → 2 is

with 1 input and 2 outputs (cf. copying)

and 1 → 0 is

with 1 input and no output (cf. erasing)

with 0 → 1 a point. Those are the entries in Q42's dropped table (§5.2), refused because none of them is unitary. The two documents even read the same map the same way before disagreeing about what to do with it: Q42 drops copy on the ground that it copies basis states only and is therefore a measurement basis rather than an illegal cloner, and the thesis of the paper it is here being compared to is that these structures are observables. ZX admits the non-unitary generators and carves the unitary maps out of the larger category; Q42 admits only unitary generators and never leaves. That is why dagger is total here, and why §5.2's other comparison landed in Contraction rather than Unitary.

ZX has no sum. One object, tensored with itself, where Q42 has a rig. The classical structure ZX obtains from Frobenius algebras sitting on the tensor is what Q42 obtains from +, which is §5.3's result — that control and the rig structure are the same thing — met from the other side. It is also why two rows of the table are empty: the bialgebra and π-copy rules govern how two observables interact, and Q42 has no rule of that kind to state, its type structure having already provided the answer.

Only the topology matters, and Q42 has no topology. Their first rule is that a diagram may be bent, stretched or knotted freely so long as the connections hold, which is a rule worth stating only because there are cups and caps to bend. A Q42 term is a tree over ;, + and × with no way to turn an output back into an input, so nothing of the kind can be said, and nothing of the kind is needed.

Put together, those three are the concrete form of a difference easier to assert than to show. A ZX diagram has no types, no names, no recursion, no notion of being run on an input and no inverse operator: it is a proof object for a circuit, and Q42 is a language whose terms happen to carry an equational theory. It cuts both ways. ZX reasons about circuits Q42 cannot express, having every angle; Q42 expresses programs ZX has no notion of, qft.42 computing a circuit as 42 data and tools/unquote.py turning that data back into a Q42 term, which is a statement about a language with a metalevel rather than about a diagram.

One last thing the table would mislead about if left unsaid. The rule set of §2 is the original one and is not complete — the paper says so itself, that

the equational theory of the zx-calculus is strictly weaker than that of Hilbert spaces

and observes that this makes it more general, since it has models the Hilbert space one does not. The completeness results of §11.3 are all later, and all reached by adding axioms to this. So the comparison above is between Q42's three equations and ZX's original rules, which is the fair comparison of presentations; the comparison of what each theory can prove is §11.3's, and it goes the other way.

#11.5 The verification languages

There is a second cluster on this axis whose concerns are orthogonal enough that it is easily mistaken for a competitor.

languagewhat its types buy
QWIRE (Paykin, Rand & Zdancewic, POPL 2017)linear types for wires, in Coq
Silq (§8.3)automatic, safe uncomputation
Twist (Yuan, McNally & Carbin, POPL 2022)purity, and the tracking of entanglement
Qunity (§8.3)one language for the quantum and the classical part

Every one of them is about safety: stopping a program from discarding a wire, uncomputing wrongly, or entangling something it promised was separable. Q42 does not have those problems to solve, which is not a virtue of its type system but of its semantics — there is no discard to misuse (§5.2), every term is unitary by construction, and the inverse is total. None of them, in turn, has an equational theory in §6's sense.

So the axis is nearly empty where Q42 sits. The languages have the safety and no equational theory; ZX has the equational theory and is not a language.

#11.6 The family problem, and who has a metalanguage

A circuit is a finite object, and every quantum algorithm worth the name is a family of them, one per input width. Shor's is a family; Grover's is a family; qft on three qubits is not the quantum Fourier transform but a member of it. So any formalism that describes circuits needs something outside the circuits to say how the family is generated — and on that question the formalisms compared above differ more sharply than on anything in §§11.1–11.5.

Quipper's answer is its whole design. It is a circuit-generating metalanguage: you write Haskell, the Haskell runs, and what it produces is a circuit. Recursion, arithmetic on the width, and everything else a family needs belong to the host language rather than to the circuit language, because a circuit has no room for them. §8.2 calls Quipper a real circuit-generating toolchain; this is what the generating consists of.

ZX has no answer, and needs none for what it is. A diagram is a diagram, and a family is handled in the surrounding mathematics, by an induction conducted in the prose rather than in the calculus. That is entirely reasonable for a proof calculus, and it is §11.4's observation — no types, no names, no recursion — in its practical form.

The Π lineage meets a wall, and says so. Πo has mu and a trace, so a reversible classical language of this family can iterate; the quantum branch cannot follow it there. §5.2 records QuantumΠ's own judgement that extending from finite Π to Πo with a trace would require answering fundamental open questions about the nature of infinite-dimensional quantum computation, and Q42 meets the same wall from the other side, closure being a least fixed point that wants 1 + 1 = 1.

Q42's answer is Quipper's, with an unusual host. qft.42 is a Q42 circuit family written in 42. It declares qterm — Q42's syntax as an ordinary 42 datatype, five atoms with ctrl and the two binary constructors — and defines aqft, a recursive 42 program taking a width n to the qterm value describing Coppersmith's approximate quantum Fourier transform on n + 1 qubits. tools/unquote.py turns that value into Q42 source, and 42q type and 42q unitary check the result exactly as they check a handwritten library. The generation is recursive; the thing generated is a finite term. The file states the position itself: every other quantum language writes its families in a classical host, Qiskit in Python and Quipper in Haskell, and this one's host is 42.

What is unusual is not the architecture but the distance to the host. Quipper's metalanguage is Haskell, a general-purpose language chosen for the job. Q42's is 42: the same language over a different semiring, sharing the parser, the type engine and dagger, which is why the bridge is twenty lines rather than a compiler. It was not designed that way. 42 was built for bidirectional grammars in machine translation and had no quantum computing in view (§0), and the metalanguage relation is a consequence of the two languages differing in exactly one thing.

**Why it generates the approximate transform is §11.3 over again.** The quantum Fourier transform wants R_k = diag(1, e^{2πi/2^k}) at every k. Q42 has R₁, R₂ and R₃ — they are z, s and t — and no exact R₄, because the phase group is Z₈ and stops there. So aqft drops the rotations past R₃, which is what hardware does anyway: at three qubits nothing is dropped and the output is the exact transform.

Past three the cost has a closed form, and it is not constant. R_k occurs n − k + 1 times in the n-qubit transform, so dropping everything past R₃ drops (n−3)(n−2)/2 rotations; the eigenvalues of U_exact† U_approx spread over an arc equal to the sum of the dropped angles, and a unitary whose eigenvalues span an arc a has worst-case overlap cos(a/2):

qubitsdroppedworst-case overlap
301.0000, the exact transform
410.9808
530.8819
660.6716
7100.3599
8150.0000

At eight qubits the arc passes π: some input is sent to a state orthogonal to the right one. So the four-qubit figure so often quoted, cos(π/16), is a fact about four qubits and not about the truncation.

The comparison this invites is worth making, and worth making carefully, because the short version of it is wrong. Coppersmith's AQFT keeps rotations down to R_m with m growing like log n — the cutoff is a design parameter, chosen so that fidelity stays bounded as the register grows. Q42's is fixed at R₃, and what fixes it is not that R₄ cannot be expressed. omega cannot name R₄ as a single gate, but Clifford+T is approximately universal, and Ross & Selinger synthesise any z-rotation to precision ε in about 3log₂(1/ε) T gates, so an R₄ good to 10⁻¹⁰ is an ordinary Q42 term about a hundred gates long. The generator's rotation table sends k ≥ 4 to the identity. That decision, taken in qft.42, is the cutoff.

So the six-qubit bound belongs to the generator, not to the language, and §11.3's coarse alphabet enters one step further back than it first appears: it does not forbid the rotation, it makes the honest version of it cost a synthesis pass written in 42 and terms two orders of magnitude longer. Which is the rotation synthesis QMANUAL §9.4 hands to a downstream compiler, met from the other end.

The object this produces has a name. A map from a width to a circuit description is a uniform circuit family, and uniformity is not a nicety: BQP and its classical siblings are defined over uniformly generated families exactly because a family with no generator may have undecidable information built into its nth member and so decide anything at all. What the arrangement above yields is therefore not "the recursion living somewhere else" but a uniform family, whose uniformity is witnessed by a 42 program.

This witness is total, and the argument is short. aqft recurses on nat, which is mu X. 1 + X. The + separates zero from a successor and the recursive call takes the predecessor, so the argument strictly decreases and the recursion stops at every width. That is structural recursion and an induction on the argument settles it; the interpreter's depth budget guards programs that lack the property and is not the reason this one has it. What the language guarantees is weaker, and the two should not be run together: §7's characterisation is that 42 denotes exactly the recursively enumerable relations, so an arbitrary generator need not terminate, and uniformity has to be argued per program rather than granted by the framework.

Measured, the generated term grows quadratically in the width — 34, 73, 119 and 172 characters at widths one to four, the second differences constant — which is the approximate QFT's gate count and is what one would expect. That is a measurement and not a bound: the family is uniform, and polynomial-time uniform is a claim nothing here has earned.

QMANUAL §9.4's depth-bounding gap looks like the same question and is not: that one is about a Q42 definition referring to itself, guarded in q42/emit.py, where this is a 42 definition recursing on a width. No definition in any Q42 library is self-referential, so in the libraries as they stand that budget bounds nesting rather than recursion.

What it is not is a mu in Q42. A recursive Q42 term would denote a single operator on an infinite-dimensional space, which is the open problem §5.2 quotes QuantumΠ naming. A uniform family denotes, for each n, a unitary on ℂ^(2ⁿ), and denotes no single operator at all: nothing assembles, and no limit is taken. So the metalanguage does not approximate the missing mu — it puts a different mathematical object in its place. Whether that is a loss depends on what was wanted from it. For running algorithms it is not one, devices being finite and the complexity theory of quantum computing having always worked in families. For a semantics of unbounded reversible quantum computation it is not an answer.

The witness runs backwards. aqft! reads a circuit back to the width that produced it, and tests/test_q42.py checks that it does. Nothing about uniformity asks for this. A uniformity witness is ordinarily a Turing machine and nobody enquires after its converse. This one is invertible because the host is 42; a Haskell function has none, so Quipper's could not be.

Three things it does not buy, which should be said plainly.

The comparison earns its place because the field's usual division — languages with a semantics on one side, toolchains that generate circuits on the other — puts Q42 on both sides of it. §8.3 says the Π lineage has no backend, and that is about lowering. This section is about generation. They are not the same lack, and Q42 no longer has either: it has an emitter (§9.4) and it has a generator. What it does not have is everything in between.

#11.7 What is left

what it isanglesequality bycomplete for
ZXa diagram calculusa continuumrewritingClifford, Clifford+T, universal
QWIRE, Silq, Twist, Qunitylanguagesa continuum——
√Π / Q42a language8th rootsevaluationClifford, ≤2-qubit Clifford+T, Gaussian Clifford+T

The bold row is the claim, as in §10.6, and the honest cell in it is the last one: completeness is where Q42 is behind rather than ahead. What is unusual is the combination — a language, carrying an exact equational theory, in which equality is computed rather than argued. Nothing else in this document's comparisons occupies that square, and what makes it reachable is what QMANUAL §9.4 says makes the alphabet coarse. Discreteness bought both.

That table is about the equational axis only, and on §11.6's the ordering comes out differently: there Quipper has the mature answer, ZX has none and needs none, and Q42's is unusual only in its host. A language can be behind on one axis and unaccompanied on another. Q42 is both, and saying only the second would be the easier document to write and the wrong one.

#References

From the 1993 thesis's bibliography (§0.4), transcribed from it:

Other references.