Hugo Herbelin
email: hugo.herbelin@inria.fr

A Constructive Proof of Dependent Choice, Compatible with Classical Logic

Keywords: Dependent choice, classical logic, constructive logic, strong existential

Martin-Löf's type theory has strong existential elimination (dependent sum type) that allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimination that makes it computationally compatible with classical logic. With this restriction, we lose the full axiom of choice but, thanks to a lazily-evaluated coinductive representation of quantification, we are still able to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic.

I. Introduction

a) Scaling Martin-Löf's proof of the axiom of choice to classical logic: In Martin-Löf's intuitionistic type theory [START_REF] Martin-Löf | A theory of types[END_REF], the functional form of the axiom of choice has a simple proof:

AC A
λH.(λx.wit (H x), λx.prf (H x)) : ∀x A ∃y B P(x, y) → ∃ f A→B ∀x A P(x, f (x))

where wit and prf are the first and second projections of a strong existential quantifier 1 .

The proof is constructive: it is a program which we can compute with in the sense that any closed proof of some Σ 0 1 -statement ∃z g(z) = 0 that uses the axiom of choice will eventually provide with a witness t such that g(t) = 0.

On the other side, classical logic is "constructive" too [START_REF] Griffin | The formulae-as-types notion of control[END_REF], [START_REF]Lambda-mu-calculus: An algorithmic interpretation of classical natural deduction[END_REF] and by interpreting Peirce's law by means of the callcc and throw control operators 2 , we can also compute witnesses from closed proofs of Σ 0 1 -statements. Combining the two is however delicate. Reminding that callcc α p has type A and binds the continuation variable α of input type A when p has type A while throw α p has arbitrary type B for p of type A and α of input type A, we cannot accept the following instance of the standard reduction rule for callcc in natural deduction: prf (callcc α (t 1 , φ(throw α (t 2 , p)))) callcc α prf (t 1 , φ(throw α prf (t 2 , p)))

since if the continuation α had input type ∃n P(n) in the lefthand side then it would have to have both input types P(t 1 )

and P(t 2 ) in the right-hand side, leading to an unexpected degeneracy of the domain of discourse 3 [19]. This first problem is solved by using higher-level reduction rules such as

E[prf (callcc α (t 1 , φ(throw α (t 2 , p))))] callcc α E[prf (t 1 , φ(throw α E[prf (t 2 , p)]))] E[wit (callcc α (t 1 , φ(throw α (t 2 , p))))] callcc α E[wit (t 1 , φ(throw α E[wit (t 2 , p)]))]
where the reduction is allowed only when E is an evaluation context whose return type does not depend on its hole. However, this does not help much because if E contained other occurrences of the expression prf (callcc α (t 1 , φ(throw α (t 2 , p)))) derived from the same initial proof (and this is precisely what would happen in Martin-Löf's proof of AC A if the two copies of H x were classical proofs of the form callcc α (t 1 , φ(throw α (t 2 , p)))), the synchronisation between the two proofs would be lost. b) Realising the axioms of countable choice and dependent choice in the presence of classical logic: The axiom of countable choice AC N : ∀x N ∃y A P(x, y) → ∃ f N→A ∀x N P(x, f (x)) and the slightly stronger axiom of dependent choice DC : ∀x A ∃y A P(x, y) → ∀x 0 ∃ f A→A ( f (0) = x 0 ∧ ∀n P( f (n), f (S (n))))

are two weak instances of the full axiom of choice and realisability contributed to understand their computational content in the presence of classical logic. Three approaches were followed.

A breakthrough was made in 1961 in the context of Gödel's functional interpretation (Dialectica) with the definition by Spector [START_REF] Spector | Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics[END_REF] of a notion of bar recursion so as to realise the principle of double negation shift from which the functional interpretation of the axiom of dependent choice follows.

Much later, in 1997, a direct realiser, in a sense close to the one of Kleene [START_REF] Kleene | On the interpretation of intuitionistic number theory[END_REF], was proposed in the context of the arithmetic in finite types by Berardi, Bezem and Coquand [START_REF] Berardi | On the computational content of the axiom of choice[END_REF] for the negative translation of the axiom of dependent choice.

In both cases, the key ingredient is a recursive loop parameterised by a finite portion of the function being built, each recursive call carrying one more piece of information than the preceding one, the whole process being terminating because, for the simply-typed λ-calculus based language of realisers they consider, closed programs over functions only uses a finite amount of information of their argument. Later on, Berger and Oliva [START_REF] Berger | Modified bar recursion[END_REF] reformulated Berardi, Bezem and Coquand's realiser in terms of some notion of modified bar recursion. Then, in 2004, Berger [START_REF] Berger | A computational interpretation of open induction[END_REF] reduced the termination of these realisers to some variant of open induction called update induction:

UI P : ∀ f (∀n( f (n) = ⊥ → ∀a P( f [n ← a])) → P( f )) → ∀ f P( f )
for f ranging over N → A ⊥ for A arbitrary and A ⊥ the extension of A with one extra element ⊥, for a ranging in A and f [n ← a] denoting the function g defined by

g(n) = a and g(p) = f (p) for p n, for P( f ) open predicate of the form ∀n Q( f |n ) → ∃n R( f |n ) assuming that f |n is the sequence ( f (0), ..., f (n -1)
). Otherwise said, Berger reduced the computational content of the axiom of dependent choice to a well-foundedness axiom whose computational content is a simple fixpoint. In practice, this means that we can prove the axioms of countable choice and dependent choice in a logic satisfying cut-elimination by just setting an axiom UI P whose computational content is a well-founded recursor:

UI P p f p f (λnλqλa.UI P p f [n ← a]).
In 2003, Krivine proposed realisers for the axioms of countable choice and dependent choice [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF] in the context of classical realisability for second-order arithmetic. Classical realisability, as developed by Krivine [START_REF]Realizability in classical logic[END_REF], can be seen as the composition of Kleene's realisability [START_REF] Kleene | On the interpretation of intuitionistic number theory[END_REF] with double negation translation and Friedman-Dragalin's A-translation4 [START_REF] Dragalin | New kinds of realizability and Markov's rule[END_REF], [START_REF] Friedman | Classically and intuitionistically provably recursive functions[END_REF]. Alternatively, it can be seen as a form of realisability allowing the use of control operators in realisers. Using our notations, the variant of countable choice realised by Krivine is

AC N : ∀x N ∃Y N→ P(x, Y) → ∃F N→N→ ∀x N P(x, F(x))
where N → and N → N → respectively denote the type of predicates and relations over N. Krivine's realiser for AC N does not use a fixpoint but instead a "quote" function which, informally, maps those Y x such that P(x, Y x ) into natural numbers that can then be compared so that the Y x with least "quote" is used to define F on x. The realiser also crucially uses control operators: if some Y x is found that has lesser quoted value than the Y x currently used to build F, the evaluation context at the time F(x) was requested is restored and a new computation of F on x with new Y x is started. In particular, Krivine's realisers are rather different in style from the ones of Berardi, Bezem and Coquand, and a fortiori from bar recursion. They do not seem either to generalise to choice functions with arbitrary, non relational, codomain A. c) Call-by-name, call-by-value and call-by-need: Church's λ-calculus [START_REF] Church | A set of postulates for the foundation of logic[END_REF], [START_REF] Barendregt | The Lambda Calculus: Its Syntax and Semantics[END_REF] comes naturally as a "call-byname" calculus and it is its use in computer programming languages that motivated the theoretical study of its more intricate 5 call-by-value counterpart, thanks successively to Plotkin [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF], Moggi [START_REF] Moggi | Computational lambda-calculus and monads[END_REF], Sabry and Felleisen [START_REF] Sabry | Reasoning about programs in continuationpassing style[END_REF], Sabry and Wadler [START_REF] Sabry | A reflection on call-by-value[END_REF], etc. Similarly, call-by-need λ-calculus, which is at the heart of programming languages like Haskell [START_REF]Haskell special issue[END_REF], progressively tends to be studied at the same foundational level its call-by-name and call-by-value variants are, see [START_REF] Ariola | The call-by-need lambda calculus[END_REF], [START_REF] Maraist | The call-by-need lambda calculus[END_REF], or, in the presence of control, [START_REF] Okasaki | Call-by-need and continuationpassing style[END_REF], [START_REF] Ariola | Classical call-by-need and duality[END_REF], [START_REF] Ariola | Classical call-by-need sequent calculi: The unity of semantic artifacts[END_REF]. Call-by-value and call-by-need are appropriate for sharing values and will turn to be useful for dealing with theories that might reflect proofs inside terms.

d) Internalising the construction of an approximation of the choice function at the level of proofs: In order to preserve the synchronisation between different instances of proofs, that are classical and hence liable to duplicate their evaluation context, call-by-value evaluation is indeed appropriate. However, in the proof of the axiom of choice above, the two occurrences of H x are in the scope of different binders of x what forbids the possibility to share them.

Let us assume that the domain of quantification A is the domain of natural numbers. Let us also assume for a while that we could define the choice function and its property by infinite terms. Then we could prove the axiom of countable choice with the following infinite proof:

AC N λH. (λn.if n = 0 then wit (H 0) else if n = 1 then wit (H 1) else ..., λn.if n = 0 then prf (H 0) else if n = 1 then prf (H 1) else ...)
Now, we have an infinite number of calls to H but each of these calls is parameter-free and hence shareable. Using the let operator of call-by-value, we can then make sharing explicit:

AC N λH. let H 0 = H 0 in let H 1 = H 1 in ... (λn.if n = 0 then wit H 0 else if n = 1 then wit H 1 else ..., λn.if n = 0 then prf H 0 else if n = 1 then prf H 1 else ...)
Now we have to capture the infinity by finitary means and this is possible by turning the infinite sequence of let into a single stream definition (H 0, H 1, ...). This leads to the following proof of the countable axiom of choice:

AC N λH. let s = cofix 0 f n (H n, f n) in (λn.wit (nth n s), λn.prf (nth n s))
where cofix 0 f n (H n, f n) is a corecursive definition of the stream iterating on f with parameter n and started at 0 while nth n s is a recursive definition of the access to the n th component of the stream s.

At the level of formulae, the stream is an inhabitant of a coinductively defined infinite conjunction ν 0 Xn (∃y P(0, y)∧X(n+ 1)). At the level of computation, since a stream is infinite, we cannot afford evaluating each of its component in advance, so we have to use a lazy call-by-value mechanism.

e) Outline: To make a sound formal system of this analysis, it remains to characterise the restriction required on strong existential elimination so that it becomes compatible with classical logic. In Section II, we study this restriction in the classical arithmetic in finite types, showing in passing how to define coinductive formulae in this context. By lazy evaluating the coinductive proofs, termination can reasonably be claimed, from which conservativity of classical logic over intuitionistic logic for Σ 0 1 formulae in the presence of strong existential elimination entails. In Section III, we show how to exploit the coinductive connectives to give a proof of the axioms of countable choice, axiom of dependent choice, and bar induction. Open issues will be discussed in Section IV together with a comparison with some other works.

II. dPA ω : Classical Arithmetic in Finite Types with Strong Existential

We now focus on the arithmetic in finite types and extend dPL with quantification over functions of higher-order types and recursion. In this logic, that we call dPA ω , the axioms of countable choice and dependent choice can be proved as will be shown in the next section.

Even though coinductive formulae can be defined in dPA ω , thanks to the quantification over functions, we will consider a primitive notion of coinductive formulae, considered positive, and that will be precisely convenient for proving the axioms of countable choice and dependent choice.

A. Proofs and Terms

Strong existential elimination forces formulae to be dependent of proofs. In dPA ω , terms t, u, ... can depend on proofs p, q, ..., and vice versa so that both are defined mutually:

t, u ::= x | 0 | S (t) | rec t of [t | (x, y).t] | λx.t | t t | wit p p, q ::= a | ι i (p) | (p 1 , p 2 ) | (t, p) | λa.p | λx.p | case p of [a 1 .p 1 | a 2 .p 2 ] | split p as (x, a) in q | dest p as (x, a) in q | prf p | p q | p t | exfalso p | refl | subst p q | ind t of [p | (x, a).q] | cofix t bx p | catch α p | throw α p | let a = p in q
where f ranges over function symbols, t denotes in f ( t) a sequence of terms of length the arity of f , the names x, y, . . . range over a set of term variables, a, b, . . . over a set of proof variables, α, β, . . . over a set of continuation variables. The constructions λa.p, case p of [a 1 .p 1 | a 2 .p 2 ], split p as (a 1 , a 2 ) in q, dest p as (x, a) in q and ind t of [p | (x, a).q] bind a, a 1 and a 2 . The constructions λx.p, dest p as (x, a) in q, dest p as (x, a) in t, λx.t, ind t of [p | (x, a).q] and rec t of [t | (x, y).t] bind x and y. The construction catch α p binds α. The binders are considered up to the actual name used to represent the binder (α-conversion) and the set of free variables FV(p) of a proof p is, as usual, the set of variables of p that are not bound inside p itself.

Most constructions speak by themselves with the peculiarity that terms can be built by case analysis (case) or destruction of proofs (split and dest). The operator rec t of [t | (x, y).t] is for recursion in finite types while ind t of [p | (x, a).q] is for induction. The construction cofix t bx p is for building coinductive formulae.

Let us say also that the operators catch and throw implement classical reasoning. They are similar to the operators of same name in Nakano [START_REF] Nakano | A constructive formalization of the catch and throw mechanism[END_REF] or Crolard [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF]. In terms of Parigot's λ-calculus [START_REF] Parigot | Free deduction: An analysis of "computations" in classical logic[END_REF], catch α p is basically equivalent to µα.[α]p and throw α p to µδ.[α]p for δ not occurring in p.

The abbreviations π 1 (p) split p as (a 1 , a 2 ) in a 1 and π 2 (p) split p as (a 1 , a 2 ) in a 2 might occasionally be useful.

To emphasise that a term variable ranges over functions, we might use symbols derived from the letters f or g instead of x or y. We might also use n or m for a variable ranging over natural numbers.

B. Operational Semantics

We equip dPA ω with a call-by-value evaluation semantics and for that, a subclass of proofs will play a particular role in extracting the intuitionistic content of positive formulae. These are the values defined by:

V ::= a | ι i (V) | (V, V) | (t, V) | λa.p | λx.p | () | refl
To define the operational semantics of dPA ω , we also need to define the class of elementary call-by-value evaluation contexts. Because of corecursion, we have potentially infinite values and we do not want to fully reduce proofs using a callby-value semantics. Therefore, we use an incremental reduction semantics which is lazy on the evaluation of corecursive values. Lazy evaluation requires to introduce specific contexts, written D, which accumulate pending delayed computation of cofixpoints. Altogether, evaluation contexts are defined as follows:

F[ ] ::

= ι i ([ ]) | ([ ], p) | (V, [ ]) | (t, [ ]) | case [ ] of [a 1 .p 1 | a 2 .p 2 ] | split [ ] as (a 1 , a 2 ) in q | dest [ ] as (x, a) in p | prf [ ] | [ ] q | [ ] t | let a = [ ] in q | subst [ ] p D[ ] ::= [ ] | D[F[ ]] | let a = cofix t bx p in D[ ] For F[ ]
let a = ι i (p) in q let b = p in q[ι i (b)/a] let a = (p 1 , p 2 ) in q let a 1 = p 1 in let a 2 = p 2 in q[(a 1 , a 2 )/a] let a = (t, p) in q let b = p in q[(t, b)/a] let a = λb.p in q q[λb.p/a] let a = λx.p in q q[λx.p/a] let a = () in q q[()/a] let a = b in q q[b/a] case ι i (p) of [a 1 .p 1 | a 2 .p 2 ] let a i = p in p i split (p 1 , p 2 ) as (a 1 , a 2 ) in q let a 1 = p 1 in let a 2 = p 2 in q dest (t, p) as (x, a) in q let a = p in q[t/x] prf (t, p) p (λa.q) p let a = p in q (λx.p) t p[t/x] subst refl p p ind 0 of [p | (x, a).q] p ind S (t) of [p | (x, a).q] q[t/x][ind t of [p | (x, a).q]/a] case cofix t bx p of [a 1 .p 1 | a 2 .p 2 ] let c = cofix t bx p in case c of [a 1 .p 1 | a 2 .p 2 ] split cofix t
bx p as (a 1 , a 2 ) in q let c = cofix t bx p in split c as (a 1 , a 2 ) in q dest cofix t bx p as (x, a) in q let c = cofix t bx p in dest c as (x, a) in q let a = cofix t bx p in exfalso q exfalso let a = cofix t bx p in q let a = cofix t bx p in throw α q throw α let a = cofix t bx p in q let a = cofix t bx p in catch α q The reduction rules are shown in Figure 1 where the substitutions p[V/a], p[u/x], t[V/a], t[u/x] and p[β/α] are capture-free with respect to the three kinds of variables (x, a and α) and where the substitution p[F/α] means replacing subterms of the form throw α q in p by throw α F[q] (including the recursive replacements in q) 6 .

catch α let a = cofix t bx p in q let a = cofix t bx p in D[case a of [a 1 .p 1 | a 2 .p 2 ]] let a = p[λy.cofix y bx p/b][t/x] in D[case a of [a 1 .p 1 | a 2 .p 2 ]] let a = cofix t bx p in D[split a as (a 1 , a 2 ) in q] let a = p[λy.cofix y bx p/b][t/x] in D[split a as (a 1 , a 2 ) in q] let a = cofix t bx p in D[dest a as (x, a ) in q] let a = p[λy.cofix y bx p/b][t/x] in D[dest a as (x, a ) in q] F[let a = cofix t bx p in q] let a = cofix t bx p in F[q] F[exfalso p] exfalso p F[throw α p] throw α p F[catch α p] catch α F[p[F/α]] exfalso exfalso p exfalso p exfalso throw β p throw β p exfalso catch β p exfalso p[exfalso [ ]/α] throw β exfalso p exfalso p throw β throw α p throw α p throw β catch α p throw β p[β/α] catch α throw α p catch α p catch β catch α p catch β p[β/α] wit (t, p) t (λx.t) u t[u/x] rec 0 of [t 0 | (x, y).t S ] t 0 rec S (t) of [t 0 | (x, y).t S ] t S [t/x][rec t of [t 0 | (x, y).t S ]/y]
We write for the reflexive-transitive closure of . We write ≡ for the reflexive-symmetric-transitive closure of .

(a : A) ∈ Γ Γ a : A axiom Γ p : A A ≡ B Γ p : B conv Γ p : A i Γ ι i (p) : A 1 ∨ A 2 ∨ i Γ, x : N, y : U t S : U Γ rec t of [t 0 | (x, y).t S ] : U Γ p : ∃x T A p is N-elimination-free Γ wit p : T ∃ wit E Fig. 2.
dPA ω : Classical arithmetic in finite types with strong existential P(wit a)) 7 . In addition to the usual connectives and quantifiers, we have coinductive formulae:

A, B ::= t = u | [a : A] → B | A ∨ B | A ∧ B | ⊥ | | ∀x T A | ∃x T A | ν t f x A
In atoms, P ranges over predicate symbols and t is a sequence of terms whose length is the arity of P. Negation ¬A is defined as A → ⊥. The construction ν t f x A stands for the instance on t of the coinductive predicate built from the monotone functor λ f.λx.A where A is made of atoms and positive connectives only (including ν-formulae themselves). In ∀x A and ∃x A, x is bound and freely subject to renaming (α-conversion). In ν t f x A, x and f are bound term variables. The formulae ∀x A and [a : A] → B are called negative. All other kinds of formulae are called positive.

Formulae are considered modulo the equational theory on terms, as it is common in Martin-Löf's intensional type theory. The equational theory is the one induced by reduction on terms and proofs plus the following reduction rules for equality 8 and coinductive formulae unfolding:

0 = 0 0 = S (u) ⊥ S (t) = 0 ⊥ S (t) = S (u) t = u ν t f x A A[t/x][ν y f x A/ f (y) = 0]
We write ≡ for the resulting 9 reflexive-symmetric-transitive closure of on formulae. When obvious from the context, or not relevant, we may occasionally drop the type of the variable in the quantifiers.

Since there are terms in all finite types in dPA ω , it is convenient to indicate the types of variables in typing contexts. Hence, contexts are defined by:

Γ ::= ∅ | Γ, x : T | Γ, a : A | Γ, α : A ⊥ ⊥
where a : A stands for an assumption of A and α : A ⊥ ⊥ for an assumption of the refutation 10 of A (with the objective of obtaining a proof by contradiction). On its side, x : T stands for the declaration of a variable of type T . It is assumed that assumptions have distinct variable names and we write Dom(Γ) for the set of names a and α thus declared in Γ.

Inference rules are given in Figure 2 with the typing rules in the bottom. The main difference with ordinary logic is the strong elimination rule of existential quantification and the appropriate support for formulae depending on proofs. 7 We do not get extra logical strength from this design choice. It can be proved in the case of predicate logic that the logic with dependent implication is conservative over ordinary predicate logic and we conjecture that dPA ω with dependent implication is conservative over its version without dependent implication.

8 See e.g. Allali [START_REF] Allali | Algorithmic equality in heyting arithmetic modulo[END_REF] for such a presentation of arithmetic. 9 Unfolding of coinductive formulae makes the reduction system non terminating. One might wonder if it would make ≡ undecidable: no, because unfolding can just be used lazily. 10 Not to be confused with the notation A B sometimes used for powerset.

In the rule ν I , the function f is said to be positive in A if A is built from atoms11 f (t) = 0 using disjunction, conjunction, existential quantification, equality or another coinductive type. That the typing rule ν I and the reduction rule for coinductive formulae do not extend by themselves the logical strength of HA ω and PA ω comes from the equations given in Figure 3 where out a implements the reduction rule for ν t f x A. However, the derived computational content is not the one we want because of the use of non positive connectives in the secondorder encoding, what justifies taking ν I and its associated reduction rule as primitive. Indeed, with a primitive notion of coinductive formula, it becomes syntactically direct to see ν as a constructor of positive formulae. In particular, and this is important later on to prove the axioms of countable choice and dependent choice, strong existential elimination is allowed to descend through coinductive formulae.

Dependent proofs have to be N-elimination-free (negativeelimination-free). N-elimination-freeness is defined by the following rules:

• a, (), λx.p and λa.p are N-elimination-free • if p, q, p 1 and p 2 are N-elimination-free then

ι i (p), (p 1 , p 2 ), (t, p), case a of [a 1 .p 1 | a 2 .p 2 ],
split q as (a 1 , a 2 ) in p, dest q as (x, a) in p, prf p, refl, subst p q, ind t of [p 1 | (x, a).p 2 ] and let a = p in q are N-elimination-free. Otherwise said, in N-elimination-free proofs, expressions of the form p q, p t, exfalso p, catch α p or throw α p can only occur in the body of a λx or of a λa.

The N-elimination-free condition is what ensures in particular that wit will never be applied to a classical proof, i.e. to a proof starting with catch α p or throw α p.

The resulting theory is then essentially Troelstra's arithmetic in all finite types HA ω (with equality on N) extended with classical logic and strong existential elimination. We write dHA ω for the version of dPA ω with rules catch and throw removed. Since dPA ω has classical reasoning, quantification over functional symbols and, as will be shown in Section III, dependent choice, it can simulate quantification over the predicates talking about N (since from the classical statement ∀n ∃b

(b = 0 ∧ φ(n)) ∨ (b = 1 ∧ ¬φ(n)), we get a characteristic function f for φ, i.e. a function that satisfies ∀n ( f (n) = 0 ∧ φ(n)) ∨ ( f (n) = 1 ∧ ¬φ(n))
). However, to get quantification over predicates talking about larger domains than N, one would also typically need the axiom of unique choice 12 on arbitrary large domains

∀x T ∃!n P(x, n) → ∃ f ∀x T P(x, f (x))
and there is no reason to think that this holds.

We are now ready to state the operational and logical properties of dPA ω .

Theorem 1 (Subject reduction): If Γ p : A and p q then Γ q : A.

ν t f x A ∃ f ( f (t) = 0 ∧ ∀x ( f (x) = 0 → A)) cofix t bx p (λx.0, (refl, λx.λb.p)) out a dest a as ( f, b) in split b as (c, d) in mon A[ f / f ][t/x] f,d (d t c)
where, for d : ∀x f (x) = 0 → A, and a : B, mon B f,d a is defined inductively: Proof: Most reduction rules are standard in a call-byvalue setting with control and a simple analysis shows that they preserve the correctness of derivations. The difficulty comes from strong existential elimination. The N-eliminationfreeness of p in prf p then ensures that the cases where F is prf [ ] in those reduction rules that explicitly mention F cannot happen. In particular, the only rule involving prf is prf (t, p) p which preserves the correctness of derivations. Note also that N-elimination-freeness is stable by substitution of values.

mon B f,d a : B[ν y f x A/ f (y) = 0] mon f (t)=0 f,d a ( f, (a, d)) mon B 1 ∧B 2 f,d a split a as (a 1 , a 2 ) in (mon B 1 f,d a 1 , mon B 2 f,d a 2 ) mon B 1 ∨B 2 f,d a case a of [a 1 .mon B 1 f,d a 1 | a 2 .mon B 2 f,d a 2 ] mon ∃x B f,
We claim normalisation by giving a sketch of proof. Claim 1 (Normalisation): If Γ p : A then p is normalisable.

Proof: (sketch) We follow the ideas of [START_REF] Coquand | A semantics of evidence for classical arithmetic[END_REF] and interpret proofs in infinitary logic. Normal proofs expand into wellfounded infinitary trees up to the presence of infinite branches coming from the expansion of cofixpoints and such that, beyond some given depth, only introduction rules of positive connectives occur. Otherwise said, along all branches, infinitely many nested introduction rules of positive connectives can occur but only finitely many nested elimination rules can be found. Let us consider a minimal proof having an infinite reduction sequence. Such an infinite reduction sequence can be seen as an infinite interaction between the immediate normal subproofs of the given proof. Laziness of cofixpoint unfolding now ensures that any time an infinite branch is explored in its part made only of introduction rules, nested elimination rules of another branch are explored simultaneously. If nested elimination rules of arbitrary depths are explored, then, by dependent choice, there is an infinite sequence of nested elimination rules. This is not the case, hence, only a finite portion of the infinite branches can be explored. Therefore, the infinite reduction sequence can be turned into an infinite interaction between modified proofs obtained by artificially cutting at some large enough occurrences the infinite branches of the original interacting normal subproofs. Such modified proofs are well-founded. But using the result of [START_REF] Coquand | A semantics of evidence for classical arithmetic[END_REF], interaction between well-founded normal proofs in infinitary logic necessarily terminates, a contradiction.

Theorem 2 (Conservativity, first version):

If A is a closed ∀-→-ν-wit-free formula then p : A in dPA ω implies that there is some V such that V : A in HA ω .

Proof: Our choice of rules makes that any closed proof of A eventually produces, by normalisation, either an expression D[V] or an expression catch α D[V] where D is made only of nested let a = cofix t bx q in [ ] (the case exfalso D[V] cannot happen because there is no value of type ⊥, the cases D[cofix t bx q] and catch α D[cofix t bx q] cannot happen because A is ν-free, all other possible configurations are reducible since p is closed). Now, because A is ∀-→-ν-wit-free, V does not contain any subexpression of the form λa.q or λx.q. In particular, in the catch α D[V] case, it does not contain any occurrences of α. Similarly, no variable that is bound to some cofix t bx q in D can occur in V since otherwise V would have ν in its type. Hence V is closed and is a proof of A. Since V does not contain any catch, nor throw, nor prf, it is in HA ω .

In arithmetic, any Σ 0 1 -formula is equivalent to a ∀-→-ν-witfree formula. Hence we have: III. The Axioms of Countable Choice and Dependent Choice Our main result is that dPA ω proves the axiom of countable choice, the axiom of dependent choice, and thus equivalent axioms such as bar induction, open induction and update induction. The main trick is to turn a proof of ∀x T A(x) where possibly the proof of A(t) is classical into a coinductive conjunction A(g(0)) ∧ A(g(1)) ∧ A(g(2)) . . . for a suitable law g of type N → A, so that the coinductive stream can be reduced using a (lazy) call-by-value discipline and the resulting (nonclassical) values be shared by calls to the strong existential elimination.

A. The Axiom of Countable Choice

Here, A(x) is ∃y P(x, y) and the appropriate stream we want to build is the stream A(0) ∧ A(1) ∧ A(2) . . ., so we consider the coinductive conjunction R C (n) ν n f x (A(x) ∧ f (S (x)) = 0). The proof is now direct:

AC N λa.let b = cofix 0 bn (a n, b (S (n))) in (λn.wit (nth C n b), λn.prf (nth C n b)) : ∀n∃y P(n, y) → ∃ f ∀n P(n, f (n)) where nth C n : R C (0) → R C (n) nth C n λb.π 1 (ind n of [b | (m, c).π 2 (c)])
Note that the proof does not use classical logic and holds also in dHA ω .

B. The Axiom of Dependent Choice

Here again, A(x) is ∃y P(x, y) and the appropriate stream we want to build is the stream A(x 0 ) ∧ A(g(x 0 )) ∧ A(g 2 (x 0 )) . . . where g is the choice function implicit in some proof of ∀x ∃y P(x, y). So we consider the coinductive formula R D (z) ν z f x ∃y (P(x, y) ∧ f (y) = 0). The proof is now direct:

DC λa.λx 0 .let b = s a x 0 in (λn.wit (nth D n (x 0 , b)), (refl, λn.π 1 (prf (prf (nth D n (x 0 , b)))))) : ∀x∃y P(x, y) → ∀x 0 ∃ f ( f (0) = x 0 ∧ ∀n P( f (n), f (S (n)))) where nth D n : ∃x R D (x) → ∃x R D (x) nth D n λb.ind n of [b | (m, c).(wit (prf c), π 2 (prf (prf c)))] s a x
: R D (x) s a x cofix x bn (dest a n as (y, c) in (y, (c, by))) Note that this proof too does not use classical logic and holds in dHA ω .

C. Bar Induction

To express bar induction, we extend dPA ω with a type constructor for finite sequences:

T ::= . . . | T * t, l ::= . . . | | l t | rec l of [t | (x, y, z).t] p ::= . . . | ind l of [p | (x, y, a).p]
The corresponding reduction, inference and typing rules are canonical and we skip them.

To state bar induction, we also need to define the initial segment of length n of a function f from N to T :

f |n rec n of [ | (m, l). l f (m)]
We now have all the ingredients to state the standard formulation of bar induction in intuitionistic logic: from which BI c directly follows. Then, from BI c , we get the following weaker form of BI:

BI : ∀ f ∃n B( f |n ) → ∀P ∀l (B (
∀ f ∃n B( f |n ) → ∀g ∀l (B(l) → g(l) = 0) ∧ ∀l (∀x g(l x) = 0 → g(l) = 0) → g( ) = 0
Finally, in the special case when x ranges over N, the characteristic function g of any predicate P over N * can be built classically using the axiom of countable choice. Hence a (classical) proof of BI is obtainable in this case.

IV. Discussion and Relation to Other Works f) A constructive intuitionistic logic which proves Markov's principle, the double negation shift and the axiom of dependent choice: It has been shown that adding delimited classical logic to intuitionistic logic allows to derive weakly classical schemes such as Markov's principle and the double negation shift while still preserving the disjunction and existence properties that are specific to intuitionistic logic [START_REF]An intuitionistic logic that proves Markov's principle[END_REF], [START_REF] Ilik | Preuves constructives de complétude et contrôle délimité[END_REF]. Adding strong existential elimination to intuitionistic logic with delimited classical logic should provide with a constructive intuitionistic logic that proves Markov's principle, the double negation shift and the axiom of dependent choice, and that is therefore adequate for intuitionistic analysis.

g) Relation with Berardi, Bezem and Coquand's realiser of the axiom of countable choice: The computational content of our proof of the countable axiom of choice is slightly different from the one of the realiser given in the paper by Berardi, Bezem and Coquand [START_REF] Berardi | On the computational content of the axiom of choice[END_REF]. First, in our proof, there is no construction of a function with dummy values: when the value of a function is needed (typically because some computation with the value ends into a natural number that serves in an induction step), it is directly the (first) value given by the proof of ∀n∃y P(n, y) which is used. Secondly, in our proof, the order in which the proofs of ∀n∃y P(n, y) are evaluated is the natural order, while in the case of [START_REF] Berardi | On the computational content of the axiom of choice[END_REF], these proofs are evaluated on demand depending on which n's the context that interacts with the realiser of ∃ f ∀n P(n, f (n)) needs a certification that P(n, f (n)) holds. In this sense, our proof seems suboptimal. For instance, if only the content of the proof of ∃y P(1001, y) is needed, it will evaluate all the proofs of ∃y P(n, y) for n < 1001 first. Of course, one could be more lazy than we did in our evaluation algorithm and in particular be lazy on the evaluation of each ∃y P(n, y) that is not explicitly required. Still, the stream built will be a stream of length 1001 while in [START_REF] Berardi | On the computational content of the axiom of choice[END_REF], the stream has the same size as the number of n's for which a proof of ∃y P(n, y) is needed.

h) Dependent choice in a logic with quantification over second-order predicates: Our approach is uniform over the type of the codomain of the choice function, so it directly scales to quantification over second-order predicate. Let us call dPA 2 and dHA 2 the classical and intuitionistic systems obtained by replacing the quantification over functions in finite types with quantification over second order predicates, i.e. the systems obtained from dPA ω and dHA ω by replacing the definition of types with:

T, U ::= N | | N → T
where denotes the type of propositions. Then, the axiom of countable choice is provable in dPA 2 and dHA 2 , what typically covers the instance AC N : ∀n N ∃Y N→ P(n, Y) → ∃F N→N→ ∀n N P(n, F n) that we discuss in the next paragraph.

i) Comparison with Krivine's realiser of the axiom of countable choice: Krivine [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF] realises the axiom of countable choice 13 in the context of classical second-order arithmetic using a notion of classical realisability that interprets quantifiers by intersection types and that consequently keeps no trace of the quantifiers in the realiser. A detailed comparison can be found in [START_REF]An intuitionistic logic that proves Markov's principle[END_REF]. j) Functional interpretation and products of selection functions: Products of selection functions have been developed by Escardó and Oliva in the context of functional interpretation to interpret bar recursion [START_REF] Escardó | Computational interpretations of analysis via products of selection functions[END_REF]. This seems to correspond at the level of realisability to what we are doing at the level of proofs.

V. Conclusion

We showed how to slightly restrict strong existential elimination (Martin-Löf's dependent sum type) so that it becomes compatible with classical reasoning in a computationally sound way. In this restricted framework, we lose the full axiom of choice but keep the axioms of countable choice and dependent choice thanks to a detour via coinductively defined connectives. Because the choice functions we are able to build are paths in coinductive trees, we suspect our framework to exactly capture the strength of the axiom of dependent choice. The idea here is to reason by induction on the structure of the 13 In practise, Krivine realises the axiom CAC : ∃Z N→N→ ∀n N (P(n, Z n) → ∀Y N→ P(n, Y)) which is classically equivalent to AC N over the codomain N → . argument of strong existential elimination, but we leave this for future work.

  an elementary call-by-value evaluation context and p a proof, we write F[p] for the proof obtained by plugging p into the hole of F[ ] and similarly for D[ ].

Fig. 1 .

 1 Fig. 1. Reduction rules on terms and proofs of dPA ω

Fig. 3 .

 3 Fig. 3. Derivability of introduction and reduction of coinductive formula

Theorem 3 (

 3 Conservativity, second version):If A is Σ 0 1 then p : A in dPA ω implies p : A in HA ω .This of course implies consistency: Theorem 4 (Consistency): p : ⊥ in dPA ω .

  l) → P(l)) ∧ ∀l (∀x P(l x) → P(l)) → P( ) Let us consider a contrapositive variant of BI BI c : ν gl (¬B(l) ∧ ∃x g(l x) = 0) → ∃ f ∀n ¬B( f |n ) where we have recognised the negation of the conclusion as a coinductive positive formula. By classical reasoning and the axiom of unique choice, BI and BI C are equivalent. Let us write R BI (l) for the coinductive formula occurring in the statement of BI C . The same way as we proved the axiom of dependent choice, we have: BI + C λa.(λn.wit (π 2 (prf (nth BI n ( , a)))), λn.(wit (nth BI n ( , a)), (π 1 (prf (nth BI n ( , a))), e a n))) : R BI ( ) → ∃ f ∀n ∃l (¬B(l) ∧ l = f |n ) where nth BI n : ∃l R BI (l) → ∃l R BI (l) nth BI n λb.ind n of [b | (m, c).(wit c wit (π 2 (prf c)), prf (π 2 (prf c)))] e a n : wit (nth BI n ( , a)) = (λn.wit (π 2 (prf (nth BI n ( , a))))) |n e a n ind n of [refl | (m, c).subst c refl]

Also known as Σ-type, dependent sum, or strong sum.

We use the SML names of these operators that exist also with other names in various other programming languages.

Failure of subject reduction when combining strong existential quantification and computational classical logic was also observed by P. Blain Levy (private communication).

See e.g. Berger and Oliva[START_REF] Berger | Modified bar recursion[END_REF] for a notion of realisability obtained by combination of Kleene's realisability and Friedman-Dragalin A-translation and in which ⊥ is realisable. That Krivine's classical realisability contains Atranslation comes from the fact that ⊥ is not empty but realised by a fixed set of realisers.

Though, when looking at λ-calculus from the point of view of sequent calculus instead of from the point of view of natural deduction[START_REF] Curien | The duality of computation[END_REF],[START_REF] Herbelin | C'est maintenant qu'on calcule: au coeur de la dualité[END_REF], call-by-value λ-calculus gets no more complicated than call-by-name, both having the same -intermediate -level of intrinsic technical complexity.

Strictly speaking, the definition of p[β/α] and p[F/α] requires also to consider their variants t[β/α] and t[F/α] on terms C. Types, Formulae and Inference Rules Terms are simply typed, with the natural numbers as base type. Finite types are thus defined by: T, U ::= N | T → UIn dPA ω , we consider implication to be possibly dependent in its antecedent and use the notation [a : A] → B to express this dependency, underlining the fact that a can occur in some term in B. An advantage of allowing this dependency is the ability to express statements such as [a : ∃x P(x)] →

I Γ p : A 1 ∨ A 2 Γ, a 1 : A 1 p 1 : B Γ, a 2 : A 2 p 2 : B Γ case p of [a 1 .p 1 | a 2 .p 2 ] : B ∨ E Γ p 1 : A 1 Γ p 2 : A 2 Γ (p 1 , p 2 ) : A 1 ∧ A 2 ∧ I Γ p : A 1 ∧ A 2 Γ, a 1 : A 1 , a 2 : A 2 q : B Γ split p as (a 1 , a 2 ) in q : B ∧ E Γ p : A[t/x] Γ t : T Γ (t, p) : ∃x T A ∃ I Γ p : ∃x T A Γ, x : T, a : A q : B Γ dest p as (x, a) in q : B ∃ E Γ p : ∃x T A p is N-elimination-free Γ prf p : A[wit p/x] ∃ prf E Γ, a : A p : B Γ λa.p : [a : A] → B → I Γ p : [a : A] → B Γ q : A a FV(B) if q not N-elimination-free Γ p q : B[q/a] → E Γ, x : T p : A Γ λx.p : ∀x T A ∀ I Γ p : ∀x T A Γ t : T Γ p t : A[t/x] ∀ E Γ () : I Γ p : ⊥ Γ exfalso p : C ⊥ E Γ t : N Γ refl : t = t refl Γ p : t = u Γ q : A[t/x]x Dom(Γ)Γ subst p q : A[u/x] subst Γ t : N Γ p : A[0/x] Γ, x : T, a : A q : A[S (x)/x] Γ ind t of [p | (x, a).q] : A[t/x] ind Γ p : A Γ, a : A q : B a FV(B) if p not N-elimination-free Γ let a = p in q : B[p/a] cut Γ t : T Γ, f : T → N, x : T, b : ∀y f (y) = 0 p : A f positive in A Γ cofix t bx p : ν t f x A ν I Γ, α : A ⊥ ⊥ p : A Γ catch α p : A catch Γ p : A (α : A ⊥ ⊥ ) ∈ Γ Γ throw α p : C throw (x : T ) ∈ Γ Γ x : T Γ,x : U t : T Γ λx.t : U → T Γ t : U → T Γ u : U Γ t u : T Γ 0 : N Γ t : N Γ S (t) : N Γ t : N Γ t 0 : U

Since we have symbols for functions and not for predicates, we use expressions of the form f (t) = 0 to represent arbitrary atoms.

Acknowledgements

Concepts coming from the programming languages side were instrumental for this work and I'm grateful to the community that designed them.

On a personal side, I thank Danko Ilik, Paul-André Melliès, Guillaume Munch-Maccagnoni, and Noam Zeilberger for fruitful discussions they shared with me.


♦ •♦♥❣❡r ❛ ❝♦✲✈❛•✉❡ s✐♥❝❡ ✈❛r✐❛❜•❡ x ✐s ♥♦t ♥❡❡❞❡❞ ✖ ✐♥❞❡❡❞ x ♠✉st ✜rst ❜❡ s✉❜st✐t✉t❡❞ ❢♦r z✳ ❚❤❡ s♦•✉t✐♦♥ ❢♦••♦✇❡❞ ❤❡r❡ ✐s t♦ r❡str✐❝t t❤❡ ♥♦t✐♦♥ ♦❢ ❝♦✲✈❛•✉❡ ✉♥t✐• ✇❡ ❤❛✈❡ ♠♦r❡ ✐♥❢♦r♠❛t✐♦♥ ♦♥ t❤❡ r❡st ♦❢ t❤❡ ❝♦♠♣✉t❛t✐♦♥✳ ❚❤✉s✱ ❛ ❝♦♥t❡①t ♦❢ t❤❡ ❢♦r♠ μx. x||α ✐s ♥♦t ❛ ❝♦✲✈❛•✉❡✱ ❜❡❝❛✉s❡ ✇❡ ❞♦ ♥♦t ❦♥♦✇ ✇❤❡t❤❡r ♦r ♥♦t x ✇✐•• ❜❡ ❢♦r❝❡❞✳ ❚❤❡ ♥♦t✐♦♥ ♦❢ ✇❡❛❦ ❤❡❛❞ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ✐s ❞❡✜♥❡❞ ❛s c → β c ′ C[c] → lv C[c ′ ] c → μv c ′ C[c] → lv C[c ′ ] c → µ l c ′ C[c] → lv C[c ′ ] ❆ ✇❡❛❦ ❤❡❛❞ ♥♦r♠❛• ❢♦r♠ ✭✇❤♥❢✮ ❢♦r λ lv ✐s ❡✐t❤❡r C[ λx.t||α ] ♦r C[ z||F ] ✇❤❡r❡ z ✐s ♥♦t ❜♦✉♥❞ ✐♥ C✳ ❚❤❡ st❛♥❞❛r❞✐③❛t✐♦♥ ✐s ❝♦♠♣•❡t❡ ✇✐t❤ r❡s♣❡❝t t♦ r❡❞✉❝t✐♦♥✿ ✉s✐♥❣ st❛♥❞❛r❞ ♣r♦♦❢ t❡❝❤♥✐q✉❡s ✭s❡❡ ❡✳❣✳ ❬✷(✮✱ ♦♥❡ ❝❛♥ s❤♦✇ t❤❛t ✐❢ c → → lv c ′ ❛♥❞ c ′ ✐s ❛ ✇❤♥❢✱ t❤❡♥ t❤❡r❡ ❡①✐sts ❛ ✇❤♥❢ c ′′ s✉❝❤ t❤❛t c → → lv c ′′ ❛♥❞ c ′′ → → lv c ′ ✳ ✸ ❆ ♠✉•t✐❝✉t s❡q✉❡♥t ❝❛•❝✉•✉s ✭λ [lv τ ] ✮ ❲❡ ♥♦✇ ❡①♣•♦r❡ ❛ ❝❛•❝✉•✉s✱ ✇❤✐❝❤ ✇❡ ❝❛•• t❤❡ ♠✉•t✐❝✉t ❝❛•❝✉•✉s✱ ✇❤✐❝❤ ❦❡❡♣s t❤❡ st❛♥❞❛r❞ r❡❞❡① ❛t t❤❡ t♦♣ ♦❢ ❛ ❝♦♠♠❛♥❞ ❛♥❞ ❛✈♦✐❞s s❡❛r❝❤✐♥❣ t❤r♦✉❣❤ t❤❡ ♠❡t❛✲❝♦♥t❡①t ❢♦r ✇♦r❦ t♦ ❜❡ ❞♦♥❡✳ ❲❡ ❞❡s✐❣♥ t❤❡ ❝❛•❝✉•✉s ✐♥ t❤r❡❡ st❡♣s✳ ❋✐rst✱ ✇❡ ✐♥tr♦❞✉❝❡ ❛ s②♥t❛❝t✐❝ ♥♦t❛t✐♦♥ ❢♦r ❢♦r❝❡❞ •❡t✲❡①♣r❡ss✐♦♥s ✭μx.C[ x||F ]✮ ❛♥❞ t❤❡ ❛ss♦❝✐❛t❡❞ r❡❞✉❝t✐♦♥ r✉•❡s✳ ❙❡❝♦♥❞✱ ✇❡ ❛♣♣•② ❉❛♥✈②✬s ❬✺( t❡❝❤♥✐q✉❡ t♦ s②s✲ t❡♠❛t✐❝❛••② ❞❡r✐✈❡ t❤❡ ❛ss♦❝✐❛t❡❞ ❛❜str❛❝t ♠❛❝❤✐♥❡✳ ❚❤✐r❞✱ t❤❡ ♠✉•t✐❝✉t ❝❛•❝✉•✉s ❝♦♠❡s ♦✉t ❛s ❛ ❣❡♥❡r❛•✐③❛t✐♦♥ ♦❢ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡✳ ❲❡ ♠♦❞✐❢② t❤❡ s②♥t❛① ♦❢ λ lv ❜② ✇r✐t✐♥❣ ❢♦r❝❡❞ •❡ts ❛s μ[x]. x||F τ s♦ t❤❛t t❤❡ ❢♦r❝❡❞ ❝♦♠♠❛♥❞ ❛♥❞ ✐ts s✉rr♦✉♥❞✐♥❣ ❡♥✈✐r♦♥♠❡♥t ♦❢ ❜✐♥❞✐♥❣s ❛r❡ ❦❡♣t s❡♣❛r❛t❡✱ ❣✐✈✐♥❣ ✉s λ [lv ] ✳ ❚❤❡ s❡♣❛r❛t✐♦♥ ❜❡t✇❡❡♥ t❤❡ ❝♦♠♠❛♥❞ ❛♥❞ ✐ts ❡♥✈✐r♦♥♠❡♥t ♠❛❦❡s ✐t ❡①♣•✐❝✐t t❤❛t t❤❡ ❝♦♠♠❛♥❞ ✐s ❜r♦✉❣❤t t♦ t❤❡ t♦♣ ♦❢ ❛ ❢♦r❝❡❞ •❡t ✖ t❤❡r❡ ✐s ♥♦ ✉♥❜♦✉♥❞❡❞ s❡❛r❝❤ ❢♦r t❤❡ ❝♦♠♠❛♥❞ t❤❛t ✇❛s ❢♦r❝❡❞✳ ❚❤❡ s②♥t❛① ♦❢ λ [lv ] ✐s✿ E ∈ CoV alue ::= α | | F | | μ[x]. x||F τ τ ∈ Environment ::= ǫ | | [x = µα.c]τ ✇❤❡r❡ c, t, V, e ❛♥❞ F ❛r❡ ❞❡✜♥❡❞ ❛s ❜❡❢♦r❡✳ ❚❤❡ r❡•❛t✐♦♥s❤✐♣ ❜❡t✇❡❡♥ t❤❡ s②♥t❛① ♦❢ λ [lv ] ❛♥❞ λ lv ✐♥❝•✉❞❡s✿ μ[x]. x||F τ ≈ μx.τ [ x||F ] = ǫ µα.c||μx.C = C[x = µα.c] ǫ = τ [x = µα.c] = µα.c||μx.τ ✇❤❡r❡ ❛•• ♦t❤❡r ✐❞❡♥t✐❝❛• s②♥t❛❝t✐❝ ❢♦r♠s ❛r❡ r❡•❛t❡❞✳ ❚❤❡ λ [lv ] r❡❞✉❝t✐♦♥ s②st❡♠✱ ✐♥ ❛❞❞✐t✐♦♥ t♦ t❤❡ ♣r❡✈✐♦✉s β, μv ❛♥❞ µ l r✉•❡s✱ ❝♦♥t❛✐♥s t✇♦ ♥❡✇ r❡❞✉❝t✐♦♥s✿ ◆♦t❡ t❤❛t ✐♥ ❛ t❡r♠ ♦❢ t❤❡ ❢♦r♠ µα.c||μx. µβ.c ′ ||μz. x||F ✱ t❤❡r❡ ✐s ♥♦ ❝♦♥t❡①t s✇✐t❝❤✱ ♠❡❛♥✐♥❣ ✇❡ ❞♦ ♥♦t s✉❜st✐t✉t❡ ❢♦r α✳ ❋✐rst✱ t❤❡ ❢❛❝t t❤❛t x ✐s ♥❡❡❞❡❞ ✐s r❡❝♦r❞❡❞ ✈✐❛ t❤❡ r✉•❡ μ[] •❡❛❞✐♥❣ t♦✿ µα.c||μ[x]. x||F [z = µβ.c ′ ] ✳ ❆❢t❡r✇❛r❞✱ t❤❡ µ l r✉•❡ ❛♣♣•✐❡s✱ ❛s ✐♥ λ lv ✳ ❚❤❡ ✇❡❛❦ ❤❡❛❞ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ♦❢ λ [lv ] ✐s ❞❡✜♥❡❞ ❛s ❜❡❢♦r❡✳ ■t s✐♠✉•❛t❡s t❤❡ ✇❡❛❦ ❤❡❛❞ st❛♥❞❛r❞✐③❛t✐♦♥ ♦❢ λ lv ✳ ❚❤❡♦r❡♠ ✶✳ •✐✈❡♥ c 1 ❢r♦♠ λ [lv ] ❛♥❞ c 2 ❢r♦♠ λ lv s✉❝❤ t❤❛t c 1 ≈ c 2 ✿ ✲ ■❢ c 2 → lv c ′ 2 t❤❡♥ t❤❡r❡ ❡①✐sts c ′ 1 s✉❝❤ t❤❛t c 1 → 1/2 [lv] c ′ 1 ❛♥❞ c ′ 1 ≈ c ′ 2 ❀ ✲ ■❢ c 1 → [lv] c ′ 1 t❤❡♥ t❤❡r❡ ❡①✐sts c ′ 2 s✉❝❤ t❤❛t c 2 → 0/1 lv c ′ 2 ❛♥❞ c ′ 1 ≈ c ′ 2 ❲❡ ✉s❡ ❉❛♥✈②✬s t❡❝❤♥✐q✉❡ ❢♦r ✐♥t❡r✲❞❡r✐✈✐♥❣ s❡♠❛♥t✐❝ ❛rt✐❢❛❝ts ✐♥ ♦r❞❡r t♦ ❣❡♥❡r❛t❡ ❛♥ ❛❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r λ [lv ] ✳ ❚❤❡ ✜rst st❡♣ ✐♥ ❞❡r✐✈✐♥❣ ❛♥ ❛❜str❛❝t ♠❛✲ ❝❤✐♥❡ ❢r♦♠ ✐ts ❝❛•❝✉•✉s ✐s t♦ r❡♣r❡s❡♥t t❤❡ ♦♣❡r❛t✐♦♥❛• s❡♠❛♥t✐❝s ❢♦r t❤❛t ❝❛•❝✉•✉s ❛s ❛ s♠❛••✲st❡♣ ✐♥t❡r♣r❡t❡r✳ ❚♦ ❜❡❣✐♥✱ ✇❡ ❝❛♣t✉r❡ t❤❡ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ✐♥ ❛ s❡❛r❝❤ ❢✉♥❝t✐♦♥ t❤❛t✱ ❣✐✈❡♥ ❛ ♣r♦❣r❛♠✱ ✐❞❡♥t✐✜❡s t❤❡ ♥❡①t r❡❞❡① t♦ ❝♦♥tr❛❝t✳ ❇② ❈P❙ tr❛♥s❢♦r♠✐♥❣ ❛♥❞ t❤❡♥ ❞❡❢✉♥❝t✐♦♥❛•✐③✐♥❣ t❤❡ s❡❛r❝❤ ❢✉♥❝t✐♦♥✱ t❤❡ ❝❛•• st❛❝❦ ♦❢ t❤❡ s❡❛r❝❤✐♥❣ ♣r♦❝❡❞✉r❡ ✐s r❡✐✜❡❞ ❛s ❛ ❞❛t❛ str✉❝t✉r❡✱ ✇❤✐❝❤ ❝♦rr❡s♣♦♥❞s ✇✐t❤ t❤❡ ✐♥s✐❞❡✲♦✉t ✭♠❡t❛✲✮❝♦♥t❡①t ❞❡✜♥✐♥❣ t❤❡ st❛♥❞❛r❞✐③❛t✐♦♥✳ ❚❤❡ ❞❡❢✉♥❝t✐♦♥❛•✐③❡❞ s❡❛r❝❤ ❢✉♥❝t✐♦♥ ✐s ❡①t❡♥❞❡❞ ✐♥t♦ ❛ ❞❡❝♦♠♣♦s✐t✐♦♥ ❢✉♥❝t✐♦♥ t❤❛t s♣•✐ts ❛ ♣r♦❣r❛♠ ✐♥t♦ ❛ ♠❡t❛✲❝♦♥t❡①t ❛♥❞ r❡❞❡①✳ ❉❡❝♦♠♣♦s✐t✐♦♥✱ ❝♦♥tr❛❝t✐♦♥✱ ❛♥❞ r❡❝♦♠♣♦s✐t✐♦♥ t♦❣❡t❤❡r ❞❡✜♥❡ ❛♥ ✐t❡r❛t✐✈❡ s♠❛••✲st❡♣ ✐♥t❡r♣r❡t❡r ❛♥❞ ❛♥ ♦♣❡r❛t✐♦♥❛• s❡♠❛♥t✐❝s ❢♦r t❤❡ ❝❛•❝✉•✉s✳ ❚❤❡ ♥❡①t st❡♣ ✐♥ t❤❡ ♣r♦❝❡ss ✐s t♦ tr❛♥s❢♦r♠ t❤❡ ✐t❡r❛t✐✈❡ s♠❛••✲ st❡♣ ✐♥t❡r♣r❡t❡r ✐♥t♦ ❛ ♠✉t✉❛••② r❡❝✉rs✐✈❡ ❜✐❣✲st❡♣ ✐♥t❡r♣r❡t❡r✱ ✇❤✐❝❤ r❡♣r❡s❡♥ts t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡✳ ❋✐rst✱ t❤❡ r❡❝♦♠♣♦s✐t✐♦♥✲❞❡❝♦♠♣♦s✐t✐♦♥ st❡♣ ✐s ❞❡❢♦r❡st❡❞ ✐♥t♦ ❛ r❡❢♦❝✉s✐♥❣ st❡♣✳ |❛t❤❡r t❤❛♥ t❛❦✐♥❣ t❤❡ ❝♦♥tr❛❝t❡❞ r❡❞❡① ❛♥❞ r❡❝♦♠♣♦s❡ ✐t ✐♥t♦ t❤❡ ❢✉•• ♣r♦❣r❛♠✱ ♦♥•② t♦ ✐♠♠❡❞✐❛t❡•② ❞❡❝♦♠♣♦s❡ t❤❛t ♣r♦❣r❛♠ ❛❣❛✐♥✱ t❤❡ s❡❛r❝❤ ❢♦r t❤❡ ♥❡①t r❡❞❡① st❛rts ❢r♦♠ t❤❡ ❝✉rr❡♥t s✉❜✲♣r♦❣r❛♠ ✐♥ ❢♦❝✉s ✈✐❛ r❡❢♦❝✉s✐♥❣✳ ◆❡①t✱ t❤❡ ✐t❡r❛t✐✈❡ ✐♥t❡r♣r❡t❡r ✐s ❢✉s❡❞ t♦ ❢♦r♠ ❛ ♠✉t✉❛••② r❡❝✉r✲ s✐✈❡✱ t❛✐•✲❝❛•• ✐♥t❡r♣r❡t❡r✳ ❚♦ ✜♥✐s❤ t❤❡ ♣r♦❝❡ss✱ ✇❡ ❝♦♠♣r❡ss ❝♦rr✐❞♦r tr❛♥s✐t✐♦♥s✱ ❡•✐♠✐♥❛t❡ ❞❡❛❞ ❝♦❞❡✱ ✢❛tt❡♥ ♣r♦❣r❛♠ st❛t❡s✱ ❛♥❞ ❝♦♥✈❡rt t❤❡ ♠❡t❛✲❝♦♥t❡①t ✐♥t♦ ❛ s❡q✉❡♥❝❡ ♦❢ ❢r❛♠❡s✳ ❚❤❡ r❡s✉•t✐♥❣ ❜✐❣✲st❡♣ ✐♥t❡r♣r❡t❡r ❞❡✜♥❡s t❤❡ ❛❜str❛❝t ♠❛✲ ❝❤✐♥❡ ❢♦r t❤❡ ❝❛•❝✉•✉s✳ ❆♣♣•②✐♥❣ t❤✐s t❡❝❤♥✐q✉❡ t♦ t❤❡ λ [lv ] ✲❝❛•❝✉•✉s r❡s✉•ts ✐♥ t❤❡ ❢♦••♦✇✐♥❣ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✭❛ st❛t❡ ♦❢ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐s ❛ ❝♦♠♠❛♥❞ ♣❛✐r❡❞ ✇✐t❤ ❛♥ ❡♥✈✐r♦♥♠❡♥t τ ✮ λx.t||u • E τ [lv] u||μx. t||E τ µα.c 1 ||μx.c 2 τ [lv] c 2 [x = µα.c 1 ]τ µα.c||E τ [lv] (c[E/α])τ V ||μx.c τ [lv] (c[V /x])τ V ||μ[x]. x||F τ ′ τ [lv] V ||F [V /x] (τ ′ [V /x])τ x||F τ ′ [x = µα.c]τ [lv] µα.c||μ[x]. x||F τ ′ τ ❙✐♥❝❡ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✇❛s ❞❡r✐✈❡❞ ❢r♦♠ t❤❡ st❛♥❞❛r❞✐③❛t✐♦♥ ♦❢ λ [lv ] t❤r♦✉❣❤ ❝♦rr❡❝t♥❡ss✲♣r❡s❡r✈✐♥❣ tr❛♥s❢♦r♠❛t✐♦♥s✱ t❤❡ t✇♦ ❝♦rr❡s♣♦♥❞ ❞✐r❡❝t•②✳ ❚❤❡♦r❡♠ ✷✳ •✐✈❡♥ ❛ λ [lv ] ❝♦♠♠❛♥❞ c✱ ✲ ■❢ c → [lv] c ′ t❤❡♥ ❢♦r ❛•• c 1 , τ ✇❤❡r❡ c = τ [c 1 ]✱ t❤❡r❡ ❡①✐sts c ′ 1 , τ ′ s✉❝❤ t❤❛t c 1 τ + [lv] c ′ 1 τ ′ ❛♥❞ τ ′ [c ′ 1 ] = c ′ ✳ ✲ ■❢ cτ [lv] c ′ τ ′ t❤❡♥ τ [c] → 0/1 [lv] τ ′ [c ′ ]✳ ❲❡ ❣❡♥❡r❛•✐③❡ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r λ [lv ] ✐♥t♦ ❛ ✈❛r✐❛♥t ♦❢ t❤❡ ♦r✐❣✐♥❛• ❝❛•✲ ❝✉•✉s✱ ✇❤✐❝❤ ✇❡ ❝❛•• λ [lv τ ] ✳ ❚❤❡ λ [lv τ ] ✲❝❛•❝✉•✉s ❝❛♥ ❡①♣r❡ss ❝❛••✲❜②✲♥❡❡❞ r❡❞✉❝t✐♦♥ ✇✐t❤♦✉t t❤❡ ✉s❡ ♦❢ ❛ ♠❡t❛✲❝♦♥t❡①t✳ ❊❛❝❤ ❝♦♠♠❛♥❞ ✐s ❝♦✉♣•❡❞ ✇✐t❤ ❛♥ ❡♥✈✐r♦♥✲ ♠❡♥t ♦❢ ✉♥❡✈❛•✉❛t❡❞ ❝♦♠♣✉t❛t✐♦♥s✱ ❜r✐♥❣✐♥❣ t❤❡ st❛♥❞❛r❞ r❡❞❡① ❜❛❝❦ t♦ t❤❡ t♦♣ ♦❢ t❤❡ ❝♦♠♠❛♥❞✳ ❚❤❡ s②♥t❛① ♦❢ λ [lv τ ] ❝♦♥t❛✐♥s t❤❡ ♥❡✇ s②♥t❛❝t✐❝ ❝❛t❡❣♦r② ♦❢ ❈•♦s✉r❡s ✭r❛♥❣❡❞ ♦✈❡r t❤❡ ♠❡t❛✲✈❛r✐❛❜•❡ l✮ ❛♥❞ ✐s ❞❡✜♥❡❞ ❛s✿ l ∈ Closure ::= cτ τ ∈ Environment ::= ǫ | | [x = µα.l]τ c ∈ Command ::= t||e e ∈ Context ::= E | | μx.l t ∈ T erm ::= V | | µα.l E ∈ CoV alue ::= α | | F | | μ[x]. x||F τ V ∈ V alue ::= x | | λx.t F ∈ F orcingContext ::= α | | t • E |❡❞✉❝t✐♦♥s ✐♥ λ [lv τ ] ❛r❡ ❣❡♥❡r❛•✐③❛t✐♦♥s ♦❢ t❤❡ st❡♣s ✐♥ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r λ [lv ] ✱ ✇✐t❤ t❤❡ ❛❜✐•✐t② t♦ ❛♣♣•② r❡❞✉❝t✐♦♥s ❛♥②✇❤❡r❡ ✐♥ ❛ ❝•♦s✉r❡✳ (β) λx.t||u • E τ → [lvτ ] u||μx. t||E ǫ τ (μ τ ) µα.l||μx.cτ ′ τ → [lvτ ] cτ ′ [x = µα.l]τ (µ l ) µα.l||E τ → [lvτ ] l[E/α]τ (μ v ) V ||μx.l τ → [lvτ ] l[V /x]τ (μ [v] ) V ||μ[x].l τ → [lvτ ] l[V /x]τ (μ [] ) x||F τ ′ [x = µα.l]τ → [lvτ ] µα.l||μ[x]. x||F τ ′ τ ◆♦t❡ t❤❛t lτ ✱ ❢♦r l = cτ ′ ✱ ✐s ❞❡✜♥❡❞ ❛s cτ 1 ✇❤❡r❡ τ 1 ✐s t❤❡ ❝♦♥❝❛t❡♥❛t✐♦♥ ♦❢ τ ′ ❛♥❞ τ ✳ Pr♦♣♦s✐t✐♦♥ ✶✳ λ [lv τ ] ✐s ❝♦♥✢✉❡♥t✳ ❲❡ tr✐✈✐❛••② ❤❛✈❡ ❛ ✇❡❛❦ ❤❡❛❞ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ❢♦r λ [lv τ ] ✐♥ ✇❤✐❝❤ ❝•♦s✉r❡s ❛r❡ r❡❞✉❝❡❞ ✐♥ t❤❡ ❡♠♣t② ♠❡t❛✲❝♦♥t❡①t✿ l → [lvτ ] l ′ ✐❢ l → [lvτ ] l ′ ✳ ❆ ✇❤♥❢ ❢♦r λ [lv τ ] ✐s ❡✐t❤❡r λx.t||α τ ♦r z||F τ ✇❤❡r❡ z ✐s ❢r❡❡ ✐♥ τ ✳ ❚❤❡ st❛♥❞❛r❞✐③❛t✐♦♥ ♦❢ λ [lv τ ] ♦♣❡r❛t❡s ✐♥ •♦❝❦✲st❡♣ ✇✐t❤ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r λ [lv ] ✱ ❛♥❞ s♦ ✐t ✐s ❛•s♦ ❝♦♠♣•❡t❡ ✇✐t❤ r❡s♣❡❝t t♦ r❡❞✉❝t✐♦♥✱ ✇❤❡r❡ ❝•♦s✉r❡s ❛♥❞ ❝♦♠♠❛♥❞s ❛r❡ r❡•❛t❡❞ ❜② cτ ≈ τ [c] ❛♥❞ ❡♥✈✐r♦♥♠❡♥ts ❛r❡ r❡•❛t❡❞ ✐❢ t❤❡② ❜✐♥❞ t❤❡ s❛♠❡ ✈❛r✐❛❜•❡s ✐♥ t❤❡ s❛♠❡ ♦r❞❡r t♦ r❡•❛t❡❞ t❡r♠s✳ ❚❤❡♦r❡♠ ✸✳ •✐✈❡♥ c 1 , τ 1 ❢r♦♠ λ [lv τ ] ❛♥❞ c 2 , τ 2 ❢r♦♠ λ [lv ] s✉❝❤ t❤❛t c 1 ≈ c 2 ❛♥❞ τ 1 ≈ τ 2 ✿ ✲ ■❢ c 1 τ 1 → [lvτ ] l 1 t❤❡♥ t❤❡r❡ ❡①✐sts l ′ 1 τ ′ 1 = l 1 ❛♥❞ c ′ 2 , τ ′ 2 s✉❝❤ t❤❛t c 2 τ 2 [lv] c ′ 2 τ ′ 2 ✱ l ′ 1 ≈ c ′ 2 ✱ ❛♥❞ τ ′ 1 ≈ τ ′ 2 ✳ ✲ ■❢ c 2 τ 2 [lv] c ′ 2 τ ′ 2 t❤❡♥ t❤❡r❡ ❡①✐sts l ′ 1 , τ ′ 1 s✉❝❤ t❤❛t c 1 τ 1 → [lvτ ] l ′ 1 τ ′ 1 ✱ l ′ 1 ≈ c ′ 2 ✱ ❛♥❞ τ ′ 1 ≈ τ ′ 2 ✳ |❡♠❛r❦ ✶✳ ❯s✐♥❣ ❛ s♣❡❝✐❛• s②♥t❛❝t✐❝ ❢♦r♠ t♦ r❡♠❡♠❜❡r t❤❛t ❛ ✈❛r✐❛❜•❡ ✐s ♥❡❡❞❡❞ ♠❛❦❡s t❤❡ ❝♦♥♥❡❝t✐♦♥ t♦ t❤❡ ✜♥❛• ❛❜str❛❝t ♠❛❝❤✐♥❡ ❛♥❞ ❝♦♥t✐♥✉❛t✐♦♥✲♣❛ss✐♥❣ st②•❡ tr❛♥s❢♦r♠❛t✐♦♥ ♠♦r❡ ❞✐r❡❝t✳ ❍♦✇❡✈❡r✱ ✐❢ ♦♥❡ ✐s ✐♥t❡r❡st❡❞ ✐♥ t❤❡ ♠✉•t✐❝✉t ♣❡r s❡ t❤❡♥ t❤❡ ❝❛•❝✉•✉s ❝❛♥ ❜❡ s✐♠♣•✐✜❡❞ ❜② ❛❜❛♥❞♦♥✐♥❣ t❤❡ s♣❡❝✐❛• s②♥t❛① ❢♦r ❢♦r❝❡❞ •❡ts ❛♥❞ ♣❡r❢♦r♠✐♥❣ ❛ ❝♦♥t❡①t s✇✐t❝❤ ✇❤❡♥ ❛ ❝♦✲✈❛r✐❛❜•❡ ❛♥❞ ❛ ❢♦r❝✐♥❣ ❝♦♥t❡①t F ✐s ❡♥❝♦✉♥t❡r❡❞✳ ❲❡ ❝❛•• t❤❡ r❡s✉•t✐♥❣ ❝❛•❝✉•✉s λ lv τ ✖ ✐ts r❡❞✉❝t✐♦♥ t❤❡♦r② ❝♦♥t❛✐♥s β✱ μv ✱ μτ ✱ ❛♥❞ µ l ✱ ❛•♦♥❣ ✇✐t❤ t❤❡ ❢♦••♦✇✐♥❣ r❡♣•❛❝❡♠❡♥t ❢♦r μ[] ✿ x||F τ ′ [x = µα.l]τ → lvτ l[μx. x||F τ ′ /α]τ ❍♦✇❡✈❡r✱ ❜② r❡♠♦✈✐♥❣ t❤❡ s♣❡❝✐❛• ❛♥♥♦t❛t✐♦♥ t❤❛t ❡①♣•✐❝✐t•② ♠❛r❦s •❡ts t❤❛t ❤❛✈❡ ❜❡❡♥ ❢♦r❝❡❞✱ t❤❡r❡ ✐s s♦♠❡ ❛♠❜✐❣✉✐t② ✐♥ ♣❛rs✐♥❣ t❤❡ •❛♥❣✉❛❣❡✳ ❲❡ ❝❛♥ ✐♥t❡r♣r❡t ❛ ❝♦♥t❡①t ♦❢ t❤❡ ❢♦r♠ μx. x||F τ ❛s ❡✐t❤❡r ❛ ❢♦r❝❡❞ •❡t✱ s✐♥❝❡ ✐ts ❝♦♠♠❛♥❞ ❢♦r❝❡s t❤❡ ❜♦✉♥❞ ✈❛r✐❛❜•❡✱ ♦r ✐♥st❡❛❞ ❛s s♦♠❡ ❣❡♥❡r❛• •❡t t❤❛t •✉st ❤❛♣♣❡♥s t♦ ❤❛✈❡ t❤❡ ❝♦♠♠❛♥❞ x||F ✐♥ ❢♦❝✉s✳ ❆•t❤♦✉❣❤ t❤❡ t✇♦ ❞✐✛❡r❡♥t r❡❛❞✐♥❣s •❡❛❞ t♦ t✇♦ ❞✐✛❡r❡♥t r❡❞✉❝t✐♦♥s✱ t❤❡② q✉✐❝❦•② ❝♦♥✈❡r❣❡✳ ❚❤❡ µ l ✲r❡❞✉❝t✐♦♥ ❛♣♣•✐❡s ✐❢ ✇❡ ✐♥t❡r♣❡t t❤❡ ❝♦♥t❡①t ❛s ❛ ❝♦✲✈❛•✉❡✳ ❖t❤❡r✇✐s❡✱ ✇❡ ❤❛✈❡ t❤❡ r❡❞✉❝t✐♦♥ s❡q✉❡♥❝❡ ♦❢ μτ ❢♦••♦✇❡❞ ❜② μ[] ✱ ✇❤✐❝❤ ❜r✐♥❣s ✉s t♦ t❤❡ s❛♠❡ ❝•♦s✉r❡✳ µα.l||μx. x||F τ ′ τ µ l → lvτ l[μx. x||F τ ′ /α]τ µα.l||μx. x||F τ ′ τ μτ → lvτ x||F τ ′ [x = µα.l]τ μ[] → lvτ l[μx. x||F τ ′ /α]τ ❚♦ ✐••✉str❛t❡ t❤❡ ✉s❡❢✉•♥❡ss ♦❢ ❛ ♠✉•t✐❝✉t ❝❛•❝✉•✉s ✭❡✐t❤❡r λ lv τ ♦r λ [lv τ ] ✮ ✇❡ s❤♦✇ t❤❛t ❊①❛♠♣•❡ ✷ t❡r♠✐♥❛t❡s ❛♥❞ ♣
α = μ[a]. a||fst • μ[f ]. f ||q • (I, I) • tp [q = µδ. a||snd • δ ] → → q||(I, I) • tp [q = µδ. (I, λx.µ . x||α )||snd • δ ] → → (I, I)||α where α = μ[a]. a||fst • μ[f ]. f ||q • (I, I) • tp [q = µδ. a||snd • δ ] → → q||(I, I) • tp [q = µδ. (I, I)||snd • δ ] → → (I, I)||tp ◆♦t✐❝❡ t❤❛t t❤❡ s❡❝♦♥❞ t✐♠❡ α ✐s r❡❞✉❝❡❞✱ q st❛rts ❢r❡s❤ ❢r♦♠ ✐ts ✐♥✐t✐❛• ✉♥❡✈❛•✲ ✉❛t❡❞ ❝♦♠♣✉t❛t✐♦♥ ❛♥❞ ❝❛♥ s❡❡ t❤❡ ❝❤❛♥❣❡ ✐♥ a✳ ✹ ❊♥✈✐r♦♥♠❡♥t✲❜❛s❡❞ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✭λ [lv τ * ] ✮ ■♥ ♦r❞❡r t♦ ❝♦♥str✉❝t ❛ ♠♦r❡ ❡✣❝✐❡♥t ❛❜str❛❝t ♠❛❝❤✐♥❡✱ ✇❡ ♥❡❡❞ t♦ ❛✈♦✐❞ ♣❡r✲ ❢♦r♠✐♥❣ t❤❡ ❝♦st•② s✉❜st✐t✉t✐♦♥ ♦♣❡r❛t✐♦♥✳ ❚♦ t❤✐s ❡♥❞✱ ✇❡ ♠♦❞✐❢② λ [lv τ ] s♦ t❤❛t ❛•• s✉❜st✐t✉t✐♦♥s ❛r❡ ✐♥st❡❛❞ st♦r❡❞ ✐♥ t❤❡ ❡♥✈✐r♦♥♠❡♥t τ ✱ ❣✐✈✐♥❣ λ [lv τ * ] ✿ τ ∈ Environment ::= ǫ | | [x = t]τ | | [α = E]τ ❚❤❡ ♠♦❞✐✜❡❞ r❡❞✉❝t✐♦♥s ❢♦r λ [lv τ * ] ❛r❡✿ (β) λx.t||u • E → [lvτ * ] u||μx. t||E ǫ (μ τ ) t||μx.cτ ′ τ → [lvτ * ] cτ ′ [x = t]τ (µ l ) µα.cτ ′ ||E τ → [lvτ * ] cτ ′ [α = E]τ (μ [v] ) V ||μ[x]. x||F τ ′ τ → [lvτ * ] V ||F τ ′ [x = V ]τ (μ [] ) x||F τ ′ [x = t]τ → [lvτ * ] t||μ[x]. x||F τ ′ τ (τ α ) V ||α τ ′ [α = E]τ → [lvτ * ] V ||E τ ′ [α = E]τ ❚❤❡ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ♦❢ λ [lv τ * ] ✐s ♣❡r❢♦r♠❡❞ ✐♥ t❤❡ ❡♠♣t② ♠❡t❛✲❝♦♥t❡①t✱ ❛s ✐♥ λ [lv τ ] ✳ ❈•♦s✉r❡s ✐♥ λ [lv τ * ] r❡•❛t❡ t♦ ❝•♦s✉r❡s ✐♥ λ [lv τ ] ❜② ♣❡r❢♦r♠✐♥❣ s✉❜st✐t✉t✐♦♥ ♦♥ ✈❛•✉❡s ❛♥❞ ❝♦✲✈❛•✉❡s st♦r❡❞ ✐♥ t❤❡ ❡♥✈✐r♦♥♠❡♥t✳ l[α = E] ≈ l[E/α] l[x = V ] ≈ l[V /x] l[x = µα.c] ≈ l[x = µα.c] ❚❤❡♦r❡♠ ✹✳ •✐✈❡♥ ❛ λ [lv τ * ] ❝•♦s✉r❡ l 1 ❛♥❞ ❛ λ [lv τ ] ❝•♦s✉r❡ l 2 s✉❝❤ t❤❛t l 1 ≈ l 2 ✿ ✲ ■❢ l 2 → [lvτ ] l ′ 2 t❤❡♥ l 1 → → + [lvτ * ] l ′ 1 ✳ ✲ ■❢ l 1 → [lvτ * ] l ′ 1 t❤❡♥ t❤❡r❡ ❡①✐sts l ′′ 1 , l ′ 2 s✉❝❤ t❤❛t l 2 → 0/1 [lvτ ] l ′ 2 ❛♥❞ l ′ 1 → 0/1 [lvτ * ] l ′′ 1 ❛♥❞ l ′′ 1 ≈ l ′ 2 ✳ ❚❤❡ st❛♥❞❛r❞✐③❛t✐♦♥ ♦❢ λ [lv τ * ] ❣✐✈❡s r✐s❡ t♦ t❤❡ ❢♦••♦✇✐♥❣ ❛❜str❛❝t ♠❛❝❤✐♥❡✳ t||μx.c τ [lv * ] c[x = t]τ µα.c||E τ [lv * ] c[α = E]τ V ||α τ ′ [α = E]τ [lv * ] V ||E τ ′ [α = E]τ V ||μ[x]. x||F τ ′ τ [lv * ] V ||F τ ′ [x = V ]τ x||F τ ′ [x = t]τ [lv * ] t||μ[x]. x||F τ ′ τ λx.t||u • E τ [lv * ] u||μx. t||E τ ❚❤❡♦r❡♠ ✺✳ •✐✈❡♥ c 1 , τ 1 ❢r♦♠ λ [lv τ * ] ❛♥❞ c 2 , τ 2 ❢r♦♠ λ [lv τ ] s✉❝❤ t❤❛t c 1 ≈ c 2 ❛♥❞ τ 1 ≈ τ 2 ✿ ✲ ■❢ c 1 τ 1 → [lvτ * ] l 1 t❤❡♥ t❤❡r❡ ❡①✐sts l ′ 1 τ ′ 1 = l 1 ❛♥❞ c ′ 2 , τ ′ 2 s✉❝❤ t❤❛t c 2 τ 2 [lv * ] c ′ 2 τ ′ 2 ✱ l ′ 1 ≈ c ′ 2 ✱ ❛♥❞ τ ′ 1 ≈ τ ′ 2 ✳ ✲ ■❢ c 2 τ 2 [lv * ] c ′ 2 τ ′ 2 t❤❡♥ t❤❡r❡ ❡①✐sts l ′ 1 , τ ′ 1 s✉❝❤ t❤❛t c 1 τ 1 → [lvτ * ] l ′ 1 τ ′ 1 ✱ l ′ 1 ≈ c ′ 2 ✱ ❛♥❞ τ ′ 1 ≈ τ ′ 2 ✳ ❯♥•✐❦❡ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r λ [lv ] ✱ t❤❡ ❛❜♦✈❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐s ❝♦♥t❡①t✲ ❢r❡❡✱ s✐♥❝❡ ❛t ❡❛❝❤ st❡♣ ❛ ❞❡❝✐s✐♦♥ ❝❛♥ ❜❡ ♠❛❞❡ ❜② ❡①❛♠✐♥✐♥❣ ❡✐t❤❡r t❤❡ t❡r♠ ♦r t❤❡ ❝♦♥t❡①t ✐♥ ✐s♦•❛t✐♦♥✳ ❚♦ ♠❛❦❡ t❤✐s str✉❝t✉r❡ ♠♦r❡ ❛♣♣❛r❡♥t✱ ✇❡ ❞✐✈✐❞❡ t❤❡ ♠❛❝❤✐♥❡ ✐♥t♦ ❛ ♥✉♠❜❡r ♦❢ ❝♦♥t❡①t✲❢r❡❡ ♣❤❛s❡s ✐♥ ❋✐❣✉r❡ ✶✳ ❊❛❝❤ ♣❤❛s❡ ♦♥•② ❛♥❛•②③❡s ♦♥❡ ❝♦♠♣♦♥❡♥t ♦❢ t❤❡ ❝♦♠♠❛♥❞✱ t❤❡ ✏❛❝t✐✈❡✑ t❡r♠ ♦r ❝♦♥t❡①t✱ ❛♥❞ ✐s ♣❛r❛♠❡tr✐❝ ✐♥ t❤❡ ♦t❤❡r ✏♣❛ss✐✈❡✑ ❝♦♠♣♦♥❡♥t✳ ■♥ ❡ss❡♥❝❡✱ ❢♦r ❡❛❝❤ ♣❤❛s❡ ♦❢ t❤❡ ♠❛❝❤✐♥❡✱ ❡✐t❤❡r t❤❡ t❡r♠ ♦r t❤❡ ❝♦♥t❡①t ✐s ❢✉••② ✐♥ ❝♦♥tr♦• ❛♥❞ ✐♥❞❡♣❡♥❞❡♥t✱ r❡❣❛r❞•❡ss ♦❢ ✇❤❛t t❤❡ ♦t❤❡r ❤❛•❢ ❤❛♣♣❡♥s t♦ ❜❡✳ c [lv * ] ceǫ t||μx.c eτ [lv * ] ce[x = t]τ t||E eτ [lv * ] t||E tτ µα.c||E tτ [lv * ] ce[α = E]τ V ||E tτ [lv * ] V ||E E τ V ||α E τ ′ [α = E]τ [lv * ] V ||E E τ ′ [α = E]τ V ||μ[x]. x||F τ ′ E τ [lv * ] V ||F V τ ′ [x = V ]τ V ||F E τ [lv * ] V ||F V τ x||F V τ ′ [x = t]τ [lv * ] t||μ[x]. x||F τ ′ tτ λx.t||F V τ [lv * ] λx.t||F F τ λx.t||u • E F τ [lv * ] u||μx. t||E eτ ❋✐❣✳ ✶✳ ❆❜str❛❝t ♠❛❝❤✐♥❡ ❢♦r t❤❡ ❝•❛ss✐❝❛• ❝❛••✲❜②✲♥❡❡❞ s❡q✉❡♥t ❝❛•❝✉•✉s λ [lv τ * ] ✳ ✺ ❊♥✈✐r♦♥♠❡♥t✲❜❛s❡❞ ❈P❙ ✭λ [lv τ * ] ✮ ❍❛✈✐♥❣ ❛♥ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐♥ ❝♦♥t❡①t✲❢r❡❡ ❢♦r♠ ✐s ❣♦♦❞ ❢♦r ♠♦r❡ t❤❛♥ •✉st ❛❡s✲ t❤❡t✐❝ r❡❛s♦♥s✳ ❍❛✈✐♥❣ ❜♦t❤ t❤❡ t❡r♠ ❛♥❞ ❝♦♥t❡①t ❜❡❤❛✈❡ ✐♥❞❡♣❡♥❞❡♥t•② ♦❢ ❡❛❝❤ ♦t❤❡r ♠❛❦❡s t❤❡ ♠❛❝❤✐♥❡ ❛♠❡♥❞❛❜•❡ t♦ ❝♦♥✈❡rs✐♦♥ ✐♥t♦ ❛ ♥✐❝❡ ❈P❙ tr❛♥s❢♦r♠✳ ❙✐♥❝❡ ❛ ❈P❙ tr❛♥s❢♦r♠ ✐s ❛ ❝♦♠♣✐•❛t✐♦♥ ❢r♦♠ t❤❡ s♦✉r❝❡ •❛♥❣✉❛❣❡ ✐♥t♦ t❤❡ λ✲ ❝❛•❝✉•✉s✱ ❡❛❝❤ ❡①♣r❡ss✐♦♥ ♠✉st ❤❛✈❡ ♠❡❛♥✐♥❣ ✐♥❞❡♣❡♥❞❡♥t ♦❢ ✐ts s✉rr♦✉♥❞✐♥❣s✳ ❉✉r✐♥❣ tr❛♥s•❛t✐♦♥✱ ❛♥ ❡①♣r❡ss✐♦♥ ♠❛② t❛❦❡ ❛ ❝♦♥t✐♥✉❛t✐♦♥ ❛s ❛ ♣❛r❛♠❡t❡r✱ ❜✉t ✐t ❝❛♥♥♦t ❞✐r❡❝t•② ❡①❛♠✐♥❡ ✐t ✖ t❤❡ ❝♦♥t✐♥✉❛t✐♦♥ ✐s ❛ ❜•❛❝❦ ❜♦① t❤❛t ❝❛♥ ♦♥•② ❜❡ ❡♥t❡r❡❞ ❜② ②✐❡•❞✐♥❣ ❛•• ❝♦♥tr♦• t♦ ✐t✳ ❚❤❡ ♣❛r❛♠❡tr✐❝ ♥❛t✉r❡ ♦❢ t❤❡ st❡♣s ✐♥ ❋✐❣✉r❡ ✶✱ ❛♥❞ t❤❡ ❢❛❝t t❤❛t ❡❛❝❤ s②♥t❛❝t✐❝ ❢♦r♠ ✐s ❛♥❛•②③❡❞ ❡①❛❝t•② ♦♥❝❡ ✐♥ t❤❡ ♠❛❝❤✐♥❡✱ ♠❡❛♥s t❤❛t ✇❡ ❝❛♥ ❞✐r❡❝t•② ❞❡r✐✈❡ ❛ ❈P❙ tr❛♥s❢♦r♠ t❤❛t ❝♦rr❡s♣♦♥❞s ❡①❛❝t•② ✇✐t❤ t❤❡ ♠❛❝❤✐♥❡✳ ❉❡r✐✈✐♥❣ ❛ ❈P❙ tr❛♥s•❛t✐♦♥ ❢r♦♠ ❛ ❝♦♥t❡①t✲❢r❡❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐s ♠♦r❡ str❛✐❣❤t❢♦r✇❛r❞ t❤❛♥ ❞❡r✐✈✐♥❣ ❛ ♠❛❝❤✐♥❡ ❢r♦♠ ❛ ❝❛•❝✉•✉s✳ ❙t❛rt✐♥❣ ❢r♦♠ t❤❡ ❜✐❣✲ st❡♣ ✐♥t❡r♣r❡t❡r✱ ✐♥ ❡❛❝❤ ♣❤❛s❡✱ t❤❡ ❝❛s❡ ❛♥❛•②s✐s ✐s •✐❢t❡❞ ♦✉t s♦ t❤❛t t❤❡ ✐♥✲ t❡r♣r❡t❡r ❜❡❝♦♠❡s ❛ s❡t ♦❢ ♦♥❡✲❛r❣✉♠❡♥t ❢✉♥❝t✐♦♥s ♦♥ t❤❡ ❛❝t✐✈❡ ❡①♣r❡ss✐♦♥ t❤❛t ♣r♦❞✉❝❡ ❛ ❢✉♥❝t✐♦♥ ❛❝❝❡♣t✐♥❣ t❤❡ ♣❛ss✐✈❡ ❡①♣r❡ss✐♦♥ ❛s ❛♥ ❡①tr❛ ♣❛r❛♠❡t❡r✳ ❚❤❡♥✱ t❤❡ s②♥t❛① ✐s r❡❢✉♥❝t✐♦♥❛•✐③❡❞✿ r❛t❤❡r t❤❛♥ ♣❛ss t❤❡ s②♥t❛❝t✐❝ ❢♦r♠s ❛s✲✐s t♦ ❢✉✲ t✉r❡ st❛❣❡s ♦❢ t❤❡ ✐♥t❡r♣r❡t❡r✱ ❡❛❝❤ s②♥t❛❝t✐❝ ❢♦r♠ ✐s ✐♠♠❡❞✐❛t❡•② ❣✐✈❡♥ t♦ t❤❡ ✐♥t❡r♣r❡t❡r ❛s t❤❡② ❜❡❝♦♠❡ ❛✈❛✐•❛❜•❡✳ ❚❤❡ ♣❛rt✐❛• ❡✈❛•✉❛t✐♦♥ ♦❢ t❤❡ ✐♥t❡r♣r❡t❡r ✇✐t❤ ♦♥•② t❤❡ ❛❝t✐✈❡ ❛r❣✉♠❡♥t ❜❡❝♦♠❡s ❛ ❝♦♥t✐♥✉❛t✐♦♥ ✇❛✐t✐♥❣ ❢♦r t❤❡ ♣❛ss✐✈❡ t||e c = e e t t μx.c e t = λτ. c c ([x = t]τ ) E e t = t E E µα.c t E = c c[E/α] V t E = E V V α E V = α V μ[x]. x||F τ ′ E V = λτ. τ ′ τ V F F ([x = (λE.E V )]τ ) F E V = V F F x V F = λτ.τ (x) F λx.t V F = F (λu.λE.λτ. t t E ([x = u]τ )) α F v = α v u • E F v = v u t E E ǫ τ V F = λτ.V F τ τ ′ [x = t] τ V F = λτ. τ ′ τ V F ([x = t t]τ ) τ ′ [α = E] τ V F = λτ.( τ ′ τ V F ) [ E E /α]τ (τ ′ [x = t]τ )(x) = λF.t (λV.λτ.V F (τ ′ [x = λE.E V ]τ )) τ ❋✐❣✳ ✷✳ ❈♦♥t✐♥✉❛t✐♦♥ ❛♥❞ ❡♥✈✐r♦♥♠❡♥t ♣❛ss✐♥❣ st②•❡ tr❛♥s❢♦r♠ ❢♦r λ [lv τ * ] ✳ ❝♦✉♥t❡r♣❛rt✳ ❋✐♥❛••②✱ s✐♥❝❡ ❝♦✲✈❛r✐❛❜•❡s ✐♥ t❤❡ ❡♥✈✐r♦♥♠❡♥t ❛r❡ tr❡❛t❡❞ ❛s ♦r❞✐✲ ♥❛r② st❛t✐❝ ❜✐♥❞✐♥❣s✱ ✇❡ ❝♦♥✈❡rt ❝♦♥t❡①t ❜✐♥❞✐♥❣s ❜❛❝❦ t♦ ✐♠♣•✐❝✐t s✉❜st✐t✉t✐♦♥✳ ❲✐t❤ ❛•• s②♥t❛❝t✐❝ ❢♦r♠s ✐♥t❡r♣r❡t❡❞ ♦♥✲s✐t❡✱ t❤❡ r❡s✉•t✐♥❣ ✐♥t❡r♣r❡t❡r ✐s ❛ ❈P❙ tr❛♥s❢♦r♠❛t✐♦♥ ❢r♦♠ t❤❡ ❝❛•❝✉•✉s ✐♥t♦ t❤❡ ❤♦st •❛♥❣✉❛❣❡✳ ❋r♦♠ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐♥ ❋✐❣✉r❡ ✶✱ ✇❡ ❞❡r✐✈❡ ❛♥ ❡♥✈✐r♦♥♠❡♥t✲❜❛s❡❞ ❈P❙ tr❛♥s❢♦r♠❛t✐♦♥ ❢♦r λ [lv τ * ] ✱ ❣✐✈❡♥ ✐♥ ❋✐❣✉r❡ ✷✳ ❚❤❡ ❝♦♥❝r❡t❡ r❡♣r❡s❡♥t❛t✐♦♥ ♦❢ ❡♥✈✐✲ r♦♥♠❡♥ts ✉s❡❞ ✐♥ t❤❡ tr❛♥s❢♦r♠ ✐s •❡❢t ❛❜str❛❝t ✖ ✇❡ ❛ss✉♠❡ t❤❛t ❡♥✈✐r♦♥♠❡♥ts ❝❛♥ ❜❡ ❡①t❡♥❞❡❞✱ •♦✐♥❡❞✱ ❛♥❞ s♣•✐t ♦♥ ❛ ✈❛r✐❛❜•❡✳ ❚❤❡ t❤r❡❡✲✇❛② s♣•✐t ✐s t❤❡ s❛♠❡ ♦♥❡ t❤❛t ❛♣♣❡❛rs ✐♥ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡✿ ❢♦r ❛ ❣✐✈❡♥ ✈❛r✐❛❜•❡ x✱ t❤❡ ❡♥✈✐r♦♥♠❡♥t ✐s ♣❛rt✐t✐♦♥❡❞ ✐♥t♦ ❛•• ❜✐♥❞✐♥❣s ❜❡❢♦r❡ t❤❡ ✜rst ♦❝❝✉rr❡♥❝❡ ♦❢ x✱ t❤❡ ❜✐♥❞✐♥❣ ♦❢ x ✐ts❡•❢✱ ❛♥❞ ❛•• r❡♠❛✐♥✐♥❣ ❜✐♥❞✐♥❣s✳ x k = x k λx.t k = k (λx. t ) t1 t2 k = t1 (λf. let r = delay t2 in f (λk.!r k) k) µα.J k = J [k/α] [α]t = t α delay t = new r in r := (λk. forcer t k); r forcer t k = t (λv.r := (λk ′ .k ′ v); k v) ❋✐❣✳ ✸✳ ❖❦❛s❛❦✐ ❡t ❛•✳✬s ❈P❙ tr❛♥s❢♦r♠❛t✐♦♥ ❡①t❡♥❞❡❞ ✇✐t❤ ❝♦♥tr♦•✳ ❙✐♥❝❡ t❤❡ ❈P❙ tr❛♥s❢♦r♠ ✐♥ ❋✐❣✉r❡ ✷ ✇❛s ❞❡r✐✈❡❞ ❢r♦♠ t❤❡ ❛❜str❛❝t ♠❛❝❤✐♥❡ ✐♥ ❋✐❣✉r❡ ✶ ❜② ❝♦rr❡❝t♥❡ss✲♣r❡s❡r✈✐♥❣ tr❛♥s❢♦r♠❛t✐♦♥s✱ t❤❡ t✇♦ ❝♦rr❡s♣♦♥❞ ❞✐r❡❝t•②✳ ❚❤❡♦r❡♠ ✻✳ ■❢ cτ [lv * ] c ′ τ ′ t❤❡♥ c τ = βη c ′ τ ′ ✳ ❙t♦r❡✲❜❛s❡❞ ❈P❙ ❆♥♦t❤❡r ❛♣♣r♦❛❝❤ t♦ ❞❡r✐✈✐♥❣ ❛ ❈P❙ ❢♦r ❛ ❝•❛ss✐❝❛• ❝❛••✲ ❜②✲♥❡❡❞ ❝❛•❝✉•✉s ✐s t♦ ❡①t❡♥❞ t❤❡ ❈P❙ ❣✐✈❡♥ ❜② ❖❦❛s❛❦✐ ❡t ❛•✳ ❬✽( ✇✐t❤ ❝♦♥tr♦• ♦♣❡r❛t♦rs✳ ❲❡ ❞♦ s♦ ❜② ❛❞❞✐♥❣ t❤❡ ♦♣❡r❛t♦rs µ ❛♥❞ ✏❜r❛❝❦❡t✑ ❢r♦♠ P❛r✐❣♦t✬s λµ✲ ❝❛•❝✉•✉s ❬✾( ❢♦r r❡s♣❡❝t✐✈❡•② ❝❛♣t✉r✐♥❣ ❛♥❞ r❡✲✐♥st❛••✐♥❣ ❛♥ ❡✈❛•✉❛t✐♦♥ ❝♦♥t❡①t✳

  r♦❞✉❝❡s (I, I) ❛s ❛ r❡s✉•t✱ ✇❤❡r❡ t❤❡ r❡❞✉❝t✐♦♥s ❞♦ ♥♦t ♥❡❡❞ ❛♥ ✉♥❜♦✉♥❞❡❞ s❡❛r❝❤ ❢♦r t❤❡ st❛♥❞❛r❞ r❡❞❡①✳ µα. (I, λx.µ . x||α )||α ||μa. µβ. a||fst • β ||μf. µδ. a||snd • δ ||μq. f ||q • (I, I) • tp → → f ||q • (I, I) • tp [q = µδ. a||snd • δ ][f = µβ. a||fst • β ][a = µα. (I, λx.µ . x||α )||α ] → → (I, λx.µ . x||α )||α where

  ❚❤✐s ❡①t❡♥s✐♦♥ ❝♦rr❡s♣♦♥❞s t♦ ❛♣♣•②✐♥❣ ❛ st♦r❡ ♣❛ss✐♥❣ tr❛♥s❢♦r♠❛t✐♦♥ t♦ t❤❡ tr❛♥s❢♦r♠❛t✐♦♥ ❣✐✈❡♥ ✐♥ ❋✐❣✉r❡ ✸✳ ❚❤❡ ♥❛t✉r❛• ❡①t❡♥s✐♦♥ ♦❢ t❤❡ ❞❡•❛② ❛♥❞ ❢♦r❝❡ ❈P❙ r❡s✉•ts ✐♥ ❛ ❞✐✛❡r❡♥t s❡♠❛♥t✐❝s t❤❛♥ t❤❡ ♦♥❡ ✐♥ ❋✐❣✉r❡ ✷✳ ■♥ ♣❛rt✐❝✉•❛r✱ ❣♦✐♥❣ ❜❛❝❦ t♦ ❊①❛♠♣•❡ ✷ ❛♥❞ ✉s✐♥❣ t❤❡ st♦r❡✲❜❛s❡❞ s❡♠❛♥t✐❝s ✐♥ ❋✐❣✉r❡ ✸✱ ✇❡ ❣❡t t❤❡ ❢♦••♦✇✐♥❣ r❡❞✉❝t✐♦♥ ✭✇❤❡r❡ ❛ ♣r♦❣r❛♠ ✐s ❛ t❡r♠ t ❛♥❞ ❛ st♦r❡ s ✇r✐tt❡♥ t || s✮✿ let a = µα.[α](I, λx.µ .[α]x) in let f = fst p in let q = snd p in f q (I, I) || ǫ → → f q (I, I) || [q = forceq snd p][f = forcep fst p][a = forcea µα.[α](I, λx.µ .[α]x)] → → (force f fst(forcea µα.[α](I, λx.µ .[α]x))) q (I, I) ||[q = forceq snd p][f = force f fst p][a = forcea µα.[α](I, λx.µ .[α]x)]→ → (force f fst(forcea(I, λx.µ .(force f fst(forcea x)) q (I, I)))) q (I, I)||[q = forceq snd p][f = force f fst p][a = forcea µα.[α](I, λx.µ .[α]x)] → → q (I, I) || [q = forceq snd p][f = I][a = (I, λx.µ .(force f fst(forcea x)) q (I, I))] → → (λx.µ .(force f fst(forcea x)) q (I, I)) (I, I) ||[q = λx.(force f fst(forcea x)) q (I, I)][f = I][a = (I, λx.µ .(force f fst(forcea x)) q (I, I))] → → q (I, I) || [q = λx.µ .(force f fst(forcea x)) q (I, I)][f = I][a = (I, I)] → → . . . ❲❡ s❛✇ t❤❛t ✉s✐♥❣ t❤❡ ♠✉•t✐❝✉t ❝❛•❝✉•✉s λ [lv τ ] ✱ t❤❡ ♣r♦❣r❛♠ ♣r♦❞✉❝❡s ✭ ■ ✱ ■ ✮ ❛s ❛ r❡s✉•t ✖ ❡✈❡r② t✐♠❡ t❤❡ ❝♦♥t✐♥✉❛t✐♦♥ ❦ ✐s ✐♥✈♦❦❡❞✱ ❜♦t❤ ❢ ❛♥❞ q ❛r❡ r❡✈❡rt❡❞ t♦ t❤❡✐r ✉♥❡✈❛•✉❛t❡❞ st❛t❡s✳ ❍♦✇❡✈❡r✱ ✇✐t❤ t❤❡ s❡♠❛♥t✐❝s ✐♥ ❋✐❣✉r❡ ✸✱ t❤❡ ❝♦♥t✐♥✉✲ ❛t✐♦♥ ❜♦✉♥❞ t♦ ❦ ❝❛♣t✉r❡s ♦♥•② t❤❡ ❢♦r❝✐♥❣ ♦❢ ❢ ❛♥❞ ❛✳ ❙✐♥❝❡ q ✇❛s ♥♦t ✐♥✈♦•✈❡❞

  µα. µα.t||μx. x||α ||μz. z||δ → lv µα.t||μx. x||μz. z||δ ✱ t❤❡♥ ✐t ✐s ♥

(μ [] ) µα.c||μx.C[ x||F ] → [lv] µα.c||μ[x]. x||F C (μ [v] ) V ||μ[x]. x||F τ → [lv] (τ [ V ||F ])[V /x]