{'fraction_non_alphanumeric': 0.061769396204883614, 'fraction_numerical': 0.010680165615718863, 'mean_word_length': 3.6561307901907356, 'pattern_counts': {'":': 3, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 53, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq

This paper shows equivalence of several versions of applicative similarity and contextual approximation, and hence also of applicative bisimilarity and contextual equivalence, in LR, the deterministic call-by-need lambda calculus with letrec extended by data constructors, case-expressions and Haskell's seq-operator. LR models an untyped version of the core language of Haskell. The use of bisimilarities simplifies equivalence proofs in calculi and opens a way for more convenient correctness proofs for program transformations. The proof is by a fully abstract and surjective transfer into a call-by-name calculus, which is an extension of Abramsky's lazy lambda calculus. In the latter calculus equivalence of our similarities and contextual approximation can be shown by Howe's method. Similarity is transferred back to LR on the basis of an inductively defined similarity. The translation from the call-by-need letrec calculus into the extended call-by-name lambda calculus is the composition of two translations. The first translation replaces the call-by-need strategy by a call-by-name strategy and its correctness is shown by exploiting infinite trees which emerge by unfolding the letrec expressions. The second translation encodes letrec-expressions by using multi-fixpoint combinators and its correctness is shown syntactically by comparing reductions of both calculi. A further result of this paper is an isomorphism between the mentioned calculi, which is also an identity on letrec-free expressions.

top operator. This does not apply to calculi with letrec, since letrec-expressions may be values as well as non-values. (iii) Call-by-need calculi with letrec usually require reduction rules to shift and join letrec-bindings. These modifications of the syntactic structure of expressions do not fit well into the proof structure of Howe's method.
Nevertheless, Howe's method is also applicable to calculi with non-recursive let even in the presence of nondeterminism [MSS10], where for the nondeterministic case applicative bisimilarity is only sound (but not complete) w.r.t. contextual equivalence. However, in the case of (cyclic) letrec and nondeterminism applicative bisimilarity is unsound w.r.t. contextual equivalence [SSSM11]. This raises a question: which call-by-need calculi with letrec permit applicative bisimilarity as a tool for proving contextual equality?
Our Contribution. In [SSSM10] we have already shown that for the minimal extension of Abramsky's lazy lambda calculus with letrec which implements sharing and explicit recursion, the equivalence of contextual equivalence and applicative bisimilarity indeed holds. However, the full (untyped) core language of Haskell has data constructors, case-expressions and the seq-operator for strict evaluation. Moreover, in [SSMS13] it is shown that the extension of Abramsky's lazy lambda calculus with case, constructors, and seq is not conservative, i.e. it does not preserve contextual equivalence of expressions. Thus our results obtained in [SSSM10] for the lazy lambda calculus extended by letrec only are not transferable to the language extended by case, constructors, and seq. For this reason we provide a new proof for the untyped core language of Haskell.
As a model of Haskell's core language we use the call-by-need lambda calculus L LR which was introduced and motivated in [SSSS08]. The calculus L LR extends the lazy lambda calculus with letrec-expressions, data constructors, case-expressions for deconstructing the data, and Haskell's seq-operator for strict evaluation.
We define the operational semantics of L LR in terms of a small-step reduction, which we call normal order reduction. As it is usual for lazy functional programming languages, evaluation of L LR -expressions successfully halts if a weak head normal form is obtained, i.e. normal order reduction does not reduce inside the body of abstractions nor inside the arguments of constructor applications. The L LR calculus has been studied in detail in [SSSS08] and correctness of several important program transformations has been established for it.
Our main result in this paper is that several variants of applicative bisimilarities are sound and complete for contextual equivalence in L LR , i.e. coincide with contextual equivalence. Like context lemmas, an applicative bisimilarity can be used as a proof tool for showing contextual equivalence of expressions and for proving correctness of program transformations in the calculus L LR . Since we have completeness of our applicative bisimilarities in addition to soundness, our results can also be used to disprove contextual equivalence of expressions in L LR . Additionally, our result shows that the untyped applicative bisimilarity is sound for a polymorphic variant of L LR , and hence for the typed core language of Haskell.
Having the proof tool of applicative bisimilarity in L LR is also very helpful for more complex calculi if their pure core can be conservatively embedded in the full calculus. An example is our work on Concurrent Haskell [SSS11,SSS12], where our calculus CHF that models Concurrent Haskell has top-level processes with embedded lazy functional evaluation. We have shown in the calculus CHF that Haskell's deterministic core language can be conservatively embedded in the calculus CHF. Figure 1: Overall structure. Solid lines are fully-abstract translations, which are also isomorphisms and identities on letrec-free expressions; dotted lines are convergence preservation to/from the system L tree of infinite trees.
We prove the equivalence between the applicative similarities and contextual equivalence in L LR , by lifting the equivalence from a letrec-free call-by-name calculus L lcc . The calculus L lcc minimally extends Abramsky's lazy calculus by Haskell's primitives. As shown in [SSMS13], data constructors and seq are explicitly needed in L lcc . The structure of the proof, with its intermediate steps, is shown in Figure 1. We prove the equivalence between the applicative similarities and contextual equivalence in L lcc , by extending Howe's method. We bridge L LR and L lcc in two steps, using intermediate calculi L name and L tree . L name is the call-by-name variant of L LR , and L lcc is obtained from L name by encoding letrec using multi-fixpoint combinators. The calculi L LR and L name are related to each other via their infinite unfoldings, thus we introduce a calculus L tree of infinite trees (similar infinitary rewriting, see [KKSdV97,SS07]). Convergence of expressions in L LR and L name is shown to be equivalent to their translation as an infinite tree in the calculus L tree (dotted lines in the picture). We establish full abstractness of translation N and W between calculi L LR , L name , and L lcc with respect to contextual equivalence. Correctness of similarity is transferred back from L lcc to L LR on the basis of an inductively defined similarity (for more details see Fig. 7.2).
A consequence of our result is that the three calculi L LR , L name , and L lcc are isomorphic, modulo the equivalence (see Corollaries 6.17 and 5.33), and also that the embedding of the calculus L lcc into the call-by-need calculus L LR is an isomorphism of the respective term models.

Common Notions and Notations for Calculi
Before we explain the specific calculi, some common notions are introduced. A calculus definition consists of its syntax together with its operational semantics which defines the evaluation of programs and the implied equivalence of expressions: Definition 2.1. An untyped deterministic calculus D is a four-tuple (E, C, →, A), where E are expressions (up to α-equivalence), C : E → E is a set of functions (which usually represents contexts), → is a small-step reduction relation (usually the normal-order reduction), which is a partial function on expressions (i.e., deterministic), and A ⊂ E is a set of answers of the calculus.
For C ∈ C and an expression s, the functional application is denoted as C[s]. For contexts, this is the replacement of the hole of C by s. We also assume that the identity function Id is contained in C with Id [s] = s for all expressions s, and that C is closed under composition, i.e. C 1 , C 2 ∈ C =⇒ C 1 • C 2 ∈ C.
The transitive closure of → is denoted as + − → and the transitive and reflexive closure of → is denoted as * − →. The notation 0∨1 − − → means equality or one reduction, and k − → means k reductions. Given an expression s, a sequence s → s 1 → . . . → s n is called a reduction sequence; it is called an evaluation if s n is an answer, i.e. s n ∈ A; in this case we say s converges and denote this as s↓ D s n or as s↓ D if s n is not important. If there is no s n s.t. s↓ D s n then s diverges, denoted as s⇑ D . When dealing with multiple calculi, we often use the calculus name to mark its expressions and relations, e.g. D − → denotes a reduction relation in D.
We will have to deal with several calculi and preorders. Throughout this paper we will use the symbol for co-inductively defined preorders (i.e. similarities), and ≤ for (inductively defined or otherwise defined) contextual preorders. For the corresponding symmetrizations we use ≃ for ∩ and ∼ for ≤ ∩ ≥. All the symbols are always indexed by the corresponding calculus and sometimes more restrictions like specific sets of contexts are attached to the indices of the symbols.
Contextual approximation and equivalence can be defined in a general way: Definition 2.2 (Contextual Approximation and Equivalence, ≤ D and ∼ D ). Let D = (E, C, →, A) be a calculus and s 1 , s 2 be D-expressions. Contextual approximation (or contextual preorder) ≤ D and contextual equivalence ∼ D are defined as: A program transformation is a binary relation η ⊆ (E × E). A program transformation η is called correct iff η ⊆ ∼ D .
Note that ≤ D is a precongruence, i.e., ≤ D is reflexive, transitive, and s ≤ D t implies C[s] ≤ D C[t] for all C ∈ C, and that ∼ D is a congruence, i.e. a precongruence and an equivalence relation.
We also define a general notion of similarity coinductively for untyped deterministic calculi. We first define the operator F D,Q on binary relations of expressions: Definition 2.3. Let D = (E, C, →, A) be an untyped deterministic calculus and let Q ⊆ C be a set of functions on expressions (i.e. ∀Q ∈ Q : Q : E → E). Then the Q-experiment operator F D,Q : 2 (E×E) → 2 (E×E) is defined as follows for η ⊆ E × E: Lemma 2.4. The operator F D,Q is monotonous w.r.t. set inclusion, i.e. for all binary relations η 1 , η 2 on expressions η 1 ⊆ η 2 =⇒ F D,Q (η 1 ) ⊆ F D,Q (η 2 ).
Since F D,Q is monotonous, its greatest fixpoint exists: Definition 2.5 (Q-Similarity, D,Q ). The behavioral preorder D,Q , called Q-similarity, is defined as the greatest fixed point of F D,Q .
We also provide an inductive definition of behavioral equivalence, which is defined as a contextual preorder where the contexts are restricted to the set Q (and the empty context).
We are interested in translations between calculi that are faithful w.r.t. the corresponding contextual preorders.

Three Calculi
In this section we introduce the calculi L LR , L name , and L lcc . L LR is a call-by-need calculus with recursive let, data constructors, case-expressions, and the seq-operator. The calculus L name has the same syntactic constructs as L LR , but uses a call-by-name, rather than a callby-need, evaluation. The calculus L lcc does not have letrec, and also uses a call-by-name evaluation.
For all three calculi we assume that there is a (common) set of data constructors c which is partitioned into types, such that every constructor c belongs to exactly one type. We assume that for every type T the set of its corresponding data constructors can be enumerated as c T,1 , . . . , c T,|T | where |T | is the number of data constructors of type T . We also assume that every constructor has a fixed arity denoted as ar(c) which is a non-negative integer. We assume that there is a type Bool among the types, with the data constructors False and True both of arity 0. We require that data constructors occur only fully saturated, i.e. a constructor c is only allowed to occur together with ar(c) arguments, written as (c s 1 . . . s ar(c) ) where s i are expressions of the corresponding calculus 1 . We also write (c − → s ) as an abbreviation for the constructor application (c s 1 . . . s ar(c) ). All three calculi allow deconstruction via case-expressions: where s, s i are expressions and x i,j are variables of the corresponding calculus. Thus there is a case T -construct for every type T and we require that there is exactly one case-alternative (c T,i x i,1 . . . x i,ar(c T,i ) → s i ) for every constructor c T,i of type T . In a case-alternative (c T,i x i,1 . . . x i,ar(c T,i ) → s i ) we call c T,i x i,1 . . . x i,ar(c T,i ) a pattern and s i the right hand side of the alternative. All variables in a case-pattern must be pairwise distinct. We will sometimes abbreviate the case-alternatives by alts if the exact terms of the alternatives are not of interest. As a further abbreviation we sometimes write if s 1 then s 2 else s 3 for the case-expression (case Bool s 1 of (True → s 2 ) (False → s 3 )).
We now define the syntax of expressions with letrec, i.e. the set E L of expressions which are used in both of the calculi L LR and L name .
Definition 3.1 (Expressions E L ). The set E L of expressions is defined by the following grammar, where x, x i are variables: We assign the names application, abstraction, seq-expression, or letrec-expression to the expressions (s t), (λx.s), (seq s t), or (letrec x 1 = s 1 , . . . , x n = s n in t), respectively. A value v is defined as an abstraction or a constructor application. A group of letrec bindings is sometimes abbreviated as Env . We use the notation {x g(i) = s h(i) } n i=m for the chain x g(m) = s h(m) , x g(m+1) = s h(m+1) , . . . , x g(n) = s h(n) of bindings where g, h : N → N are injective, e.g., {x i = s i−1 } n i=m means the bindings x m = s m−1 , x m+1 = s m , . . . x n = s n−1 . We assume that variables x i in letrec-bindings are all distinct, that letrec-expressions are identified up to reordering of binding-components, and that, for convenience, there is at least one binding. letrec-bindings are recursive, i.e., the scope of x j in (letrec x 1 = s 1 , . . . , x n−1 = s n−1 in s n ) are all expressions s i with 1 ≤ i ≤ n. C L denotes the set of all contexts for the expressions E L .
Free and bound variables in expressions and α-renamings are defined as usual. The set of free variables in s is denoted as FV (s).
Convention 3.2 (Distinct Variable Convention). We use the distinct variable convention, i.e., all bound variables in expressions are assumed to be distinct, and free variables are distinct from bound variables. All reduction rules are assumed to implicitly α-rename bound variables in the result if necessary.
In all three calculi we will use the symbol Ω for the specific (letrec-free) expression (λz.(z z)) (λx.(x x)). In all of our calculi Ω is divergent and the least element of the corresponding contextual preorder. This is proven in [SSSS08] for L LR and can easily be proven for the other two calculi using standard methods, such as context lemmas. Note that this property also follows from the Main Theorem 7.6 for all three calculi.
3.1. The Call-by-Need Calculus L LR . We begin with the call-by-need lambda calculus L LR which is exactly the call-by-need calculus of [SSSS08]. It has a rather complex form of reduction rules using variable chains. The justification is that this formulation permits direct syntactic proofs of correctness w.r.t. contextual equivalence for a large class of transformations. Several modifications of the reduction strategy, removing indirections, do not change the semantics of the calculus, however, they appear to be not treatable by syntactic proof methods using diagrams (see [SSSS08]). L LR -expressions are exactly the expressions E L .
Definition 3.3. The reduction rules for the calculus and language L LR are defined in Fig. 2, where the labels S, V are used for the exact definition of the normal-order reduction below. Several reduction rules are denoted by their name prefix: the union of (llet-in) and (llet-e) is called (llet). The union of (llet), (lapp), (lcase), and (lseq) is called (lll).
For the definition of the normal order reduction strategy of the calculus L LR we use the labeling algorithm in Fig. 3 which detects the position where a reduction rule is applied according to the normal order. It uses the following labels: S (subterm), T (top term), V (visited), and W (visited, but not target). We use ∨ when a rule allows two options for a label, e.g. s S∨T stands for s labeled with S or T .
A labeling rule l ❀ r is applicable to a (labeled) expression s if s matches l with the labels given by l, where s may have more labels than l if not otherwise stated. The labeling algorithm takes an expression s as its input and exhaustively applies the rules in Fig. 3 to s T , where no other subexpression in s is labeled. The label T is used to prevent the labeling algorithm from descending into letrec-environments that are not at the top of the expression. The labels V and W mark the visited bindings of a chain of bindings, where W is used for variable-to-variable bindings. The labeling algorithm either terminates with fail or with success, where in general the direct superterm of the S-marked subexpression indicates a potential normal-order redex. The use of such a labeling algorithm corresponds to the search of a redex in term graphs where it is usually called unwinding.
Definition 3.4 (Normal Order Reduction of L LR ). Let s be an expression. Then a single normal order reduction step LR − − → is defined as follows: first the labeling algorithm in Fig. 3 is applied to s. If the labeling algorithm terminates successfully, then one of the rules in Fig. 2 is applied, if possible, where the labels S, V must match the labels in the expression , Env in r if ar(c i ) = 0 The normal order reduction of L LR implements a call-by-need reduction with sharing which avoids substitution of arbitrary expressions. We describe the rules: The rule (lbeta) is a sharing variant of classical β-reduction, where the argument of an abstraction is shared by a new letrec-binding instead of substituting the argument in the body of an abstraction. The rules (cp-in) and (cp-e) allow to copy abstractions into needed positions. The rules (lapp), (lcase), and (lseq) allow moving letrec-expressions to the top of the term if they are inside a reduction position of an application, a case-expression, or a seq-expression. To flatten nested letrec-expressions, the rules (llet-in) and (llet-e) are added to the reduction. Evaluation of seq-expressions is performed by the rules (seq-c), (seq-in), and (seq-e), where the first argument of seq must be a value (rule seq-c) or it must be a variable which is bound in the outer letrec-environment to a constructor application. Since normal order reduction avoids copying constructor applications, the rules (seq-in) and (seq-e) are required. Correspondingly, the evaluation of case-expressions requires several variants: there are again three rules for the cases where the argument of case is already a constructor application (rule (case-c)) or where the argument is a variable which is bound to a constructor application (perhaps by several indirections in the letrec-environment) which are covered by the rule (case-in) and (case-e). All three rules have two variants: one variant for the case when a constant is scrutinized (and thus no arguments need to be shared by new letrec-bindings) and another variant for the case when arguments are present (and thus the arity of the scrutinized constructor is strictly greater than 0). For the latter case the arguments of the constructor application are shared by new letrec-bindings, such that the newly created variables can be used as references in the right hand side of the matching alternative.
Definition 3.5. A reduction context R LR is any context, such that its hole is labeled with S or T by the L LR -labeling algorithm.
Of course, reduction contexts could also be defined recursively, as in [SSSS08, Definition 1.5], but such a definition is very cumbersome due to a large number of special cases. The labeling algorithm provides a definition that, in our experience, is easier to work with.  By induction on the term structure one can easily verify that the normal order redex, as well as the normal order reduction, is unique. A weak head normal form in L LR (L LR -WHNF) is either an abstraction λx.s, a constructor application (c s 1 . . . s ar(c i ) ), or an expression (letrec Env in v) where v is a constructor application or an abstraction, or an expression of the form (letrec We distinguish abstraction-WHNF (AWHNF) and constructor WHNF (CWHNF) based on whether the value v is an abstraction or a constructor application, respectively. The notions of convergence, divergence and contextual approximation are as defined in Sect. 2. If there is no normal order reduction originating at an expression s then s⇑ LR . This, in particular, means that expressions for which the labeling algorithm fails to find a redex, or for which there is no matching constructor for a subexpression (that is a WHNF) in a case redex position, or expressions with cyclic dependencies like letrec x = x in x, are diverging.
The labeling algorithm applied to s 1 yields (letrec x = (y V λu.u) V , y = (λz.z) S in x V ) V .
Concluding, the calculus L LR is defined by the tuple (E L , C L , LR − − →, A LR ) where A LR are the L LR -WHNFs, where we equate alpha-equivalent expressions, contexts and answers.
In [SSSS08] correctness of several program transformations was shown: Theorem 3.7 ([SSSS08, Theorems 2.4 and 2.9]). All reduction rules shown in Fig. 2 are correct program transformations, even if they are used with an arbitrary context C in the rules without requiring the labels. The transformations for garbage collection (gc) and for shifting of letrec-expressions (lwas) shown in Fig. 4 are also correct program transformations.  3.2. The Call-by-Name Calculus L name . Now we define a call-by-name calculus on E Lexpressions. The calculus L name has E L as expressions, but the reduction rules are different from L LR . The calculus L name does not implement a sharing strategy but instead performs the usual call-by-name beta-reduction and copies arbitrary expressions directly into needed positions. In Fig. 5 the rules of the labeling algorithm for L name are given. The algorithm uses the labels S and T . For an expression s the labeling starts with s T .
An L name reduction context R name is any context where the hole is labeled T or S by the labeling algorithm, or more formally they can be defined as follows:  Fig. 6 where the labeling algorithm according to Fig. 5 must be applied first. Note that the rules (seq-c), (lapp), (lcase), and (lseq) are identical to the rules for L LR (in Fig. 2), but the labeling algorithm is different.
Unlike L LR , the normal order reduction of L name allows substitution of arbitrary expressions in (beta), (case), and (gcp) rules. An additional simplification (compared to L LR ) is that nested letrec-expressions are not flattened by reduction (i.e. there is no (llet)-reduction in L name ). As in L LR the normal order reduction of L name has reduction rules (lapp), (lcase), and (lseq) to move letrec-expressions out of an application, a seqexpression, or a case-expression.
Note that name − −− → is unique. An L name -WHNF is defined as an expression either of the form L[λx.s] or of the form L[(c s 1 . . . s ar(c) )] where L is an L context. Let A name be the set of L name -WHNFs, then the calculus L name is defined by the tuple (E L , C L , 3.3. The Extended Lazy Lambda Calculus L lcc . In this subsection we give a short description of the lazy lambda calculus [Abr90] extended by data constructors, case-expressions and seq-expressions, denoted with L lcc . Unlike the calculi L name and L LR , this calculus has no letrec-expressions. The set E λ of L lcc -expressions is that of the usual (untyped) lambda calculus extended by data constructors, case, and seq: Contexts C λ are E λ -expressions where a subexpression is replaced by the hole [·]. The set A lcc of answers (or also values) are the L lcc -abstractions and constructor applications. Reduction contexts R lcc are defined by the following grammar, where s is any E λ -expression: An lcc −→-reduction is defined by the three rules shown in Fig. 7, and thus the calculus L lcc is defined by the tuple (E λ , C λ , lcc −→, A lcc ) (modulo α-equivalence).

Properties of Similarity and Equivalences in L lcc
An applicative bisimilarity for L lcc and other alternative definitions are presented in subsection 4.2. As a preparation, we first analyze similarity for deterministic calculi in general.

Characterizations of Similarity in Deterministic
Calculi. In this section we prove that for deterministic calculi (see Def. 2.1), the applicative similarity and its generalization to extended calculi, defined as the greatest fixpoint of an operator on relations, is equivalent to the inductive definition using Kleene's fixpoint theorem.
This implies that for deterministic calculi employing only beta-reduction, applicative similarity can be equivalently defined as s t, iff for all n ≥ 0 and closed expressions r i , i = 1, . . . , n, the implication (s r 1 . . . r n )↓ D =⇒ (t r 1 . . . r n )↓ D holds, provided the calculus is convergence-admissible, which means that for all r: This approach has a straightforward extension to calculi with other types of reductions, such as case-and seq-reductions. The calculi may also consist of a set of open expressions, contexts, and answers, as well as a subcalculus consisting of closed expressions, closed contexts and closed answers. We will use convergence-admissibility only for closed variants of the calculi.
In the following we assume D = (E, C, →, A) to be an untyped deterministic calculus and Q ⊆ C be a set of functions on expressions. Note that the relations D,Q and ≤ D,Q are defined in Definitions 2.5 and 2.6, respectively.
. This equation is equivalent to the claim of the lemma. Now we show that the operator F D,Q is lower-continuous, and thus we can apply Kleene's fixpoint theorem to derive an alternative characterization of D,Q .
For infinite chains of sets S 1 , S 2 . . . , we define the greatest lower bound w.r.t. set- ). Now we can move the universal quantifier for i inside the formula: Definition 4.3. Let D,Q,i for i ∈ N 0 be defined as follows: Proof. The claim follows from Kleene's fixpoint theorem, since F Q is monotonous and lowercontinuous, and since D,Q,i+1 ⊆ D,Q,i for all i ≥ 0.
This representation of D,Q allows inductive proofs to show similarity. Now we show that Q-similarity is identical to ≤ D,Q under moderate conditions, i.e. our characterization result will only apply if the underlying calculus is convergence-admissible w.r.t. Q: Convergence-admissibility can be seen as a restriction on choosing the set Q: In most calculi (subsets of) reduction contexts satisfy the property for convergence-admissibility, while including non-reduction contexts into Q usually breaks convergence-admissibility.
Lemma 4.6. Let (E, C, →, A) be convergence-admissible w.r.t. Q. Then the following holds: Proof. The first part is easy to verify. For the second part it is important that D is deterministic. Let s 1 ≤ D,Q s 2 , and holds. We prove that D,Q respects functions Q ∈ Q provided the underlying deterministic calculus is convergence-admissible w.r.t. Q: It remains to show for all Q ∈ Q: We now prove that ≤ D,Q and Q-similarity coincide for convergence-admissible deterministic calculi: Proof. "⊆": Let s 1 ≤ D,Q s 2 . We use Theorem 4.4 and show s 1 D,Q,i s 2 for all i. We use induction on i. The base case (i = 0) obviously holds. Let i > 0 and let s 1 ↓ D v 1 . Then for all Q ∈ Q: As induction hypothesis we use that s 1 ≤ D,Q s 2 =⇒ s 1 D,Q,i−1 s 2 holds. Using Lemma 4.6 twice and "⊇": Let s 1 D,Q s 2 . By induction on the number n of Q-contexts we show ∀n, Q i ∈ Q : The base case follows from s 1 D,Q s 2 . For the induction step we use the following induction hypothesis:

4.2.
Applicative Simulation in L lcc . In this section we will show that applicative similarity and contextual preorder coincide in L lcc .
Notation. In abuse of notation we use higher order abstract syntax as e.g. in [How89] for the proof and write τ (..) for an expression with top operator τ , which may be all possible term constructors, like case, application, a constructor, seq, or λ, and θ for an operator that may be the head of a value, i.e. a constructor or λ. We say a binary relation µ is operator-respecting, iff s i µ t i for i = 1, . . . , n implies τ (s 1 , . . . , s n ) µ τ (t 1 , . . . , t n ).
Note that τ and θ may also represent the binding λ using λ(x.s) as representing λx.s. For consistency of terminology and treatment with that in other papers such as [How89], we assume that removing the top constructor λx in relations is done after a renaming. For example, λx.s µ λy.t is renamed before further treatment to λz.s[z/x] µ λz.t[z/y] for a fresh variable z.
Plan of Subsection 4.2. We start by explaining the subgoals of the soundness and completeness proofs for similarities in L lcc and its structure, illustrated in Fig. 8 is the open extension of lcc,Q lcc , and lcc,Q lcc is Q-similarity introduced in Definition 2.5 instantiated with the subcalculus of L lcc which consists of closed expressions, closed contexts, and closed answers, and Q lcc is a specific set of small closed L lcc -contexts. Q-similarity does not allow a direct proof of soundness and completeness for contextual equivalence using Howe's method [How89,How96], since it is not stated in terms of the syntactic form of values derived by evaluation. We overcome this obstacle by defining another similarity lcc in L lcc for which we will perform the proof of soundness and completeness w.r.t. contextual preorder. Since the definition of lcc does not obviously imply that lcc is a precongruence, a candidate relation cand is defined, which is trivially compatible with contexts, but needs to be shown to be transitive. After proving cand = o lcc , i.e. that o lcc is a precongruence, soundness of o lcc w.r.t. contextual preorder ≤ lcc follows. Completeness can then also be proven. In a second step we prove that o lcc,Q lcc is sound and complete for contextual equivalence, i.e.≤ lcc = o lcc,Q lcc . After showing that L lcc is convergence-admissible we are also able to show that the inductive description ≤ lcc,Q lcc of Q-similarity coincides with lcc,Q lcc . Another obstacle is that the contextual preorder contains the irregularity λx.Ω ≤ lcc c s 1 . . . s n for any constructor c. This requires an adapted definition of the similarity relation, and a slightly modified proof route.
In the following let cBot be the set of E λ -expressions s with the property that for all E λ -substitutions σ: if σ(s) is closed, then σ(s)⇑ lcc . That λx.s ≤ lcc (c s 1 . . . s n ) indeed holds is shown in Proposition 4.32. Now we define an applicative similarity lcc in L lcc analogous to [How89,How96], where this irregularity is taken into account.
Definition 4.10 (Similarity in L lcc ). Let η be a binary relation on closed E λ -expressions. Let F lcc be the following operator on relations on closed E λ -expressions: Note that the operator F lcc is monotone, hence the greatest fixpoint lcc exists.

Similarity and Contextual Preorder
Coincide in L lcc . Although applying Howe's proof technique is standard, for the sake of completeness, and to demonstrate that the irregularity λx.Ω ≤ lcc (c s 1 . . . s n ) can also be treated, we will explicitly show in this section that o lcc = ≤ lcc using Howe's method [How89,How96]. Proposition 4.12 (Co-Induction). The principle of co-induction for the greatest fixpoint of F lcc shows that for every relation η on closed expressions with η ⊆ F lcc (η), we derive η ⊆ lcc . This obviously also implies (η) o ⊆ ( lcc ) o .
The goal in the following is to show that lcc is a precongruence. This proof proceeds by defining a precongruence candidate cand as a closure of lcc within contexts, which obviously is operator-respecting, but transitivity needs to be shown. By proving that o lcc and cand coincide, on the one hand transitivity of cand follows (since lcc is transitive) and on the other hand (and more importantly) it follows that o lcc is operator-respecting (since cand is operator-respecting) and thus a precongruence.
Definition 4.16. The precongruence candidate cand is a binary relation on open expressions and is defined as the greatest fixpoint of the monotone operator F cand on relations on all expressions: Since cand is a fixpoint of F cand , we have: Some technical facts about the precongruence candidate are now proved: Lemma 4.19. The following properties hold: (1) cand is reflexive.
(2) cand and ( cand ) c are operator-respecting. ( In the case y cand r, we obtain y o lcc r ′ from the definition, and y[s . Part (6) follows from item (5). Part (7) follows from item (6) and Lemma 4.11.
Lemma 4.20. The middle expression in the definition of cand can be chosen to be closed if s, t are closed: Let s = τ (s 1 , . . . , s ar(τ ) ), such that s cand t holds. Then there are operands Proof. The definition of cand implies that there is an expression τ (s ′′ 1 , . . . , s ′′ ar(τ ) ) such that where r x is any closed expression. Lemma 4.19 now shows that o lcc t holds, since t is closed and due to the definition of an open extension. The requested expression is τ (σ(s ′′ 1 ), . . . , σ(s ′′ ar(τ ) )).
Since reduction lcc −→ is deterministic: We show that cand is left-stable w.r.t. reduction: Lemma 4.23. Let s, t be closed expressions such that s = θ(s 1 , . . . , s n ) is a value and s cand t. Then there are two possibilities: i for all i. By definition of cand and Lemma 4.19 (4), we obtain s i cand t ′′ i for all i.
again using Lemma 4.19. • Similar arguments as for the second case apply to the case-reduction.
• Suppose, the reduction is a (nseq)-reduction. Then s cand t and s = (seq s 1 s 2 ). Lemma 4.20 implies that there is some closed where we assume that the redex s is not at the top level and that R is an L lcc -reduction context. The relation R[s] cand t implies that R[s] = τ (s 1 , . . . , s n ) and that there is some Proof. For any closed r, we also have (λx.s) r cand (λx.t) r, since cand is operatorrespecting. From t ∈ cBot, we obtain that ((λx.t) r)⇑ lcc . Now suppose that (λx.s) r where c is a constructor, and s 1 ∈ cBot.
Proof. This follows from Lemma 4.23 and Lemma 4.26. Now we are ready to prove that the precongruence candidate and similarity coincide.   Proposition 4.32. Let s be a closed L lcc -expression. Then there are three cases: s ∼ lcc Ω, s ∼ lcc λx.s ′ for some s ′ , s ∼ lcc (c s 1 . . . s n ) for some terms s 1 , . . . , s n and constructor c.
For two closed L lcc -expressions s, t with s ≤ lcc t: Either s ∼ lcc Ω, or s ∼ lcc (c s 1 . . . s n ), t ∼ lcc (c t 1 . . . t n ) and s i ≤ lcc t i for all i for some terms s 1 , . . . , s n , t 1 , . . . , t n and constructor c, or s ∼ lcc λx.s ′ and t ∼ lcc λx.t ′ for some expressions s ′ , t ′ with s ′ ≤ o lcc t ′ , or s ∼ lcc λx.s ′ and t ∼ lcc (c t 1 . . . t n ) for some term s ′ ∈ cBot, expressions t 1 , . . . , t n and constructor c.
Proof. We apply Lemma 4.30. Corollary 4.31 then shows that using reduction the classification of closed expressions into the classes w.r.t. ∼ lcc holds.
For two closed L lcc -expressions s, t with s lcc t: we obtain the classification in the lemma but with lcc instead of ≤ lcc . For the three cases s ≃ lcc Ω, both s, t are equivalent to constructor expressions, and both s, t are equivalent to abstractions, we obtain also that s ≤ lcc t. In the last case λx.s ′ lcc (c s 1 . . . s n ), we also obtain from the lcc -definition, that it is valid and from Lemma 4.30, that it implies λx.s ′ ≤ lcc (c s 1 . . . s n ). Other combinations of constructor applications, abstractions and Ω cannot be in ≤ lcc -relation: • (c t 1 . . . t n ) ≤ lcc Ω and λx.s ≤ lcc Ω since the empty context distinguishes them.

4.2.2.
Alternative Definitions of Bisimilarity in L lcc . We want to analyze the translations between our calculi, and the inherent contextual equivalence. This will require to show that several differently defined relations are all equal to contextual equivalence. Using Theorem 4.8 we show that in L lcc , behavioral equivalence can also be proved inductively: where all right hand sides of other case-alternatives are Ω. The relations lcc,Q lcc , ≤ lcc,Q lcc are instantiations of Definitions 2.5 and Definition 2.6, respectively, with the set Q lcc and the closed part of L lcc consisting of the subsets of all closed E λ -expressions, closed contexts C λ , and closed answers A lcc .  If v = λx.s ′ with s ′ ∈ cBot and w = c(t 1 , . . . , t n ), Q(v) diverges for all Q, hence s F Q ( lcc ) t. • lcc,Q lcc ⊆ F lcc ( lcc,Q lcc ): Assume s lcc,Q lcc t. Let s↓ lcc v. Then also t↓ lcc w for some value w. In the cases that v, w are both abstractions or both constructor applications, when using appropriate Q of kind (ii) or (iii), the F lcc -conditions are satisfied. If v = λx.s ′ and w = c(t 1 , . . . , t n ), we have to show that s ′ ∈ cBot: this can be done using all Q-contexts of the form ([] r), since (w r)⇑ lcc in any case.
Definition 4.38. Let CE lcc be the following set of closed E λ -expressions built from constructors, Ω, and closed abstractions. These can be constructed according to the grammar: where λx.s is any closed E λ -expression. The set Q CE is defined like the set Q lcc in Definition 4.35, but only expressions r from CE lcc are taken into account in the contexts ([·] r) in (i).
We summarize several alternative definitions for contextual preorder and applicative simulation for L lcc , where we also include further alternatives. (1) is contextual preorder, (2) the applicative simulation, (3), (4) and (5) are similar to the usual call-by-value variants, where (4) and (5) separate the closing part of contexts, where (5) can be seen as bridging the gap between call-by-need and call-by-name. (7) is the Q-similarity, (8) is a further improved inductive Q-simulation by restricting the set of test arguments for abstractions, and (9) is the co-inductive version of (8). i.e. that C[s 2 ]↓ lcc . Note that this also shows by the previous items (and Corollary 4.31) that (nbeta) is correct for ∼ lcc .
• (1) ⇐⇒ (4): This follows from Corollary 4.31 since closing substitutions can be simulated by a context with subsequent (nbeta)-reduction. This also implies that (nbeta) is correct for ∼ lcc,2 and by the previous item it also correct for ∼ lcc,1 (where ∼ lcc i = ≤ lcc,i ∩ ≥ lcc,i ). . .] to an L lcc -WHNF. Since the reduction rules are correct w.r.t. ∼ lcc , for every subexpression r of the contexts Q i , there is some r ′ with r ′ ≤ lcc r, where r ′ ∈ Q CE , which is derived from r by (top-down)-reduction, which may also be non-normal order, i.e. r lcc, * − −− → r m+1 where r m+1 has reducible subexpressions (not in an abstraction) only at depth at least m + 1. All those deep subexpressions are then replaced by Ω, and this construction results in r ′ . By construction, r ′ ≤ lcc r. We do this for all the contexts Q i , and obtain thus contexts Q ′ i . The construction using the depth m shows that (  Definition 4.43 (Similarity up to ∼ lcc ). Let lcc,∼ be the greatest fixpoint of the following operator F lcc,∼ on closed L lcc -expressions: We define an operator F lcc,∼ on binary relations η on closed L lcc -expressions: s F lcc,∼ (η) t iff the following holds:  If s↓ lcc λx.s ′ and t↓ lcc λx.t ′ then similar arguments show ((λx.s ′ ) r) lcc,∼ ((λx.t ′ ) r) for all r. If s↓ lcc λx.s ′ and t↓ lcc (c t 1 . . . t n ), then s ∼ lcc λx.s ′ and t ∼ lcc (c t 1 . . . t n ). Again the fixpoint property of lcc,∼ shows s ′ ∈ cBot.
(ii) We prove that the relation lcc satisfies the fixpoint equation for F lcc,∼ : Let s lcc t for closed s, t. We know that this is the same as s ≤ lcc t. If s ∼ lcc (c s 1 . . . s n ), then clearly , and also s i lcc,∼ t i for all i holds, since reduction is correct. If s ∼ lcc λx.s ′ and s ∼ lcc λx.t ′ then s↓ lcc λx.s ′′ and t↓ lcc λx.t ′′ and ((λx.s ′ ) r) lcc,∼ ((λx.t ′ ) r).

The Translation W : L LR → L name
The translation W : L LR → L name is defined as the identity on expressions and contexts, but the definitions of convergence predicates are different. In this section we prove that contextual equivalence based on L LR -evaluation and contextual equivalence based on L nameevaluation are equivalent. We use infinite trees to connect both evaluation strategies. In [SS07] a similar result was shown for a lambda calculus without seq, case, and constructors. 5.1. Calculus for Infinite Trees L tree . We define infinite expressions which are intended to be the letrec-unfolding of the E L -expressions with the extra condition that cyclic variable chains lead to local nontermination represented by Bot. We then define the calculus L tree which has infinite expressions and performs reduction on infinite expressions.
Definition 5.1. Infinite expressions E I are defined like expressions E L without letrecexpressions, adding a constant Bot, and interpreting the grammar co-inductively, i.e. the grammar is as follows In order to distinguish in the following the usual expressions from the infinite ones, we say tree or infinite expressions. As meta-symbols we use s, s i , t, t i for finite expressions and S, T, S i , T i for infinite expressions. The constant Bot is without any reduction rule.
In the following definition of a mapping from finite expressions to their infinite images, we sometimes use the explicit binary application operator @ for applications inside the trees (i.e. an application in the tree is sometimes written as (@ S 1 S 2 ) instead of (S 1 S 2 )), since it is easier to explain, but use the common notation in other places. A position is a finite sequence of positive integers, where the empty position is denoted as ε. We use Dewey notation for positions, i.e. the position i.p is the sequence starting with i followed by position p. For an infinite tree S and position p, the notation S| p means the subtree at position p and p(S) denotes the head symbol of S| p . This induces the representation of an infinite expression S as a (partial) function S from positions to labels where application of the function S to a position p is written as p(S) and where the labels are @, case T , (c x 1 . . . x n ) (for a case-alternative), seq, c, λx, and x. The domain of such a function must be a prefix-closed set of positions, and the continuations of a position p depend on the label at p and must coincide with the syntax according to the grammar in Definition 5.1.
Definition 5.2. The translation IT : E L → E I translates an expression s ∈ E L into its infinite tree IT (s) ∈ E I . We define the mapping IT by providing an algorithm that, computes the partial function IT (s) from positions to labels. Given a position p, computing p(IT (s)) starts with s p and then proceeds with the rules given in Fig. 9. The first group of rules defines the computed label for the position ε, the second part of the rules describes the general case for positions. If the computation fails (or is undefined), then the position is not valid in the tree IT (s). The equivalence of infinite expressions is extensional equality of the corresponding functions, where we additionally do not distinguish α-equal trees.
The cases for general positions p: The set C I of infinite tree contexts includes any infinite tree where a subtree is replaced by a hole [·]. Reduction contexts on trees are defined as follows: Definition 5.4. Call-by-name reduction contexts R tree of L tree are defined as follows, where the grammar is interpreted inductively and S ∈ E I : For an infinite tree, a reduction position p is any position such that p(S) is defined and there exists some R ∈ R tree with R[S ′ ] = S and R| p = [·] Definition 5.5. An L tree -answer (or an L tree -WHNF) is any infinite E I -expression S which is an abstraction or constructor application, i.e. ε(S) = λx or ε(S) = c for some constructor c. The reduction rules on infinite expressions are allowed in any context and are as follows: Here S 1 is the tree-redex of the tree-reduction. We also use the convergence predicate ↓ tree for infinite trees defined as: S↓ tree iff S  . (. . . x ) x ) x )) r → ((. . . (. . . r) r) r) replaces the infinite number of occurrences of x by r.
Concluding, the calculus L tree is defined by the tuple (E I , C I , In the following we use a variant of infinite outside-in developments [Bar84, KKSdV97] as a reduction on trees that may reduce infinitely many redexes in one step. The motivation is that the infinite trees corresponding to finite expressions may require the reduction of infinitely many redexes of the trees for one For every p ∈ M i,d construct an infinite tree T p from S i | p by iterating the following reduction until the root of S i | p is not labeled: remove the label from the top of S i | p , then perform a labeled reduction inheriting all the labels. If this iteration does not terminate, because the root of S i | p gets labeled in every step, then the result is T p := Bot (unlabeled), otherwise a result T p is computed after finitely many reductions. Now construct S i+1 by replacing every subtree at a position p ∈ M i,d in S i by T p : for the positions p of S i that do not have a prefix that is in M i,d , we set p(S i+1 ) := p(S i ) and for p ∈ M i,d we set S i | p := T p .
Let M i+1 be the set of positions in S i+1 which carry a label †. The length of the shortest position is now at least d + 1. Then iterate again with M i+1 , S i+1 . • S ′ is defined as the result after (perhaps infinitely many) construction steps S 1 , S 2 , . . .

Standardization of Tree Reduction.
Before considering the concrete calculi L LR and L name and their correspondence to the calculus with infinite trees, we show that for an arbitrary reduction sequence on infinite trees resulting in an answer we can construct a tree-reduction sequence that results in an L tree -WHNF. Proof. This follows from Lemma 5.9 by induction on n. • The positions p k of the reduction contexts R k will grow indefinitely. Then there is an infinite path (together with the constructs and symbols) p such that p k is a prefix of p for every k. Moreover, p is a position of T ′ . The sets M k,1 are an infinite ascending set w.r.t.
⊆, hence there is a limit tree T ∞ with T tree,∞ − −−− → T ∞ , which is exactly the limit of the contexts R k for k → ∞. There is a reduction T ∞ Hence T ′ has the path p, and we see that the tree T ′ cannot have a normal order redex, since the search for such a redex goes along p and thus does not terminate. This is a contradiction, and hence this case is not possible.
Now we can apply the induction hypothesis to T ′′ Proposition 5.15 (Standardization). Let T 1 , . . . , T k be infinite trees such that T k Proof. We use induction on k. If k = 1 then the claim obviously holds since T k = T 1 is already an L tree -WHNF. For the induction step assume that T i If M i contains a normal order redex, then we apply Lemma 5.12 and have the following situation T i+1 tree, * i is an L tree -WHNF. We apply Lemma 5.14 to T ′ i+1 I,¬tree i+1 ↓ tree and thus also T i+1 ↓ tree . If M i contains no normal order redex, we have where T ′ i is an L tree -WHNF. We apply Lemma 5.14 to T i+1 5.3. Equivalence of Tree-Convergence and L LR -Convergence. In this section we will show that L LR -convergence for finite expressions s ∈ E L coincides with convergence for the corresponding infinite tree IT (s).
Lemma 5.17. Let s be a finite expression. If s is an L LR -WHNF then IT (s) is an answer. If IT (s) is an answer, then s↓ LR .
Proof. If s is an L LR -WHNF, then obviously, IT (s) is a answer. If IT (s) is an answer, then the label computation of the infinite tree for the empty position using s, i.e. s ε , must be λx or c for some constructor. If we consider all the cases where the label computation for s ε ends with such a label, we see that s must be of the form NL[v ], where v is an L LR -answer and the contexts NL are constructed according to the grammar: where v is a value, can be reduced by normal order (cp)-and (llet)-reductions to a WHNF in L LR . We use the following induction measure µ on NL[v ]: The base case obviously holds, since v is already an L LR -WHNF. For the induction step as- Let NL, and v be fixed, such that µ(NL[v ]) = k ≥ 1 . There are two cases: is a letrec-expression. Thus we can apply an (LR, (llet-in))-reduction to NL[v ], where the measure µ is decreased by one. The induction hypothesis shows the claim.
] is a letrec-expression, then we can apply an (LR, llet-in)-reduction to NL[v ] and the measure µ is decreased by 1. If NL n+1 is the empty context, and there is some i such that NL i is not the empty context, then we can choose the largest number i and apply an (LR, llet-e)-reduction to NL [v ]. Then the measure µ is strictly decreased and we can use the induction hypothesis. If all the contexts NL i for i = 1, . . . , n + 1 are empty contexts, then either NL[v ] is an L LR -WHNF (if v is a constructor application) or we can apply an (LR, cp) reduction to obtain an L LR -WHNF. Proof. Only the latter needs a justification. Therefore, we label every redex in IT (s) that is derived from the redex s LR − − → t by IT (.). This results in the set M for IT (s). There will be at least one position in M that is a normal order redex of IT (s).
Proposition 5.19. Let s ∈ E L such that s↓ LR . Then IT (s)↓ tree .
Proof. We assume that s Proof. Let p be the position of the hole of R. We follow the label computation to T along p inside s and show that the redex corresponding to T can be found in s after some (lll) and (cp) reductions. For applications, seq-expressions, and case-expressions there is a one-toone correspondence. If the label computation shifts a position into a "deep" letrec, i.e. Proof. Let is the redex of the name −−− →reduction and R name is an L name -reduction context. First one can observe that the redex s ′ 1 is mapped by IT to a unique tree position within a tree reduction context in IT (s 1 ). We only consider the (beta)-reduction, since for a (case)-or a (seq)-reduction the reasoning is completely analogous. So let us assume that s ′ 1 = ((λx.s ′′ 1 ) s ′′ 2 ). Then IT transforms s ′ 1 into a subtree σ((λx.IT (s ′′ 1 )) IT (s ′′ 2 )) where σ is a substitution replacing variables by infinite trees. The tree reduction replaces σ((λx.IT (s ′′ 1 )) IT (s ′′ 2 )) by σ(IT (s ′′ 1 ))[σ(IT (s ′′ 2 ))/x ], hence the lemma holds. ] is a reduction context for some L-context L and some A-context A, s ′′ may be an abstraction, a constructor application, or a beta-, case-or seq-redex iff T is an abstraction, a constructor application, or a betaTr-, caseTr-or seqTr-redex, respectively, and the position p of the hole in R is also the position of the hole in A[·].
Proof. The tree T may be an abstraction, a constructor application, an application, or a betaTr-, caseTr-or seqTr-redex in R[T ]. Let p be the position of the hole of R. We will show by induction on the label-computation for p in s that there is a reduction We consider the label-computation for p to explain the induction measure, where we use the numbers of the rules given in Fig. 9. Let q be such that the label computation for p is of the form (10) * .q and q does not start with (10). The measure for induction is a tuple (a, b), where a is the length of q, and b ≥ 0 is the maximal number with q = (2 ∨ 4 ∨ 6) b .q ′ . The base case is (a, a): Then the label computation is of the form (2 ∨ 4 ∨ 6) * and indicates that s is of the form L[A[s ′′ ]] and satisfies the claim of the lemma. For the induction step we have to check several cases: (1) The label computation starts with (10) * (2 ∨ 4 ∨ 6) + (10). Then a normal-order (lapp), (lcase), or (lseq) can be applied to s resulting in s 1 . The label-computation for p w.r.t. s 1 is of the same length, and only applications of (10) and (2 ∨ 4 ∨ 6) are interchanged, hence the second component of the measure is strictly decreased. (2) The label computation starts with (10) * (2 ∨ 4 ∨ 6) * (11). Then a normal-order (gcp) can be applied to s resulting in s 1 . The length q is strictly decreased by 1, and perhaps one (12)-step is changed into a (11)-step. Hence the measure is strictly decreased. In every case the claim on the structure of the contexts and s ′ can easily be verified. Proof. In Corollary 5.30 we have shown that L name -convergence is equivalent to infinite tree convergence. In Theorem 5.23 we have shown that L LR -convergence is equivalent to infinite tree convergence. Hence, L name -convergence and L LR -convergence are equivalent, which further implies that both contextual preorders and also the contextual equivalences are identical.
Corollary 5.32. The translation W is convergence equivalent and fully abstract.
Since W is the identity on expressions, this implies: Corollary 5.33. W is an isomorphism according to Definition 2.7.
A further consequence of our results is that the general copy rule (gcp) is a correct program transformation in L LR . This is a novel result, since in previous work only special cases were proved correct.
Proposition 5.34. The program transformation (gcp) is correct in L name and L LR .
Proof. Correctness of (gcp) in L name holds, since for s, t ∈ E L with s gcp − − → t and for any context C: IT (C [s]) = IT (C [t]). Hence Corollary 5.30 implies that C[s]↓ name ⇐⇒ C[t]↓ name and thus s ∼ name t. Theorem 5.31 finally also shows s ∼ LR t.
6. The Translation N : L name → L lcc We use multi-fixpoint combinators as defined in [Gol05] to translate letrec-expressions E L of the calculus L name into equivalent ones without a letrec. The translated expressions are E λ and belong to the calculus L lcc .
Definition 6.1. Given n ≥ 1, a family of n fixpoint combinators Y n i for i = 1, . . . , n can be defined as follows: The idea of the translation is to replace (letrec x 1 = s 1 , . . . , x n = s n in t) by t[B 1 /x 1 , . . . , B n /x n ] where B i := Y n i F 1 . . . F n and F i := λx 1 , . . . , x n .s i . In this way the fixpoint combinators implement the generalized fixpoint property: . However, our translation uses modified expressions, as shown below.
Consider the expression (Y n i F 1 . . . F n ). After expanding the notation for Y n i we obtain the expression ((λf 1 , . . . , f n .(X i X 1 . . . X n )) F 1 . . . F n ) where X i can be expanded to X i = λx 1 . . . x n .(f i (x 1 x 1 . . . x n ) . . . (x n x 1 . . . x n )). If we reduce further then we get: . . x n )) We take the latter expression as the definition of the multi-fixpoint translation, where we avoid substitutions and instead generate (nbeta)-redexes which ensures that contexts are mapped to contexts Definition 6.2. The translation N : L name → L lcc is recursively defined as: The proof of convergence equivalence of the translation N may be performed directly, but it would be complicated due to the additional (nbeta)-reductions required in L lcc . For this technical reason we provide a second translation N ′ , which requires a special treatment for the translation of contexts and uses a substitution function σ: Definition 6.3. The translation N ′ : L name → L lcc is recursively defined as: This translation does not duplicate holes of contexts.
Lemma 6.4. The translation N is equivalent to N ′ on expressions, that is for all E Lexpressions s the equivalence N (s) ∼ lcc N ′ (s) holds.
Proof. This follows from the definitions and correctness of (nbeta)-reduction in L lcc by Theorem 4.31.
We first prove that the translation N ′ is convergence-equivalent. Due to Lemma 6.4 this will also imply that N is convergence-equivalent. All reduction contexts L[A [·]] in L name translate into reduction contexts R lcc in L lcc since removing the case of letrec from the definition of a reduction context in L name results in the reduction context definition in L lcc .
However, this cannot be reversed, since a translated expression of L name may have a redex in L lcc , but it is not a normal order redex in L name since (lapp), (lseq), or (lcase) reductions must be performed first to shift letrec-expressions out of an application, a seq-expression, or a case-expression. The lemma below gives a more precise characterization of this relation: , where R is a reduction context in L lcc and σ is a substitution.
If R is a reduction context in L lcc , and N ′ (C ′ ) = (R, σ) for some substitution σ and some context C ′ in L name , then C ′ is a B-context. The other part can be shown by induction on the number of translation steps. It is easy to observe that the definition of a reduction context in L name does not descend into letrec-expressions below applications, seq-, and case-expressions. For instance, in ((letrec Env in ((λx.s 1 ) s 2 )) s 3 ) the reduction contexts are [·] and ([·] s 3 ) and the redex is (lapp), i.e. the reduction context does not reach ((λx.s 1 ) s 2 ). In general, applications, seq-, and case-expressions in such cases appear in B-contexts, as defined above. By examining the expression definition we observe that these (lapp), (lseq), and/or (lcase)-redexes are the only cases where non-reduction contexts may be translated into reduction contexts.
Lemma 6.6. Let N ′ (s) = t. Then: (1) If s is an abstraction then so is t.
We will now use reduction diagrams to show the correspondence of L name -reduction and L lcc -reduction w.r.t. the translation N ′ .
Transferring L name -reductions into L lcc -reductions. In this section we analyze how normal order reduction in L name can be transferred into L lcc via N ′ . We illustrate this by using reduction diagrams. For s Since R ′ is a reduction context in L lcc , this shows N ′ (s) where the last step follows, since x 1 cannot be substituted by σ R , and where it is again necessary to observe that σ R (s 1 ) = s 1 must hold. The context R ′′ = σ L (σ Env (R ′ )) must be a reduction context, since R ′ is a reduction context. This means that we need to show that R ′′ [σ L (σ Env (x 1 ))] lcc, * − −− → R ′′ [σ L (σ Env (N ′ (s 1 )))] holds. By Definition 6.3 of the translation N ′ we have σ L (σ Env ( . . x n ), and F i = λx 1 , . . . , x n .σ L (N ′ (s i )), i.e., N ′ (t) = R ′′ [U 1 ].
Performing the applications, we transform U 1 in 2n steps as Obviously, for all reduction contexts in L lcc holds: Hence N ′ (s) lcc,nbeta,2n and since x 1 , . . . , x n cannot occur free in L, the last expression is the same as R ′′ [σ L (σ Env (N ′ (s)))]. Thus we obtain the diagram (2) in Figure 10, where n is the number of bindings in the letrec-subexpression where the copied binding is. Since R ′ is a reduction context in L lcc , this shows N ′ (s) Since free variables of s 2 do not depend on Env , the translation of s 2 does not change by adding Env . I.e., for N ′ (R) = (R ′ , σ R ) and N ′ (letrec Env in [·]) = ([·], σ Env ) we have and thus the diagram for this case is as the one marked (4) in Figure 10.
• (lcase) The case is analogous to that of (lapp), with the diagram marked as (5) By Lemma 6.6 N ′ (v) is a value in L lcc (which cannot be changed by the substitution σ) and thus N ′ (s) The diagram for this case is (7) in Figure 10. We inspect how WHNFs and values of both calculi are related w.r.t. N ′ : Lemma 6.7. Let s be irreducible in L name , but not an L name -WHNF. Then N ′ (s) is irreducible in L lcc and also not an L lcc -WHNF.
Proof. Assume that expression s is irreducible in L name but not an L name -WHNF. There are three cases:  s 1 )) . . . σ(N ′ (s ar(c) ))) respectively, both of which are L lcc -WHNFs. For the other direction assume that N ′ (s) is an abstraction or a constructor application. The analysis of the reduction correspondence in the previous paragraph shows that s cannot have a normal order redex in L name , since otherwise N ′ (s) cannot be an L lcc -WHNF. Lemma 6.7 shows that s cannot be irreducible in L name , but not an L name -WHNF. Thus s must be an L name -WHNF.
Transferring L lcc -reductions into L name -reductions. We will now analyze how normal order reductions for N ′ (s) can be transferred into normal order reductions for s in L name .
Let s be an E L -expression and N ′ (s) lcc −→ t. We split the argument into three cases based on whether or not a normal order reduction is applicable to s: −−−−→ r, then we can use the already developed diagrams, since normal-order reduction in both calculi is unique. • s is a WHNF. This case cannot happen, since then N ′ (s) would also be a WHNF (see Lemma 6.8) and thus irreducible. • s is irreducible but not a WHNF. Then Lemma 6.7 implies that N ′ (s) is irreducible in L lcc which contradicts the assumption N ′ (s) lcc −→ t. Thus this case is impossible.
We summarize the diagrams in the following lemma: Lemma 6.9. Normal-order reductions in L name can be transferred into reductions in L lcc , and vice versa, by the diagrams in Figure 10. where s 1 is a WHNF. We show that there exists an L lcc -WHNF s 2 such that N ′ (s) lcc, * − −− → s 2 by induction on k. The base case follows from Lemma 6.8. The induction step follows by applying a diagram from Lemma 6.9 and then using the induction hypothesis.
For the other direction we assume that N ′ (s)↓ lcc , i.e. there exists a WHNF s 1 ∈ L lcc s.t.
N ′ (s) lcc,k − −− → s 1 . By induction on k we show that there exists a L name -WHNF s 2 such that s name, * −−−−→ s 2 . The base case is covered by Lemma 6.8. The induction step uses the diagrams. Here it is necessary to observe that the diagrams for the reductions (lapp), (lcase), and (lseq) cannot be applied infinitely often without being interleaved with other reductions. This holds, since let-shifting by (lapp), (lcase), and (lseq) moves letrec-symbols to the top of the expressions, and thus there are no infinite sequences of these reductions.
It remains to show convergence equivalence of N : Let s↓ name then N ′ (s)↓ lcc , since N ′ is convergence equivalent. Lemma 6.4 implies N ′ (s) ∼ lcc N (s) and thus N (s)↓ lcc must hold. For the other direction Lemma 6.4 shows that N (s)↓ lcc implies N ′ (s)↓ lcc . Using convergence equivalence of N ′ yields s↓ name . Proof. This easily follows by structural induction on the definition.
Proof. Note that the claim only makes sense since clearly E λ ⊆ E L . Let s 1 , s 2 be letrec-free such that s 1 ≤ name s 2 . Let C be an L lcc -context such that C[s 1 ]↓ lcc , i.e. C[s 1 ] lcc,k − −− → λx.s ′ 1 . By comparing the reduction strategies in L name and L lcc , we obtain that C[s 1 ] name,k −−−−→ λx.s ′ 2 (by the identical reduction sequence) since C[s 1 ] is letrec-free. Thus, C[s 1 ]↓ name and also C[s 2 ]↓ name , i.e. there is a normal order reduction in L name for C[s 2 ] to a WHNF. Since C[s 2 ] is letrec-free, we can perform the identical reduction in L lcc and obtain C[s 2 ]↓ lcc .
The language L lcc is embedded into L name (and also L LR ) by ι(s) = s. Proposition 6.14. For all s ∈ E L : s ∼ name ι(N (s)).
Proof. We first show that for all expressions s ∈ E L : s ∼ name ι(N (s)). Since N is the identity mapping on letrec-free expressions of L name and N (s) is letrec-free, we have N (ι(N (s))) = N (s). Hence adequacy of N (Proposition 6.12) implies s ∼ name ι(N (s)).
Proof. For this proof it is necessary to observe that E λ ⊆ E L , thus we can treat L lcc expressions as L name expressions. Let s 1 , s 2 ∈ E L and s 1 ≤ name s 2 . By Proposition 6.14: N (s 1 ) ∼ name s 1 ≤ name s 2 ∼ name N (s 2 ), thus N (s 1 ) ≤ name N (s 2 ). Since N (s 1 ) and N (s 2 ) are letrec-free, we can apply Lemma 6.13 and thus have N (s 1 ) ≤ lcc N (s 2 ). Now we put all parts together, where (N • W )(s) means N (W (s)): Theorem 6.16. N and N • W are fully-abstract, i.e. for all expressions s 1 , s 2 ∈ E L : s 1 ≤ LR s 2 ⇐⇒ N (W (s 1 )) ≤ lcc N (W (s 2 )).
Proof. Full-abstractness of N follows from Propositions 6.12 and 6.15. Full-abstractness of N • W thus holds, since W is fully-abstract (Corollary 5.32).
Since N is surjective, this and Corollary 6.17 imply: Corollary 6.17. N and N • W are isomorphisms according to Definition 2.7.
The results also allow us to transfer the characterization of expressions in L lcc into L LR . With cBot LR we denote the set of E L -expressions s with the property that for all substitutions σ: if σ(s) is closed, then σ(s) ⇑ LR .
Proposition 6.18. Let s be a closed E L -expression. Then there are three cases: s ∼ Ω, s ∼ LR λx.s ′ for some s ′ , s ∼ LR c s 1 . . . s n for some terms s 1 , . . . , s n and constructor c. Moreover, the three cases are disjoint. For two closed E L -expressions s, t with s ≤ LR t: Either s ∼ LR Ω, or s ∼ LR c s 1 . . . s n , t ∼ c t 1 . . . t n and s i ≤ LR t i for all i for some terms s 1 , . . . , s n , t 1 , . . . , t n and constructor c, or s ∼ LR λx.s ′ and t ∼ LR λx.t ′ for some expressions s ′ , t ′ with s ′ ≤ LR t ′ , or s ∼ LR λx.s ′ and t ∼ LR c t 1 . . . t n for some term s ′ ∈ cBot LR , expressions t 1 , . . . , t n and constructor c.
Proof. This follows by Proposition 4.32 and since N • W is surjective, compositional and fully abstract, and the identity on constructors.

On Similarity in L LR
In this section we will explain co-inductive and inductive (bi)similarity for L LR . Our results of the previous sections then enable us to show that these bisimilarities coincide with contextual equivalence in L LR . 7.1. Overview of soundness and completeness proofs for similarities in L LR . Before we give details of the proof for lifting soundness and completeness of similarities from L lcc to L LR , we show an outline of the proof in Fig. 11. The diagram shows fully abstract translations between the calculi L LR , L name , and L lcc defined and studied in Sections 5 and 6, where Corollary 5.32 and Theorem 6.16 show full abstractness for W and N , respectively. These fully-abstract translations that are also surjective, and the identity on letrec-free expressions, allow us to prove that s 1 ≤ LR s 2 ⇐⇒ N (W (s 1 )) ≤ lcc N (W (s 2 )). By Theorem 4.37 in L lcc , this is equivalent to N (W (s 1 )) o lcc N (W (s 2 )). The proof is completed by using the translations by transferring the equations back and forth between L LR and L lcc in this section in order to finally show that s 1 ≤ LR s 2 ⇐⇒ s 1 o LR,Q CE s 2 in Theorem 7.6. if v is a constructor application. Note that L LR -AWHNF-contexts and L LR -CWHNF-contexts are special L LRreduction contexts, also called L LR -WHNF-contexts.
First we show that finite simulation (see [SSM08]) is correct for L LR : Definition 7.1. Let ≤ LR,Q CE be defined for L LR as instantiating the relation ≤ Q in Definition 2.6 with the closed subcalculus of the calculus L LR and the set Q with Q CE from Definition 4.38. The relation LR,Q CE is Q-similarity (Definition 2.5) instantiated for the calculus L LR with the set of contexts Q CE (Definition 4.38). Its open extension is denoted with o LR,Q CE . Proposition 7.2. Let s 1 , s 2 be closed E L -expressions. Then s 1 ≤ LR s 2 iff s 1 ≤ LR,Q CE s 2 .
The following lemma is helpful in applying Theorem 4.8.
Lemma 7.3. The closed part of the calculus L LR is convergence-admissible: For all contexts Q ∈ Q CE , and closed L LR -WHNFs w: Q(s)↓ LR w iff ∃v : s↓ LR v and Q(v)↓ LR w.
Proof. "⇒": First assume Q is of the form ([·] r) for closed r. Let (s r)↓ LR w. There are two cases, which can be verified by induction on the length k of a reduction sequence (s r) Theorem 7.7. The identical embedding ι : E λ → E L is an isomorphism according to Definition 2.7.
for the polymorphically typed variant of L LR . As a further work one may try to establish a coincidence of the typed applicative bisimilarity and contextual equivalence for a polymorphically typed core language of Haskell.