3.1 Call-by-name abstract machine

The call-by-name abstract machine for System T is based on the Krivine machine (Krivine, 2007), which is defined in terms of these continuations (representing evaluation contexts, for example, $\operatorname{\mathbf{tp}}$ represents the empty, top-level context) and transition rules: ^{Footnote 1} $^{\kern-1pt,}$ ^{Footnote 2}

\begin{align*} E &::= \operatorname{\mathbf{tp}} \mid N \cdot E \mid \operatorname{\mathbf{rec}} \{ \operatorname{zero} \to M \mid \operatorname{succ} x \to z. N \} \operatorname{\mathbf{with}} E\end{align*}

Refocusing rules:

\begin{align*} \langle {M~N} |\!| {E} \rangle &\mapsto \langle {M} |\!| {N \cdot E} \rangle \\ \langle {\operatorname{\mathbf{rec}} M \operatorname{\mathbf{as}} \{\dots\} } |\!| {E} \rangle &\mapsto \langle {M} |\!| {\operatorname{\mathbf{rec}} \{\dots\} \operatorname{\mathbf{with}} E} \rangle\end{align*}

Reduction rules:

The first two rules are refocusing rules that move the attention of the machine closer to the next reduction building a larger continuation: $N \cdot E$ corresponds to the context $E[\square~N]$ , and the continuation $\operatorname{\mathbf{rec}} \{\operatorname{zero} \to N \mid \operatorname{succ} x \to y.N'\} \operatorname{\mathbf{with}} E$ corresponds to the context $E[\operatorname{\mathbf{rec}} \square \operatorname{\mathbf{as}} \{\operatorname{zero} \to N \mid \operatorname{succ} x \to y.N'\} ]$ . The latter three rules are reduction rules which correspond to steps of the operational semantics in Fig. 3. While the distinction between refocusing and reduction rules is just a mere classification now, the difference will become an important tool for generalizing the abstract machine into a more uniform presentation later in Section 3.3.

3.2 Call-by-value abstract machine

A CEK-style (Felleisen & Friedman, 1986), call-by-value abstract machine for System T—which evaluates applications $M_1~M_2~\dots~M_n$ left-to-right to match the call-by-value semantics in Fig. 3—is given by these continuations E and transition rules:

\begin{align*} E &::= \operatorname{\mathbf{tp}} \mid n \cdot E \mid V \circ E \mid \operatorname{succ} \circ E \mid \operatorname{\mathbf{rec}} \{\operatorname{zero} \to M \mid \operatorname{succ} x \to y. N\} \operatorname{\mathbf{with}} E\end{align*}

Refocusing rules:

\begin{align*} \langle {M~N} |\!| {E} \rangle &\mapsto \langle {M} |\!| {N \cdot E} \rangle \\ \langle {V} |\!| {R \cdot E} \rangle &\mapsto \langle {R} |\!| {V \circ E} \rangle \\ \langle {V} |\!| {V' \circ E} \rangle &\mapsto \langle {V'} |\!| {V \cdot E} \rangle \\ \langle {\operatorname{\mathbf{rec}} M \operatorname{\mathbf{as}} \{\dots\}} |\!| {E} \rangle &\mapsto \langle {M} |\!| {\operatorname{\mathbf{rec}} \{\dots\} \operatorname{\mathbf{with}} E} \rangle \\ \langle {\operatorname{succ} R} |\!| {E} \rangle &\mapsto \langle {R} |\!| {\operatorname{succ} \circ E} \rangle \\ \langle {V} |\!| {\operatorname{succ} \circ E} \rangle &\mapsto \langle {\operatorname{succ} V} |\!| {E} \rangle\end{align*}

Reduction rules:

where R stands for a non-value term. Since the call-by-value operational semantics has more forms of evaluation contexts, this machine has additional refocusing rules for accumulating more forms of continuations including applications of functions ( $V \circ E$ corresponding to $E[V~\square]$ ) and the successor constructor ( $\operatorname{succ} \circ E$ corresponding to $E[\operatorname{succ}~\square]$ ). Also note that the final reduction rule for the $\operatorname{succ}$ case of recursion is different, accounting for the fact that recursion in call-by-value follows a different order than in call-by-name. Indeed, the recursor must explicitly accumulate and build upon a continuation, “adding to” the place it returns to with every recursive call. But otherwise, the reduction rules are the same. ^{Footnote 3}

3.3 Uniform abstract machine

We now unite both evaluation strategies with a common abstract machine, shown in Fig. 4. As before, machine configurations are of the form

$$\langle {v} |\!| {e} \rangle$$

which put together a term v and a continuation e (often referred to as a coterm). However, both terms and continuations are more general than before. Our uniform abstract machine is based on the sequent calculus, a symmetric language reflecting many dualities of classical logic (Curien & Herbelin, 2000; Wadler, Reference Wadler2003). An advantage of this sequent-based system is that the explicit symmetry inherent in its syntax gives us a language to express and understand the implicit symmetries that are hiding in computations and types. This utility of a symmetric language is one of the key insights of our approach, which will let us syntactically derive a notion of corecursion which is dual to recursion.

Fig. 4. Uniform, recursive abstract machine for System T.

Unlike the previous machines, continuations go beyond evaluation contexts and include ${\tilde{\mu}}{x}. \langle {v} |\!| {e} \rangle$ , which is a continuation that binds its input value to x and then steps to the machine state $\langle {v} |\!| {e} \rangle$ . This new form allows us to express the additional call-by-value evaluation contexts: $V \circ E$ becomes ${\tilde{\mu}}{x}. \langle {V} |\!| {x \cdot E} \rangle$ , and $\operatorname{succ} \circ E$ is ${\tilde{\mu}}{x}. \langle {\operatorname{succ} x} |\!| {E} \rangle$ . Evaluation contexts are also more restrictive than before; only values can be pushed on the calling stack. We represent the application continuation $M \cdot E$ with a non-value argument M by naming its partner—the generic value V—with y: $ {\tilde{\mu}}{y}. \langle {M} |\!| {{\tilde{\mu}}{x}. \langle {y} |\!| {x \cdot E} \rangle} \rangle$ . ^{Footnote 4}

The refocusing rules can be subsumed all together by extending terms with a dual form of ${\tilde{\mu}}$ -binding. The $\mu$ -abstraction expression $\mu{\alpha}. \langle {v} |\!| {e} \rangle$ binds its continuation to $\alpha$ and then steps to the machine state $\langle {v} |\!| {e} \rangle$ . With $\mu$ -bindings, all the refocusing rules for call-by-name and call-by-value can be encoded in terms of $\mu$ and ${\tilde{\mu}}$ . ^{Footnote 5} It is also not necessary to do these steps at run-time, but can all be done before execution through a compilation step. The target language of this compilation step becomes the syntax of the uniform abstract machine, as shown in Fig. 4. This language does not include anymore applications $M~N$ and the recursive term $\operatorname{\mathbf{rec}} M \operatorname{\mathbf{as}} \{\dots\}$ . Also, unlike System T, the syntax of terms and coterms depends on the definition of values and covalues; $\operatorname{succ} V$ , $\operatorname{\mathbf{rec}} \{\dots\} \operatorname{\mathbf{with}} E$ , and call stacks $V \cdot E$ are valid in both call-by-name and call-by-value, just with different definitions of V and E. Yet, all System T terms can still be translated to the smaller language of the machine, as shown in Fig. 5. General terms also include the $\mu$ - and ${\tilde{\mu}}$ -binders described above: $\mu{\alpha}. c$ is not a value in call-by-value, and ${\tilde{\mu}}{x}. c$ is not a covalue in call-by-name. So for example, $\operatorname{succ} (\mu{\alpha}. c)$ is not a legal term in call-by-value, but can be translated instead to $\mu{\beta}. \langle {\mu{\alpha}. c} |\!| {{\tilde{\mu}}{x}. \langle {\operatorname{succ} x} |\!| {\beta} \rangle} \rangle$ following Fig. 5. Similarly $x \cdot {\tilde{\mu}}{y}. c$ is not a legal call stack in call-by-name, but it can be rewritten to ${\tilde{\mu}}{z}. \langle {\mu{\alpha}.\langle {z} |\!| {x \cdot \alpha} \rangle} |\!| {{\tilde{\mu}}{y}. c} \rangle$ .

Fig. 5. The translation from System T to the uniform abstract machine.

As with System T, the notions of values and covalues drive the reduction rules in Fig. 4. In particular, the $\mu$ and ${\tilde{\mu}}$ rules will only substitute a value for a variable or a covalue for a covariable, respectively. Likewise, the $\beta_\to$ rule implements function calls, but taking the next argument value off of a call stack and plugging it into the function. The only remaining rules are $\beta_{\operatorname{zero}}$ and $\beta_{\operatorname{succ}}$ for reducing a recursor when given a number constructed by $\operatorname{zero}$ or $\operatorname{succ}$ . While the $\beta_{\operatorname{zero}}$ is exactly the same as it was previously in both specialized machine, notice how $\beta_{\operatorname{succ}}$ is different. Rather than committing to one evaluation order or the other, $\beta_{\operatorname{succ}}$ is neutral: the recursive predecessor (expressed as the term $\mu{\alpha}.\langle {V} |\!| {\operatorname{\mathbf{rec}}\{\dots\}\operatorname{\mathbf{with}}\alpha} \rangle$ on the right-hand side) is neither given precedence (at the top of the command) nor delayed (by substituting it for y). Instead, this recursive predecessor is bound to y with a ${\tilde{\mu}}$ -abstraction. This way, the correct evaluation order can be decided in the next step by either an application of $\mu$ or ${\tilde{\mu}}$ reduction.

Notice one more advantage of translating System T at “compile-time” into a smaller language in the abstract machine. In the same way that the $\lambda$ -calculus supports both a deterministic operational semantics along with a rewriting system that allows for optimizations that apply reductions to any sub-expression, so too does the syntax of this uniform abstract machine allow for optimizations that reduce sub-expressions in advance of the usual execution order. For example, consider the term $\operatorname{\mathbf{let}} f = (\lambda{x}. (\lambda{y}. y)~x) \operatorname{\mathbf{in}} M$ . ^{Footnote 6} Its next step is to substitute the abstraction $(\lambda{x}. (\lambda{y}. y)~x)$ for f in M, and every time M calls $(f~V)$ we must repeat the steps \begin{align*} (\lambda{x}. (\lambda{y}. y)~x)~V \mapsto (\lambda{y}. y)~V \mapsto V\end{align*} again. But applying a $\beta$ reduction under the $\lambda$ bound to f, we can instead optimize this expression to $\operatorname{\mathbf{let}} f = (\lambda{x}. x) \operatorname{\mathbf{in}} M$ . With this optimization, when M calls $(f~V)$ it reduces as $(\lambda{x}. x)~V \mapsto V$ in one step. This same approach applies to the uniform abstract machine, too, because all elimination forms like $\square~N$ and $\operatorname{\mathbf{rec}} \square \operatorname{\mathbf{as}} \{\dots\}$ have been compiled to continuations of the form $N \cdot \alpha$ and $\operatorname{\mathbf{rec}}\{\dots\}\operatorname{\mathbf{with}}\alpha$ that we can use to apply machine reductions. For example, the translation of $\operatorname{\mathbf{let}} f = (\lambda{x}. (\lambda{y}. y)~x) \operatorname{\mathbf{in}} M$ is quite large, but we can optimize away several $\mu$ and ${\tilde{\mu}}$ reductions—which are responsible for the administrative duty of directing information and control flow—in advance inside sub-expressions to simplify the translation to: ^{Footnote 7}

where $\mathrel{\to\!\!\!\!\to}$ denotes zero or more reduction steps $\mapsto$ applied inside any context. From there, we can further optimize the program by simplifying the application of $\lambda{y}. y$ in advance, by applying the $\beta_\to$ rule inside the $\mu$ s binding $\alpha$ and $\beta$ and the $\lambda$ binding x like so:

This way, we are able to still optimize the program even after compilation to the abstract machine language, the same as if we were optimizing the original $\lambda$ -calculus source code.

Intermezzo 3.1 We can now summarize how some basic concepts of recursion are directly modeled in our syntactic framework:

• – With inductive data types, values are constructed and the consumer is a recursive process that uses the data. Natural numbers are terms or producers, and their use is a process which is triggered when the term becomes a value.

• – Construction of data is finite and its consumption is (potentially) infinite, in the sense that there must be no limit to the size of the data that a consumer can process. We can only build values from a finite number of constructor applications. However, the consumer does not know how big of an input it will be given, so it has to be ready to handle data structures of any size. In the end, termination is preserved because only finite values are consumed.

• – Recursion uses the data, rather than producing it. $\operatorname{\mathbf{rec}}$ is a coterm, not a term.

• – Recursion starts big and potentially reduces down to a base case. As shown in the reduction rules, the recursor breaks down the data structure and might end when the base case is reached.

• – The values of a data structures are all independent from each other but the results of the recursion potentially depend on each other. In the reduction rule for the successor case, the result at a number n might depend on the result at $n-1$ .

3.4 Examples of recursion

Restricting the $\mu$ and ${\tilde{\mu}}$ rules to only binding (co)values effectively implements the chosen evaluation strategy. For example, consider the application $(\lambda z. \operatorname{succ}\operatorname{zero})~((\lambda x. x)~\operatorname{zero})$ . Call-by-name evaluation will reduce the outer application first and return $\operatorname{succ}\operatorname{zero}$ right away, whereas call-by-value evaluation will first reduce the inner application $((\lambda x.x)~\operatorname{zero})$ . How is this different order of evaluation made explicit in the abstract machine, which uses the same set of rules in both cases? First, consider the translation of $[\![ (\lambda z. x)~((\lambda x. x)~y) ]\!]$ :

This is quite a large term for such a simple source expression. To make the example clearer, let us first simplify the administrative-style ${\tilde{\mu}}$ -bindings out of the way (using applications of ${\tilde{\mu}}$ rules for to substitute $\lambda$ -abstractions and variables in a way that is valid for both call-by-name and call-by-value) to get the shorter term:

\begin{align*} [\![ (\lambda z. x)~((\lambda x. x)~y) ]\!] &\mathrel{\to\!\!\!\!\to}_{{\tilde{\mu}}} \mu{\alpha}. \langle {\mu{\beta}.\langle {\lambda x. x} |\!| {y \cdot \beta} \rangle} |\!| {} {{\tilde{\mu}}{z}. \langle {\lambda z. x} |\!| {z \cdot \alpha} \rangle \rangle}\end{align*}

To execute it, we need to put it in interaction with an actual context. In our case, we can simply use a covariable $\alpha$ . Call-by-name execution then proceeds from the simplified as:

And call-by-value execution of the simplified proceeds as:

The first two steps are the same for either evaluation strategy. Where the two begin to diverge is in the third step (marked by a $*$ ), which is an interaction between a $\mu$ - and a ${\tilde{\mu}}$ -binder. In call-by-name, the ${\tilde{\mu}}$ rule takes precedence (because a ${\tilde{\mu}}$ -coterm is not a covalue), leading to the next step which throws away the first argument, unevaluated. In call-by-value, the $\mu$ rule takes precedence (because a $\mu$ -term is not a value), leading to the next step which evaluates the first argument, producing y to bind to z that eventually gets thrown away.

Consider the System T definition of $\mathit{plus}$ from Example 2.1, which is expressed by the machine term

The application $\mathit{plus}~2~3$ is then expressed as $ \mu{\alpha}. \langle {\mathit{plus}} |\!| { } \rangle {2 \cdot 3 \cdot \alpha}$ , which is obtained by reducing some $\mu$ - and ${\tilde{\mu}}$ -bindings in advance. Putting this term in the context $\alpha$ , in call-by-value it executes (eliding the branches of the $\operatorname{\mathbf{rec}}$ continuation, which are the same in every following step) like so:

Notice how this execution shows how, during the recursive traversal of the data structure, the return continuation of the recursor is updated (in blue) to keep track of the growing context of pending operations, which must be fully processed before the final value of 5 ( $\operatorname{succ}(\operatorname{succ} 3)$ ) can be returned to the original caller ( $\alpha$ ). This update is implicit in the $\lambda$ -calculus-based System T, but becomes explicit in the abstract machine. In contrast, call-by-name only computes numbers as far as they are needed, otherwise stopping at the outermost constructor. The call-by-name execution of the above command proceeds as follows, after fast-forwarding to the first application of $\beta_{\operatorname{succ}}$ :

Unless $\alpha$ demands to know something about the predecessor of this number, the term $\mu{\beta}.\langle {\operatorname{succ}\operatorname{zero}} |\!| {\operatorname{\mathbf{rec}}\{\dots\}\operatorname{\mathbf{with}}\beta} \rangle$ will not be computed.

Now consider $\mathit{pred}~(\operatorname{succ}(\operatorname{succ}\operatorname{zero}))$ , which can be expressed in the machine as:

\begin{align*} & \mu{\alpha}. \langle {\mathit{pred}} |\!| {} \rangle {\operatorname{succ}(\operatorname{succ}\operatorname{zero}) \cdot \alpha} \\ \mathit{pred} &= \lambda x. \mu{\beta}.\langle {x} |\!| {\operatorname{\mathbf{rec}}\{\operatorname{zero}\to\operatorname{zero}\mid\operatorname{succ} x\to z.x\}\operatorname{\mathbf{with}}\beta} \rangle\end{align*}

In call-by-name, it executes with respect to $\alpha$ like so:

Notice how, after the first application of $\beta_{\operatorname{succ}}$ , the computation finishes in just one ${\tilde{\mu}}$ step, even though we began recursing on the number 2. In call-by-value instead, we have to continue with the recursion even though its result is not needed. Fast-forwarding to the first application of the $\beta_{\operatorname{succ}}$ rule, we have:

3.5 Recursion versus iteration: Expressiveness and efficiency

Recall how the recursor performs two jobs at the same time: finding the predecessor of a natural number as well as calculating the recursive result given for the predecessor. These two functionalities can be captured separately by continuations that perform shallow case analysis and iteration, respectively. Rather than including them as primitives, both can be expressed as syntactic sugar in the form of macro-expansions in the language of the abstract machine like so:

\begin{align*}\begin{aligned} & \operatorname{\mathbf{case}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to v \\ \mid& \operatorname{succ} x &&\to w \} \end{alignedat} \\ &\operatorname{\mathbf{with}} E\end{aligned}&:=\!\!\begin{aligned} &\operatorname{\mathbf{rec}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to v \\ \mid& \operatorname{succ} x &&\to \rule{1ex}{0.5pt}\,. w \} \end{alignedat} \\ &\operatorname{\mathbf{with}} E\end{aligned}&~~\begin{aligned} & \operatorname{\mathbf{iter}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to v \\ \mid& \operatorname{succ} &&\to x.w \} \end{alignedat} \\ &\operatorname{\mathbf{with}} E\end{aligned}&:=\!\!\begin{aligned} &\operatorname{\mathbf{rec}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to v \\ \mid& \operatorname{succ} \rule{1ex}{0.5pt} &&\to x.w \} \end{alignedat} \\ &\operatorname{\mathbf{with}} E\end{aligned}\end{align*}

The only cost of this encoding of $\operatorname{\mathbf{case}}$ and $\operatorname{\mathbf{iter}}$ is an unused variable binding, which is easily optimized away. In practice, this encoding of iteration will perform exactly the same as if we had taken $\operatorname{\mathbf{iter}}$ ation as a primitive.

While it is less obvious, going the other way is still possible. It is well known that primitive recursion can be encoded as a macro-expansion of iteration using pairs. The usual macro-expansion in System T is:

\begin{align*} \begin{aligned} & \operatorname{\mathbf{rec}} M \operatorname{\mathbf{as}} \\ &\quad \begin{alignedat}{2} &\{~ \operatorname{zero} &&\to N \\ &\mid \operatorname{succ} x &&\to y. N' \} \end{alignedat} \end{aligned} &:= \begin{aligned} &\operatorname{snd}~ ( \operatorname{\mathbf{iter}} M \operatorname{\mathbf{as}} \\ &\qquad\quad \begin{alignedat}{2} &\{~ \operatorname{zero} &&\to (\operatorname{zero}, N) \\ &\mid \operatorname{succ} &&\to (x,y).\, (\operatorname{succ} x, N') \} ) \end{alignedat} \end{aligned}\end{align*}

The trick to this encoding is to use $\operatorname{\mathbf{iter}}$ to compute both a reconstruction of the number being iterated upon (the first component of the iterative result) alongside the desired result (the second component). Doing both at once gives access to the predecessor in the $\operatorname{succ}$ case, which can be extracted from the first component of the previous result (given by the variable x in the pattern match (x,y)).

To express this encoding in the abstract machine, we need to extend it with pairs, which look like (Wadler, Reference Wadler2003):

\begin{align*} \langle {(v, w)} |\!| {\operatorname{fst} E} \rangle &\mapsto \langle {v} |\!| {E} \rangle & \langle {(v, w)} |\!| {\operatorname{snd} E} \rangle &\mapsto \langle {w} |\!| {E} \rangle & (\beta_\times)\end{align*}

In the syntax of the abstract machine, the analogous encoding of a $\operatorname{\mathbf{rec}}$ continuation as a macro-expansion looks like this:

\begin{align*}\begin{aligned} &\operatorname{\mathbf{rec}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to v \\ \mid& \operatorname{succ} x &&\to y.w \} \end{alignedat} \\ &\operatorname{\mathbf{with}} E\end{aligned}&:=\begin{aligned} &\operatorname{\mathbf{iter}} \begin{alignedat}[t]{2} \{& \operatorname{zero} &&\to (\operatorname{zero}, v) \\ \mid& \operatorname{succ} &&\to (x,y). (\operatorname{succ} x, w) \} \end{alignedat} \\ &\operatorname{\mathbf{with}}{} \operatorname{snd} E\end{aligned}\end{align*}

Since the inductive case w might refer to both the predecessor x and the recursive result for the predecessor (named y), the two parts must be extracted from the pair returned from iteration. Here we express this extraction in the form of pattern matching, which is shorthand for:

\begin{equation*} (x,y). (v_1,v_2) := z. \mu{\alpha}. \langle {z} |\!| {\operatorname{fst}({\tilde{\mu}}{x}. \langle {z} |\!| {\operatorname{snd}({\tilde{\mu}}{y}. \langle {(v_1,v_2)} |\!| {\alpha} \rangle)} \rangle)} \rangle\end{equation*}

Note that the recursor continuation is tasked with passing its final result to E once it has finished. In order to give this same result to E, the encoding has to extract the second component of the final pair before passing it to E, which is exactly what $\operatorname{snd} E$ expresses.

Unfortunately, this encoding of recursion is not always as efficient as the original. If the recursive parameter y is never used (such as in the $\mathit{pred}$ function), then $\operatorname{\mathbf{rec}}$ can provide an answer without computing the recursive result. However, when encoding $\operatorname{\mathbf{rec}}$ with $\operatorname{\mathbf{iter}}$ , the result of the recursive value must always be computed before an answer is seen, regardless of whether or not y is needed. As such, redefining $\mathit{pred}$ using $\operatorname{\mathbf{iter}}$ in this way changes it from a constant time (O(1)) to a linear time (O(n)) function. Notice that this difference in cost is only apparent in call-by-name, which can be asymptotically more efficient when the recursive y is not needed to compute N’, as in $\mathit{pred}$ . In call-by-value, the recursor must descend to the base case anyway before the incremental recursive steps are propagated backward. That is to say, the call-by-value $\operatorname{\mathbf{rec}}$ has the same asymptotic complexity as its encoding via $\operatorname{\mathbf{iter}}$ .

3.6 Types and correctness

We can also give a type system directly for the abstract machine, as shown in Fig. 6. This system has judgments for assigning types to terms as usual: $\Gamma \vdash v : A$ says v produces an output of type A. In addition, there are also judgments for assigning types to coterms ( $\Gamma \vdash e \div A$ says e consumes an input of type A) and commands ( $\Gamma \vdash c \ $ says c is safe to compute, and does not produce or consume anything).

Fig. 6. Type system for the uniform, recursive abstract machine.

This type system ensures that the machine itself is type safe: well-typed, executable commands don’t get stuck while in the process of computing a final state. For our purposes, we will consider “programs” to be commands c with just one free covariable (say $\alpha$ ), representing the initial, top-level continuation expecting a natural number as the final answer. Thus, well-typed executable commands will satisfy $\alpha\div\operatorname{Nat} \vdash c \ $ . The only final states of these programs have the form $\langle {\operatorname{zero}} |\!| {\alpha} \rangle$ , which sends 0 to the final continuation $\alpha$ , or , which sends the successor of some V to $\alpha$ . But the type system ensures more than just type safety: all well-typed programs will eventually terminate. That’s because $\operatorname{\mathbf{rec}}$ -expressions, which are the only form of recursion in the language, always decrement their input by 1 on each recursive step. So together, every well-typed executable command will eventually (termination) reach a valid final state (type safety).

The truth of this theorem follows directly from the latter development in Section 6, since it is a special case of Theorem 6.14.

Intermezzo 3.3 Since our abstract machine is based on the logic of Gentzen’s sequent (Gentzen, 1935), the type system in Fig. 6 too can be viewed as a term assignment for a particular sequent calculus. In particular, the statement $v : A$ corresponds to a proof that A is true. Dually $e \div A$ corresponds to a proof that A is false, and hence the notation, which can be understood as a built-in negation $-$ in $e : -A$ . As such, the built-in negation in every $e \div A$ (or $\alpha \div A$ ) can be removed by swapping between the left- and right-hand sides of the turnstyle ( $\vdash$ ), so that $e \div A$ on the right becomes $e : A$ on the left, and $\alpha \div A$ on the left becomes $\alpha : A$ on the right. Doing so gives a conventional two-sided sequent calculus as (Ariola et al., 2009; Downen & Ariola, 2018b), where the rules labeled L with conclusions of the form $x_i : B_i, \alpha_j \div C_j \vdash e \div A$ correspond to left rules of the form $x_i:B_i \mid e : A \vdash \alpha_j:C_j$ in the sequent calculus. In general, the three forms of two-sided sequents correspond to these three different typing judgments used here (with $\Gamma$ rearranged for uniformity):

• \begin{align*} x_i : B_i, \overset{i}\dots, \alpha_j \div C_j, \overset{j}\dots \vdash v : A \end{align*} corresponds to \begin{align*} x_i : B_i, \overset{i}\dots \vdash v : A \mid \alpha_j : C_j, \overset{j}\dots \end{align*} .

• \begin{align*} x_i : B_i, \overset{i}\dots, \alpha_j \div C_j, \overset{j}\dots \vdash e \div A \end{align*} corresponds to \begin{align*} x_i : B_i, \overset{i}\dots \mid e : A \vdash \alpha_j : C_j, \overset{j}\dots \end{align*} .

• \begin{align*} x_i : B_i, \overset{i}\dots, \alpha_j \div C_j, \overset{j}\dots \vdash c \ \end{align*} corresponds to \begin{align*} c : (x_i : B_i, \overset{i}\dots \vdash \alpha_j : C_j, \overset{j}\dots) \end{align*} .

4.1 Examples of corecursion

The infinite streams $x, x, x, x, \dots$ and $x, f~x, f~(f ~ x), \dots$ , which are written in Haskell as

\begin{align*} \mathit{always}~x &= x : \mathit{always}~x & \mathit{repeat}~f~x &= x : \mathit{repeat}~f~(f~x)\end{align*}

can be calculated by the abstract machine terms

\begin{align*} \begin{aligned}[t] \textit{always} \ x = \operatorname{\mathbf{corec}}{} \{& \operatorname{head} \alpha \to \alpha \\ \mid& \operatorname{tail} \_ \to \gamma.\gamma \} \\ \operatorname{\mathbf{with}}{}& x \end{aligned} \qquad \begin{aligned}[t] \textit{repeat} \ f \ x = \operatorname{\mathbf{corec}}{} \{& \operatorname{head} \alpha \to \alpha \\ \mid& \operatorname{tail} \_ \to \gamma.{\tilde{\mu}}{x}. \langle {f} |\!| { x \cdot \gamma} \rangle \} \\ \operatorname{\mathbf{with}}{}& x \end{aligned}\end{align*}

So when an observer asks $\mathit{always} \ x$ ( $\mathit{repeat}\ f \ x$ ) for its head element (matching the copattern $\operatorname{head}\alpha$ ), $\mathit{always} \ x$ ( $\mathit{repeat} \ f \ x$ ) returns (to $\alpha$ ) the current value of the seed x. Otherwise, when an observer asks for its tail (matching the copattern $\operatorname{tail}\beta$ ), $\mathit{always} \ x$ ( $\mathit{repeat} \ f \ x$ ) continues corecursing with the same seed x ( $\mu{\gamma}. \langle {f} |\!| {x \cdot \gamma} \rangle$ ).

The infinite streams containing all zeroes, and the infinite stream of all natural numbers counting up from 0, are then represented as:

\begin{align*} \mathit{zeroes} = \mu{\alpha}.\langle {\mathit{always}} |\!| {\operatorname \cdot zero\alpha} \rangle \\ \mathit{nats} = \mu{\alpha}.\langle {\mathit{repeat}} |\!| {succ \cdot \operatorname \cdot zero \alpha} \rangle\end{align*}

where $\mathit{succ}$ is defined as $\lambda x. \mu{\alpha}. \langle {\operatorname{succ} x} |\!| { } \rangle\alpha$ .

To better understand execution, let’s trace how computation works in both call-by-name and call-by-value. Asking for the third element of $\mathit{zeroes}$ proceeds with the following calculation in call-by-value (we let $\mathit{always}_x$ stand for the stream with x being the seed):

In contrast, notice how the same calculation in call-by-name builds up a delayed computation in the seed:

Consider the function that produces a stream that counts down from some initial number n to 0, and then staying at 0. Informally, this function can be understood as:

\begin{align*} \mathit{countDown} &: \operatorname{Nat} \to \operatorname{Stream} \operatorname{Nat} \\ \mathit{countDown}~n &= n, n-1, n-2, \dots, 3, 2, 1, 0, 0, 0, \dots\end{align*}

which corresponds to the Haskell function

\begin{align*} \mathit{countDown}~0 &= \mathit{zeroes} \\ \mathit{countDown}~n &= n : \mathit{countDown}~(n-1)\end{align*}

It is formally defined in the abstract machine like so:

\begin{align*}\begin{aligned}[t] \textit{countDown} \ n = \operatorname{\mathbf{corec}}{} \{& \operatorname{head} \alpha \to \alpha \\ \mid& \operatorname{tail} \_ \to \gamma. \begin{aligned}[t] \operatorname{\mathbf{rec}}{} \{& \operatorname{zero} \to \operatorname{zero} \\ \mid& \operatorname{succ} n \to n \} \operatorname{\mathbf{with}} \gamma \} \end{aligned} \\ \operatorname{\mathbf{with}}{}& n\end{aligned}\end{align*}

This definition of $\mathit{countDown}$ can be understood as follows:

• If the head of the stream is requested (matching the copattern $\operatorname{head}\alpha$ ), then the current value x of the seed is returned (to $\alpha$ ) as-is.

• Otherwise, if the tail is requested (matching the copattern $\operatorname{tail}\_$ ), then the current value of the seed is inspected: if it is 0, then 0 is used again as the seed; otherwise, the seed is the successor of some y, in which case y is given as the updated seed.

The previous definition of $\mathit{countDown}$ is not very efficient; once n reaches zero, one can safely returns the zeroes stream thus avoiding the test for each question. This can be avoided with the power of the corecursor as so:

\begin{align*}\begin{aligned}[t] \mathit{countDown'} \ n = \operatorname{\mathbf{corec}}{} \{& \operatorname{head} \alpha \to \alpha \\ \mid& \operatorname{tail} \beta \to \gamma. \begin{aligned}[t] \operatorname{\mathbf{rec}}{} \{& \operatorname{zero} \to \mu{\_}. \langle {\mathit{zeroes}} |\!| {\beta} \rangle \\ \mid& \operatorname{succ} n \to \gamma. n \} \operatorname{\mathbf{with}} \gamma \} \end{aligned} \\ \operatorname{\mathbf{with}}{}& n\end{aligned}\end{align*}

Note that in the coinductive step, the decision on which continuation is taken (the observer of the tail $\beta$ or the continuation of corecursion $\gamma$ ) depends on the current value of the seed. If the seed reaches 0 the corecursion is stopped and the stream of zeros is returned instead.

Another example of this “switching” behavior, where one corecursive loop (like $\mathit{countDown'}~0$ ) ends and switches to another corecursive loop (like $\mathit{zeroes}$ ) is the $\mathit{switch0}$ function informally written as

\begin{align*} \mathit{switch0}~(x_0,x_1,\dots,0,x_{i+1},\dots)~(y_0,y_1,\dots) &= x_0, x_1, \dots, 0, y_0, y_1, \dots &(\text{if } \forall j < i. x_j \neq 0) \\ \mathit{switch0}~(x_0,x_1,\dots)~(y_0,y_1,\dots) &= x_0, x_1, \dots &(\text{if } \forall j. x_j \neq 0)\end{align*}

which corresponds to the Haskell code:

\begin{align*} \mathit{switch0}~(0:xs)~ys &= 0 : ys \\ \mathit{switch0}~(x:xs)~ys &= x : \mathit{switch0}~xs~ys\end{align*}

Intuitively, $\mathit{switch0}~xs~ys$ will generate the stream produced by xs until a 0 is reached; at that point, the $\mathit{switch0}$ loop ends by returning 0 followed by the whole stream ys as-is. This example is more interesting than $\mathit{countDown}$ because there is no inductive argument (like a number or a list) that the function can inspect in advance to predict when the switch will occur. Instead, $\mathit{switch0}$ must generate its elements on demand only when they are requested, and the switch to ys will only happen if an observer decides to look deep enough into the stream to hit an 0 inside xs, which might never even happen. $\mathit{switch0}$ can be efficiently implemented in the abstract machine using both continuations provided by the corecursor like so:

\begin{align*} \mathit{switch0}~xs~ys = \operatorname{\mathbf{corec}} &\{ \operatorname{head} \alpha \to \alpha \\ &\mid \operatorname{tail} \beta \to \gamma. {\tilde{\mu}}{xs}. \langle {xs} |\!| { \operatorname{head} \begin{aligned}[t] \operatorname{\mathbf{rec}} &\{ \operatorname{zero} \to ys \\ &\mid \operatorname{succ} n \to \mu{\_}.\langle {xs} |\!| {\operatorname{tail} \gamma} \rangle \} \\ &\operatorname{\mathbf{with}} \beta \rangle \} \end{aligned} } \\ &\operatorname{\mathbf{with}} xs\end{align*}

The internal state to this corecursive loop contains the remainder of xs that hasn’t been seen yet. While the $\mathit{switch0}$ $\operatorname{\mathbf{corec}}$ loop is active, it will always generate the $\operatorname{head}$ of the current remainder of xs as its own $\operatorname{head}$ element. When the $\operatorname{tail}$ is requested, this loop checks the $\operatorname{head}$ of the xs remainder to decide what to do:

• if it is $\operatorname{zero}$ , then the whole stream ys gets returned to $\beta$ , which is the original caller who requested the $\operatorname{tail}$ of the stream, otherwise

• if it is $\operatorname{succ} n$ , the $\operatorname{\mathbf{corec}}$ loop inside $\mathit{switch0}$ will continue by returning the $\operatorname{tail}$ of the remaining xs to the continuation $\gamma$ which will update the internal state of the loop with one fewer element that has not yet been seen.

4.2 Properly de Morgan Dual (co)recursive types

Although we derived corecursion from recursion using duality, our prototypical examples of natural numbers and streams were not perfectly dual to one another. While the (co)recursive case of $\operatorname{tail} E$ looks similar enough to $\operatorname{succ} V$ , the base cases of $\operatorname{head} E$ and $\operatorname{zero}$ don’t exactly line up, because $\operatorname{head}$ takes a parameter but $\operatorname{zero}$ does not.

One way to perfect the duality is to generalize $\operatorname{Nat}$ to $\operatorname{Numbered} A$ which represents a value of type A labeled with a natural number (also known as Burroni naturals). $\operatorname{Numbered} A$ has two constructors: the base case $\operatorname{zero} : A \to \operatorname{Numbered} A$ labels an A value with the number 0, and $\operatorname{succ} : \operatorname{Numbered} A \to \operatorname{Numbered} A$ increments the numeric label while leaving the A value alone, as shown by the following rules:

In order to match the generalized $\operatorname{zero}$ constructor, the base case of the recursor needs to be likewise generalized with an extra parameter. In System T, this looks like \begin{align*} \operatorname{\mathbf{rec}} M \operatorname{\mathbf{as}}{} \{\operatorname{zero} x \to N \mid \operatorname{succ} y \to z.N'\} ,\end{align*} while in the abstract machine we get the generalized continuation \begin{align*} \operatorname{\mathbf{rec}}{} \{\operatorname{zero} x \to v \mid \operatorname{succ} y \to z.w\} \operatorname{\mathbf{with}} E .\end{align*} The typing rule for this continuation is:

It turns out that $\operatorname{Numbered} A$ is the proper de Morgan dual to $\operatorname{Stream} A$ . Notice how the two constructors $\operatorname{zero} V$ and $\operatorname{succ} W$ exactly mirror the two destructors $\operatorname{head} E$ and $\operatorname{tail} F$ when we swap the roles of values and covalues. The recursor continuation of the form \begin{align*} \operatorname{\mathbf{rec}}{} \{\operatorname{zero} x \to v \mid \operatorname{succ} y \to z.w\} \operatorname{\mathbf{with}} E\end{align*} is the perfect mirror image of the stream corecursor \begin{align*} \operatorname{\mathbf{corec}}{} \{\operatorname{head}\alpha \to e \mid \operatorname{tail}\beta \to \gamma.f\} \operatorname{\mathbf{with}} V\end{align*} when we likewise swap variables with covariables in the (co)patterns. In more detail, we can write the duality relation between values and covalues as $\mathrel{\overline\sim}$ . Assuming that $V \mathrel{\overline\sim} E$ , we have the following duality between the constructors and destructors of these two types:

\begin{align*} \operatorname{zero} V &\mathrel{\overline\sim} \operatorname{head} E & \operatorname{succ} V &\mathrel{\overline\sim} \operatorname{tail} E\end{align*}

For (co)recursion, we have the following dualities, assuming $v \mathrel{\overline\sim} e$ (under $x \mathrel{\overline\sim} \alpha$ ) $w \mathrel{\overline\sim} f$ (under $y \mathrel{\overline\sim} \beta$ and $z \mathrel{\overline\sim} \gamma$ ), and $V \mathrel{\overline\sim} E$ :

\begin{align*} \operatorname{\mathbf{corec}} \{\operatorname{head} \alpha \to e \mid \operatorname{tail} \beta \to \gamma. f\} \operatorname{\mathbf{with}} V &\mathrel{\overline\sim} \operatorname{\mathbf{rec}} \{\operatorname{zero} x \to v \mid \operatorname{succ} y \to z.w\} \operatorname{\mathbf{with}} E\end{align*}

We could also express the proper de Morgan duality by restricting streams instead of generalizing numbers. In terms of the type defined above, $\operatorname{Nat}$ is isomorphic to $\operatorname{Numbered} \top$ , where $\top$ represents the usual unit type with a single value (often written as ()). Since $\top$ corresponds to logical truth, its dual is the $\bot$ type corresponding to logical falsehood with no (closed) values, and a single covalue that represents an empty continuation. With this in mind, the type $\operatorname{Nat}$ is properly dual to $\operatorname{Stream} \bot$ , i.e., an infinite stream of computations which cannot return any value to their observer. ^{Footnote 8}

In order to fully realize this de Morgan duality in an interesting way that can talk about functions, we need to refer to the duals of those functions. Logically, the dual to the function type $A \to B$ (classical equivalent to $(\neg A) \vee B$ and $\neg (A \wedge (\neg B))$ , whose continuations $V \cdot E $ contain an argument V of type A paired with a consumer E of Bs) is a subtraction type $B - A$ (classically equivalent to $B \wedge (\neg A)$ for typing a pair $E \cdot V$ of a value V of type B and a continuation E expecting As). Following (Curien & Herbelin, 2000), this subtraction type, along with the units $\top$ and $\bot$ , can be added to our uniform abstract machine with the following extended syntax of (co)values, reduction rule $\beta_-$ for when a subtraction pair $E \cdot V$ interacts with the continuation abstraction $\tilde{\lambda} \alpha e$ , and typing rules:

Extending the uniform abstract machine with these new rules, lets us formally define a de Morgan duality transformation, shown in Fig. 9, that converts any term v producing type A into the coterm $v^\bot$ consuming type $A^\bot$ , converts any coterm e expecting type A to a term $e^\bot$ giving type $A^\bot$ , and converts a command c to its dual command $c^\bot$ . The duality transformation assumes a bijection between variables and covariables (so that $x^\bot$ denotes a unique covariable $\alpha$ such that $\alpha^\bot = x$ , and vice versa), which makes the whole transformation involutive (e.g., $c^{\bot\bot} = c$ and $A^{\bot\bot} = A$ ) by definition. This generalizes the previous duality theorems for the classical sequent calculus (Curien & Herbelin, 2000; Wadler, Reference Wadler2003)—namely that involutive duality inverts typing and operational semantics in a meaningful way—to also incorporate (co)recursion on numbers and streams.

Fig. 9. Duality of types, (co)terms, and commands in the uniform abstract machine.

The proof of Theorem 4.2 just follows by induction on the given typing derivation or reduction rule and is an application of the duality theorem of general data and codata types (Downen, 2017), extended with the new form of primitive (co)recursor.

Intermezzo 4.3 The reader already familiar with other work on streams and duality, who has heard that finite lists are “dual” to (possibly) infinite streams, might be surprised to see the statement in Fig. 9 and Theorem 4.2 that streams are dual to (a generalization of) natural numbers. How can this be? The conflict is in two different meanings of the word “dual.”

The meaning of “dual” we use here corresponds exactly to the usual notion of de Morgan duality from classical logic. De Morgan duality flips between “true” ( $\top$ ) and “false” ( $\bot$ ), and between “and” ( $A \times B$ ) and “or” ( $A + B$ ), so that the dual of a proposition A is $A^\bot$ (logically equivalent to $\neg A$ ) defined like so:

\begin{align*} \top^\bot &:= \bot & \bot^\bot &:= \top & (A + B)^\bot &:= (A^\bot) \times (B^\bot) & (A \times B)^\bot &:= (A^\bot) + (B^\bot) \end{align*}

Importantly, notice how the duality transformation is deep: $A^\bot$ does not just flip the top connective, it flips all the connectives down to the leaves. For example, the proposition dual to $(\top + \bot) \times \top$ (which is tautologically true) is \begin{align*} ((\top + \bot) \times \top)^\bot = (\bot \times \top) + \bot \end{align*} (which denotes a falsehood, the dual to truth) and not the erroneous illogical inequality \begin{align*} ((\top + \bot) \times \top)^\bot \neq (\top + \bot) + \top \end{align*} (which still tautology true, and not the dual).

Previous (Curien & Herbelin, 2000; Wadler, Reference Wadler2003) has showed how this duality of propositions in a logic can naturally extend to a duality of types in a programming language based on the classical sequent calculus. Because we are interested in (co)inductive types here, we also need to consider how this relates to recursion in types. As usual, inductive types like $\operatorname{Nat}$ are modeled as a least fixed point, that we write as $\operatorname{LFP} X. A$ , whereas coinductive types like $\operatorname{Stream} A$ are modeled as a greatest fixed point, that we write as $\operatorname{GFP} X. A$ . ^{Footnote 9} A key aspect of this paper is to effectively generalize the classical de Morgan duality of Curien & Herbelin (2000); Wadler (Reference Wadler2003) to the known dualities of least and greatest fixed points:

\begin{align*} (\operatorname{LFP} X. A)^\bot &:= \operatorname{GFP} X. (A^\bot) & (\operatorname{GFP} X. A)^\bot &:= \operatorname{LFP} X. (A^\bot) \end{align*}

The $\operatorname{Stream} A$ , $\operatorname{Nat}$ , and $\operatorname{Numbered} A$ types we have seen thus far are isomorphic (denoted as $\approx$ ) to these usual encodings in terms of greatest and least fixed points built on top of basic type constructors like $+$ and $\times$ :

\begin{align*} \operatorname{Stream} A &\approx \operatorname{GFP} X.~ A \times X & \operatorname{Nat} &\approx \operatorname{LFP} X.~ \top + X & \operatorname{Numbered} A &\approx \operatorname{LFP} X.~ A + X \end{align*}

By applying the usual de Morgan duality of classical logic along with the duality of greatest and least fixed points above, we can calculate these duals of streams and natural numbers:

\begin{align*} (\operatorname{Stream} A)^\bot &\approx \operatorname{LFP} X.~ A^\bot + X \approx \operatorname{Numbered} (A^\bot) & \operatorname{Nat}^\bot &\approx \operatorname{GFP} X.~ \bot \times X \approx \operatorname{Stream} \bot \end{align*}

Contrastingly, other work on (co)inductive types instead calls two types “duals” by just flipping between the greatest or fixed point at the top of the top, but leaving everything else alone. In other words, this other literature says that the dual of $\operatorname{LFP} X. A$ is just $\operatorname{GFP} X. A$ , instead of $\operatorname{GFP} X. (A^\bot)$ . In comparison, this is a shallow notion of duality that does not look deeper into the type. The typical working example of this notion of duality is that the inductive type of lists ( $\operatorname{List} A$ ) is dual to the coinductive type of possibly infinite or finite lists (InfList A), modeled like so:

\begin{align*} \operatorname{List} A &\approx \operatorname{LFP} X. \top + (A \times X) & InfList A &\approx \operatorname{GFP} X. \top + (A \times X) \end{align*}

This other notion of duality, which only swaps a greatest for a list fixed point, is closest to the work on corecursion in lazy functional languages like Haskell, where InfList A represents Haskell’s usual list type [a]. The work has undoubtedly been very productive in showing how to solve practical programming problems involving infinite data in the context of lazy functional languages, but covers different ground than our main objective. For example, shallow duality that just swaps the top-most fixed point—and ignores the rest of the underlying type—fails at providing an involutive duality of types and computation like the one shown in Theorem 4.2 and Fig. 9. Intuitively, $(\operatorname{List} A)^\bot \neq$ InfList A because a finite list of As looks nothing like the continuation expecting a (possibly infinite) list of A, and vice versa!

5.1 Corecursion in terms of coiteration

Recall in Section 3.5 that we were able to encode $\operatorname{\mathbf{rec}}$ in terms of $\operatorname{\mathbf{iter}}$ , though at an increased computational cost. Applying syntactic duality, we can write a similar encoding of $\operatorname{\mathbf{corec}}$ as a macro-expansion in terms of $\operatorname{\mathbf{coiter}}$ . Doing so requires the dual of pairs: sum types. Sum types in the abstract machine look like (Wadler, Reference Wadler2003):

\begin{align*} \langle {\operatorname{left} V} |\!| {[e_1,e_2]} \rangle &\mapsto \langle {V} |\!| {e_1} \rangle & \langle {\operatorname{right} V} |\!| {[e_1,e_2]} \rangle &\mapsto \langle {V} |\!| {e_2} \rangle &(\beta_+)\end{align*}

The macro-expansion for encoding $\operatorname{\mathbf{corec}}$ as $\operatorname{\mathbf{coiter}}$ derived from duality is:

\begin{align*}\begin{aligned} & \operatorname{\mathbf{corec}} \begin{alignedat}[t]{2} \{& \operatorname{head} \alpha &&\to e \\ \mid& \operatorname{tail} \beta &&\to \gamma.f \} \end{alignedat} \\ & \operatorname{\mathbf{with}} V\end{aligned}&:=\begin{aligned} &\operatorname{\mathbf{coiter}} \begin{alignedat}[t]{2} \{& \operatorname{head} \alpha &&\to [\operatorname{head}\alpha, e] \\ \mid& \operatorname{tail} &&\to [\beta, \gamma].[\operatorname{tail}\beta, f] \} \end{alignedat} \\ & \operatorname{\mathbf{with}}{} \operatorname{right} V\end{aligned}\end{align*}

Note how the coinductive step of $\operatorname{\mathbf{coiter}}$ has access to both an option to update the internal seed, or to return some other, fully formed stream as its tail. So dually to the encoding of the recursor, this encoding keeps both options open by reconstructing the original continuation alongside the continuation which uses its internal seed. In the base case matching $\operatorname{head}\alpha$ , it rebuilds the observation $\operatorname{head}\alpha$ and pairs it up with the original response e to the base case. In the coinductive case matching $\operatorname{tail}\beta$ , the projection $\operatorname{tail}\beta$ is combined with the continuation f which can update the internal seed via $\gamma$ . Since f might refer to one or both of $\beta$ and $\gamma$ , we need to “extract” the two parts from the corecursive tail observation. Above, we express this extraction as copattern matching (Abel et al., 2013), which is shorthand for

Because this encoding is building up a pair of two continuations, the internal seed which is passed to them needs to be a value of the appropriately matching sum type. Thus, the encoding has two modes:

• If the seed has the form $\operatorname{right} x$ , then the $\operatorname{\mathbf{coiter}}$ is simulating the original $\operatorname{\mathbf{corec}}$ process with the seed x. This is because the $\operatorname{right}$ continuations for the base and coinductive steps are exactly those of the encoded recursor (e and f, respectively) which get applied to x.

• If the seed has the form $\operatorname{left} s$ , containing some stream s, then the $\operatorname{\mathbf{coiter}}$ is mimicking s as-is. This is because the $\operatorname{left}$ continuations for the base and coinductive steps exactly mimic the original observations ( $\operatorname{head}\alpha$ and $\operatorname{tail}\beta$ , respectively) which get applied to the stream s.

To start the corecursive process off, we begin with $\operatorname{right} V$ , which corresponds to the original seed V given to the corecursor. Then in the coinductive step, if f updates the seed to V’ via $\gamma$ , the seed is really updated to $\operatorname{right} V'$ , continuing the simulation of corecursion. Otherwise, if f returns some other stream s to $\beta$ , the seed gets updated to $\operatorname{left} s$ , and the coiteration continues but instead mimics s at each step.

As with recursion, encoding $\operatorname{\mathbf{corec}}$ in terms of $\operatorname{\mathbf{coiter}}$ forces a performance penalty for functions like $\mathit{scons}$ which can return a stream directly in the coinductive case instead of updating the accumulator. Recall how call-by-value execution was more efficient than call-by-name. Yet, the above encoding results in this same inefficient execution even in call-by-value, as in this command which accesses the $(n+2)^{th}$ element:

Notice how the internal seed (in blue) changes through this computation. To begin, the seed is . The first $\operatorname{tail}$ projection (triggering the $\beta_{\operatorname{tail}}$ rule) leads to the decision point (by $\beta_+$ ) which chooses to update the seed with . From that point on, each $\operatorname{tail}$ projection to follow will trigger the next step of this coiteration (and another $\beta_{\operatorname{tail}}$ rule). Each time, this will end up asking for its $\operatorname{tail}$ , , which will be then used to build the next seed, .

In order to continue, we need to know something about s, specifically, how it responds to a $\operatorname{tail}$ projection. For simplicity, assume that the tail of s is $s_1$ , i.e., $\langle {s} |\!| {\operatorname{tail} E} \rangle \mathrel{\mapsto\!\!\!\!\to} \langle {s_1} |\!| {E} \rangle$ . And then for each following $s_i$ , assume its tail is $s_{i+1}$ . Under this assumption, execution will proceed to the base case $\operatorname{head}$ projection like so:

In total, this computation incurs additional $\beta_{\operatorname{tail}}$ steps linearly proportional to $n+2$ , on top of any additional work needed to compute the same number of $\operatorname{tail}$ projections for each $\langle {s_i} |\!| {\operatorname{tail} E} \rangle \mathrel{\mapsto\!\!\!\!\to} \langle {s_{i+1}} |\!| {E} \rangle$ along the way.

6.1 Safety and candidates

To begin, we derive our notion of safety from the conclusion of Theorem 3.2. Ultimately we will only run commands that are closed, save for one free covariable $\alpha$ taking a $\operatorname{Nat}$ , so we expect all such safe commands to eventually finish execution in a valid final state that provides that $\alpha$ with a $\operatorname{Nat}$ construction: either a $\operatorname{zero}$ or $\operatorname{succ}$ essor.

Definition 6.1 (Safety) The set of safe commands, $\unicode{x2AEB}$ , is:

\begin{align*} \unicode{x2AEB} &:= \{ c \mid \exists c' \in \mathit{Final}.~ c \mathrel{\mapsto\!\!\!\!\to} c' \} \\ \mathit{Final} &:= \{\langle {\operatorname{zero}} |\!| {\alpha} \rangle \mid \alpha \in \mathit{CoVar}\} \cup \{\langle {\operatorname{succ} V} |\!| {\alpha} \rangle \mid V \in \mathit{Value}, \alpha \in \mathit{CoVar}\}\end{align*}

From here, we will model types as collections of terms and coterms that work well together. A sensible place to start is to demand soundness: all of these terms and coterms can only form safe commands (i.e., ones found in $\unicode{x2AEB}$ ). However, we will quickly find that we also need completeness: any terms and coterms that do not break safety are included.

As notation, given any pre-candidate $\mathbb{A}$ , we will always write $\mathbb{A}^+$ to denote the first component of $\mathbb{A}$ (the term set $\pi_1(\mathbb{A})$ ) and $\mathbb{A}^-$ to denote the second one (the coterm set $\pi_2(\mathbb{A})$ ). As shorthand, given a reducibility candidate $\mathbb{A}=(\mathbb{A}^+,\mathbb{A}^-)$ , we write $v \in \mathbb{A}$ to mean $v \in \mathbb{A}^+$ and likewise $e \in \mathbb{A}$ to mean $e \in \mathbb{A}^-$ . Given a set of terms $\mathbb{A}^+$ , we will occasionally write the pre-candidate $(\mathbb{A}^+,\{\})$ as just $\mathbb{A}^+$ when the difference is clear from context. Likewise, we will occasionally write the pre-candidate $(\{\},\mathbb{A}^-)$ as just the coterm set $\mathbb{A}^-$ when unambiguous.

The motivation behind soundness may seem straightforward. It ensures that the Cut rule is safe. But soundness is not enough, because the type system does much more than Cut: it makes many promises that several terms and coterms inhabit the different types. For example, the function type contains $\lambda$ -abstractions and call stacks, and every type contains $\mu$ - and ${\tilde{\mu}}$ -abstractions over free (co)variables of the type. Yet, there is nothing in soundness that keeps these promises. For example, the trivial pre-candidate $(\{\},\{\})$ is sound but it contains nothing, even though ActR and ActL promise many $\mu$ - and ${\tilde{\mu}}$ -abstractions that are left out! So to fully reflect the rules of the type system, we require a more informative model.

Completeness ensures that every reducibility candidate has “enough” (co)terms that are promised by the type system. For example, the completeness requirements given in Definition 6.2 are enough to guarantee every complete candidate contains all the appropriate $\mu$ - and ${\tilde{\mu}}$ -abstractions that always step to safe commands for any allowed binding.

Proof. Consider the first fact (the second is perfectly dual to it and follows analogously) and assume that $c[{{E}/{\alpha}}] \in \unicode{x2AEB}$ for all $E \in \mathbb{A}$ . In other words, the definition of $c[{{E}/{\alpha}}] \in \unicode{x2AEB}$ says $c[{{E}/{\alpha}}] \mathrel{\mapsto\!\!\!\!\to} c'$ for some valid command $c' \in \mathit{Final}$ . For any specific $E \in \mathbb{A}$ , we have:

\begin{align*} \langle {\mu{\alpha}. c} |\!| {E} \rangle &\mapsto c[{{E}/{\alpha}}] \mathrel{\mapsto\!\!\!\!\to} c' \in \mathit{Final} \end{align*}

By definition of $\unicode{x2AEB}$ (Definition 6.1) and transitivity of reduction, as well for any $E \in \mathbb{A}$ . Thus, $\mathbb{A}$ must contain $\mu{\alpha}.c$ , as required by positive completeness (Definition 6.2)

Notice that the restriction to values and covalues in the definition of completeness (Definition 6.2) is crucial in proving Lemma 6.3. We can easily show that the $\mu$ -abstraction steps to a safe command for every given (co)value, but if we needed to say the same for every (co)term we would be stuck in call-by-name evaluation where the $\mu$ -rule might not fire. Dually, it is always easy to show that the ${\tilde{\mu}}$ safely steps for every value, but we cannot say the same for every term in call-by-value. The pattern in Lemma 6.3 of reasoning about commands based on the ways they reduce is a crucial key to proving properties of particular (co)terms of interest. The very definition of safe commands $\unicode{x2AEB}$ is closed under expansion of the machine’s operational semantics.

Proof. Follows from the definition of $\unicode{x2AEB}$ (Definition 6.1) and transitivity of reduction.

This property is the key step used to conclude the proof Lemma 6.3 and can be used to argue that other (co)terms are in specific reducibility candidates due to the way they reduce.

6.2 Subtyping and completion

Before we delve into the interpretations of types as reducibility candidates, we first need to introduce another important concept that the model revolves around: subtyping. The type system (Figs. 6 and 7) for the abstract machine has no rules for subtyping, but nevertheless, a semantic notion of subtyping is useful for organizing and building reducibility candidates. More specifically, notice that there are exactly two basic ways to order pre-candidates based on the inclusion of their underlying sets:

Definition 6.5 (Refinement and Subtype Order) The refinement order ( $\mathbb{A} \sqsubseteq \mathbb{B}$ ) and subtype order ( $\mathbb{A} \leq \mathbb{B}$ ) between pre-candidates is:

\begin{align*} (\mathbb{A}^+,\mathbb{A}^-) \sqsubseteq (\mathbb{B}^+,\mathbb{B}^-) &:= (\mathbb{A}^+ \subseteq \mathbb{B}^+) \mathbin{\mathrm{and}} (\mathbb{A}^- \subseteq \mathbb{B}^-) \\ (\mathbb{A}^+,\mathbb{A}^-) \leq (\mathbb{B}^+,\mathbb{B}^-) &:= (\mathbb{A}^+ \subseteq \mathbb{B}^+) \mathbin{\mathrm{and}} (\mathbb{A}^- \supseteq \mathbb{B}^-)\end{align*}

The reverse extension order $\mathbb{A} \sqsupseteq \mathbb{B}$ is defined as $\mathbb{B} \sqsubseteq \mathbb{A}$ , and supertype order $\mathbb{A} \geq \mathbb{B}$ is $\mathbb{B} \leq \mathbb{A}$ .

Refinement just expresses basic inclusion: $\mathbb{A}$ refines $\mathbb{B}$ when everything in $\mathbb{A}$ (both term and coterm) is contained within $\mathbb{B}$ . With subtyping, the underlying set orderings go in opposite directions! If $\mathbb{A}$ is a subtype of $\mathbb{B}$ , then $\mathbb{A}$ can have fewer terms and more coterms than $\mathbb{B}$ . While this ordering may seem counter-intuitive, it closely captures the understanding of sound candidates where coterms are tests on terms. If $\unicode{x2AEB}$ expresses which terms pass which tests (i.e., coterms), the soundness requires that all of its terms passes each of its tests. If a sound candidate has fewer terms, then it might be able to safely include more tests which were failed by the removed terms. But if a sound candidate has more terms, it might be required to remove some tests that the new terms don’t pass.

This semantics for subtyping formalizes Liskov’s substitution principle (Liskov, 1987): if $\mathbb{A}$ is a subtype of $\mathbb{B}$ , then terms of $\mathbb{A}$ are also terms of $\mathbb{B}$ because they can be safely used in any context expecting inputs from $\mathbb{B}$ (i.e., with any coterm of $\mathbb{B}$ ). Interestingly, our symmetric model lets us express the logical dual of this substitution principle: if $\mathbb{A}$ is a subtype of $\mathbb{B}$ , then the coterms of $\mathbb{B}$ (i.e., contexts expecting inputs of $\mathbb{B}$ ) are coterms of $\mathbb{A}$ because they can be safely given any input from $\mathbb{A}$ . These two principles lead to a natural subtype ordering of reducibility candidates, based on the sets of (co)terms they include.

The usefulness of this semantic, dual notion of subtyping comes from the way it gives us a complete lattice, which makes it possible to combine and build new candidates from other simpler ones.

>Definition 6.6 (Subtype Lattice). There is a complete lattice of pre-candidates in ${\mathcal{PC}}$ with respect to subtyping order, where the binary intersection ( $\mathbb{A} \wedge \mathbb{B}$ , a.k.a meet or greatest lower bound) and union ( $\mathbb{A} \vee \mathbb{B}$ , a.k.a join or least upper bound) are defined as:

\begin{align*} \mathbb{A} \wedge \mathbb{B} &:= (\mathbb{A}^+ \cap \mathbb{B}^+, \mathbb{A}^- \cup \mathbb{B}^-) & \mathbb{A} \vee \mathbb{B} &:= (\mathbb{A}^+ \cup \mathbb{B}^+, \mathbb{A}^- \cap \mathbb{B}^-)\end{align*}

Moreover, these generalize to the intersection ( $\bigwedge \mathcal{A}$ , a.k.a infimum) and union ( $\bigvee \mathcal{A}$ , a.k.a supremum) of any set $\mathcal{A} \subseteq {\mathcal{PC}}$ of pre-candidates

\begin{align*} \bigwedge \mathcal{A} &:= \left( \bigcap \{\mathbb{A}^+ \mid \mathbb{A} \in \mathcal{A}\} , \bigcup \{\mathbb{A}^- \mid \mathbb{A} \in \mathcal{A}\} \right) \\ \bigvee \mathcal{A} &:= \left( \bigcup \{\mathbb{A}^+ \mid \mathbb{A} \in \mathcal{A}\} , \bigcap \{\mathbb{A}^- \mid \mathbb{A} \in \mathcal{A}\} \right)\end{align*}

The binary least upper bounds and greatest lower bounds have these standard properties:

\begin{align*} \mathbb{A}\wedge\mathbb{B} &\leq \mathbb{A},\mathbb{B} \leq \mathbb{A}\vee\mathbb{B} & \mathbb{C} \leq \mathbb{A},\mathbb{B} &\implies \mathbb{C} \leq \mathbb{A}\wedge\mathbb{B} & \mathbb{A},\mathbb{B} \leq \mathbb{C} &\implies \mathbb{A}\vee\mathbb{B} \leq \mathbb{C}\end{align*}

In the general case for the bounds on an entire set of pre-candidates, we know:

\begin{align*} \forall \mathbb{A} \in \mathcal{A}.~ & \textstyle \left( \bigwedge \mathcal{A} \leq \mathbb{A} \right) & (\forall \mathbb{A} \in \mathcal{A}.~ \mathbb{C} \leq \mathbb{A}) &\implies \textstyle \mathbb{C} \leq \bigwedge \mathcal{A} \\ \forall \mathbb{A} \in \mathcal{A}.~ & \textstyle \left( \mathbb{A} \leq \bigvee \mathcal{A} \right) & (\forall \mathbb{A} \in \mathcal{A}.~ \mathbb{A} \leq \mathbb{C}) &\implies \textstyle \bigvee \mathcal{A} \leq \mathbb{C}\end{align*}

These intersections and unions both preserve soundness, and so they form a lattice of sound candidates in ${\mathcal{SC}}$ as well. However, they do not preserve completeness in general, so they do not form a lattice of reducibility candidates, i.e., sound and complete pre-candidates. Completeness is not preserved because $\mathbb{A} \vee \mathbb{B}$ might be missing some terms (such as $\mu$ s) which could be soundly included, and dually $\mathbb{A} \wedge \mathbb{B}$ might be missing some coterms (such as ${\tilde{\mu}}$ s). So because all reducibility candidates are sound pre-candidates, $\mathbb{A} \vee \mathbb{B}$ and $\mathbb{A} \wedge \mathbb{B}$ are well-defined, but their results will only be sound candidates (not another reducibility candidate). ^{Footnote 10}

What we need is a way to extend arbitrary sound candidates, adding “just enough” to make them full-fledged reducibility candidates. Since there are two possible ways to do this (add the missing terms or add the missing coterms), there are two completions which go in different directions. Also, since the completeness of which (co)terms are guaranteed to be in reducibility candidates is specified up to (co)values, we cannot be sure that absolutely everything ends up in the completed candidate. Instead, we can only ensure that the (co)values that started in the pre-candidate are contained in its completion. This restriction to just the (co)values of a pre-candidate, written $\mathbb{A}^v$ and defined as

\begin{align*} (\mathbb{A}^+,\mathbb{A}^-)^v &:= (\{V \mid V \in \mathbb{A}^+\}, \{E \mid E \in \mathbb{A}^-\})\end{align*}

becomes a pivotal part of the semantics of types. With this in mind, it follows there are exactly two “ideal” completions, the positive and negative ones, which give a reducibility candidate that is the closest possible to the starting point.

The full proof of these completions (and proofs of the other remaining propositions not given in this section) is given in Appendix 1. We refer to $\operatorname{Pos}(\mathbb{A})$ as the positive completion of $\mathbb{A}$ because it is based entirely on the values of $\mathbb{A}$ (i.e., its positive components): $\operatorname{Pos}(\mathbb{A})$ collects the complete set of coterms that are safe with $\mathbb{A}$ ’s values and then collects the terms that are safe with the covalues from the previous step, and so on until a fixed point is reached (taking three rounds total). As such, the covalues included in $\mathbb{A}$ can’t influence the result of $\operatorname{Pos}(\mathbb{A})$ . Dually, $\operatorname{Neg}(\mathbb{A})$ is the negative completion of $\mathbb{A}$ because it is based entirely on $\mathbb{A}$ ’s covalues in the same manner.

This extra fact gives us another powerful completeness property. We can reason about covalues in the positive candidate $\operatorname{Pos}(\mathbb{A})$ purely in terms of how they interact with $\mathbb{A}$ ’s values, ignoring the rest of $\operatorname{Pos}(\mathbb{A})$ . Dually, we can reason about values in the negative candidate $\operatorname{Neg}(\mathbb{A})$ purely based on of $\mathbb{A}$ ’s covalues.

Proof. Follows directly from Lemmas 6.7 and 6.8.

Now that we know how to turn sound pre-candidates $\mathbb{A}$ into reducibility candidates $\operatorname{Pos}(\mathbb{A})$ or $\operatorname{Neg}(\mathbb{A})$ — $\operatorname{Pos}$ and $\operatorname{Neg}$ take anything sound and deliver something sound and complete—we can spell out precisely the subtype-based lattice of reducibility candidates.

Theorem 6.10 (Reducibility Subtype Lattice). There is a complete lattice of reducibility candidates in ${\mathcal{RC}}$ with respect to subtyping order, with this binary intersection $\mathbb{A}\curlywedge\mathbb{B}$ and union $\mathbb{A}\curlyvee\mathbb{B}$

\begin{align*} \mathbb{A} \curlywedge \mathbb{B} &:= \operatorname{Neg}(\mathbb{A} \wedge \mathbb{B}) & \mathbb{A} \curlyvee \mathbb{B} &:= \operatorname{Pos}(\mathbb{A} \vee \mathbb{B})\end{align*}

and this intersection (

) and union (

) of any set $\mathcal{A} \subseteq {\mathcal{RC}}$ of reducibility candidates

6.3 Interpretation and adequacy

Using the subtyping lattice, we have enough infrastructure to define an interpretation of types and type-checking judgments as given in Fig. 10. Each type is interpreted as a reducibility candidate. Even though we are dealing with recursive types ( $\operatorname{Nat}$ and $\operatorname{Stream}$ ), the candidates for them are defined in a non-recursive way based on Knaster-Tarski’s fixed point construction (Knaster, 1928; Tarski, 1955) and can be read with these intuitions:

• $[\![ A \to B ]\!]$ is the negatively complete candidate containing all the call stacks built from $[\![ A ]\!]$ arguments and $[\![ B ]\!]$ return continuations. Note that this is the same thing (via Lemmas 6.7 and 6.8) as largest candidate containing those call stacks.

• $[\![ \operatorname{Nat}]\!]$ is the smallest candidate containing $\operatorname{zero}$ and closed $\operatorname{succ}$ essor constructors.

• $[\![ \operatorname{Stream} A ]\!]$ is the largest candidate containing $\operatorname{head}$ projections expecting an $[\![ A ]\!]$ element and closed under $\operatorname{tail}$ projections.

Fig. 10. Model of termination and safety of the abstract machine.

Typing environments ( $\Gamma$ ) are interpreted as the set of valid substitutions $\rho$ which map variables x to values and covariables $\alpha$ to covalues. The interpretation of the typing environment $\Gamma, x : A$ places an additional requirement on these substitutions: a valid substitution $\rho \in [\![\Gamma, x : A]\!]$ must substitute a value of $[\![ A ]\!]$ for the variable x, i.e., $x[{\rho}] \in [\![ A ]\!]$ . Dually, a valid substitution $\rho \in [\![\Gamma, \alpha \div A]\!]$ must substitute a covalue of $[\![ A ]\!]$ for $\alpha$ , i.e., $\alpha[{\rho}] \in [\![ A ]\!]$ . Finally, typing judgments (e.g., $\Gamma \vdash c \ $ ) are interpreted as statements which assert that the command or (co)term belongs to the safe set $\unicode{x2AEB}$ or the assigned reducibility candidate for any substitution allowed by the environment. The key lemma is that typing derivations of a judgment ensure that the statement they correspond to holds true.

Proof. Observe that, for any $V \in [\![ A ]\!]$ and $E \in [\![ B ]\!]$ :

\begin{align*} \langle {\lambda x. v} |\!| {V \cdot E} \rangle &\mapsto \langle {v[{{V}/{x}}]} |\!| {E} \rangle \in \unicode{x2AEB} \end{align*}

where $\langle {v[{{V}/{x}}]} |\!| {E} \rangle \in \unicode{x2AEB}$ is guaranteed due to soundness for the reducibility candidate $[\![ B ]\!]$ . By expansion (Property 6.4), we know that $\langle {\lambda x. v} |\!| {V \cdot E} \rangle \in \unicode{x2AEB}$ as well. So from Corollary 6.9:

\begin{equation*} \lambda x. v \in \operatorname{Neg}\{V \cdot E \mid V \in [\![ A ]\!], E \in [\![ B ]\!]\} = [\![ A \to B ]\!] \end{equation*}

But what about $[\![ \operatorname{Nat}]\!]$ and $[\![ \operatorname{Stream} A ]\!]$ ? The interpretations of (co)inductive types are not exactly instances of $\operatorname{Pos}$ or $\operatorname{Neg}$ as written, because unlike $[\![ A \to B ]\!]$ , they quantify over elements in the possible $\mathbb{C}$ s they are made from. This lets us say these $\mathbb{C}$ s are closed under $\operatorname{succ}$ or $\operatorname{tail}$ , but it means that we cannot identify a priori a set of (co)values that generate the candidate independent of each $\mathbb{C}$ .

A solution to this conundrum is to instead describe these (co)inductive types incrementally, building them step-by-step instead of all-at once à la Kleene’s fixed point construction (Kleene, 1952). For example, the set of the natural numbers can be defined incrementally from a series of finite approximations by beginning with the empty set, and then at each step adding the number 0 and the successor of the previous set:

\begin{align*} \mathbb{N}_0 &:= \{\} & \mathbb{N}_{i+1} &:= \{0\} \cup \{n+1 \mid n \in \mathbb{N}_i\} & \mathbb{N} &:= \bigcup_{i=0}^\infty \{\mathbb{N}_i\}\end{align*}

So that each $\mathbb{N}_i$ contains only the numbers less than i. The final set of all natural numbers, $\mathbb{N}$ , is then the union of each approximation $\mathbb{N}_i$ along the way. Likewise, we can do a similar incremental definition of finite approximations of $[\![ \operatorname{Nat}]\!]$ like so:

The starting approximation $[\![ \operatorname{Nat}]\!]_0$ is the smallest reducibility candidate, which is given by $\operatorname{Pos}\{\}$ . From there, the next approximations are given by the positive candidate containing at least $\operatorname{zero}$ and the $\operatorname{successor}$ of every value of their predecessor. This construction mimics the approximations $\mathbb{N}_i$ , where we start with the smallest possible base and incrementally build larger and larger reducibility candidates that more accurately approximate the limit.

The typical incremental coinductive definition is usually presented in the reverse direction: start out with the “biggest” set (whatever that is), and trim it down step-by-step. Instead, the coinductive construction of reducibility candidates is much more concrete, since they form a complete lattice (with respect to subtyping). There is a specific biggest candidate

(equal to

) containing every term possible and the fewest coterms allowed. From there, we can add explicitly more coterms to each successive approximation, which shrinks the candidate by ruling out some terms that do not run safely with them. Thus, the incremental approximations of $[\![ \operatorname{Stream} A ]\!]$ are defined negatively as:

We start with the biggest possible candidate given by $\operatorname{Neg}\{\}$ . From there, the next approximations are given by the negative candidate containing at least $\operatorname{head} E$ (for any E expecting an element of type $[\![ A ]\!]$ ) and the $\operatorname{tail}$ of every covalue in the previous approximation. The net effect is that $[\![ \operatorname{Stream} A ]\!]_i$ definitely contains all continuations built from (at most) i $\operatorname{head}$ and $\operatorname{tail}$ destructors. As with $[\![ \operatorname{Nat} ]\!]_i$ , the goal is to show that $[\![ \operatorname{Stream} A ]\!]$ is the limit of $[\![ \operatorname{Stream} A ]\!]_i$ , i.e., that it is the intersection of all finite approximations.

Lemma 6.13 ((Co)Induction Inversion).

This fact makes it possible to use expansion (Property 6.4) and strong completeness (Corollary 6.9) to prove that the recursor belongs to each of the approximations $[\![ \operatorname{Nat}]\!]_i$ ; and thus also to by induction on i. Dually, the corecursor belongs to each approximation $[\![ \operatorname{Stream} A ]\!]_i$ , so it is included in . This proof of safety for (co)recursion is the final step in proving overall adequacy (Lemma 6.11). In turn, the ultimate type safety and termination property we are after is a special case of a more general notion of observable safety and termination, which follows directly from adequacy for certain typing environments.

Proof. From Lemma 6.11, we have $[\![\alpha\div\operatorname{Nat} \vdash c \ ]\!]$ . That is, for all $E \in [\![ \operatorname{Nat} ]\!]$ , $c[{{E}/{\alpha}}] \in \unicode{x2AEB}$ . Note that both $\langle {\operatorname{zero}} |\!| {\alpha} \rangle \in \unicode{x2AEB}$ and $\langle {\operatorname{succ} V} |\!| {\alpha} \rangle \in \unicode{x2AEB}$ (for any V whatsoever) by definition of $\unicode{x2AEB}$ (Definition 6.1). So by Corollary 6.9, $\alpha$ itself is a member of $[\![ \operatorname{Nat} ]\!]$ , i.e., $\alpha \in [\![ \operatorname{Nat} ]\!]$ . Thus, $c[{{\alpha}/{\alpha}}] = c \in \unicode{x2AEB}$ , and the necessary reduction follows from the definition of $\unicode{x2AEB}$ .

Intermezzo 6.15. The wordings of Theorems 3.2 and 6.14 are meant to reflect the typical statement of type safety for functional and $\lambda$ -calculus-based languages. In a $\lambda$ -based language, type safety (and notably the “progress” half of a progress and preservation proof) is limited to closed programs which return some basic, observable data type like a boolean value, string, number, or list. For example, type safety might ensure that a term M never gets stuck when $\bullet \vdash M : \operatorname{Nat}$ . In our typed abstract machine, commands are the unit of execution rather than terms. So instead of a closed term $\bullet \vdash v : \operatorname{Nat}$ , we state type safety and termination for a starting command like $\alpha \div \operatorname{Nat} \vdash \langle {v} |\!| {\alpha} \rangle \ $ , where v is the closed “source program” and $\alpha$ represents an initial continuation or empty context waiting for the final result, which is expected to be a natural number.

The fact that the safe command described by Theorems 3.2 and 6.14 is not closed, ^{Footnote 11} but has a free covariable, raises the question: can safety and termination be generalized to cover other open commands with additional variables or covariables? And what might we require of those open commands in general to still ensure termination?

It turns out, very little of the proof methodology depends the specifics of our particular notion of safety captured by the sets of commands $\unicode{x2AEB}$ and $\mathit{Final}$ from Definition 6.1. Rather, the only property of these sets that is pervasively used is the Property 6.4 that $\unicode{x2AEB}$ is closed under expansion ( $c \mapsto c' \in \unicode{x2AEB}$ implies $c \in \unicode{x2AEB}$ ). In fact, there is only one place in the proof that requires another fact about $\unicode{x2AEB}$ , which is showing that for Lemma 6.13; this step uses the fact that there is at least one command, namely $\langle {\operatorname{zero}} |\!| {\alpha} \rangle$ , in $\unicode{x2AEB}$ . However, this choice of example inhabitant of $\unicode{x2AEB}$ is arbitrary, and could be replaced with any other choice of $\langle {V_0} |\!| {E_0} \rangle \in \unicode{x2AEB}$ without otherwise changing the proof.

This independence of the general proof methodology from the notion of safety (captured by $\unicode{x2AEB}$ ) makes it a rather straightforward exercise to generalize to other results by just redefining the set $\unicode{x2AEB}$ of safe commands. For example, we could consider additional examples of $\mathit{Final}$ commands which also includes stopping with any variable x observed by a destructor $\operatorname{head} E$ , $\operatorname{tail} E$ , or $V \cdot E$ , letting us observe a larger collection of safe commands $\unicode{x2AEB}$ .

Definition 6.16 (Observable Safety). The set of observably safe commands, $\unicode{x2AEB}$ , is:

The same theorems still hold, up to and including adequacy (Lemma 6.11) and the specific lemmas about the nature of function and (co)inductive types (Lemmas 6.12 and 6.13) after replacing Definition 6.1 with Definition 6.16. As a consequence, we can use this bigger definition of $\unicode{x2AEB}$ to meaningfully observe a larger collection of safe commands than before.

Proof First, note that the interpretations of specific types are guaranteed to contain variables or covariables as follows:

1. 1. $\alpha \in [\![ \operatorname{Nat} ]\!]$ . This is because $\langle {\operatorname{zero}} |\!| {\alpha} \rangle \in \mathit{Final} \supseteq \unicode{x2AEB}$ and for any V whatsoever by definition of $\unicode{x2AEB}$ (Definition 6.16).So by the updated Corollary 6.9, $\alpha$ itself is a member of $[\![ \operatorname{Nat} ]\!]$ .

2. 2. $x \in [\![ \operatorname{Stream} A ]\!]$ . This is because $\langle {x} |\!| {\operatorname{head} E} \rangle \in \mathit{Final} \supseteq \unicode{x2AEB}$ and $\langle {x} |\!| {\operatorname{tail} E} \rangle \in \mathit{Final} \supseteq \unicode{x2AEB}$ for any E by definition of $\unicode{x2AEB}$ (Definition 6.16), so x is a member of $[\![ \operatorname{Stream} A ]\!]$ for any A by the updated Corollary 6.9.

3. 3. $x \in [\![ A \to B ]\!]$ . This is because $\langle {x} |\!| {V \cdot E} \rangle \in \mathit{Final} \supseteq \unicode{x2AEB}$ for any V and E by definition of $\unicode{x2AEB}$ (Definition 6.16), so x is a member of $[\![ A \to B ]\!]$ for any A and B by the updated Corollary 6.9.

It follows that for any observable typing environment $\Gamma$ , there is $\mathit{id}_\Gamma \in [\![ \Gamma ]\!]$ where the identity substitution $\mathit{id}_\Gamma$ is defined as:

\begin{align*} \mathit{id}_\Gamma(x) &= x &(\text{if } (x : A) &\in \Gamma) & \mathit{id}_\Gamma(\alpha) &= \alpha &(\text{if } (\alpha \div A) &\in \Gamma) \end{align*}

Now, updated adequacy (Lemma 6.11) ensures $[\![\Gamma \vdash c \ ]\!]$ . That is, for all $\rho \in [\![ \Gamma ]\!]$ , $c[{\rho}] \in \unicode{x2AEB}$ . Since $\Gamma$ is observable, $\mathit{id}_\Gamma \in [\![ \Gamma ]\!]$ , and thus $c[{\mathit{id}_\Gamma}] = c \in \unicode{x2AEB}$ . So by definition of $\unicode{x2AEB}$ (Definition 6.16), $c \mathrel{\mapsto\!\!\!\!\to} c' \in \mathit{Final}$ .