Synthetic Guarded Domain Theory and Step-Indexed Semantics

Proof. By the presheaf exponential, $(B^A{)}_n=\mathrm{Nat}(\mathrm{y}(n)\times A,B)$. Since $\mathrm{y}(n{)}_m$ is a one-point set for $m\le n$ and empty otherwise, such a natural transformation is exactly a family $f_m:A_m⟶B_m$ for $m\le n$ subject to the displayed naturality squares. Restriction along $n+1\ge n$ deletes $f_{n+1}$. The displayed description mentions no datum at a level above $n$. ◻

Proof. Closure under restriction at the step from level $2$ to level $1$ is the inclusion into $X_1$, which holds because $(⊳P{)}_1=X_1$. For the step from $n+2$ to $n+1$, let $\alpha \in (⊳P{)}_{n+2}$, so $r_{n+1}^X(\alpha )\in P_{n+1}$; since $P$ is closed under restriction, $r_n^X(r_{n+1}^X(\alpha ))\in P_n$, which says $r_{n+1}^X(\alpha )\in (⊳P{)}_{n+1}$.

For the inclusion, $P_1\subseteq X_1=(⊳P{)}_1$; and if $\alpha \in P_{n+1}$ then $r_n^X(\alpha )\in P_n$ by closure, that is $\alpha \in (⊳P{)}_{n+1}$. ◻

Proof. By induction on $n$.

Stage $1$. $(⊳P{)}_1=X_1$ by definition 163.3, and $⊳P\subseteq P$ gives $X_1\subseteq P_1$.

Stage $n+1$. Let $\alpha \in X_{n+1}$. The induction hypothesis gives $P_n=X_n$, so $r_n^X(\alpha )\in P_n$, that is $\alpha \in (⊳P{)}_{n+1}$; the hypothesis $⊳P\subseteq P$ then gives $\alpha \in P_{n+1}$. ◻

Proof. The isomorphism is the identity on the displayed disjoint unions, using $(▸\mathsf{L}X{)}_1=\{\ast \}$ and $(▸\mathsf{L}X{)}_{n+1}=(\mathsf{L}X{)}_n$. The normal form follows by induction on $n$: at level $1$ an element is in $X_1$ or is $\mathrm{\perp }$; at level $n+1$ it is in $X_{n+1}$, or lies in $(\mathsf{L}X{)}_n$ and has the stated form by the induction hypothesis, and in the second case one further $\theta$ is prefixed. Uniqueness of $Y$: $Y_1\cong X_1\uplus \{\ast \}$, and if $Y_n\cong (\mathsf{L}X{)}_n$ then $Y_{n+1}\cong X_{n+1}\uplus Y_n\cong (\mathsf{L}X{)}_{n+1}$; these bijections commute with restriction because the isomorphism $Y\cong X+▸Y$ does. ◻

Proof. The middle equation is the first clause of definition 163.8. The other two are proved by induction on the level, using proposition 163.7 to split an element as $\eta (a)$, as $\theta (t)$ with $t$ at a strictly smaller level, or as $\mathrm{\perp }$ at level $1$. In the $\theta$ case both sides are $\theta$ applied to the corresponding equation one level down, which is the induction hypothesis; in the $\eta$ case both sides reduce by the middle equation; at level $1$ both sides are $\mathrm{\perp }$. ◻

Proof. The isomorphism. By the description of $▸$ in convention 163.1, $(▸\mathcal{F}{)}_1=\{\ast \}={\mathcal{H}}_1$ and $(▸\mathcal{F}{)}_{n+1}={\mathcal{F}}_n={\mathcal{H}}_{n+1}$ by definition 163.10. The restriction maps agree by construction.

Uniqueness. Let ${\mathcal{H}}^{\prime }$ satisfy the same isomorphism. At level $1$ both are one-point sets. Suppose a family of bijections ${\mathcal{H}}_m^{\prime }\to {\mathcal{H}}_m$ commuting with restriction has been given for $m\le n$. By lemma 163.2 and definition 163.6, the set ${\mathcal{F}}_n$ is built from ${\mathcal{H}}_1,\dots ,{\mathcal{H}}_n$ by disjoint unions, products and function sets, so those bijections induce a bijection ${\mathcal{F}}_n^{\prime }\to {\mathcal{F}}_n$; composing with the two isomorphisms gives a bijection ${\mathcal{H}}_{n+1}^{\prime }\to {\mathcal{H}}_{n+1}$, and it commutes with restriction because the isomorphisms do. ◻

Proof. Suppose a transition sequence from $⟨h\mid e⟩$ performs no Read step. Replace $\mathsf{get}$ everywhere by a fresh variable $g:F$ and $\mathsf{set}(e_1;e_2)$ by $(\lambda z:F.e_2)e_1$ with $z$ not free in $e_2$. This translation sends every Beta step to a Beta step, every Succ step to a Succ step and every Write step to a Beta step of the simply typed calculus, and it sends well-typed terms of ${\mathrm{\Lambda }}_{\mathsf{cell}}$ to well-typed terms of the simply typed calculus over the context $g:F$. By the normalization theorem of chapter 2 that calculus has no infinite reduction sequence from a well-typed term, so the original sequence is finite.

Hence a transition sequence with only finitely many Read steps decomposes into finitely many Read-free segments, each finite, and is therefore finite itself. ◻

Proof. By induction on $E$. For $E=[]$ take $K_{[]}(\rho ,a,{\hslash }^{\prime }):=\eta (a,{\hslash }^{\prime })$; the equation is then ${\eta }^{†}([[e]]\rho \hslash )=[[e]]\rho \hslash$, which is proposition 163.9. For each other case the corresponding clause of definition 163.16 is already of the displayed form with the inductively given $K$ substituted into the outer continuation; associativity of $(-{)}^{†}$, again from proposition 163.9, merges the two continuations into one. We display the case $E=E^{\prime }{e}_2$: the clause for application gives where $c$ is the continuation of the application clause; the second equality is the induction hypothesis followed by associativity, and the bracketed map is $K_{E^{\prime }{e}_2}$. The remaining three cases are the same computation with $c$ replaced by the continuation of the clause for $v[]$, for $\mathsf{suc}$, and for $\mathsf{set}$. ◻

Proof. By induction on the derivation of $\mathrm{\Gamma },x:\tau ⊢e:\sigma$. We display the two cases in which the variable is consumed or captured; the remaining four clauses of definition 163.16 are composites of the subterm interpretations with maps not mentioning $\rho$, so each is the induction hypothesis applied componentwise.

Variable case. If $e=x$ then $e[v/x]=v$ and $[[v]]\rho \hslash =\eta ([[v{]]}^{\mathrm{v}},\hslash )=[[x]](\rho ,[[v{]]}^{\mathrm{v}})\hslash$ by the clause for variables. If $e=y$ with $y$ distinct from $x$, both sides are $\eta ({\rho }_y,\hslash )$.

Binder case. If $e=\lambda y:{\sigma }_1.e_1$ with $y\notin \mathrm{FV}(v)\cup \{x\}$, then and the right-hand side is $[[\lambda y:{\sigma }_1.e_1]](\rho ,[[v{]]}^{\mathrm{v}})\hslash$ after exchanging the last two components of the environment, which is legal because the two variables are distinct. ◻

Proof. By lemma 163.17 it suffices to treat the redex, since both sides are the same continuation applied to the interpretation of the redex.

Beta. Unfolding the clauses for application and abstraction, $$[[(\lambda x:\tau .e)v]]\rho \hslash \stackrel{definition163.16}{=}(\lambda a.[[e]](\rho ,a))[[v{]]}^{\mathrm{v}}\hslash \stackrel{lemma163.18}{=}[[e[v/x]]]\rho \hslash ,$$ where $[[v{]]}^{\mathrm{v}}$ is the value component of $[[v]]\rho \hslash$.

Succ. Both sides are $\eta (n+1,\hslash )$.

Write. The clause for $\mathsf{set}$ evaluates $e_1$ to a value $v$ with function component ${\phi }_v$ and continues with $[[e_2]]\rho (\mathrm{next}{\phi }_v)$, and $\mathrm{next}{\phi }_v=[[v{]]}_{\mathcal{H}}$ by definition 163.16. No $\theta$ is produced.

Read. Write $\hslash =[[h{]]}_{\mathcal{H}}=\mathrm{next}({\phi }_h)$. Then the middle step by naturality of $\mathrm{next}$. Applying lemma 163.17 to both sides and using that $(-{)}^{†}$ commutes with $\theta$ by definition 163.8 gives the displayed equation. ◻

Proof. Induction on the length of the transition sequence, applying the appropriate clause of theorem 163.19 at each step; the Read clause contributes one $\theta$ and the other three contribute none. At the end the configuration is a value, and the clauses of definition 163.16 for numerals and abstractions give the displayed $\eta$. ◻

Proof. Every closed well-typed term is a value or decomposes uniquely as $E⟨e_0⟩$ with $e_0$ one of $(\lambda x:\tau .e)v$, $\mathsf{suc}\underset{―}{n}$, $\mathsf{get}$, $\mathsf{set}(v;e)$; the decomposition is unique because the grammar of $E$ in definition 163.13 fixes, at each constructor, which subterm is evaluated first, and the value grammar determines when to move on. Exactly one transition applies to each of the four redexes. For progress, a closed well-typed non-value term has such a decomposition by induction on its typing derivation: at an application $e_1{e}_2$ either $e_1$ is not a value, and the induction hypothesis gives a decomposition inside $E{e}_2$, or $e_1$ is a value of function type, hence an abstraction by inspection of the value grammar, and the same argument applies to $e_2$. ◻

Proof. By lemma 163.22 exactly one of two things happens: the transition sequence from $⟨h\mid e⟩$ is finite and ends in a value, or it is infinite.

Convergent case. Corollary 163.20 gives the displayed right-hand side, with $m$ the value of the numeral reached.

Divergent case. By proposition 163.15 the sequence contains infinitely many Read steps. Fix $n$ and take a prefix containing $n$ Read steps, ending at $⟨h_n\mid e_n⟩$. Applying theorem 163.19 along that prefix gives $[[⟨h\mid e⟩]]={\theta }^n(u)$ for some $u$. By proposition 163.7 the only element of $(\mathsf{L}(\mathrm{\Delta }(\mathbb{N})\times \mathcal{H}){)}_n$ with $n$ leading $\theta$’s is ${\theta }^n(\mathrm{\perp })$, so $[[⟨h\mid e⟩{]]}_n=(\mathrm{\perp }{)}_n$. As $n$ was arbitrary, $[[⟨h\mid e⟩]]=\mathrm{\perp }$.

The two right-hand sides are distinct, since ${\theta }^k(\eta (m,{\hslash }^{\prime }))$ at stage $k+1$ is not ${\theta }^{k+1}(\mathrm{\perp })$; so each direction of the stated equivalences follows from the other case. ◻

Proof. For ${\mathcal{V}}_{\mathbb{N}}$ the level plays no role. For ${\mathcal{V}}_{\tau \to \sigma }$ the defining condition quantifies over all $m\le n$, so it is inherited at $n-1$; and restriction of $\phi$ from level $n$ to level $n-1$ deletes its top component by lemma 163.2, leaving the components at $m\le n-1$ unchanged. For $\mathcal{W}$: an element of ${\mathcal{W}}_{n+2}$ is a pair in $({\mathcal{V}}_F{)}_{n+1}$, which restricts into $({\mathcal{V}}_F{)}_n$, that is into ${\mathcal{W}}_{n+1}$; and every pair lies in ${\mathcal{W}}_1$. For ${\mathcal{C}}_{\tau }$, restriction of $\theta (t)$ from level $n+1$ is $\theta (r(t))$ or, at $n=1$, the element $\mathrm{\perp }$; the first case is the induction hypothesis and the second is unconditional. Restriction of $\eta (a,\hslash )$ is $\eta (r(a),r(\hslash ))$, and the operational conditions do not mention the level. ◻