Reversible Classical Computation

Proof. Preservation. By induction on the derivation of $t⟶t^{\prime }$. The two iso rules replace an iso variable by an iso of the same type, which is typed by IFix and ILam respectively. For the clause rule, Clauses gives $\mathrm{\Psi };{\mathrm{\Delta }}_i⊢v_i:A$ and $\mathrm{\Psi };{\mathrm{\Delta }}_i⊢e_i:B$ with the same ${\mathrm{\Delta }}_i$; a matching substitution $\sigma$ assigns to each variable of ${\mathrm{\Delta }}_i$ a value of its type, so $\sigma (e_i)$ has type $B$. For $\mathsf{let}$, Let makes the types of the pattern variables the components of the tuple. The two context rules are the induction hypothesis.

Determinism. Each term has at most one decomposition $E⟨t_0⟩$ with $t_0$ a redex, since the grammar of $E$ fixes which subterm is evaluated first and values are not redexes. At a clause application, at most one $v_i$ matches $v^{\prime }$: two matching clauses would give $v_i⟂v_j$ with a common instance, and by definition 168.3 orthogonal terms differ by a choice of injection at some position, so no value instantiates both. ◻

Proof. By induction on the structure of $\omega$ and, inside a clause set, on the value $v$. For a clause set, exhaustiveness gives an $i$ and a $\sigma$ with $\sigma (v_i)=v$, so the clause rule fires and produces $\sigma (e_i)$; by lemma 168.5 it has type $B$, and every $\mathsf{let}$ and every iso application inside $e_i$ is handled by the induction hypothesis for the smaller isos occurring in it. For $\lambda \phi .\omega$ and ${\omega }_1{\omega }_2$ the two iso rules of definition 168.4 reduce to a smaller iso. With $\mathsf{fix}$ excluded, the induction is well founded. ◻

Proof. By induction on $\omega$. The four non-clause cases are immediate from definition 168.8. For a clause set, the inner definition reverses the order of the $\mathsf{let}$ bindings and swaps the two sides; applying it twice reverses the order twice and swaps twice, and each ${\omega }_k$ is replaced by $({\omega }_k^{-1}{)}^{-1}$, which is ${\omega }_k$ by the induction hypothesis. ◻

Proof. By induction on the typing derivation. The rules IVar, IFix, ILam and IApp each produce a derivation of the same shape with every iso type inverted, because definition 168.8 inverts $T$ structurally.

For Clauses, the premises are $\mathrm{\Psi };{\mathrm{\Delta }}_i⊢v_i:A$, $\mathrm{\Psi };{\mathrm{\Delta }}_i⊢e_i:B$, and the two orthogonality conditions. The inverted clause set has left-hand sides the $v_i^{\prime }$ appearing as the bodies of the $e_i$ and right-hand sides built from the $v_i$. Its two orthogonality conditions are the two of the original exchanged, and the linear contexts are unchanged because reversing a chain of $\mathsf{let}$ bindings permutes the same bindings. The type of each ${\omega }_k$ occurring in a body is inverted by the induction hypothesis, and the direction of each $\mathsf{let}$ is exchanged accordingly, so the inverted clause set is typed at $B\leftrightarrow A$ by Clauses. ◻

Proof. There are two iso reductions. For $\mathsf{fix}\phi .\omega ⟶\omega [\mathsf{fix}\phi .\omega /\phi ]$, apply definition 168.8 to both sides: the iso $(\mathsf{fix}\phi .\omega {)}^{-1}$, which is $\mathsf{fix}\phi .{\omega }^{-1}$, reduces to ${\omega }^{-1}[\mathsf{fix}\phi .{\omega }^{-1}/\phi ]$, and that is $(\omega [\mathsf{fix}\phi .\omega /\phi ]{)}^{-1}$ because inversion commutes with substitution of an iso for an iso variable, which is an induction on $\omega$ using ${\phi }^{-1}=\phi$. The same two steps apply to $(\lambda \phi .{\omega }_1){\omega }_2⟶{\omega }_1[{\omega }_2/\phi ]$. ◻

Proof. Proof idea. A forward run of a clause is a chain of $\mathsf{let}$ bindings executed left to right, each applying some ${\omega }_k$; the inverted clause is the same chain read right to left with each ${\omega }_k$ inverted, so a backward run replays the bindings in reverse. The induction is on the length of the forward run, with the clause case carried by the orthogonality of the right-hand sides.

Claim 1. Induct on the length of $\omega v{⟶}^{\ast }w$. If the first step is an iso reduction, lemma 168.11 gives the corresponding step for ${\omega }^{-1}$ and the induction hypothesis applies. Otherwise the first step is the clause rule: some $\sigma$ has $\sigma (v_i)=v$, and the run continues from $\sigma (e_i)$. Write $e_i$ as the chain $\mathsf{let}{p}_1={\omega }_1{p}_1^{\prime }\mathsf{in}\cdots \mathsf{in}{v}_i^{\prime }$ of definition 168.8. Each binding fires in turn, producing an extended substitution; let ${\sigma }_k$ be the substitution after the $k$th binding, so that $w={\sigma }_n(v_i^{\prime })$.

Now run ${\omega }^{-1}$ on $w$. By orthogonality of the right-hand sides, at most one inverted clause matches $w$, and $v_i^{\prime }$ does, with the substitution ${\sigma }_n$ restricted to the variables of $v_i^{\prime }$. The inverted body binds $p_n^{\prime }={\omega }_n^{-1}{p}_n$ first; by the induction hypothesis applied to the strictly shorter run of ${\omega }_n$, that binding recovers the value that $p_n^{\prime }$ had in the forward run. Repeating for $k=n-1,\dots ,1$ recovers $\sigma$, and the body of the inverted clause is $v_i$, so the result is $\sigma (v_i)=v$.

Claim 2. If $\omega v$ does not reach a value, then ${\omega }^{-1}(\omega v)$ does not either, by determinism (lemma 168.5), and the hypothesis is vacuous. Otherwise $\omega v{⟶}^{\ast }w$ and Claim 1 gives ${\omega }^{-1}w{⟶}^{\ast }v$; determinism makes that the only run, so $v^{\prime }=v$. ◻

Proof. Orthogonality. Left-hand sides: $(\mathsf{tt},\mathsf{tt})$ and $(\mathsf{tt},\mathsf{ff})$ differ in the second component by the choice of injection, so they are orthogonal by definition 168.3 with the context $(\mathsf{tt},[-])$; each is orthogonal to $(\mathsf{ff},y)$ by the first component with the context $([-],-)$. Right-hand sides: the same three pairs in a different order, so the same argument applies.

Self-inversion. Each clause of $\mathsf{cnot}$ has a body that is a value with no $\mathsf{let}$, so definition 168.8 simply exchanges the two sides; the resulting clause set is the original one with the first two clauses exchanged.

Map. By definition 168.8, $(\lambda \psi .\mathsf{fix}\phi .\omega {)}^{-1}=\lambda \psi .\mathsf{fix}\phi .{\omega }^{-1}$, and ${\omega }^{-1}$ is $$\{\mathsf{nil}\leftrightarrow \mathsf{nil}\mid h^{\prime }::t^{\prime }\leftrightarrow \mathsf{let}t={\phi }^{-1}{t}^{\prime }\mathsf{in}\mathsf{let}h={\psi }^{-1}{h}^{\prime }\mathsf{in}h::t\},$$ which is the body of $\mathsf{map}$ with $\psi$ replaced by ${\psi }^{-1}$, up to the order of the two independent bindings. Since ${\phi }^{-1}=\phi$, the recursion variable is unchanged. ◻

Proof. The forward run fires the single clause, then the two bindings in order: ${\mathsf{Dup}}_{A}v{⟶}^{\ast }(v,v)$ by induction on $A$ using definition 168.17, and $\omega v{⟶}^{\ast }w$ by hypothesis, so the body evaluates to $(w,v)$. For the backward run, definition 168.8 gives $$\mathsf{bennett}(\omega {)}^{-1}=\{(y,x_2)\leftrightarrow \mathsf{let}{x}_1={\omega }^{-1}y\mathsf{in}\mathsf{let}x={\mathsf{Dup}}_A^{-1}(x_1,x_2)\mathsf{in}x\},$$ and on $(w,v)$ the first binding gives $x_1=v$ by theorem 168.13(1), so the second is ${\mathsf{Dup}}_A^{-1}(v,v)$, which is $v$. The second binding is where the ancilla is discharged: it is defined only because the two components agree, and that is what uncomputation means here. ◻

Proof. $f\otimes g$ is a partial injection because the two summands are disjoint and each of $f,g$ is one; functoriality of $\otimes$ is the corresponding fact for disjoint unions of partial functions. The associator, unitors and symmetry are total bijections, hence partial injections, and every coherence equation is an equation between bijections of finite disjoint unions, checked by following an element through both sides. ◻

Proof. Suppose ${\mathrm{Tr}}^U(f)(x)={\mathrm{Tr}}^U(f)(x^{\prime })=y$, with traversal sequences $z_0,\dots ,z_n$ and $z_0^{\prime },\dots ,z_m^{\prime }$. Then $f(z_n)=y=f(z_m^{\prime })$, so $z_n=z_m^{\prime }$ by injectivity of $f$. Suppose $n,m\ge 1$. Then $f(z_{n-1})=z_n=z_m^{\prime }=f(z_{m-1}^{\prime })$, so $z_{n-1}=z_{m-1}^{\prime }$ by injectivity again; iterating, the two sequences agree from the end backwards. They must run out together: if say then after $m$ steps backwards we reach $z_{n-m}=z_0^{\prime }=x^{\prime }\in X$, contradicting $z_i\in U$ for $i\ge 1$. Hence $n=m$ and $x=z_0=z_0^{\prime }=x^{\prime }$. ◻

Proof. Throughout, “the run of $f$ from $x$” means the sequence of construction 168.22. Each law is proved by comparing two runs element by element.

Tight, first equation. Let $g:X^{\prime }\to X$. The run of $f\circ (g\otimes {\mathrm{id}}_U)$ from $x^{\prime }\in X^{\prime }$ begins by applying $g$ and then proceeds exactly as the run of $f$ from $g(x^{\prime })$, since on the $U$ summand $g\otimes {\mathrm{id}}_U$ is the identity. Both sides are therefore defined at $x^{\prime }$ precisely when $g$ is defined at $x^{\prime }$ and ${\mathrm{Tr}}^U(f)$ at $g(x^{\prime })$, with the same value.

Tight, second equation. Let $h:Y\to Y^{\prime }$. The run of $(h\otimes {\mathrm{id}}_U)\circ f$ from $x$ visits the same elements of $U$ as the run of $f$, because $h\otimes {\mathrm{id}}_U$ is the identity on $U$; it exits when $f$ exits, and then applies $h$.

Slide. Let $g:U\to U^{\prime }$. Write $f:X\bigsqcup U\to Y\bigsqcup U^{\prime }$. The run of $({\mathrm{id}}_Y\otimes g)\circ f$ from $x$ has the form $$x\stackrel{f}{\mapsto }{u}_1^{\prime }\stackrel{g}{\mapsto }{u}_1\stackrel{f}{\mapsto }{u}_2^{\prime }\stackrel{g}{\mapsto }{u}_2\cdots ,$$ and the run of $f\circ ({\mathrm{id}}_X\otimes g)$ from $x$ has the form $$x\stackrel{f}{\mapsto }{u}_1^{\prime }\stackrel{g}{\mapsto }{u}_1\stackrel{f}{\mapsto }{u}_2^{\prime }\cdots ,$$ the two sequences differing only in whether the last recorded state is taken before or after the application of $g$. Both exit at the same application of $f$ into $Y$, and with the same value; and one is defined exactly when the other is.

Vanish, first equation. $U=\mathrm{\varnothing }$, so no run has a step: the sequence stops at $z_0=x$ and the value is $f(x)$.

Vanish, second equation. Let $g:X\bigsqcup U\bigsqcup V\to Y\bigsqcup U\bigsqcup V$. The run of $g$ from $x$ visits a sequence of elements of $U\bigsqcup V$. The inner trace ${\mathrm{Tr}}^V(g)$ collapses each maximal stretch of consecutive elements of $V$ into a single step, and the outer trace then iterates over the elements of $U$. The composite therefore visits exactly the same elements of $U$ in the same order and exits at the same application, so the two sides agree; and the composite is defined at $x$ exactly when the run of $g$ leaves $U\bigsqcup V$, since an infinite run either has infinitely many $U$-states, when the outer trace diverges, or a final infinite $V$-stretch, when the inner trace diverges.

Super. Write the right-hand side as ${\mathrm{Tr}}^U(k)$ with $k:=(\mathrm{id}\otimes c^{-1})\circ (f\otimes g)\circ (\mathrm{id}\otimes c)$, a morphism $(X\bigsqcup X^{\prime })\bigsqcup U\to (Y\bigsqcup Y^{\prime })\bigsqcup U$. On the summand $X\bigsqcup U$ the two symmetries cancel and $k$ acts as $f$; on $X^{\prime }$ it acts as $g$ and lands in $Y^{\prime }$ at once. Hence the run of $k$ from an element of $X$ is the run of $f$, giving ${\mathrm{Tr}}^U(f)$, and the run from an element of $X^{\prime }$ has length zero, giving $g$. That is ${\mathrm{Tr}}^U(f)\otimes g$.

Yank. Here $f=c_{U,U}:U\bigsqcup U\to U\bigsqcup U$ exchanges the two summands, with $X=Y=U$ the first summand. For $x$ in the first summand, $c_{U,U}(x)$ is the copy of $x$ in the second summand, which is the traced summand, so $z_1$ is that copy; applying $c_{U,U}$ again returns the copy in the first summand, which is in $Y$. The run stops after one step with value $x$. Hence ${\mathrm{Tr}}^U(c_{U,U})={\mathrm{id}}_U$. ◻

Proof. Each clause determines a partial injection: matching $v_i$ against a value determines the substitution uniquely, and building $e_i$ from it is a composite of injections by induction on $e_i$. For the union, two clauses have disjoint domains because $v_i⟂v_j$ and orthogonal patterns have no common instance, by definition 168.3; and they have disjoint images because $e_i⟂e_j$, by the same argument applied to the right-hand sides. A union of partial injections with pairwise disjoint domains and pairwise disjoint images is a partial injection. ◻

Proof. By induction on $\omega$.

Clause set. By lemma 168.27 the denotation is a disjoint union of clause denotations. Definition 168.8 exchanges the two sides of each clause and reverses the chain of $\mathsf{let}$ bindings, so the denotation of the inverted clause is the composite of the converses in reverse order, which is the converse of the composite; and the union of the converses is the converse of the union, the domains and images being disjoint.

Abstraction and application. Definition 168.8 inverts both components, and the induction hypothesis applies to each.

Fixed point. Inversion sends $\mathsf{fix}\phi .\omega$ to $\mathsf{fix}\phi .{\omega }^{-1}$, so it suffices that the trace commutes with converse: for $f:X\bigsqcup U\to Y\bigsqcup U$, ${\mathrm{Tr}}^U(f^{-1})={\mathrm{Tr}}^U(f{)}^{-1}$. That is the calculation in lemma 168.23: the run of $f^{-1}$ from $y$ is the reversal of the run of $f$ that ends at $y$, which the proof there constructs by stepping backwards through the injectivity of $f$. ◻

Proof. By induction on the length of the run, using lemma 168.5 for the typing at each step. The two iso reductions do not change the denotation: $\mathsf{fix}$ unfolds to a term whose denotation is the same trace by the fixed-point property of construction 168.22, and $\beta$ for iso abstraction is substitution, which the interpretation of definition 168.26 respects. The clause rule selects the unique matching clause, whose denotation is by lemma 168.27 the restriction of $[[\omega ]]$ to the values matching $v_i$. The $\mathsf{let}$ rule is composition of partial injections. ◻