Classical (Co)Recursion: Mechanics

Primitive recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, primitive corecursion, is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation, giving a terminating calculus analogous to the original computational foundation of recursion. We show how the implementation details in an abstract machine strengthens their connection, syntactically deriving corecursion from recursion via logical duality. We also observe the impact of evaluation strategy on the computational complexity of primitive (co)recursive combinators: call-by-name allows for more efficient recursion, but call-by-value allows for more efficient corecursion.

Introduction
Primitive recursion has a solid foundation in a variety of different fields. In the categorical setting, it can be seen in the structures of algebras. In the logical setting, it corresponds to proofs by induction. And in the computational setting, it can be phrased in terms of languages and type theories with terminating loops, like Gödel's System T (Gödel, 1980). The latter viewpoint of computation reveals a fine-grained lens with which we can study the subtle impact of the primitive combinators that capture different forms of recursion. For example, the recursive combinators given by Mendler (1987Mendler ( , 1988) yield a computational complexity for certain programs when compared to encodings in System F (Böhm & Berarducci, 1985;Girard et al., 1989). Recursive combinators have desirable propertieslike the fact that they always terminate-which make them useful for the design of well-behaved programs (Meijer et al., 1991;Gibbons, 2003), also for optimizations made possible by applying those properties and theorems (Malcom, 1990).
The current treatment of the dual of primitive recursion-primitive corecursion-is not so fortunate. Being the much less understood of the two, corecursion is usually only viewed in light of this duality. Consequently, corecursion tends to be relegated to a notion of coalgebras (Rutten, 2019), because only the language of category theory speaks clearly enough about their duality. This can be seen in the study of corecursion schemes, where coalgebraic "anamorphisms" (Meijer et al., 1991) and "apomorphisms" (Vene & Uustalu, 1998) are the dual counterparts to algebraic "paramorphisms" (Meertens, 1992) and "catamorphisms" (Hinze et al., 2013). Yet the logical and computational status of corecursion is not so clear. For example, the introduction of stream objects is sometimes described as the "dual" to the elimination of natural numbers (Sangiorgi, 2011;Roy, 2003), but how is this so?
The goal of this paper is to provide a purely computational and logical foundation for primitive corecursion based on classical logic. Specifically, we will express different principles of corecursion in a small core calculus, analogous to the canonical computational presentation of recursion (Gödel, 1980). Instead of the (co)algebraic approach, we derive the symmetry between recursion and corecursion through the mechanics of programming language implementations, formalized in terms of an abstract machine. This symmetry is encapsulated by the duality (Hagino, 1987;Downen et al., 2015) between data types-defined by the structure of objects-and codata types-defined by the behavior of objects.
We begin in Section 2 with a review of the formalization of primitive recursion in terms of a foundational calculus: System T (Gödel, 1980). We point out the impact of evaluation strategy on different primitive recursion combinators, namely the recursor and the iterator: • In call-by-value, the recursor is just as (in)efficient as the iterator. • In call-by-name, the recursor may end early; an asymptotic complexity improvement. Section 3 presents an abstract machine for both call-by-value and -by-name evaluation, and unifies both into a single presentation (Ariola et al., 2009;Downen & Ariola, 2018b). The lower level nature of the abstract machine explicitly expresses how the recursor of inductive types, like numbers, accumulates a continuation during evaluation, maintaining the progress of recursion. This is implicit in the operational model of System T. The machine is shown correct, in the sense that a well typed program will always terminate and produce an observable value (Theorem 3.2), which in our case is a number.
Section 4 continues by extending the abstract machine with the primitive corecursor for streams. The novelty is that this machine is derived by applying syntactic duality to the previous one, naturally leading us to a classical corecursive combinator with multiple outputs, modeled as multiple continuations. From duality in the machine, we can see that the corecursor relies on a value accumulator; this is logically dual to the recursor's return continuation. Like recursion versus iteration, in Section 5 we compare corecursion versus coiteration: corecursion can be more efficient than coiteration by letting corecursive processes stop early. Since corecursion is dual to recursion, and call-by-value is dual to call-by-name (Curien & Herbelin, 2000;Wadler, 2003), this improvement in algorithmic complexity is only seen in call-by-value corecursion. Namely: • In call-by-name, the corecursor is just as (in)efficient as the coiterator. • In call-by-value, the corecursor may end early; an asymptotic complexity improvement.
Yet, even though we have added infinite streams, we don't want to ruin System T's desirable properties. So in Section 6, we give an interpretation of the type system which extends previous models of finite types (Downen et al., 2020(Downen et al., , 2019 with the (co)recursive types of numbers and streams. The novel key step in reasoning about (co)recursive types is in reconciling two well-known fixed point constructions-Kleene's and Knaster-Tarski'swhich is non-trivial for classical programs with control effects. This lets us show that, even with infinite streams, our abstract machine is terminating and type safe (Theorem 6.14). Proofs to all theorems that follow are given in the appendix.

Recursion on Natural Numbers: System T
We start with Gödel's System T (Gödel, 1980), a core calculus which allows us to define functions by structural recursion. Its syntax is given in Fig. 1. It is a canonical extension of the simply-typed λ -calculus, whose focus is on functions of type A → B, with ways to construct natural numbers of type Nat. The Nat type comes equipped with two constructors zero and succ, and a built-in recursor, which we write as rec M as {zero → N | succ x → y.N ′ }. This rec-expression analyzes M to determine if it has the shape zero or succ x, and the matching branch is returned. In addition to binding the predecessor of M to x in the succ x branch, the recursive result-calculated by replacing M with its predecessor x-is bound to y.
The type system of System T is given in Fig. 2. The Var, →I and →E typing rules are from the simply typed λ -calculus. The two NatI introduction rules give the types of the constructors of Nat, and the NatE elimination rule types the Nat recursor.
System T's call-by-name and -value operational semantics are given in Fig. 3. Both of these evaluation strategies share operational rules of the same form, with β → being the well-known β rule of the λ -calculus, and β zero and β succ defining recursion on the two Nat constructors. The only difference between call-by-value and -name evaluation lies in their notion of values V (i.e., those terms which can be substituted for variables) and evaluation contexts (i.e., the location of the next reduction step to perform). Note that we take this notion seriously, and never substitute a non-value for a variable. As such, the β succ rule does not substitute the recursive computation rec V as {zero → N | succ x → y.N ′ } for y, since it might not be a value (in call-by-value). The next reduction step depends on the

Call-by-value values (V ) and evaluation contexts (E):
Value ∋ V, W :: evaluation strategy. In call-by-name, this next step is indeed to substitute rec V as {zero → N | succ x → y.N ′ } for y, and so we have: So call-by-name recursion is computed starting with the current (largest) number first and ending with the smallest number needed (possibly the base case for zero). If a recursive result is not needed then it is not computed at all, allowing for an early end of the recursion. In contrast, call-by-value must evaluate the recursive result first before it can be substituted for y. As such, call-by-value recursion always starts by computing the base case for zero (whether or not it is needed), and the intermediate results are propagated backwards until the case for the initial number is reached. So call-by-value allows for no opportunity to end the computation of rec early. Executing pred (succ(succ zero)) in call-by-name proceeds like so: pred (succ(succ zero)) → rec succ(succ zero) as {zero → zero | succ x → z.x} (β → ) → (λ z. succ zero) (rec succ zero as {zero → zero | succ x → z.x}) (β succ ) → succ zero (β → ) Whereas, in call-by-value, the predecessor of both succ zero and zero is computed even though these intermediate results are not needed in the end: In general, pred is a constant time (O(1)) function over the size of its argument when following the call-by-name semantics, which computes the predecessor of any natural number in a fixed number of steps. In contrast, pred is a linear time (O(n)) function when following the call-by-value semantics, where pred (succ n zero) executes with a number of steps proportional to the size n of its argument because it requires at least n applications of the β succ rule before an answer can be returned.

Recursion in an Abstract Machine
In order to explore the lower-level performance details of recursion, we can use an abstract machine for modeling an implementation of System T. Unlike the operational semantics given in Fig. 3, which has to search arbitrarily deep into an expression for the next redex at every step, an abstract machine explicitly includes this search in the computation itself. As such, every step of the machine can be applied by matching only on the top-level form of the machine state, which more closely models a real implementation in a machine where each step is performed sequentially in a fixed amount of time. Thus, in an abstract machine instead of working with terms one works with configurations of the form:

M| |E
where M is a term also called a producer, and E is a continuation or evaluation context, also called a consumer. A state, also called a command, puts together a producer and a consumer, so that the output of M is given as the input to E. We first present distinct abstract machines for call-by-name and -value, we then smooth out the differences in the uniform abstract machine.

Call-by-Name Abstract Machine
The call-by-name abstract machine for System T is based on the Krivine machine (Krivine, 2007) The first two rules are refocusing rules that move the attention of the machine closer to the next reduction building a larger continuation: The latter three rules are reduction rules which correspond to steps of the operational semantics in Fig. 3.

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 . . . M n left-to-right to match the call-by-value semantics in Fig. 3: 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 • E corresponding to E[V ]) and the successor constructor (succ •E corresponding to E[succ ]). Also note that the final reduction rule for the 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.

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 v| |e 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, 2003).
Unlike the previous machines, continuations go beyond evaluation contexts and includẽ µx. v| |e , which is a continuation that binds its input value to x and then steps to the machine state v| |e . This new form allows us to express the additional call-by-value evaluation contexts: V • E becomesμx. V | |x · E , and succ •E isμx. succ x| |E . Evaluation contexts are also more restrictive than before; only values can be pushed on the calling stack. We represent the application continuation R · E with a non-value argument R by naming its partner-the generic value V -with y:μy. R| |μx. y| |x · E .
The refocusing rules can be subsumed all together by extending terms with a dual form ofμ-binding. The µ-abstraction expression µα. v| |e binds its continuation to α and then steps to the machine state v| |e . With µ-bindings, all the refocusing rules for call-by-name and -value can be encoded in terms of µ andμ. It is also not necessary to do these steps at run-time, but can all be done before execution through a compilation step. Indeed, all of System T terms can be translated to a smaller language, as shown in Fig. 5 where R stands for a non-value. The target language of this compilation step becomes the language of the uniform abstract machine. This language does not include anymore applications M N and the recursive term rec M as{. . . }. Also, unlike System T, the syntax of terms and coterms depends on the definition of values and covalues; succ V , rec{. . . } with E, and call stacks V · E are valid in both call-by-name and -value, just with different definitions of V and E. General terms also include the µandμ-binders described above: µα.c is not a value in call-by-value, andμx.c is not a covalue in call-by-name. So for example, succ(µα.c) is not a legal term in call-by-value, similarly (µα.c) · β is not a legal call stack in call-by-name.
As with System T, the notions of values and co-values drive the reduction rules, as shown in Fig. 4. In particular, the µ andμ rules will only substitute a value for a variable or a covalue for a covariable, respectively. Likewise, the β → 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 β zero and β succ for reducing a recursor when given a number constructed by zero or succ. While the β zero is exactly the same as it was previously in both specialized machine, notice how β succ is different. Rather than committing to one evaluation order or the other, β succ is neutral: the recursive predecessor (expressed as the term µα. V | |rec{. . . } with α 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μ-abstraction. This way, the correct evaluation order can be decided in the next step by either an application of µ orμ reduction.
Intermezzo 3.1. We can now summarize how some basic concepts of recursion are directly modeled in our syntactic framework: (c), general terms (v), and general coterms (e):

Call-by-name values (V ) and evaluation contexts (E):
Operational reduction rules:  -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. 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 brakes 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.

Examples of Recursion
By being restricted to capturing only (co)values, the µ andμ rules effectively implement the chosen evaluation strategy. For example, consider the application (λ z. succ zero) ((λ x.x) zero). Call-by-name evaluation will reduce the outer application first and return succ zero right away, whereas call-by-value evaluation will first reduce the inner application ((λ x.x) 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 (λ z.x) ((λ x.x) y) : To execute it, we need to put it in interaction with an actual context. In our case, we can simply use a covariable α. Call-by-name execution then proceeds as: Whereas call-by-value execution 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 µand ã µ-binder. In call-by-name, theμ rule takes precedence (because aμ-coterm is not a covalue), which leads to the next step which throws away the first argument, unevaluated. In call-by-value, the µ rule takes precedence (because a µ-term is not a value), which leads to the next step which evaluates the first argument.
Consider the System T definition of plus from Example 2.1, which is expressed by the machine term plus = λ x.λ y.µβ . x| |rec{zero → y | succ → z. succ z} with β The application plus 2 3 is then expressed as µα. plus| |2 · 3 · α , which is obtained by reducing some µandμ-bindings in advance. Putting this term in the context α, in call-byvalue it executes (eliding the branches of the 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 (succ(succ 3)) can be returned to the original caller (α). This update is implicit in the λcalculus-based System T, but becomes explicit in the abstract machine. In contrast, call-byname 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 β succ : Unless α demands to know something about the predecessor of this number, the term µβ . succ zero| |rec{. . . } with β will not be computed. Now consider pred (succ(succ zero)), which can be expressed in the machine as: In call-by-name it executes with respect to α like so: µα. pred| |succ(succ zero) · α | |α → pred| |succ(succ zero) · α (µ) Notice how, after the first application of β succ , the computation finishes in just oneμ 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 β succ rule, we have:

Recursion vs 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 the primitive iterator, respectively. Rather than including them as primitives, both can be expressed as syntactic sugar in the form macro-expansions in the language of the abstract machine like so: The only cost of this encoding of case and 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 iteration 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: The trick to this encoding is to use 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 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, 2003): In the syntax of the abstract machine, the analogous encoding of a rec continuation as a macro-expansion looks like this: 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: 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 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 pred function), then rec can provide an answer without computing the recursive result. However, when encoding rec with 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 pred using 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 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 rec has the same asymptotic complexity as its encoding via iter.

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: Γ ⊢ v : A says v produces an output of type A. In addition, there are also judgments for assigning types to coterms (Γ ⊢ e ÷ A says e consumes an input of type A) and commands (Γ ⊢ c says c is safe to compute, and does not produce or consume anything).
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 only execute commands c with just one free covariable (say α), representing the final, top-level continuation. Thus, well-typed executable commands will satisfy α ÷ Nat ⊢ c. The only final states of these executable commands have the form zero| |α , which sends 0 to the final continuation α, or succ V | |α , which sends the successor of some V to α. But the type system ensures more than just type safety: all well-typed programs will eventually terminate. That's because 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).

Theorem 3.2 (Type safety & Termination). For any command c of the recursive abstract
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 calculus (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 ÷ 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 ÷ A (or α ÷ A) can be removed by swapping between the left-and right-hand sides of the turnstyle (⊢), so that e ÷ A on the right becomes e : A on the left, and α ÷ A on the left becomes α : A on the right. Doing so gives a conventional two-sided sequent calculus as in (Ariola et al., 2009;Downen & Ariola, 2018b), where the rules labeled L with conclusions of the form

Corecursion in an Abstract Machine
Instead of coming up with an extension of System T with corecursion, and then define an abstract machine we start directly with the abstract machine which we obtain by applying duality. As a prototypical example of a coinductive type, we consider infinite streams of

Call-by-value values (V ) and evaluation contexts (E):
Operational rules: values, chosen for their familiarity (other coinductive types work just as well), which we represent by the type Stream A, as given in Fig. 7.
The intention is that Stream A is roughly dual to Nat, and so we will flip the roles of terms and coterms belonging to streams. In contrast with Nat, which has constructors for building values, Stream A has two destructors for building covalues. First, the covalue head E (the base case dual to zero) projects out the first element of its given stream and passes its value to E. Second, the covalue tail E (the coinductive case dual to succ V ) discards the first element of the stream and passes the remainder of the stream to E. The corecursor is defined by dualizing the recursor, whose general form is: Notice how the internal seed V corresponds to the return continuation E. In the base case of the recursor, term v is sent to the current value of the continuation E. Dually, in the base case of the corecursor, the coterm e receives the current value of the internal seed V . In the recursor's inductive case, y receives the result of the next recursive step (i.e., the predecessor of the current one). Whereas in the corecursor's coinductive case, γ sends the updated seed to the next corecursive step (i.e., the tail of the current one). The two cases of the recursor match the patterns zero (the base case) and succ x (the inductive case). Analogously, the corecursor matches against the two possible copatterns: the base case is head α, and the coinductive case is tail β . So the full form of the stream corecursor is: The uniform abstract machine is given in Fig. 8, where we highlight the extensions. Note how the corecursor generates (on the fly) the values of the stream using V as an incremental accumulator or seed, saving the progress made through the stream so far. In particular, the base case head α → e matching the head projection just passes the accumulator to e, which (may) compute the current element and send it to α. The corecursive case tail β → γ. f also passes the accumulator to f , which may return an updated accumulator (through γ) or circumvent further corecursion by returning another stream directly to the remaining projection (via β ). As with the syntax, the operational semantics is roughly symmetric to the rules for natural numbers, where roles of terms and coterms have been flipped.
Intermezzo 4.1. We review how the basic concepts of corecursion are reflected in our syntactic framework. Note how these observations are dual to the basic concepts of recursion.
-With coinductive data types, covalues are constructed and the producer is a process that generates the data. Observers of streams are constructed via the head and tail projections, and their construction is a process. -Use of codata is finite and its creation is (potentially) infinite in the sense that there must be no limit to the size of the codata that a producer can process. We can only build covalues from a finite number of destructor applications. However, the producer does not know how big of a request it will be given, so it has to be ready to handle codata structures of any size. In the end, termination is preserved because only finite covalues are consumed. -Corecursion produces the data, rather than using it. corec is a term, not a coterm.
-Corecursion starts from a seed and potentially produces bigger and bigger internal states; the corecursor brakes down the codata structure and might end when the base case is reached.
-The values of a codata structure potentially depend on each other. The n-th value of a stream might depend on the value at the index n-1.

Examples of corecursion
We represent the streams x, x, x, x, . . . and x, f x, f 2 x, · · · as: So when an observer asks always x (repeat f x) for its head element (matching the copattern head α), always x (repeat f x) returns (to α) the current value of the seed x. Otherwise, when an observer asks for its tail (matching the copattern tail β ), always x (repeat f x) continues corecursing with the same seed x (µγ. f | |x · γ ).
The infinite streams containing all zeroes, and the infinite stream of all natural numbers counting up from 0, are then represented as: To better understand execution, let's trace how computation works in both call-by-name and -value. Asking for the third element of zeroes proceeds with the following calculation in call-by-value (we let always x stands 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: countDown : Nat → Stream Nat countDown n = n, n − 1, n − 2, . . . , 3, 2, 1, 0, 0, 0, . . .
It is formally defined like so: This definition of countDown can be understood as follows: • If the head of the stream is requested (matching the copattern head α), then the current value x of the seed is returned (to α) as-is. • Otherwise, if the tail is requested (matching the copattern tail β ), then the current value of the seed is inspected: if it is 0, then 0 is the value of the updated seed; otherwise, the seed is the successor of some y, in which case y is given as the updated seed.
The previous definition of 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: Note that in the coinductive step, the decision on which continuation is taken (the observer of the tail β or the continuation of corecursion γ) depends on the current value of the seed. If the seed reaches 0 the corecursion is stopped and the streams of zero's is returned instead.

Properly 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 tail E looks similar enough to succ V , the base cases of head E and zero don't exactly line up, because head takes a parameter but zero does not.
One way to perfect the duality is to generalize Nat to Numbered A which represents a value of type A labeled with a natural number. Numbered A has two constructors: the base case zero : A → Numbered A labels an A value with the number 0, and succ : Numbered A → Numbered A increments the numeric label while leaving the A value alone, as shown by the following rules: In order to match the generalized zero constructor, the base case of the recursor needs to be likewise generalized with an extra parameter. In System T, this looks like rec M as {zero x → N | succ y → z.N ′ }, while in the abstract machine we get the generalized continuation rec {zero x → v | succ y → z.w} with E. The typing rule for this continuation is: It turns out that Numbered A is the proper dual to Stream A. Notice how the two constructors zero V and succ W exactly mirror the two destructors head E and tail F when we swap the roles of values and covalues. The recursor continuation rec {zero x → v | succ y → z.w} with E is the perfect mirror image of the stream corecursor corec {head α → e | tail β → γ. f } with F when we likewise swap variables with covariables in the (co)patterns. In more detail, we can formalize the duality relation (which we write as ∼) between values and covalues. Assuming that V ∼ E, we have the following duality between the constructors and destructors of these two types: We could also express the proper duality by restricting streams instead of generalizing numbers. In terms of the type defined above, Nat is isomorphic to Numbered ⊤, where ⊤ represents the usual unit type with a single value (often written as ()). Since ⊤ corresponds to logical truth, its dual is the ⊥ type corresponding to logical falsehood with no (closed) values, and a single covalue that represents an empty continuation. With this in mind, the type Nat is properly dual to Stream ⊥, i.e., an infinite stream of computations which cannot return any value to their observer 2 .

Corecursion vs Coiteration: Expressiveness and Efficiency
Similar to recursion, we can define two special cases of corecursion which only use part of its functionality by just ignoring a parameter in the corecursive branch. We derive the encodings for the creation of streams by applying the syntactic duality to the encodings presented in Section 3.5: Specifically, cocase simply matches on the shape of its projection, which has the form head α or tail β , without corecursing at all. In contrast, coiter always corecurses by providing an updated accumulator in the tail β case without ever referring to β . We have seen already several examples of coiteration. Indeed, all examples given in the previous section, except countDown ′ , are examples of coiteration, as indicated by the absence of the rest of the continuation (named _).
Recall from Section 2 that recursion in call-by-name versus call-by-value have different algorithmic complexities. The same holds for corecursion, with the benefit going instead to call-by-value. Indeed, in call-by-value the simple cocase continuation avoids the corecursive step entirely in two steps: whereas, cocase continues corecursing in call-by-name, despite the fact that this work will ultimately be thrown away once any element is requested via head: As an example of cocase, consider the following stream: Ideally, scons should not leave a lingering effect on the underlying stream. That is to say, the tail of scons x s should just be s. This happens directly in call-by-value. Consider indexing the n + 1 th element of scons in call-by-value, where we write tail n E to mean the n-fold application of tail over E (i.e., tail 0 E = E and tail n+1 E = tail(tail n E)): Notice how, after the first tail is resolved, the computation incurred by scons has completely vanished. In contrast, the computation of scons continues to linger in call-by-name: Here, we will spend time over the next n tail projections to build up an ever larger accumulator until the head is reached, even though the result will inevitably just backtrack to directly ask s for tail n E. However, one question remains: how do we accurately measure the cost of a stream? The answer is more subtle than the cost of numeric loops, because streams more closely resemble functions. With functions, it is not good enough to just count the steps it takes to calculate the closure. We also need to count the steps taken in the body of the function when it is called, i.e., what happens when the function is used. The same issue occurs with streams, where we also need to count what happens when the stream is used, i.e., the number of steps taken inside the stream in response to a projection. Of course, the internal number of steps in both cases can depend on the "size" of the input. For functions, this is the size of its argument; in the simple case of Nat → Nat, this size is just the value n of the numeric argument succ n zero itself. For streams, the input is the stream projection of the form tail n (head α), whose size is proportional to the number n of tail projections. Therefore, the computational complexity of a stream value s-perhaps defined by a corec term-is expressed as some O( f (n)), where n denotes the depth of the projection given by the number of tails. Now, let us consider the asymptotic cost of scons under both call-by-value and call-byname evaluation. In general, the difference in performance between scons| |x · s · E and s| |E in call-by-value is just a constant time (O(1)) overhead. So, given that the cost of s is O( f (n)), then the cost of scons| |x · s · E will also be O( f (n)). In contrast, the callby-name evaluation of scons incurs an additional linear time (O(n)) overhead based on depth of the projection: scons| |x · s · tail n+1 (head E) takes an additional number of steps proportional to n compared to the cost of executing s| |tail n (head E) . As a consequence, the call-by-name cost of scons| |x · s · E is O(n + f (n)), given that the cost of s is O( f (n)). So the efficiency of corecursion is better in call-by-value than in call-by-name.
To make the analysis more concrete, lets look at an application of scons to a specific underlying stream. Recall the countDown function from Section 4.1 which produces a stream counting down from a given n: n, n − 1, . . . , 2, 1, 0, 0, . . . . This function (and the similar countDown ′ ) is defined to immediately return a stream value that captures the starting number n, and then incrementally counts down one at a time with each tail projection. An alternative method of generating this same stream is to do all the counting up front: recurse right away on the starting number and use scons to piece together the stream from each step towards zero. This algorithm can be expressed in terms of System T-style recursion like so: So that the translation of countNow to the abstract machine language is: What is the cost of countNow? First, the up-front cost of calling the function with the argument succ n zero is unsurprisingly O(n), due to the use of the recursor. But this doesn't capture the full cost; what is the efficiency of using the stream value returned by countNow? To understand the efficiency of the stream, we have to consider both the initial numeric argument as well as the depth of the projection: countNow| |succ n zero · tail m (head α) in the abstract machine language, which corresponds to head(tail m (countNow (succ n zero))) in a functional style. In the base case, we have the stream zeroes, whose cost is O(m) because it must traverse past all m tail projections before it can return a 0 to the head projection. On top of this, we apply n applications of scons. Recall that in call-by-value, we said that the cost of scons is the same as the underlying stream. Thus, the call-by-value efficiency of the stream returned by countNow| |succ n zero · tail m (head α) is just O(m). In call-by-name in contrast, scons adds an additional linear time overhead to the underlying stream. Since there are n applications of scons and the projection is m elements deep, the call-by-name efficiency of the stream returned by countNow| |succ n zero · tail m (head α) is O(m(n + 1)). If the count n and depth m are roughly proportional to each other (so that n ≈ m), the difference between call-by-value and call-by-name evaluation of countNow's stream is a jump between a linear time and quadratic time computation.

Corecursion in Terms of Coiteration
Recall in Section 3.5 that we were able to encode rec in terms of iter, though at an increased computational cost. Applying syntactic duality, we can write a similar encoding of corec as a macro-expansion in terms of coiter. Doing so requires the dual of pairs: sum types. Sum types in the abstract machine look like (Wadler, 2003): The macro-expansion for encoding corec as coiter derived from duality is: Note how the coinductive step of 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 use its internal seed. In the base case matching head α, it rebuilds the observation head α and pairs it up with the original response e to the base case. In the coinductive case matching tail β , the projection tail β is combined with the continuation f which can update the internal seed via γ. Since f might refer to one or both of β and γ, we need to "extract" the two parts from the corecursive tail observation. Above, we express this extraction as copattern matching , 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 right x, then the coiter is simulating the original corec process with the seed x. This is because the 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 left s, containing some stream s, then the coiter is mimicking s as-is. This is because the left continuations for the base and coinductive steps exactly mimic the original observations (head α and tail β , respectively) which get applied to the stream s.
To start the corecursive process off, we begin with 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 γ, the seed is really updated to right V ′ , continuing the simulation of corecursion.
Otherwise, if f returns some other stream s to β , the seed gets updated to left s, and the coiteration continues but instead mimics s at each step. As with recursion, encoding corec in terms of coiter forces a performance penalty for functions like 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 right x. The first tail projection (triggering the β tail rule) leads to the decision point (by β + ) which chooses to update the seed with left s. From that point on, each tail projection to follow will trigger the next step of this coiteration (and another β tail rule). Each time, this will end up asking s for its tail, s 1 , which will be then used to build the next seed, left s 1 .
In order to continue, we need to know something about s, specifically, how it responds to a tail projection. For simplicity, assume that the tail of s is s 1 , i.e., s| |tail E → → s 1 | |E . And then for each following s i , assume its tail is s i+1 . Under this assumption, execution will proceed to the base case head projection like so: In total, this computation incurs additional β tail steps linearly proportional to n + 2, on top of any additional work needed to compute the same number of tail projections for each s i | |tail E → → s i+1 | |E along the way.

Safety and Termination
Just like System T Theorem 3.2, the (co)recursive abstract machine is both type safe (meaning that well-typed commands never get stuck) and terminating (meaning that well-typed commands always cannot execute forever). In order to prove this fact, we can build a model of type safety and termination rooted in the idea of Girard's reducibility candidates (Girard et al., 1989), but which matches closer to the structure of the abstract machine. In particular, we will use a model from (Downen et al., 2020(Downen et al., , 2019 which first identifies a set of commands that are safe to execute (in our case, commands which terminate on a valid final configuration). From there, types are modeled as a combination of terms and coterms that embed this safety property of executable commands.

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 α taking a Nat, so we expect all such safe commands to eventually finish execution in a valid final state that provides that α with a Nat construction: either a zero or successor.
Definition 6.1 (Safety). The set of safe commands, ‚, is: 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 (that is, ones found in ‚). However, we will quickly find that we also need completeness: any terms and coterms that do not break safety are included.
Definition 6.2 (Candidates). A pre-candidate is any pair A = (A + , A − ) where A + is a set of terms, and A − is a set of coterms, i.e., A ∈℘(Term) ×℘(CoTerm). A sound (pre-)candidate satisfies this additional requirement: • Soundness: for all v ∈ A + and e ∈ A − , the command v| |e is safe (i.e., v| |e ∈ ‚).
A complete (pre-)candidate satisfies these two completeness requirements: A reducibility candidate is any sound and complete (pre-)candidate. PC denotes the set of all pre-candidates, S C denotes the set of sound ones, C C the set of complete ones, and RC denotes the set of all reducibility candidates.
As notation, given any pre-candidate A, we will always write A + to denote the first component of A (the term set π 1 (A)) and A − to denote the second one (the coterm set π 2 (A)). As shorthand, given a reducibility candidate A = (A + , A − ), we write v ∈ A to mean v ∈ A + and likewise e ∈ A to mean e ∈ A − . Given a set of terms A + , we will occasionally write the pre-candidate (A + , {}) as just A + when the difference is clear from context. Likewise, we will occasionally write the pre-candidate ({}, A − ) as just the coterm set 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 λ -abstractions and call stacks, and every type contains µandμ-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 µandμ-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 µandμ-abstractions that always step to safe commands for any allowed binding. Lemma 6.3 (Activation). For any complete candidate A: Proof Consider the first fact (the second is perfectly dual to it and follows analogously), and assume that c[E/α] ∈ ‚ for all E ∈ A. In other words, the definition of c[E/α] ∈ ‚ says c[E/α] → → c ′ for some valid command c ′ ∈ Final. For any specific E ∈ A, we have:
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 µ-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 µ-rule might not fire. Dually, it is always easy to show theμ 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 ‚ is closed under expansion of the machine's operational semantics.

Property 6.4 (Expansion). If c → c ′ ∈ ‚ then c ∈ ‚.
Proof Follows from the definition of ‚ (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.

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: The reverse extension order A ⊒ B is defined as B ⊑ A, and supertype order A ≥ B is B ≤ A.

Refinement just expresses basic inclusion:
A refines B when everything in A (both term and coterm) is contained within B. With subtyping, the underlying set orderings go in opposite directions! If A is a subtype of B, then A can have fewer terms and more coterms than B. While this ordering may seem counter-intuitive, it closely captures the understanding of sound candidates where coterms are tests on terms. If ‚ 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 A is a subtype of B, then terms of A are also terms of B because they can be safely used in any context expecting inputs from B (i.e., with any coterm of B). Interestingly, our symmetric model lets us express the logical dual of this substitution principle: if A is a subtype of B, then the coterms of B (i.e., contexts expecting inputs of B) are coterms of A because they can be safely given any input from 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 PC with respect to subtyping order, where the binary intersection (A ∧ B, a.k.a meet or greatest lower bound) and union (A ∨ B, a.k.a join or least upper bound) are defined as: Moreover, these generalize to the intersection ( A , a.k.a infimum) and union ( A , a.k.a supremum) of any set A ⊆ PC of pre-candidates The binary least upper bounds and greatest lower bounds have these standard properties: In the general case for the bounds on an entire set of pre-candidates, we know: These intersections and unions both preserve soundness, and so they form a lattice of sound candidates in S C 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 A ∨ B might be missing some terms (such as µs) which could be soundly included, and dually A ∧ B might be missing some coterms (such asμs). So because all reducibility candidates are sound pre-candidates, A ∨ B and A ∧ B are well-defined, but their results will only be sound candidates (not another reducibility candidate). 3 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 A v and defined as 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.

They are (co)value extensions: Every (co)value of A is included in Pos(A) and
Neg(A).
3. They are the least/greatest such candidates: Any reducibility candidate that extends the (co)values of A lies between Pos(A) and Neg(A), with Pos(A) being smaller and Neg(A) being greater. In other words, given any reducibility candidate C such that A v ⊑ C: The full proof of these completions (and proofs of the other remaining propositions not given in this section) are given in Appendix 1. We refer to Pos(A) as the positive completion of A because it is based entirely on the values of A (i.e., its positive components): Pos(A) collects the complete set of coterms that are safe with A's values, 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 A can't influence the result of Pos(A). Dually, Neg(A) is the negative completion of A because it is based entirely on A's covalues in the same manner. Corollary 6.9 (Strong Positive & Negative Completeness). For any sound candidate A: Proof Follows directly from Lemmas 6.7 and 6.8. Now that we know how to turn sound pre-candidates A into reducibility candidates Pos(A) or Neg(A)-Pos and Neg take anything sound and deliver something sound and complete-we can spell out precisely the subtype-based lattice of reducibility candidates.

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. 9. Each type is interpreted as a reducibility candidate. Even though we are dealing with recursive types (Nat and 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 → 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. • Nat is the smallest candidate containing zero and closed successor constructors. • Stream A is the largest candidate containing head projections expecting an A element and closed under tail projections. Typing environments (Γ) are interpreted as the set of valid substitutions ρ which map variables x to values and covariables α to covalues. The interpretation of the typing environment Γ, x : A places an additional requirement on these substitutions: a valid substitution ρ ∈ Γ, x : A must substitute a value of A for the variable x, i.e., x[ρ] ∈ A . Dually, a valid substitution ρ ∈ Γ, α ÷ A must substitute a covalue of A for α, i.e., α[ρ] ∈ A . Finally, typing judgments (e.g., Γ ⊢ c) are interpreted as statements which assert that the command or (co)term belongs to the safe set ‚ 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.

If Γ ⊢ c is derivable then
In order to prove adequacy (Lemma 6.11), we need to know something more about which (co)terms are in the interpretation of types. For example, how do we know that the well-typed call stacks and λ -abstractions given by the rules in Fig. 6 end up in A → B ? Intuitively, function types themselves are non-recursive. In Fig. 9, the union over the possible candidates C defining A → B requires that certain call stacks must be in each C, but it does not quantify over the (co)values already in C to build upon them. Because of this, A → B is equivalent to the negative candidate Neg{V · E | V ∈ A , E ∈ B }, as noted in Fig. 9. It follows from Corollary 6.9 that A → B must contain any value which is compatible with just these call stacks, regardless of whatever else might be in A → B . This means we can use expansion (Property 6.4) to prove that A → B contains all λ -abstractions that, when given one of these call stacks, step via β → reduction to a safe command.
Proof Observe that, for any V ∈ A and E ∈ B : where v[V /x]| |E ∈ ‚ is guaranteed due to soundness for the reducibility candidate B . By expansion (Property 6.4), we know that λ x.v| |V · E ∈ ‚ as well. So from Corollary 6.9: But what about Nat and Stream A ? The interpretations of (co)inductive types are not exactly instances of Pos or Neg as written, because unlike A → B , they quantify over elements in the possible Cs they are made from. This lets us say these Cs are closed under succ or tail, but it means that we cannot identify a priori a set of (co)values that generate the candidate independent of each 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, 1971). 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: The starting approximation Nat 0 is the smallest reducibility candidate, which is given by Pos{}. From there, the next approximations are given by the positive candidate containing at least zero and the successor of every value of their predecessor. This construction mimics the approximations 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 RC (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 Stream A are defined negatively as: We start with the biggest possible candidate given by Neg{}. From there, the next approximations are given by the negative candidate containing at least head E (for any E expecting an element of type A ) and the tail of every covalue in the previous approximation. The net effect is that Stream A i definitely contains all continuations built from (at most) i head and tail destructors. As with Nat i , the goal is to show that Stream A is the limit of Stream A i , i.e., that it is the intersection of all finite approximations.
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 Nat i ; and thus also to ∞ i=0 Nat i = Nat by induction on i. Dually, the corecursor belongs to each approximation Stream 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 adequacy.

Related Work
The corecursor presented here is a computational interpretation of the categorical model of corecursion in a coalgebra (Geuvers, 1992). A (weak) coalgebra for a functor F is defined by a morphism α : A → F(A) for some A. A corecursive coalgebra extends this idea, by commuting with other morphisms of the form X → F(A + X). Intuitively, the option A + X in the result is interpreted as a pure sum type by (Geuvers, 1992). Here, we use a different interpretation of A + X as multiple outputs, represented concretely by multiple continuations. The continuation-based interpretation gives improved generality, and can express some corecursive algorithms that the other interpretations cannot (Downen & Ariola, 2021).
The coiterator, which we define as the restriction of the corecursor to never short-cut corecursion, corresponds exactly to the Harper's strgen (Harper, 2016). In this sense, the corecursor is a conservative extension of the purely functional coiterator. Coiteration with control operators is considered in (Barthe & Uustalu, 2002), which gives a call-by-name CPS translation for a stream coiterator and constructor, corresponding to coiter and cocase, but not for corec. Here, the use of an abstract machine serves a similar role as CPSmaking explicit information-and control-flow-but allows us to use the same translation for both call-by-value and -name. An alternative approach to (co)recursive combinators is sized types (Hughes et al., 1996;Abel, 2006), which give the programmer control over recursion while still ensuring termination, and have been used for both purely functional  and classical (Downen et al., 2015) coinductive types.
Our investigation on evaluation strategy showed the (dual) impact of call-by-value versus call-by-name evaluation (Curien & Herbelin, 2000;Wadler, 2003) on the efficiency of (co)recursion. In contrast to having a monolithic evaluation strategy, another approach is to use a hybrid evaluation strategy as done by call-by-push-value (Levy, 2001) or polarized languages (Zeilberger, 2009;Munch-Maccagnoni, 2013). With a hybrid approach, we could define one language which has the efficient version of both the recursor and corecursor. Polarity also allows for incorporating other evaluation strategies, such as callby-need which shares the work of computations (Downen & Ariola, 2018a;McDermott & Mycroft, 2019). We leave the investigation of a polarized version of corecursion to future work.

Conclusion
This paper provides a foundational calculus for (co)recursion in programs phrased in terms of an abstract machine language. The impact of evaluation strategy is also illustrated, where call-by-value and -name have (opposite) advantages for the efficiency of corecursion and recursion, respectively. These (co)recursion schemes are captured by (co)data types whose duality is made apparent by the language of the abstract machine. In particular, inductive data types, like numbers, revolve around constructing concrete, finite values, so that observations on numbers may be abstract and unbounded. Dually, coinductive codata types, like streams, revolve around concrete, finite observations, so that values may be abstract and unbounded objects. The computational interpretation of this duality lets us bring out hidden connections underlying the implementation of recursion and corecursion. For example, the explicit "seed" or accumulator usually used to generate infinite streams is, in fact, dual to the implicitly growing evaluation context of recursive calls. To show that the combination of primitive recursion and corecursion is well-behaved-that is, every program safely terminates with an answer-we interpreted the type system as a form of classical (bi)orthogonality model capable of handling first-class control effects, and extended with (co)inductive reducibility candidates. Our model reveals how the incremental Kleene-style and wholesale Knaster-Tarski-style constructions of greatest and least fixed points have different advantages for reasoning about program behavior. By showing the two fixed point constructions are the same-a non-trivial task for types of effectful computation-we get a complete picture of the mechanics of classical (co)recursion.

Proof of Type Safety and Termination
Here we give the full details to the proof of the main result, Theorem 6.14, ensuring both safety and termination for all well-typed, executable commands. We use a proof technique suitable for abstract machines based on (Downen et al., 2020(Downen et al., , 2019, which we extend with the inductive type Nat and the coinductive type Stream A. To begin in Appendices 1.1 to 1.3, we give a self-contained introduction and summary of the fundamental concepts and results from (Downen et al., 2020(Downen et al., , 2019. Appendix 1.2 in particular gives a new account of positive and negative completion which simplifies the sections that follow. From there, Appendix 1.4 establishes the definition and properties of the (co)inductive types Nat and Stream A in this model, which lets us prove the fundamental adequacy lemma in Appendix 1.5.

Orthogonal Fixed-Point Candidates
Our proof technique revolves around pre-candidates (Definition 6.2) and their more informative siblings reducibility candidates. The first, and most important, operation on pre-candidates is orthogonality. Intuitively, on the one side orthogonality identifies all the terms which are safe with everything in a given set of coterms, and on the other side it identifies the coterms which are safe with a set of terms. These two dual operations converting back and forth between terms and coterms naturally extends to a single operation on pre-candidates. Definition 1.1 (Orthogonality). The orthogonal of any set of terms, A + , written A +‚ , is the set of coterms that form safe commands (i.e., in ‚) with all of A + : Dually, the orthogonal of any set of coterms A − , also written A −‚ and disambiguated by context, is the set of terms that form safe commands with all of A − : Finally, the orthogonal of any pre-candidate A = (A + , A − ) is: As a shorthand for mapping over sets, given any set of pre-candidates A ⊆ PC , we write A ‚ * for the set of orthogonals to each pre-candidate in A : We use the same notation for the orthogonals of any set of term-sets (A ⊆ ℘(Term)) or coterm-sets (A ⊆ ℘(CoTerm)), individually.
Orthogonality is interesting primarily because of the logical structure it creates among pre-candidates. In particular, orthogonality behaves very much like intuitionistic negation (¬). Intuitionistic logic rejects double negation elimination (¬¬A ⇐⇒ A) in favor of the weaker principle of double negation introduction (A =⇒ ¬¬A). This fundamental property of intuitionistic negation is mimicked by pre-candidate orthogonality. Property 1.2 (Orthogonal Negation). The following holds for any pre-candidates A and B: 1. Contrapositive (i.e., antitonicity): . Therefore, e ∈ A ‚ by definition of orthogonality (Definition 1.1). Dually, given any e ∈ B ‚ and v ∈ A, we know v ∈ B and thus v| |e ∈ ‚, so e ∈ B ‚ as well. 2. DOI: Suppose v ∈ A. For any e ∈ A ‚ , we know v| |e ∈ ‚ by definition of orthogonality (Definition 1.1). Therefore, v ∈ A ‚‚ also by definition of orthogonality. Dually, every e ∈ A yields v| |e ∈ ‚ for all v ∈ A ‚ , so e ∈ A ‚‚ as well. 3. TOE: Note that A ⊑ A ‚‚ is an instance of double orthogonal introduction above for A, so by contrapositive, A ‚‚‚ ⊑ A ‚ . Another instance of double orthogonal introduction for A ‚ is A ‚ ⊑ A ‚‚‚ . Thus the two pre-candidates are equal.
The second operation on pre-candidates is the (co)value restriction. This just limits a given pre-candidate to only the values and covalues contained within it, and gives us a way to handle the chosen evaluation strategy (here, call-by-name or call-by-value) in the model. In particular, the (co)value restriction is useful for capturing the completeness requirement of reducibility candidates (Definition 6.2), which only tests (co)terms with respect to the (co)values already in the candidate. Definition 1.3 ((Co)value Restriction). The (co)value restriction of a set of terms A + , set of coterms A − , and pre-candidates A = (A + , A − ) is: As another shorthand, given any set of pre-candidates A , we will occasionally write A v * to be the set of (co)value restrictions of each pre-candidate in A : We use the same notation for the (co)value restriction of any set of term-sets or coterm-sets.
Property 1.4 (Monotonicity). Given any pre-candidates A and B, Proof Subtype monotonicity of orthogonality follows from contrapositive (Property 1.2) and the opposed definitions of refinement versus subtyping. Specifically, A ≤ B means the same thing as (A + , B − ) ⊑ (B + , A − ), which contrapositive (Property 1.2) turns into Monotonicity of the (co)value restriction with respect to both subtyping and refinement follows directly from its definition.
Putting the two operations together, (co)value restricted orthogonality (A v‚ ) becomes our primary way of handling reducibility candidates. This combined operation shares essentially the same negation-inspired properties of plain orthogonality (Property 1.2), but is restricted to just (co)values rather than general (co)terms.

Every reducibility candidate is a fixed point of orthogonality:
Proof Unfolding the definitions of orthogonality (Definition 1.1) and the (co)-value restriction (Definition 1.3) shows that the first two refinements are equivalent to soundness and completeness from Definition 6.2. For the last fact, first recall A ‚ ⊑ A v‚ (Property 1.5). So if a pre-candidate A is both sound and complete, Going the other way, suppose that A = A v‚ . Completeness is guaranteed by definition, but what of soundness? Suppose that v and e come from the fixed point pre-candidate A = A v‚ = (A −v‚ , A +v‚ ). The reason why A = A v‚ forces v| |e ∈ ‚ depends on the evaluation strategy.
• Call-by-value, where every coterm is a covalue. Thus, the positive requirement on terms of reducibility candidates is equivalent to: v ∈ A + if and only if, for all e ∈ A − , v| |e ∈ ‚. • Call-by-name, where every term is a value. Thus, the negative requirement on coterms of reducibility candidates is equivalent to: e ∈ A − if and only if, for all v ∈ A + , v| |e ∈ ‚.
In either case, v| |e ∈ ‚ for one of the above reasons, since v, e ∈ A = A v‚ .

Positive and Negative Completion
Now that we know reducibility candidates are the same thing as fixed points of (co)value restricted orthogonality ( v‚ ), we have a direct method to define the completion of a sound pre-candidate into a sound and complete one. To complete some A, there are two opposite points of view: (Pos) start with the terms of A and build everything else around those, or (Neg) start with the coterms of A and build around them. Both of these definitions satisfy all the defining criteria promised by Lemmas 6.7 to 6.8 due to the logical properties of orthogonality (Property 1.5). A 3. They are the least/greatest such candidates: Any reducibility candidate that extends the (co)values of A lies between Pos(A) and Neg(A), with Pos(A) being smaller and Neg(A) being greater. In other words, given any reducibility candidate C such that A v ⊑ C: Proof The definitions given in Definition 1.7 satisfy all three requirements: 1. They are reducibility candidates: Observe that by restricted triple orthogonal elimination (Property 1.5), Pos(A) and Neg(A) are reducibility candidates because they are fixed-points of v‚ (Lemma 1.6): 2. They are (co)value extensions: First, note that by restricted double orthogonal introduction (Property 1.5). Furthermore, soundness of A means A ⊑ A ‚ (i.e., A + ⊆ A −‚ and A − ⊆ A +‚ ), so again by Property 1.5:

3.
They are the least/greatest such candidates: Suppose there is a reducibility candidate C such that A v ⊑ C. Because C is a fixed point of v‚ (Lemma 1.6), iterating contrapositive (Property 1.2) on this refinement gives: Expanding the definition of Pos, Neg, and refinement, this means: In addition to these defining properties of Pos and Neg, the two completions are also idempotent (i.e., they are closure operations, because multiple applications are the same as just one) and monotonic (i.e., they preserve the subtyping order, by converting any two sound subtype candidates to two sound and complete subtype reducibility candidates).

Refinement and Subtyping Lattices
Because pre-candidates have two different orderings (Definition 6.5), they also have two very different lattice structures. We are primarily interested in the subtyping lattice because it is compatible with both soundness and completeness in both directions. In particular, the naïve subtype lattice as-is always preserves soundness, and combined with the dual completions (Pos and Neg) the subtype lattice preserves completeness as well. This gives us a direct way to assemble complex reducibility candidates from simpler ones.
Theorem 1.10 (Sound Subtype Lattice). The subtype intersection and union forms a complete semi-lattice over sound candidates in S C .
Proof Let A ⊆ S C be a set of sound candidates, and suppose v, e ∈ A . By definition: • for all A ∈ A , v ∈ A, and • there exists an A ∈ A such that e ∈ A.
Therefore, we know that v ∈ A for the particular sound candidate that e inhabits, and thus v| |e by soundness of A. Soundness of A follows dually, because v, e ∈ A implies: • there exists an A ∈ A such that v ∈ A, and • for all A ∈ A , e ∈ A. Proof Let A ⊆ RC be any set of reducibility candidates. First, note that A and A are sound (Theorem 1.10) because every reducibility candidate is sound. Thus, for all A ∈ A , monotonicity (Lemma 1.9) and idempotency (Corollary 1.8) of Pos and Neg implies: Lemma 1.9 and Corollary 1.8 also imply that these are the tightest such bounds. Suppose there are reducibility candidates B and C such that From the lattice properties of and , monotonicity, and idempotency, we have: The other lattice is based on refinement, instead of subtyping. In contrast, the refinement lattice has a opposing relationship with soundness and completeness: one direction of the lattice preserves only soundness, and the other one preserves only completeness. Definition 1.11 (Refinement Lattice). There is a complete lattice of pre-candidates in PC with respect to refinement order, where the binary intersection (A ⊓ B a.k.a meet) and union (A ⊓ B, a.k.a join) are defined as: Moreover, these generalize to the intersection ( A, a.k.a infimum) and union ( A, a.k.a supremum) of any set A ∈ PC of pre-candidates . The refinement intersection forms a meet semi-lattice over sound candidates in S C , and the refinement union forms a join semi-lattice over complete candidates in C C .
Proof Let A ∈ S C be a set of sound candidates, i.e., for all A ∈ A , we know A ⊑ A ‚ .
In the refinement lattice on pre-candidates, de Morgan duality (Property 1.13) implies: So that A is also sound.
Let A ∈ C C be a set of complete candidates, i.e., for all A ∈ A , we know A v‚ ⊑ A. In the refinement lattice on pre-candidates, de Morgan duality (Property 1.13) and the fact that the (co)value restriction v distributes over unions implies: So that A is also complete.
Because soundness and completeness are each broken by different directions of this refinement lattice, it doesn't give us a complete lattice for assembling new reducibility candidates. However, what it does give us is additional insight into the logical properties of orthogonality. That is, while orthogonality behaves like intuitionistic negation, the intersections ( ) and unions ( ) act like conjunction and disjunction, respectively. Together, these give us properties similar to the familiar de Morgan laws of duality intuitionistic logic.

Property 1.13 (Orthogonal de Morgan). Given any pre-candidates A and B:
Proof We will show only the de Morgan properties for union and intersection over any sets of pre-candidate A ; the binary versions are special cases of these. Note that the union and intersection of the refinement lattice on pre-candidates have these lattice properties: Taking the contrapositive (Property 1.2) to the facts on the left, and instantiating the facts on the right to A ‚ * , gives: In the reverse direction, suppose v ∈ (A ‚ * ). For every e ∈ A , we know there is (at least) one A ∈ A such that e ∈ A. So since v ∈ (A ‚ * ) ⊑ A ‚ , we know v| |e ∈ ‚ by definition of orthogonality (Definition 1.1). Therefore, v ∈ ( A ) ‚ as well. Dually, for every e ∈ (A ‚ * ) and v ∈ A , there it at least one v ∈ A ∈ A , forcing v| |e ∈ ‚ and thus e ∈ ( A ) ‚ . So in general (A ‚ * ) ⊑ ( A ) ‚ , making the two sets equal.

We know
Consider the possibility that each A ∈ A might contain a term v A incompatible with e (i.e., v A | |e / ∈ ‚), and yet each such v A might not end up in the intersection of A (v A / ∈ A ). In this case, e is still orthogonal to every term in A , but there is no individual A ∈ A such that e ∈ A ‚ because each one has an associated counter-example v A ruling it out. 3. The last fact follows from the above and triple orthogonal elimination (Property 1.2).
Take note that the missing direction in the asymmetric property (2) ) exactly corresponds to the direction of the de Morgan laws which is rejected by intuitionistic logic (the negation of a conjunction does not imply the disjunction of the negations). Instead, we have a weakened version of (2) presented in (3), adding additional applications of orthogonality to restore the symmetric equality rather than an asymmetric refinement. As with other properties like triple orthogonal elimination, this also has a (co)value restricted variant. Lemma 1.14 (Restricted de Morgan). For any set of pre-candidates A ⊆ PC : Proof Follows from the de Morgan laws (Property 1.13), restricted triple orthogonal elimination (Property 1.5), and the fact that the (co)value restriction v distributes over intersection and unions: With these de Morgan properties of intersection and union, we can be more specific about how the subtype lattice operations and on pre-candidates are lifted into the complete versions and that form the subtype lattice among reducibility candidates. Lemma 1.15. Let A ⊆ RC be any set of reducibility candidates.
Proof Follows from de Morgan duality (Property 1.13 and Lemma 1.14) and the fact that reducibility candidates are fixed points of v‚ (Lemma 1.6). Let

(Co)Induction and (Co)Recursion
We now examine how the (co)inductive types Nat and Stream A are properly defined as reducibility candidates in this orthogonality-based, symmetric model. As shorthand, we will use these two functions on reducibility candidates These capture the (co)inductive steps for the iterative definitions of Nat i and Stream A i : They also capture the all-at-once definitions of Nat and Stream A as due to the fact that their closure conditions (under zero, succ and head, tail, respectively) are equivalent to these subtyping conditions. Proof The "only if" directions follow directly from Lemma 6.7 by the definitions of N, S A , and subtyping. That is, we know that zero ∈ N(C) and succ V ∈ N(C) (for all V ∈ C) by definition of N in terms of Pos, and thus they must be in C ≥ N(C) by subtyping. Similarly, head E, tail F ∈ S A (C) ≤ C (for all E ∈ A and F ∈ C) by subtyping and the definition of S in terms of Neg. The "if" direction follows from the universal properties of Pos and Neg (Lemma 6.7): for any reducibility candidate C ⊒ B v Pos(B) ≤ C ≤ Neg(B). Now note that Therefore, if zero ∈ C and succ V ∈ C (for all V ∈ C) then Likewise if head E ∈ C and tail F ∈ C (for all E ∈ A and F ∈ C) then First, consider the model of the Nat type in terms of the infinite union of approximations: ∞ i=0 Nat i . This reducibility candidate should contain safe instances of the recursor. The reason it does is because the presence of a recursor is preserved by the N stepping operation on reducibility candidates, and so it must remain in the final union ∞ i=0 Nat i because it is in each approximation Nat i . Lemma 1.17 (Nat Recursion Step). For any reducibility candidates B and C, for all E ∈ B whenever the following conditions hold: • v ∈ B, • w[V /x, W /y] ∈ B for all V ∈ C and W ∈ B, and • rec{zero → v | succ x → y.w} with E ∈ C for all E ∈ B.
Proof Note that the accumulator continuation E changes during the successor step, so we will need to generalize over it. As shorthand, let E rec E := rec{zero → v | succ x → y.w} with E where E ′ stands for the given continuation accumulator. It suffices to show (via Corollary 6.9) that for all E ∈ B, zero| |E rec E and succ V | |E rec E (for all V ∈ C). Observe that, given any E ∈ B and V ∈ C, we have these two possible reductions: Now, we note the following series facts: Therefore, both V | |E rec E reduces to to a command in ‚ for any V ∈ N(C). It follows from Property 6.4 and Corollary 6.9 that E rec E ∈ N(C).
Nat i for all E ′ ∈ B. Applying Lemma 1.17 to Nat i , we have (for all E ′ ∈ B): Thus, we know that the least upper bound of all Nat i in the subtype lattice (Theorem 6.10) contains the instance of this recursor with E ′ = E ∈ B because it is a covalue (Lemma 6.7): Nat i Showing that the union ∞ i=0 Nat i is closed under the succ constructor is more difficult. The simple union ∞ i=0 Nat i is clearly closed under succ: every value in ∞ i=0 Nat i must come from some individual approximation Nat n , so its successor is in the next one Nat n+1 . However, ∞ i=0 Nat i is not just a simple union; it has been completed by Pos, so it might-hypothetically-contain more terms which do not come from any individual Nat n . Thankfully, this does not happen. It turns out the two unions are one in the same-the Pos completion cannot add anything more because of infinite recursors which can inspect numbers of any size-which lets us show that ∞ i=0 Nat i is indeed closed under succ.
Proof We already know that ∞ i=0 Nat i ≤ ∞ i=0 Nat i by definition (since all reducibility candidates are pre-candidates), so it suffices to show the reverse: Nat i . Since we know that every V ∈ ∞ i=0 Nat i and E ∈ ∞ i=0 Nat i forms a safe command V | |E ∈ ‚, this proves the result.
First, observe that ∞ i=0 Nat i contains the following instance of the recursor (Lemma 1.18): Nat i which has these reductions with zero and succ: The reason why this covalue forces values of ∞ i=0 Nat i into values of ∞ i=0 Nat i depends on the evaluation strategy.
In call-by-value, the first successor reduction proceeds as: where the continuation accumulator has beenμ-expanded. In general, an arbitrary step in this reduction sequence looks like: The only values (in call-by-value) which do not get stuck with rec ∞ (i.e., values V such that V | |rec ∞ → → c ∈ Final) have the form succ n zero which is in Nat n+1 ≤ ∞ i=0 Nat i . In call-by-name, the successor reduction proceeds as: Call-by-name includes another form of value, µβ .c, which is not immediately stuck with rec ∞ . We now need to show that V | |rec ∞ ∈ ‚, i.e., V | |rec ∞ → → c ∈ Final, forces V ∈ Nat n for some n. Let's examine this reduction more closely and check the intermediate results by abstracting out rec ∞ with a fresh covariable β : V | |rec ∞ → → c ∈ Final because V | |rec ∞ → → c ′ [rec ∞ /β ] for some V | |β → → c ′ → and then c ′ [rec ∞ /β ] → → c ∈ Final. We now proceed by (strong) induction on the length of the remaining reduction sequence (i.e., the number of steps in c ′ [rec ∞ /β ] → → c) and by cases on the shape of the intermediate c ′ : • c ′ = W | |β . Then c ′ [rec ∞ /β ] ∈ Final already. In this case, W | |E ∈ ‚ for any E whatsoever by expansion (Property 6.4), and so W ∈ Nat 0 = Pos{}. • c ′ = W | |β . Then we know that c ′ [rec ∞ Since W | |β → we know W [rec ∞ /β ] is not a µ-abstraction. The only other possibilities for W [rec ∞ /β ], given the known reduction to c, are zero or succ V ′ for some V ′ . zero ∈ Nat 1 by definition. In the case of succ V ′ , we have the (nonreflexive) reduction sequence c ′ [rec ∞ /β ] = succ V ′ | |rec ∞ → → V ′ | |rec ∞ → → c. The inductive hypothesis on the smaller reduction V ′ | |rec ∞ → → c ensures V ′ ∈ Nat n for some n, so that succ V ′ ∈ Nat n+1 by definition, and thus V ∈ Nat n+1 as well by expansion.
Due to the symmetry of the model, the story for Stream A is very much the same as Nat. We can show that the intersection of approximations-∞ i=0 Stream A i -contains safe instances of the corecursor because its presence is preserved by the stepping function S. The task of showing that this intersection is closed under the tail destructor is more challenging in the same way as succ closure. We solve it with the dual method: the presence of corecursors which "inspect" stream continuations of any size ensures that there are no new surprises that are not already found in one of the approximations Stream A n . Lemma 1.20 (Stream Corecursion Step). For any reducibility candidates A, B and C, for all V ∈ B whenever the following conditions hold: • e[E/α] ∈ B for all E ∈ A, • f [E/β , F/γ] ∈ B for all E ∈ C and F ∈ B, and • corec{head α → e | tail β → γ. f } with V ∈ C for all V ∈ B.
Proof Since the value accumulator V will change in the tail step, we have to generalize over it. Let V corec V := corec{head α → e | tail β → γ. f } with V, where V stands for a given Proof Note from Lemma 1.15 that We will proceed by showing there is a V ∈ ∞ i=0 Stream A i such that V | |E ∈ ‚ forces E ∈ ∞ i=0 Stream A i . Since we know that every E ∈ ∞ i=0 Stream A i and V ∈ ∞ i=0 Stream A i forms a safe command V | |E ∈ ‚, this proves the result. First, we define the following corecursive term: Stream A i (Lemma 1.21) for all V ∈ A . In general, corec ∞ [V ] has these reductions with head and tail: The reason why this value forces covalues of ∞ i=0 Stream A i into covalues of ∞ i=0 Stream A i depends on the evaluation strategy.
In call-by-name, the tail reduction proceeds as: where the value accumulator has been µ-expanded. The only covalues (in call-by-name) which do not get stuck with corec ∞ (i.e., covalues E such that corec ∞ [V ]| |E → → c ∈ Final) have the form tail n (head E) with E ∈ A , which is in Stream A n+1 ≥ ∞ i=0 Stream A i . In call-by-value, the tail reduction proceeds as: So in both call-by-name and -value, we have Finally, because all reducibility candidates are fixed points of v‚ (Lemma 1.6), de Morgan duality further implies: Now that we know that the iterative interpretations of Nat and Stream A contain all the expected parts-the (de)constructors and (co)recursors-we are ready to show that they are the same as the all-at-once definition given in Fig. 9. More specifically, the iterative ∞ i=0 Nat i and ∞ i=0 Stream A i correspond to the Kleene notion of (least and greatest, respectively) fixed points. Instead, the all-at-once Nat and Stream A correspond to the Knaster-Tarski fixed point definitions. These two correspond because the generating functions N and S are monotonic, and due to the fact that we can choose which approximation each value of ∞ i=0 Nat i and covalue of ∞ i=0 Stream A i comes from (Lemmas 1.19 and 1.22). Lemma 6.13 ((Co)Induction Inversion).
Proof First note that the values of ∞ i=0 Nat i is closed under zero a and succ: • zero ∈ Nat 1 ≤ ∞ i=0 Nat i by definition. • Given V ∈ ∞ i=0 Nat i , we know V ∈ ∞ i=0 Nat i (Lemma 1.19), and thus V ∈ Nat n for some n. So succ V ∈ Nat n+1 ≤ ∞ i=0 Nat i by definition.
Similarly, the covalues of ∞ i=0 Stream A i is closed under head and tail: • For all E ∈ A , head E ∈ Stream A 1 ≤ ∞ i=0 Stream A i by definition. • Given E ∈ ∞ i=0 Stream A i , we know E ∈ ∞ i=0 Stream A i (Lemma 1.22), and thus E ∈ Stream A n for some n. So tail E ∈ Stream A n+1 ≤ ∞ i=0 Stream A i by definition.
Because of these closure facts, we know from the definition of and , respectively, that ∞ i=0 Nat i ≥ {C | (zero ∈ C) and (∀V ∈ C. succ V ∈ C)} = Nat ∞ i=0 Stream A i ≤ {C | (∀E ∈ A . head E ∈ C) and (∀E ∈ C. tail E ∈ C)} = Stream A Going the other way, it we need to show that each approximation Nat i is a subtype of the Cs that make up Nat , and dually that each approximation Stream A i is a supertype of the Cs that make up Stream A . Suppose that C is any reducibility candidate such that N(C) ≤ C. Then Nat i ≤ C follows by induction on i: • (0) Nat 0 = Pos{} is the least reducibility candidate w.r.t subtyping, so Nat 0 ≤ C. • (i + 1) Assume that Nat i ≤ C. The next approximation is Nat i+1 = N( Nat i ).
Similarly, suppose that C is any reducibility candidate such that S A (C) ≥ C. Then Stream A i ≥ C follows by induction on i: • (0) Stream A 0 = Neg{} is the greatest reducibility candidate w.r.t subtyping, so Stream A 0 ≥ C trivially. • (i + 1) Assume that Stream A i ≥ C. The next approximation is Stream A i+1 = S A ( Stream A i ). Therefore, Stream A i+1 = S A ( Stream A i ) ≥ S A (C) ≥ C by monotonicity of S A (Lemma 1.23).
In other words, we know that every C ≥ N(C) is an upper bound of all approximations Nat i , and every C ≤ S A (C) is a lower bound of all approximations Stream A i . So because is the least upper bound and is the greatest lower bound, we have In other words, ∞ i=0 Nat i is a lower bound of the Cs that make up Nat and ∞ i=0 Stream A i is an upper bound of the Cs that make up Stream A (Lemma 1.16). Again, since is the greatest lower bound and is the least upper bound, we have

Adequacy
To conclude, we give the full proof of adequacy (Lemma 6.11) here. With the lemmas that precede in Appendix 1.4, the remaining details are now totally standard. Soundness ensures the safety of the Cut rule and completeness ensures that the terms of each type are included in their interpretations as reducibility candidates. The main role of adequacy is to show that the guarantees given by the premises of each typing rule are strong enough to Thus, Stream A i = Stream A by Lemmas 6.13 and 1.21. In other words