Manfred Schmidt-Schauß

David Sabel

Joachim Niehren

Jan Schwinghammer

Observational Program Calculi and the Correctness of Translations

Keywords: Contextual equivalence, correctness, semantics, translations

For the issue of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods; it constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness, with a special emphasis on observational correctness. We will demonstrate that a wide range of programming languages and programming calculi and their translations can make advantageous use of our framework for focusing the analysis of their correctness.

Introduction

Motivated by our experience in analyzing and proving properties of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods, and also constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness. The presented framework can directly be applied to the observational equivalences derived from the operational semantics of programming calculi (also with concurrency), to the relationship between specification and implementation, to the issue of correctness of embedding a language into another, and also to further issues in translations, and thus has a wide range of applications.

In order to be as general as possible, we use the term observation in this paper for any predicate on programs, without any further restriction like being a constructive one or an e↵ectively computable property.

Motivation. Translating programs is an important operation in several fields of computer science. There are four main tasks where translations play an important role:

(1) Translation is the standard task of a compiler, where this is usually a conversion from a high-level language into an intermediate or low-level one, like an abstract machine language or an assembly-like language. Correctness of such a translation ensures correctness of the compiler.

(2) Translations are required in programming languages for explaining the meaning of surface language constructs by decomposing them into a number of more primitive operations in the core part of the programming language. The translation paradigm is also useful for reasoning about the implementations of language extensions in terms of a core language (which are often packaged into the language's library). Typical examples are implementations of channels, bu↵ers, or semaphores using a synchronizing primitive in the core part of the language, for example using mutable reference cells and futures in Alice ML [START_REF]The Alice Project[END_REF][START_REF] Niehren | A concurrent lambda calculus with futures[END_REF][START_REF] Schwinghammer | Correctly translating concurrency primitives[END_REF], or using MVars in Concurrent Haskell [START_REF] Jones | Concurrent Haskell[END_REF]. Correctness of these implementations can be proved by interpreting the implementation as a translation from the extended language into the original language and then showing correctness of the translation.

(3) Optimization of programs by transforming them into programs of the same language, like inlining, partial evaluation and dead code removal are a special case of translations, where source and target language are the same. Again correctness of the program transformations can be seen correctness of translations.

(4) Translations are used to compare the expressiveness (and obtain corresponding expressiveness results) between di↵erent languages or programming models. Examples are showing adequacy or full abstractness of denotational models (e.g. [START_REF] Plotkin | LCF considered as a programming language[END_REF][START_REF] Milner | Fully abstract models of typed lambda calculi[END_REF][START_REF] Astesiano | Nondeterminism and fully abstract models[END_REF][START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF]), where the translation computes the denotation of the program, proving a language extension being conservative, or even showing non-expressiveness by proving the non-existence of "correct" translations (one such example is the non-encodability of the synchronous ⇡-calculus in its asynchronous variant under mild restrictions [START_REF] Palamidessi | Comparing the expressive power of the synchronous and the asynchronous pi-calculus[END_REF]). A further example is the question for the expressive power of a sublanguage, viewed as embedded, and whether the language can be seen as a conservative extension of the sublanguage. An example scenario is removing syntactic sugar.

Correctness of these translations is an indispensable prerequisite for their safe use. However, there are various di↵erent views of the strength of correctness of a translation. This pluralism appears to be necessary and driven by practical needs, since the desired strength of correctness of a translation may depend on the specific setting.

From a bird's eye view a programming language is a set of programs P equipped with a notion of equivalence ⇠ of programs (the semantics). A translation T maps programs from a source language K into a target language K 0 . This su ces to define the commonly used notions of adequacy and full abstractness: The translation T is adequate i↵ for all (closed) programs p 1 , p 2 2 K the implication T (p 1 ) ⇠ K 0 T (p 2 ) =) p 1 ⇠ K p 2 holds; this can also be seen as the "no confusion" property, since it is equivalent to p 1 6 ⇠ K p 2 =) T (p 1 ) 6 ⇠ K 0 T (p 2 ). If additionally p 1 ⇠ K p 2 =) T (p 1 ) ⇠ K 0 T (p 2 ) holds then T is fully abstract. Requiring fully abstract translations is often a too hard condition, while adequacy is a necessity. Without adequacy, in the target language equivalent programs may be interchanged correctly (since they are equivalent), but from the source level view, the semantics is changed. From a compilation point of view, full abstractness ensures that optimizations of programs can be performed only in K or only in K 0 without missing opportunities. If a compilation is adequate, but not fully abstract (which is unavoidable in a majority of cases), then optimizing in K 0 and K is permitted, but optimizing only in K 0 may miss certain optimizations, since after compilation, some intentional knowledge may be lost.

Depending on the definitions of ⇠ K and ⇠ K 0 , adequacy and even full abstractness may be too weak as a correctness notion. E.g., none of the properties ensures that programs before and after the translation have the same termination behavior, which is an inevitable requirement to conclude that T together with K 0 is a correct evaluator for K. Thus we will be more concrete, and provide a general approach for program calculi with an operational semantics, which beside others covers the termination behavior of programs.

Results and Applications. We give a short and informal overview of the results and applications. Within the scope are (at least) programming languages where programs can be written down (using a syntax) and evaluated (using an operational semantics) and of several observations like successful evaluation in a program context (may-convergence, mustconvergence). Syntactically, typing can be formulated and open and closed programs can be distinguished, and operationally, also concurrent systems, e.g. process calculi are in the scope.

A first useful result (where variants are already in the literature) is Theorem 3.16 which shows that there are easily checkable criteria for adequacy, namely compositionality and convergence equivalence. In this paper there are further extensions and variations of this method.

A general result concerning translations is Theorem 3.21 which exhibits conditions, when the translated programs are more or less equivalent to the original programs (in the image calculus); which is a theorem similar to an algebraic homomorphism theorem. It also provides a first result on conditions when a translation is an embedding.

Section 4 exhibits several conditions and scenarios for extending (resp. embedding) languages. Theorem 4.3 puts a common technique in semantics (approximation by ?) for showing full abstraction into the context of our framework, where the approximations are represented as a family of translations.

Theorem 4.6 is a criterion for full abstractness under a minimal set of conditions. It complements the full abstractness criteria of Theorem 3.21. Corollaries 4.7 and 4.8 show that there are easy-to-check preconditions for applying Theorem 4.6.

Applications of the framework and the methods are in Section 5.2 and in Section 5.3. In particular Corollary 4.8 was applied in [START_REF] Niehren | Observational semantics for a concurrent lambda calculus with reference cells and futures[END_REF]. Another published result is the proof of conservativity of embedding the deterministic part of the language in the full language [START_REF] Sabel | Conservative concurrency in Haskell[END_REF].

This paper presents a unifying approach for di↵erent variations of observational semantics and translations of programming languages. The usage may be as turnkey solution for proving properties of translations, and if this is not applicable, the usage will also be as a paradigm and guidance to clearly understand the real issues when analyzing the semantics and the correctness of translations for a programming language together with its evaluation.

Observational Program Calculi. For the formal semantics of a programming language several di↵erent approaches exist, e.g. there are equivalence notions based on the denota-tional semantics, on logical relations, on bisimulations, and observational equivalence.

We will consider observational semantics for several reasons:

• Observational equivalence is based on the operational semantics and thus is naturally available for almost all programming languages. In case other semantics are available, the observational semantics is often the reference for various correctness criteria, like adequacy or full abstractness in denotational semantics. In addition, observational equivalences tend to be the maximal useful equivalences.

• A simple approach for defining a program equivalence is the extensional approach: compare the output of the programs (perhaps on all inputs) and request that the programs are equivalent i↵ the output is identical (the same value). However, this leads to lots of variations of definitions, and also might require extra testing abilities which might not be included in the expressive power of the languages. In contrast, for observational semantics the main criterion is convergence (or successful termination), which allows for a common notion of program equivalence. Moreover, usually observational semantics includes the above program equivalence defined by comparing outputs.

The notion of observational semantics is a syntactic approach and thus we will speak of programs, contexts, open and closed programs and convergence (i.e. successful termination), however, with an abstract meaning.

Observational semantics identifies programs if, and only if their successful termination (convergence) behavior is indistinguishable if one program is interchanged by the other one in any larger surrounding program. The most important instance of observational semantics is the well-known notion of contextual equivalence ( [START_REF] Morris | Lambda-Calculus Models of Programming Languages[END_REF][START_REF] Plotkin | LCF considered as a programming language[END_REF][START_REF] Milner | Fully abstract models of typed lambda calculi[END_REF][START_REF] Barendregt | The Lambda Calculus, Its Syntax and Semantics[END_REF]): two programs p 1 , p 2 are considered equivalent if they exhibit the same convergence behavior in all contexts C, denoted as p 1 ⇠ p 2 . Note that it is usually not necessary to observe convergence to the same value, since the contexts of the underlying language have enough discrimination power to distinguish di↵erent values by convergence. However, for non-deterministic and concurrent programming languages a single (may-) convergence predicate p îs insu cient, in the sense that the induced program equivalence does not distinguish programs that exhibit intuitively distinct behaviors. Instead, for non-deterministic and concurrent languages, a suitable equivalence arises from a combination of may-with must-or should-convergence (see e.g. [START_REF] De Nicola | Testing equivalences for processes[END_REF][START_REF] De'liguoro | Must preorder in non-deterministic untyped lambda-calculus[END_REF][START_REF] Carayol | On the representation of McCarthy's amb in the pi-calculus[END_REF][START_REF] Sabel | A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations[END_REF][START_REF] Niehren | Observational semantics for a concurrent lambda calculus with reference cells and futures[END_REF][START_REF] Schmidt-Schauß | Closures of may-, should-and must-convergences for contextual equivalence[END_REF]). Accordingly, we will also consider an observational semantics which may be based on multiple convergence predicates. Observational semantics that consider convergence with some specific output, (for instance a name of a channel in barbed congruence in the ⇡-calculus), could be modeled by (an infinite) set of convergence predicates (e.g. one for every channel name). If the languages are su ciently expressive, these convergence predicates are in general undecidable and the derived relations are not recursively enumerable. Only may-convergence is recursively enumerable in several languages. Due to this undecidability and also due to the quantification over all contexts, establishing concrete contextual equivalences is usually not easy. However, various (in general incomplete) proof methods have been developed, general ones and calculus-specific ones. These include context lemmas (e.g., [START_REF] Milner | Fully abstract models of typed lambda calculi[END_REF][START_REF] Mason | From operational semantics to domain theory[END_REF][START_REF] Jim | Full abstraction and the context lemma[END_REF][START_REF] Ford | Formal foundations of operational semantics[END_REF][START_REF] Schmidt-Schauß | On generic context lemmas for higher-order calculi with sharing[END_REF]), bisimulation methods (for instance, [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF][START_REF] Sumii | A bisimulation for type abstraction and recursion[END_REF][START_REF] Pitts | Howe's method for higher-order languages[END_REF]), diagram-based methods (e.g., [START_REF] Kutzner | A nondeterministic call-by-need lambda calculus[END_REF][START_REF] Wells | Diagrams for meaning preservation[END_REF][START_REF] Niehren | Observational semantics for a concurrent lambda calculus with reference cells and futures[END_REF][START_REF] Rau | A unification algorithm to compute overlaps in a call-by-need lambdacalculus with variable-binding chains[END_REF][START_REF] Rau | Correctness of program transformations as a termination problem[END_REF]), and characterizations of contextual equivalence in terms of logical relations (e.g., [START_REF] Pitts | Parametric polymorphism and operational equivalence[END_REF][START_REF] Appel | An indexed model of recursive types for foundational proof-carrying code[END_REF][START_REF] Ahmed | Step-indexed syntactic logical relations for recursive and quantified types[END_REF][START_REF] Ahmed | State-dependent representation independence[END_REF]).

To express observational semantics for a broad class of programming languages, we define so-called observational program calculus. It abstracts from the details of a concrete programming language and -as we illustrate by examples -captures a lot of programming calculi, which are instances of an observational program calculus.

The main ingredients of an observational program calculus are programs, contexts, types, and convergence predicates (called observation predicates to stress the abstract level). However, convergence of programs is only tested for closed programs: This is more common in the literature, in particular for call-by-value languages, and also leads to more equations and thus a better language model. Contextual equivalence then only tests (open) programs in those contexts that close the programs. So we add further components to the observational program calculus: an abstract notion of closedness, which is represented as a subset of all programs, and an abstract notion of so-called generalized closing substitutions, which allow to close any program and are a subset of the contexts with specific properties. The latter component helps, among others, to ensure that contextual equivalence is a congruence.

Correctness of Translations.

The goal of this paper is to present our approach on proving correctness of translations between two observational program calculi, which we applied for concrete and complex and quite di↵erent instances several times in the past (see Section 5.3), and will also lead to a better focus in future work. Thus we consider translations T : K ! K 0 between source and target languages K and K 0 where both K and K 0 are observational program calculi. More specifically, in our setting T has to translate types and programs, but also the contexts and it maps observation predicates to observation predicates. One may argue that translating the contexts is a too strict requirement. However, for deeply comparing the observational semantics of K and K 0 this is inevitable. Even for noncontextual translations our framework may be helpful, since translations often can be split into a composition of several sub-translations such that several of the subtranslations are contextual where our framework is applicable.

Besides the notions of adequacy and full abstractness (where ⇠ is contextual equivalence) we consider and examine further properties of the translation T which are important for its correctness. As explained before, it is a basic requirement that K 0 evaluates translated programs as they are evaluated in K. This property is called convergence equivalence and means for all closed K-programs p and all observation predicates ôf K that the equivalence )) which emphasizes that the translation preserves and reflects the specification and that the specification itself must be translatable.

Observational correctness can also be expressed as convergence equivalence plus compositionality up to observation, where the latter means that T (C(p))

T () T (C)(T (p)) T . Compositionality up to observation is weaker than compositionality (i.e. T (C(p)) = T (C)(T (p))), and thus any compositional and convergence equivalent translation is observationally correct. As a consequence for compositional translations reasoning about contexts is not necessary to prove observational correctness.

As we show (see Proposition 3.16), a consequence of observational correctness is adequacy, i.e. once observational correctness of T is proved, we get for free that T is adequate. Note that the reverse implication does not hold (see Proposition 3.18).

Full abstractness of T often does not hold, since the target calculus K 0 has more contexts than K and thus translated programs can be distinguished by these contexts. However, in Section 4 we will also examine when and how full abstractness can be obtained for observationally correct translations provided K 0 can be embedded in K, which is typically the case if K extends K 0 by new language constructs. Applications. To illustrate our framework and demonstrate its applicability, we will point to rather diverse examples. During the definition of the framework and the properties of the translations, we use as running examples mostly variations of PCF as a well-known example of a typed lambda calculus both in its call-by-value and call-by-name variants.

As a fully worked out example we consider the Church encoding of pairs in a call-by-value lambda calculus; this example shows that our basic requirement for correctness, convergence equivalence, fails without an appropriate notion of typing. This example is important, since the typing issues raised by the encoding of pairs is an instance of the common situation where an abstract data type is implemented in terms of some operations on a given type.

These worked-out examples are rather small, but in a lot of works we applied the techniques represented in this paper to larger -real world -examples. In Section 5.3 we will give an overview of the quite di↵erent applications of the framework. We will also discuss other related work and how it is related to our abstract notions and which questions are addressed in the terms of our framework.

Overview. The paper is structured as follows: In Section 2 we present our notion of observational program calculi and show how to define the observational semantics for them. In Section 3 we define the notion of a translation between observational program calculi, introduce and discuss the fundamental properties of translations, and finally show some relations between these properties. In Section 4 we consider the specific case of language extensions and analyze the conditions under which full abstractness of embeddings and encodings can be deduced. In Section 5 we first consider some specializations of our framework, provide the observational correctness proof of Church's encoding of pairs, and we give an overview of larger examples where we applied the techniques of our framework. The discussion of related work is deferred to Section 6. We conclude in Section 7.

Observational Program Calculi

Our objective is to introduce a general notion of an observational program calculus that provides all ingredients for defining the observational semantics of a programming language in a systematic manner.

Starting Example

As a prototypical example for a sequential functional language, we present variants of PCF [START_REF] Plotkin | LCF considered as a programming language[END_REF][START_REF] Pierce | Types and programming languages[END_REF]. We will also extend it with a nondeterministic choice operator, in order to illustrate the methods for treating concurrent programming languages.

The simply typed lambda calculus pcf cbv . This is a call-by-value lambda calculus with fixed point operators, Booleans, and natural numbers. It can also be obtained by making Plotkin's language PCF [START_REF] Plotkin | LCF considered as a programming language[END_REF][START_REF] Pierce | Types and programming languages[END_REF] call-by-value. The types ⌧ are either the base types o for Booleans and ◆ for natural numbers, or function types recursively constructed from the base types, that is

⌧ ::= o | ◆ | ⌧ 1 ! ⌧ 2 .
We assume an infinite set of variables ranged over by x, y, z and assume that every variable x has a predefined type (x). The programs are well-typed expressions p built from variables, constants for the Boolean values and all nonnegative numbers i 2 N, abstraction and application, conditionals, function constants for arithmetic operations, a family of fixed point operators fix ⌧ for all types ⌧ of the form

((⌧ 1 ! ⌧ 2 ) ! ⌧ 1 ! ⌧ 2 ) ! (⌧ 1 ! ⌧ 2 )
. The values v of pcf cbv are variables, constants, and lambda-abstractions.

v ::= x | b | i | succ | pred | zero? | fix ⌧ | x.p p ::= v | (p 1 p 2 ) | if p then p 1 else p 2
A program is closed if it does not contain free variables, i.e., if every occurrence of a variable is in the scope of some lambda-binder. We only consider well-typed programs. Every welltyped program has a unique type, since we assume that all variables have a unique type (given by ). The typing rules are omitted, since these are standard. A context C is like a program p except that it contains a single occurrence of a "hole". We assume that all holes are annotated by a type and write [.] ⌧ for the hole of type ⌧ . The program obtained by replacing the hole of context C by a program p of the same type is denoted by C(p). A context C of type ⌧ 0 with a hole of type ⌧ can thus be identified with a function that maps programs of type ⌧ to programs of type ⌧ 0 . Note that the free variables in p may be bound in C(p), so that C(p) may become closed even though p was not.

We next define the evaluation in pcf cbv by a small-step operational semantics p ! p 0 . The possible reductions are defined below:

( x.p) v ! p[v/x] ( succ i) ! i + 1 fix ⌧ x.p ! p[ y.(fix ⌧ x.p) y/x] (pred i) ! i 1 if i > 0 (if true then p 1 else p 2 ) ! p 1 (zero? 0) ! true (if false then p 1 else p 2 ) ! p 2 (zero? i) ! false if i > 0
These reduction rules can be performed in all reduction contexts R defined as follows:

R ::= [.] ⌧ | (R p) | (v R) | if R then p 1 else p 2
The standard reduction is R(p) ! R(p 0 ), if p ! p 0 by one of the reductions above. We say that a program p converges and write p# pcfcbv if there exists a value v, such that p ! ⇤ v. Otherwise we say that p diverges and write p" pcfcbv . Note that programs of the form R(pred 0) are irreducible even though they are not a value, and thus such (erroneous) programs diverge, thus they represent diverging programs, sometimes written ?. Other divergent programs are non-terminating programs. There are some nonterminating programs in pcf cbv even though we impose simple typing, since pcf cbv admits fixed point operators. Moreover, we can define a non-terminating closed program for every type ⌧ as ⌦ ⌧ := (fix ⌧ 0 ( x.x)) 0, where

⌧ 0 = ((◆ ! ⌧ ) ! ◆ ! ⌧ ) ! (◆ ! ⌧ ) and x is a variable with (x) = (◆ ! ⌧ ).
Contextual equivalence for programs p and p 0 of type ⌧ is defined by observing termination in all closing contexts, i.e. p ⇠ ⌧ p 0 i↵ C(p)# pcfcbv , C(p 0 )# pcfcbv for all appropriately typed contexts C closing p and p 0 . This captures the intuition that p and p 0 may be freely exchanged in any larger closed program without a↵ecting its observable behavior. For instance, if x then true else true ⇠ o true holds in pcf cbv . The intuition is that free variables in a call-by-value language can only be substituted by correctly typed values, so that x must be instantiated by true or false. The instantiation can be done by reduction in contexts such as ( x. [.] o ) p where p converges to some Boolean. Since the argument p must be evaluated before call-by-value beta reduction can be applied, x can only be substituted by a Boolean this way. Note, however, that if also non-closing contexts were permitted in the definition of contextual equivalence, then the identity context [.] o could be used to distinguish both expressions.

Extension to pcf

cbv , with nondeterministic choice. More evolved concurrent programming languages can be obtained by extending sequential programming languages by communicating threads. In order to illustrate the main consequences for observational semantics, we consider a more modest extension pcf cbv , which adds nondeterministic choice to pcf cbv . pcf cbv , extends pcf cbv by a family of constants choice ⌧ !⌧ !⌧ for any type ⌧ . The additional reduction axioms are choice

⌧ v 1 v 2 ! v 1 and choice ⌧ v 1 v 2 ! v 2 .
For such nondeterministic languages it is not su cient to observe only whether a program may terminate, but also termination properties in all computation paths. May-convergence can be defined in the same way as the observation predicate # pcfcbv before, but cannot be understood as convergence any more. Its negation "

pcfcbv has now to be read as must-divergence. In addition, we observe so-called should-convergence1 where a program p should-converges (p+ pcfcbv ) if it is impossible to reduce p to a must-divergent expression, i.e. p+ pcfcbv i↵ for every p 0 the implication p ! ⇤ p 0 =) p 0 # pcfcbv holds. The contextual equivalence is now defined with respect to both may-and shouldconvergence, i.e., p ⇠ ⌧ p 0 holds for two expressions p and p 0 of type ⌧ if for all appropriately typed contexts C closing p and p 0 :

C(p)# pcfcbv , C(p 0 )# pcfcbv and C(p)+ pcfcbv , C(p 0 )+ pcfcbv . For instance, if (x) = ⌧ , then we obtain choice ⌧ !⌧ ( x.x) ( x.⌦ ⌧ ) 6 ⇠ ⌧ !⌧ x.x,
since should-convergence in the context ([.] ⌧ !⌧ v) for a value v of type ⌧ distinguishes these two expressions (in contrast to may-convergence). As in deterministic pcf cbv , the contextual equivalence in pcf cbv , is a typed congruence relation, as we will show in Proposition 2.6.

Observational Semantics

In order to develop observational semantics for various programming languages in a uniform framework, we need an abstract notion of a program calculus that abstracts from various kinds of typed programs, typed contexts, observation predicates and closed programs.

C 2 C ⌧ 1 ,⌧ 2 , C 0 2 C ⌧ 2 ,⌧ 3 : C 0 C 2 C ⌧ 1 ,⌧ 3 . ⇤
Even though observational program pre-calculi are typed, untyped calculi do also fit into our framework, since one can choose T to be a singleton containing the 'universal' type. In this case, the set of contexts is a semigroup. It is possible to describe calculi as an observational program pre-calculus, where programs may have several types in which case type is a proper relation. An example is a "polymorphic" PCF-variant where fix is a single constant with an infinite number of types, and where the identity x.x has an infinite number of types of the form ⌧ ! ⌧ . In this calculus, x.x ⇠ o!o y.y as well as x.x ⇠ ◆!◆ y.y holds. Another example would be a calculus with an ordering on the types, i.e. there may be supertypes and subtypes, which can be modelled by assigning several types to expressions.

Including the component Clos is necessary to define an observational equivalence on open programs, while only taking the convergence behavior in closing contexts into account. As already argued before, this is a necessity for call-by-value calculi.

Example 2.2. The call-by-value lambda calculus pcf cbv from Section 2.1 matches the definition of an observational program pre-calculus as follows. The set T contains all simple types ⌧ , the set of P all well-typed lambda expressions p, the set Clos all closed well-typed lambda expressions, and the set C all well-typed contexts C. The function type maps a program p to its unique type ⌧ , and a context C of type ⌧ and a hole of type ⌧ 0 to the pair (⌧ 0 , ⌧). The set of observation predicates is O = {# pcfcbv }. The extended call-by-value lambda calculus pcf cbv , also matches the definition of an observational program pre-calculus. Programs and contexts may now contain the choice operator in addition, so that the function type needs to be extended too, as well as the set of closed programs. The most important di↵erence is the set of observation predicates O = {# pcfcbv , + pcfcbv }, which are needed to account for nondeterminism properly. We next define an observational equivalence that can be defined for any observational program pre-calculus. We will derive it from an observational preorder that allows more flexibility, and is an analogue of the domain-theoretic information preorder: Definition 2.3. Let K be an observational program pre-calculus. For any type ⌧ of K, we define the following binary relations for all programs p 1 , p

Congruences

We present a general restriction on observational program pre-calculi to ensure that its observational equivalence becomes a congruence. The idea is to impose the existence of a set of generalized closing substitutions that can be applied to non-closed programs so that they become comparable to other closed programs. These substitutions should be chosen similarly to substitutions for the lambda calculus replacing free variables by closed expressions.

⌧ 0 2 T , all contexts C 2 C ⌧,⌧ 0 : p 1  ,⌧ p 2 ) C(p 1 )  ,⌧ 0 C(p 2
) and in analogy:

p 1  ⌧ p 2 ) C(p 1 )  ⌧ 0 C(p 2 ). The relations ⇠ ,⌧
and ⇠ ⌧ are typed congruences, i.e. they are typed precongruences and equivalence relations.

Proof. We only consider the observational preorder, which implies the part for observational equivalence. It is easy to see that  ,⌧ is reflexive. In order to check that each

 ,⌧ is transitive, let p 1  ,⌧ p 2  ,⌧ p 3 and C be a context in C ⌧,⌧ 0 , such that C(p 1
) and C(p 3 ) are closed, and such that C(p 1 )

.W e have to show that

C(p 3 ) .I f C(p 2 ) is closed, then C(p 1 ) îm plies C(p 2 )
,w hich in turn implies C(p 3 ) .I n the other case, where C(p 2 ) is not closed, Lemma 2.5 implies that there is a type ⌧ 00 and a generalized closing substitution D 2 S ⌧ 0

,⌧ 00

such that D(C(p i )) for i = 1, 2, 3 are closed. Condition (4) of Definition 2.4 shows that D(C(p 1 )) () C(p 1 ) ân d that D(C(p 3 )) () C(p 3 ) ,h ence D(C(p 1 )) .S ince D C is also a context by Definition 2.1, we obtain D(C(p 2 )) (f rom p 1  ,⌧ p 2 ), which in turn implies also D(C(p 3 )) (s ince p 2  ,⌧ p 3 and since D(C(p 3 )) is closed), and thus C(p 3 ) . It remains to show that  ,⌧ is compatible with contexts: Let p 1  ,⌧ p 2 and C 2 C ⌧,⌧ 0 . For any context C 0 2 C ⌧ 0 ,⌧ 00 where C 0 (C(p 1 )) and C 0 (C(p 2 )) are closed, the inequation p 1  ,⌧ p 2 obviously implies that C 0 (C(p 1 )) =) C 0 (C(p 2 )) ,s ince C 0 C is also a context. A
p 1 ⇠ ⌧ p 2 , p 1 ⇠ ,⌧ p 2 , p 1  ⌧ p 2 , or p 1  ,⌧
p 2 , then also p 2 . Proof. Let p 1 , p 2 be closed and p 1 .T hen Lemma 2.5 and condition (4) of Definition 2.4 show that there is some C 2 S such that C(p 1 ) and C(p 2 ) are closed, and C(p 1 )

.T hen every relation above implies C(p 2 )

,a nd again the condition (4) shows that p 2 . In the following, types are sometimes omitted in the notation, and we implicitly assume that type information follows from the context.

Further Examples

We sketch some further examples to illustrate the range of situations that fit the definition of an observational program calculus. Many other lambda calculi fit into our framework, like the lazy lambda calculus or call-by-need lambda calculi. Observational Program Calculi can also capture models of concurrent computation, such as CCS or other process calculi. Also abstract machines fit into this framework, where machine environments, stacks, heaps etc. may be modelled as contexts. Given that observational program calculi do not rely on small-step semantics, also calculi with big-step semantics fit into our framework.

Example 2.8 (Call-by-name pcf). We consider the call-by-name lambda calculus pcf cbn , which is a variant of the call-by-value lambda calculus pcf cbv with the same expressions. The call-by-name beta-reduction is now applicable for any argument p 0 : ( x.p) p 0 ! p[p 0

/x] and the fixpoint reduction is modified similarly: fix ⌧ p ! p (fix ⌧ p). The reduction contexts are di↵erent, since they do not force evaluation of arguments, so they are:

R ::= [.] ⌧ | (R p 0 ) | if R then p 1 else p 2 | pred R | succ R | zero? R.
The generalized closing substitutions in S are the compositional closure of all appropriately typed contexts (( x.

[.] ⌧ ) p 0 ) where p 0 is any closed expression. In contrast to pcf cbv , now it does no longer make a di↵erence if convergence is defined for all expressions, and contextual equivalence could be defined w.r.t. all (perhaps open) contexts. E.g., the two expressions if x then true else true and true are not observationally equivalent in pcf cbn , since they can be distinguished by the context C := ( x. ⌧ ) p 0 ) where p 0 must be closed and converging. In particular, Definition 2.1 captures not only lambda calculi, but also process calculi:

Example 2.9 (CCS). CCS [START_REF] Milner | Communication and Concurrency[END_REF] may be viewed as an (untyped) observational program calculus: for a fixed action set ⌃, both programs and contexts are given by the set of CCS processes P, Q, . . ., and P Q as well as P (Q) are given by the parallel composition P | Q. More precisely, contexts are given by the functions f P with f P (Q) = P | Q. Since there are no variables, we define Clos = P, and generalized closing substitutions S = {id} where id is the identity. By considering observation predicates # CCS , for every 2 ⌃ ! such that P # CCS , holds if is a trace of P , we obtain a trace-based testing equivalence ⇠ on processes. Variations are possible, e.g. by restricting the observations to finite traces 2 ⌃ ⇤ (see [START_REF] Nain | Branching vs. linear time: Semantical perspective[END_REF]).

The terms "calculus" and "observation" in Definition 2.1 are to be understood in a loose sense, especially "observable" does not mean that the predicates are e↵ectively computable or even recursively enumerable. Hence our notion of an observational program calculus is very general, and for instance, semantic models also fit the definition of an admissible observational program calculus: Example 2.10 (CPOs). A semantic counterpart to call-by-value PCF is given by !-complete pointed partial orders (cppos) and continuous maps. More precisely, if D B and D N are the flat cppos with underlying sets {0, 1} and Z respectively, we let D

⌧ 1 !⌧ 2 = (D ⌧ 1 ! D ⌧ 2 ) ? be the set of strict continuous functions from D ⌧ 1 to D ⌧ 2 extended
with a new least element, and order D ⌧ 1 !⌧ 2 pointwise. We can then take P ⌧ to be the underlying set of D ⌧ . Since there are no variables, we choose Clos = P. The contexts are continuous maps, i.e., C

⌧ 1 ,⌧ 2 = D ⌧ 1 ! D ⌧ 2
, and for a 2 P ⌧ the observation a# cpo holds if a 6 = ?. Since every program is closed, we set S := {id ⌧ | for any type ⌧ } where id ⌧ is the identity on type ⌧ . In this example, a ⇠ ⌧ a 0 if and only if a = a 0 .

Translations

A translation is a mapping between observational program calculi that often arises very concretely when relating two programming languages. Examples are compilations of one programming language into another one, which may induce a mapping between possibly rather di↵erent calculi, or the removal of syntactic sugar, which may be expressed as a mapping from an extended calculus into a core calculus, or the embedding of a calculus into its extended version. Furthermore, expressivity results between di↵erent programming languages are usually obtained by mapping one programming language into another one. As a simple concrete example let us consider the removal of Booleans in pcf cbv , i.e. pcf cbv , B is the calculus pcf cbv where types do not contain o, there are no Boolean values, the constant zero? is not included and conditionals if p 1 then p 2 else p 3 require p 1 to be of type ◆. The reduction axioms for conditionals are replaced by

(if i then p 1 else p 2 ) ! p 1 if i > 0 ( if 0 then p 1 else p 2 ) ! p 2
The questions that arise are: Is there an encoding from pcf cbv ! pcf cbv , B ? In which sense are such translations (of course, also even more complex ones) between observational program calculi correct, i.e., how does the semantics in source and target calculus relate with respect to the translation, and what are the correctness requirements?

Pre-Translations

From a very general view, a translation is a mapping from types to types and a type correct mapping from programs to programs. Let K and K 0 be two observational program pre-calculi with types T and T 0 , programs P, P 0 , and observational preorders  ⌧ and  0 ⌧ 0 . Definition 3.1. A pre-translation T from an observational program pre-calculus K to an observational program pre-calculus K 0 is a function which maps types to types and programs to programs, i.e. T : T ! T 0 and T : P ! P 0 such that for all p 2 P ⌧ : T (p) 2 P T (⌧ ) . Already for pre-translations we can define adequacy, full abstractness and the isomorphism property as correctness notions. Both properties speak about the relation between the observational preorders of the source and the target calculus of a pre-translation. These properties are quite standard and sometimes are also used for relating other formalisms, e.g. a contextual semantics and denotational semantics. Definition 3.2. We call a pre-translation T from K to K 0 adequate if T is -reflecting, i.e., for all types ⌧ 2 T and programs p 1 , p 2 2 P ⌧ :

T (p 1 )  0 T (⌧ ) T (p 2 ) =) p 1  ⌧ p 2 , fully abstract if T is -preserving and -reflecting; i.e., for all types ⌧ 2 T and programs p 1 , p 2 2 P ⌧ : p 1  ⌧ p 2 () T (p 1 )  0 T (⌧ ) T (p 2
), an isomorphism if T is a bijection on the types, T is a bijection between P/ ⇠ and P 0 / ⇠ 0 , and T is fully abstract. defined by T incl (⌧ ) = ⌧ and T incl (p) = p. One may expect that T incl is fully abstract (but not an isomorphism). However, the (direct) proof is non-trivial, since it requires to reason about all contexts in pcf cbv , . As another example we define a pre-translation T B from pcf cbv into pcf cbv , B as follows: On the types, T B replaces all occurrences of o by ◆, and on programs, T B is defined as T B (true) = 1, T B (false) = 0, T B (zero?) = x.if x then 0 else 1; ⌧ ) and applied homomorphically to all other language constructs. Clearly, T B is not an isomorphism (since T B is not bijective on types). T B is adequate (see Example 3.9 and Theorem 3.16). However, it is not fully abstract, since e.g. for p 1 := x.x and p 2 = x.if x then true else false the equation

T B (fix ⌧ ) = fix T B (
p 1 ⇠ o!o p 2 holds in pcf cbv , but T B (p 1 ) 6 ⇠ ◆!◆ T B (p 2 ) in pcf cbv , B .
Note that the notion of translation and isomorphism is consistent with viewing observational program pre-calculi and pre-translations as a category. Every observational program pre-calculus has Id as an isomorphism, and an isomorphism between K and K 0 has an inverse translation that composes to the identity on K (or K 0 , respectively).

One obvious consequence of the definition is that all three properties are closed w.r.t. composition of translations:

Proposition 3.4. Let K, K 0
, K 00 be program calculi and P be one of the properties of pretranslations, adequacy, full abstractness or being an isomorphism. If T : K ! K 0 and T 0 : K 0 ! K 00 are pre-translations with property P then functional composition T 0 T : K ! K 00 is also a pre-translation with property P . This proposition allows us to prove adequacy (or full abstractness) of a pre-translation by decomposing it and proving the adequacy (or full abstractness) of all of its parts.

Before introducing further methods and properties, let us discuss in which case a translation should be called correct. More generally, if we view a translation as a compilation of one calculus into another, where the intuition is to compile programs of a high level language K into a low level language K 0 . When would we accept a compilation (translation) as correct?

K p 1 p 2 K 0 T (K) T (p 1 ) p 0 2 ⇠ T (p 2 )
T One minimal sensible correctness requirement is that convergence of programs is unchanged; a second one is that testing a program and its result "through the compiler" must be the same as within the high-level language itself; a third requirement is that if T (p 1 ) is the result of a compilation of p 1 , and p 0 2 is the result of optimizing the program T (p 1 ) in the low level language where p 0 2 ⇠ T (p 2 ) for some K-program p 2 , then p 2 must be equivalent to p 1 in the high level language. The third requirement is the already introduced notion of adequacy. A compilation of a high-level program into a rather low level programming language is usually not fully abstract, since it is possible to test the implemented program or function for implementation details, which is impossible in the high-level language, and which may lead to the counter-intuitive e↵ect that programs (functions) p 1 , p 2 that are indistinguishable in the high-level language are observably di↵erent after their compilation. This is often called a loss of knowledge or of intention of the programmer, but this is in general unavoidable, since the low level language can see and observe the implementation details. This can be partly overcome by optimizing the programs using the semantics of the high-level language. 2The first requirement is called convergence equivalence (see (ce) in Def. 3.8), and the first and second together are exactly the property of observational correctness (see (oc) in Def. 3.8 and its alternative characterization (acooc) in Lemma 3.12). Neither of these notions can be expressed for a pre-translation, and thus we require a more specific definition of a translation: Almost all components of the observational program calculi need to be translated, i.e. also a translation of contexts, generalized closing substitutions and convergence predicates is required. The advantages of these translations are: i) The required notion of convergence equivalence can be defined. ii) The notion of observational correctness can be introduced, which provides a systematic method to prove adequacy of the translation (see Proposition 3.16). iii) As argued in the introduction, if a context together with a convergence predicate is viewed as a specification of a program, then the more specific definition of a translation ensures that the specification itself can be translated.

Translations between Observational Program Calculi

In the following and in the remainder of the paper we consider translations between observational program calculi. Definition 3.5. A translation T : K ! K 0 between two observational program calculi K = (P, Clos, C, O, T , type, S) and K 0 = (P 0 , Clos 0 , C 0 , O 0 , T 0 , type 0 , S 0 ) is a mapping from types to types T : T ! T 0 , programs to programs T : P ! P 0 , contexts to contexts T : C ! C 0 , and observation predicates to observation predicates T : O ! O 0 , such that:

1. (p, ⌧ ) 2 type implies (T (p), T (⌧ )) 2 type 0 and (C, ⌧ 1 , ⌧ 2 )) 2 type implies (T (C), T (⌧ 1 ), T (⌧ 2 )) 2 type 0 ;
2. closedness is preserved for all p: p 2 Clos =) T (p) 2 Clos 0 ;

3. for all types ⌧, ⌧ 0 , contexts C 2 C ⌧,⌧ 0 and all p 2 P ⌧ : C(p) 2 Clos =) T (C)(T (p)) 2 Clos 0 ; and 4. generalized closing substitutions are preserved, i.e., T (S) ✓ S 0 . ⇤

Clearly, every such translation is also a pre-translation according to Definition 3.1 if it is restricted to types and programs only. The notion of translations is more restrictive as it must also apply to contexts, observation predicates, and even be compatible w.r.t. closedness with contexts as stated in condition 3. Conditions 2 and 4 are rather natural even though of technical nature. The relevance of condition 4 will become clear in Lemma 3.12. Conditions 2 and 3 are su ciently relaxed to also permit for example dead code elimination that may turn non-closed (i.e. open) programs into closed ones.

Since convergence predicates can be translated arbitrarily, we can also compare observational program calculi with di↵erent numbers of convergence predicates. Given an observation predicate în O, we will write T

for its translation T ( )f or convenience. We will also often use the notational convenience to indicate components in the image of a translation T : K ! K 0 by a prime. Lemma 3.6. Let T : K ! K 0 be a translation. Then T (P ⌧ ) ✓ T (P)

T (⌧ ) and T (C ⌧ 1 ,⌧ 2 ) ✓ T (C) T (⌧ 1 ),T (⌧ 2 )
Proof. This follows from Definition 3.5, condition (1). Lemma 3.7. For all translations T :

K ! K 0 , types ⌧ 1 , ⌧ 2 , programs p of type ⌧ 1 , and contexts C of type (⌧ 1 , ⌧ 2 ): If C(p) is closed then both T (C(p)) and T (C)(T (p)) are closed.
Proof. The first implication is condition (2) and the second implication is condition (3) of Definition 3.5 of translations.

Observational Correctness

In this section we define additional properties of translations and emphasize which of these properties ensure "correctness" of the translation. Thereafter we will investigate relations between the di↵erent notions. We now consider the behavior of translations operationally, i.e. the following notion of observational correctness captures the intuition that compiled tests applied to compiled programs have the same result as in the source language, i.e. it ensures that the translation preserves and reflects the observations together with the contexts. This notion requires a translation on observational program calculi, and as we show gives a guide on how to prove adequacy of the translation. Definition 3.8. A translation T : K ! K 0 is called observationally correct (oc, for short) if it is convergence equivalent and compositional up to observations, where a translation T is:

convergence equivalent (ce) if
T (C(p)) = T (C)(T (p)) such that T (C) is a reduction context of pcf cbv , B i↵ C is a reduc- tion context of pcf cbv .
All reduction steps directly correspond, i.e. p ! p 0 i↵ T (p) ! T (p 0 ) except for reducing the constant zero? where one reduction is replaced by two reduction, i.e. R(zero? i) ! R(b) i↵ T (R(zero? i)) ! p 0 ! T (R(b)). Hence, by induction on the length of converging reduction sequences of p (T (p) resp.) convergence equivalence can be proved. Thus T B is observationally correct.

Note that convergence equivalence is often called "computational adequacy" when relating an operational semantics with a denotational semantics. However, observational correctness additionally requires (a weak form of) compositionality, which allows to translate contexts separately from programs. Of course compositionality up to observations is a generalization of usual compositionality and its variants: Definition 3.10. Let T : K ! K 0 be a translation. Then

1. T is compositional i↵ for all ⌧, ⌧ 0 2 T , for all C 2 C ⌧,⌧ 0 and p 2 P ⌧ , if C(p) is closed then T (C(p)) = T (C)(T (p)). 2. T is compositional modulo ⇠, i↵ for all types ⌧ 1 , ⌧ 2 , p 2 P ⌧ 1 , C 2 C ⌧ 1 ,⌧ 2 : if C(p) is closed, then T (C(p)) ⇠ 0 T (⌧ 2 ) T (C)(T (p)). Lemma 3.11. Let T : K ! K 0 be a translation. Then T is ( cuo) provided it is compositional or compositional modulo ⇠.
Proof. If T is compositional, then (cuo) holds obviously. Let T be compositional modulo ⇠ and assume that C(p) is closed. Then Lemma 3.7 implies that T (C(p)) and T (C)(T (p)) are closed. Lemma 2.7 is now applicable and shows that for all :T (C(p)) T ()

T (C)(T (p)) T .
Observational correctness has a more explicit description by a homomorphism-like condition:

The translation retains the results of applying contexts and then applying a convergence test.

Lemma 3.12 (Alternative characterization of (oc)). Suppose T : K ! K 0 is a translation. Then T is observationally correct if, and only if: . Let us also emphasize that Definitions 3.2, 3.5 and 3.8 are stated only in terms of observational program calculi, and hence they can be used for all calculi with such a description.

(acooc) For all ⌧, ⌧ 0 2 T , all p 2 P ⌧ 1 , C 2 C ⌧ 1 ,⌧ 2 : if C(p) is closed, then for all 2O : C(p) () T (
In the remainder of this section, we show di↵erences and similarities between the introduced properties of translations, and we give some small examples for translations.

Comparing the Properties of Translations

In this section we compare the di↵erent correctness notions and show how they are related. First, Proposition 3.4 can be extended to translations, convergence equivalence, and observational correctness: the introduced correctness properties are closed under the composition of translations: Proposition 3.13 (Closure under composition). Let K, K 0 , K 00 be program calculi, and T : K ! K 0 , T 0 : K 0 ! K 00 be translations. Then T 0 T : K ! K 00 is also a translation. For every property P from Definitions 3.2, for the properties ( ce) and ( oc) from Definition 3.8, and for the property "compositional" from Definition 3.10: if T and T 0 have property P , then so has their composition T 0 T . Proof. For adequacy, full abstractness, and the isomorphism property the claim follows from Proposition 3.4, since every translation is also a pre-translation. If T and T 0 are compositional, then clearly also T 0 T is compositional. We consider the remaining properties: T is (cuo).

Remark 3.14. We show that the previous Proposition 3. [START_REF] Chlipala | A verified compiler for an impure functional language[END_REF] does not hold for (cuo). As a counter-example let

K i = (P i , Clos i , C i , { î },
K 2 ! K 2 be the translation with T 2,3 (A) = ↵, T 2,3 (B) = and T 2,3 ([.]) = [.]. Then T 1,2 clearly is (cuo) (since all programs of P 2 diverge). Also T 2,3 is (cuo), since T 2,3 ([A]) = T 2,3 ([.])(T 2,3 (A)) = ↵ and T 2,3 ([B]) = T 2,3 ([.])(T 2,3 (B)) = .
However, the composition

T 2,3 T 1,2 is not (cuo): T 2,3 (T 1,2 (C(b))) 3 , since T 2,3 (T 1,2 (a)) = T 2,3 (A) = ↵, but ¬(T 2,3 (T 1,2 (C))(T 2,3 (T 1,2 (b))) 3 ), since T 2,3 (T 1,2 (C))(T 2,3 (T 1,2 (b))) = T 2,3 ([.])(T 2,3 (T 1,2 (b))) = T 2,3 (T 1,2 (b)) = T 2,3 (B) = .
For compositionality modulo ⇠ and cuo an extra requirement is necessary:

Proposition 3.15. Let T , T 0 be translations such that T 0 is fully abstract. If T and T 0 are compositional modulo ⇠ , then their composition T 0 T is compositional modulo ⇠. If T and T 0 are cuo, then their composition

T 0 T is cuo. Proof. We have to show that (T 0 T )(C(p)) ⇠ 00 T 0 (T (C))(T 0 (T (p))) for closed C(p). The translation T is compositional modulo ⇠, hence T (C(p)) ⇠ 0 T (C)(T (p)), and since T 0 is compositional modulo ⇠, also T 0 (T (C)(T (p))) ⇠ 00 T 0 (T (C))(T 0 (T (p))). Since T 0 is fully abstract, T (C(p)) ⇠ 0 T (C)(T (p)) implies T 0 T (C(p)) ⇠ 00 T 0 (T (C)(T (p)))
, hence the first claim holds. The second claim follows from the first and Lemma 3.11.

The following result links the operational correctness notions and the correctness notions concerning the preorders of the source and the target calculus: .T his proves p 1  ⌧ p 2 . This result also shows that observational correctness provides a method on how to prove adequacy of a translation. It is su cient to show convergence equivalence provided the translation is compositional (or even only compositional up to observation). The value of this approach is that the proof of convergence equivalence does not require to reason about all contexts which is usually hard. So observational correctness separates the contextual reasoning from the reasoning about convergence.

Note that several papers (e.g. [START_REF] Sanjabi | Fully abstract semantics of additive aspects by translation[END_REF][START_REF] Ahmed | An equivalence-preserving cps translation via multi-language semantics[END_REF]) use a similar pattern for proving adequacy (or sometimes called "equivalence reflection") of (almost) compositional translations. We also gave an abstract proof for a class of observational program calculi in [START_REF] Schmidt-Schauß | Adequacy of compositional translations for observational semantics[END_REF].

Example 3.17. For our running examples (Example 3.9), observational correctness of T incl and T B and Proposition 3.16 imply that both translations are adequate.

The following proposition shows: (ce) is in general not su cient for adequacy, and full abstractness is not implied by observational correctness. Similarly, (ce) is not even implied by full abstractness (and thus neither by adequacy).

Proposition 3.18. The following holds:

1. Convergence equivalence does not imply adequacy.

2. Observational correctness does not imply full abstractness.

3. Convergence equivalence is not implied by the conjunction of compositionality up to observations and preservation and reflection of . 2. Example 3.25 is a witness for this. Another simple example taken from [START_REF] Mitchell | On abstraction and the expressive power of programming languages[END_REF] is the identity encoding into (call-by-name) pcf with product types from pcf but without the projections fst and snd. Then, in the restricted calculus, all pairs are indistinguishable but the presence of the contexts fst [.] (⌧,⌧ 0 ) and snd [.] (⌧,⌧ 0 ) in pcf with products permits more distinctions to be made.

3.

A trivial example is given by two calculi K with p# K for all p, and K 0 with the same programs and p" K 0 for all p. For the identity translation

T (p) = p, T (# K ) = # K 0 for all p it is clear that 8p 1 , p 2 : p 1  p 2 () T (p 1 )  0 T (p 2
) holds, and that the translation is compositional up to observations, but clearly T does not preserve convergence. Our definition of translations implies that the image of a translation is also an observational program calculus: Consider a translation T : K ! K 0 , where K = (P, Clos, C, O, T , type, S) and K 0 = (P 0 , Clos 0 , C 0 , O 0 , T 0 , type 0 , S 0 ) then the image of K under T , denoted T (K), is also an observational program calculus T (K) := (T (P), T (Clos), T (C), T (O), T (T ), T (type), T (S)) where T (type) is the image of type as a relation.

Note that this definition is only possible, since contexts and programs are translated separately by T , and by the conditions in the definition of translations. We will use the symbol  00 ⌧ for the (type-indexed) observational preorder of K 00 = T (K). A further preorder for the image calculus T (K) can be defined, which only allows to compare programs with the same source types, and also only uses contexts which are applicable for source programs.

We call this preorder  T,⌧ , which is defined on K 00 = T (K) but with K-type ⌧ . It is defined as follows: let ⌧ be a K-type. For programs p 0 1 , p 0

2 2 P 0 T (⌧ ) the inequation p 0 1  T,⌧ p 0 2 holds, i↵ for all T 2 T (O), all p 1 , p 2 2 P ⌧ with T (p 1 ) = p 0 1 , T (p 2 ) = p 0 2 , and all C 2 C ⌧,⌧ 0 , such that T (C)(T (p i )) are closed for i = 1, 2: T (C)(T (p 1 )) T =) T (C)(T (p 2 ))
T . We will now show that observing the translated programs using translated contexts under type restrictions makes the same distinctions between the original and the translated programs if the translation is observationally correct and in addition closedness reflecting Theorem 3.21. Let K, K 0 be observational program calculi and T : K ! K 0 be an observationally correct and closedness reflecting translation. Let K 00 := T (K) be the image subcalculus of K 0 under T and for ⌧ 0 2 T 0 , let  00 ⌧ 0 be the observational preorder of K 00 , and for ⌧ 2 T , let  T,⌧ be the preorder on K 00 (on programs of types T (⌧ )) as defined above. Then the following holds:

1. For all types ⌧ 2 T and programs p 1 , p 2 2 P ⌧ :

p 1  ⌧ p 2 () T (p 1 )  T,⌧ T (p 2 ). 2.
If T is injective on T , then for all types ⌧ and programs p 1 , p 2 2 P ⌧ :

p 1  ⌧ p 2 () T (p 1 )  00
T (⌧ ) T (p 2 ), i.e. the restricted translation T : K ! K 00 is fully-abstract and also an isomorphism between K and K 00 T . We show that C 0 (T (p 2 )) T . Since T is injective on T , the translation

T : K ! K 00 is surjective from C ⌧,⌧ 0 ! C 00 T (⌧ ),T (⌧ 0 ) : If a triple (C 0 , ⌧ 0 1 , ⌧ 0 2 ) 2 T (type), then there is a triple (C, ⌧ 1 , ⌧ 2 ) 2 type, with T (⌧ 1 ) = ⌧ 0 1 and T (⌧ 2 ) = ⌧ 0 2 .
Injectivity on types implies that ⌧ 1 , ⌧ 2 are unique, hence surjectivity holds. Thus there is a context C with input type ⌧ , such that T (C) = C 0 . Clearly, since T is closedness reflecting, C(p 1 ) and C(p 2 ) are closed. Observational correctness and Lemma 3.12 show C 0 (T (p 1 ))

T , T (C)(T (p 1 )) T and T (C)(T (p 1 )) T =) C(p 1 ) ân d C(p 1 ) =) C(p 2 ) .T his in turn implies T (C)(T (p 2 )) T which is equivalent to C 0 (T (p 2 )) T .
Since this holds for all contexts C 0 , we have shown T (p 1 )  00 T (⌧ ) T (p 2 ). Corollary 3.22. Let K, K 0 be observational program calculi and T : K ! K 0 be an observationally correct and closedness reflecting translation, such that T is an isomorphism on the type structure, surjective on programs, contexts, and observation predicates. Then T : K ! K 0 is an isomorphism. Proof. This follows from Theorem 3.21 [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF].

For many translations, being injective on types is too strict a requirement, for instance, if a newly added data structure is compiled into existing ones. However, in these cases, provided the translation is observationally correct and closedness reflecting, part (1) of Theorem 3.21 is applicable (see also Remark 4.12 and Example 4.13).

Example 3.23. The classical Church-encoding of the untyped lambda calculus with pairs and selectors into the pure untyped lambda calculus is neither convergence equivalent nor adequate. The problem is that dynamically untyped programs like fst ( x.x) are translated into convergent programs. An observationally correct (and thus also adequate) encoding can be established if the lambda calculus with pairs is simply typed (and thus the above mentioned counter-examples are excluded) and the lambda calculus without pairs is untyped. In Section 5.2 the encodings and proofs are given in detail.

Further Examples

We provide some simple uses of translations which illustrate the introduced properties.

Example 3.24. Let pcf cbv , fix be the restriction of pcf cbv from Section 2.1 where the fixed point operators are dropped. The embedding ◆ : pcf fix ! pcf cbv is defined as the identity on types and expressions, and hence ◆ is compositional and ( ce), hence adequate by Proposition 3.16. Below in Example 4.4 we show that it is also fully abstract.

Example 3.25. We give an example of an adequate, but not fully abstract, embedding: Let pcf cbv , fix,0 be pcf cbv , fix (see Example 3.24) with the additional reduction rule pred 0 ! 0 and let pcf cbv ,0 be pcf cbv with the same modification. The embedding ◆ : pcf cbv , fix,0 ! pcf cbv ,0 is the identity on types and expressions, and hence the embedding is compositional and ( ce), hence adequate. However, the embedding is not fully abstract: The expressions p 1 = x.0 and p 2 = x.if (zero? (x 0)) then 0 else 0 are observationally equivalent w.r.t. pcf cbv , fix,0 , since pcf cbv , fix,0 is a simply typed lambda calculus where every closed expression is terminating, but are not observationally equivalent w.r.t. pcf cbv ,0 : They can be distinguished by applying both to y.?, where ? is a non-converging pcf cbv ,0 -expression. Finally, we compare call-by-name pcf and call-by-value pcf.

Example 3.26. Let pcf cbn be call-by-name pcf and pcf cbv be call-by-value pcf and let T : pcf cbn ! pcf cbv be given by the identity on types, programs, and contexts. Then T is compositional, but it is not ( ce) since, for example, the expression ( x.0) ? has di↵erent convergence behaviors in call-by-name and call-by-value pcf. Since ( x.0) ? ⇠ 0 in pcf cbn but not in pcf cbv , the translation is not fully abstract. In the converse direction, the expressions x.0 and x. if x then 0 else 0 are equivalent in pcf cbv , but not in pcf cbn , hence the translation is also not adequate.

Obtaining Full Abstractness for Language Extensions

We now consider cases and techniques where besides observational correctness and adequacy also full abstractness or even the isomorphism property of a translation can be shown. We only consider the case of language extensions or, taking a slightly more general point of view, embeddings of one language into another, which generalizes the situation of Corollary 3.22 in several respects. A typical case is that new language primitives are added to a calculus, together with their (operational) semantics, which is represented by an encoding, which is also a translation.

One issue is whether the extension is conservative, i.e. whether the embedding of the non-extended language into the extended one is fully abstract. This ensures that the newly added primitives cannot be used for distinguishing existing programs. The second issue is whether the encoding of the extended language into the base language is fully abstract. If also the embedding is fully abstract, then the extension can be viewed as 'syntactic sugar'.

Extensions and Embeddings Definition 4.1 (Extension and embedding

). An observational program calculus K is an extension of the observational program calculus K 0 i↵ there is a translation ◆ : K 0 ! K which is observationally correct, i.e. (ce) and (cuo), and which is injective on the types. In this case the translation ◆ is called an embedding. If the embedding is in addition fully abstract, then it is also called a conservative embedding.

Note that an embedding ◆ is adequate by Proposition 3.16, i.e. injective modulo ⇠, but in general not necessarily fully abstract. Informally, the embedding situation can be described (after identifying K 0 -programs with their image under ◆ and modulo ⇠) as follows: every K 0 -type is also a K-type, P 0 ⌧ ✓ P ⌧ , and C 0 ⌧,⌧ 0 can be seen as a subset of C ⌧,⌧ 0 , more precisely: C 0 ⌧,⌧ 0 is the same as {C ◆(P 0 ) | C 2 C ⌧,⌧ 0 }, (where f A is the function f restricted to the set A) and the observation predicates coincide on K 0 -programs.

K 0 K ◆(K 0 ) ◆ T
If K is an extension of K 0 , then an observationally correct translation T : K ! K 0 (the encoding), where T ◆ is the identity, has the nice consequence of T and ◆ being fully abstract under certain preconditions (see Theorem 4.6, Corollaries 4.7 and 4.8; and see also Corollary 3.22).

Conservativeness of Embeddings

We first look for the issue whether K extends K 0 conservatively, i.e. whether ◆ is a conservative embedding, or in other words; whether ◆ is fully abstract. This includes the case that there is no sensible back-translation (the encoding) T : K ! K 0 . If full abstractness of ◆ can be shown, then all equations that hold in K 0 also hold for K and thus the newly added language constructs cannot be used to distinguish the "old" programs. This property is of practical importance, since e.g. optimizations that are valid for K 0 are still valid for K (restricted to K 0 ) programs. On the other hand, disproving conservativity implies that the new constructs add expressivity to the language. A classical and paradigmatic example is the extension of the call-by-name lambda calculus (or call-by-name PCF) by a "parallel or", and the question whether this extension changes the semantics. The classical answer is "yes": the semantics is changed [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF]: a parallel-or construct por added to the call-by-name lambda calculus (call-by-name PCF) permits to observationally distinguish two functions, which were contextually equal without the extension. Therefore consider the function

F (of type o ! (o ! o ! o) ! o),
where not and and3 are defined as usual: There are other investigations into extensions and whether these are conservative. For example in [START_REF] Felleisen | On the expressive power of programming languages[END_REF] and for more calculi in [START_REF] Schmidt-Schauß | Extending Abramsky's lazy lambda calculus: (non)conservativity of embeddings[END_REF], among others, the question whether the lazy lambda calculus [START_REF] Abramsky | The lazy lambda calculus[END_REF] is conservatively extended by a strict operator was answered negatively. We will discuss larger examples for these conservativity questions in Section 5.3.

F := x. f. if and3 (f true ?) (f ? true) (not (f false false)) then x else true Then (F true) ⇠ (F false) in pcf cbn but (F true) 6 ⇠ (F
We provide a criterion for full abstractness of the embedding in the case where the extended calculus cannot be translated into the base calculus. The main idea is to use a family of translations as an approximation of a translation that cannot be otherwise represented. For example, if the translation has to deal with recursive programs (or types), then it may be possible to consider (all) the finitary approximations instead.

The following definition intuitively describes that two programs have the same sets of free variables. However, our framework has no notion of free variables, and thus the definition is given in terms of contexts and the closedness property: Definition 4.2. For p, p 0 2 P ⌧ we say p and p 0 are contextually closedness equivalent, denoted by p ⇠ = cl p 0 , i↵ for all contexts C of type (⌧, ⌧ 0 ): C(p) is closed i↵ C(p 0 ) is closed. Theorem 4.3 (Families of Translations). Let K be an extension of K 0 , i.e. with an observationally correct translation ◆ : K 0 ! K. Let J be a partially ordered index set, such that for all j 1 , j 2 , there is some j 3 2 J with j 1  j 3 and j 2  j 3 . Let {T j } j be a J-indexed family of translations T j : K ! K 0 , j 2 J such that the following conditions hold: 1. For all j 2 J: T j ◆ is the identity on O 0 and on K 0 -types. 2. for all j 2 J and for all types ⌧ 0 : (T j ◆)(p 0 ) ⇠ 0 ⌧ 0 p 0 for all K 0 -programs p 0 of type ⌧ 0 ; 3. for all j 2 J and for all K 0 -programs p 0 : (T . For contradiction, let us assume that C(◆(p 0 2 )) _ ◆ . Then there is some k 1 such that for all j 1 k 1 : T

j 1 (C)(T j 1 (◆(p 0 1 ))) is closed and T j 1 (C)(T j 1 (◆(p 0 1 ))) ^0
. There is also some

k 2 such that for all j 2 k 2 : T j 2 (C)(T j 2 (◆(p 0 2 ))) is closed but T j 2 (C)(T j 2 (◆(p 0 2 ))) _0
. Due to the condition on the order, there is some common k 3 2 J with k 1  k 3 , k 2  k 3 such that for all j k 3 : T j (C)(T j (◆(p 0 1 ))) and T j (C)(T j (◆(p 0 2 ))) are closed, and

T j (C)(T j (◆(p 0 1 ))) ^0 , but T j (C)(T j (◆(p 0 2 ))) _0 . By condition (3), T j (C)(p 0 1 ) as well as T j (C)(p 0
2 ) are closed, and by condition (2), we obtain

T j (C)(p 0 1 ) ^0 and T j (C)(p 0 2 ) _0 , for j k 3 . Now T j (C)(p 0 1 ) ^0 and p 0 1  0 0 ,⌧ p 0 2 imply T j (C)(p 0 2 ) ^0
, which is a contradiction.

Note that the condition (3) of Theorem 4.3 is satisfied in a program calculus that has a (common) notion of free and bound variables, and if the translation keeps the free variables. cbv be the identity on types and expressions in the two PCF-variants. The embedding ◆ is compositional and ( ce), and hence adequate. While there appears to be no (recursioneliminating) translation T : pcf cbv ! pcf cbv , fix , it is possible to find a family of translations T j as in Theorem 4.3: Let T j be the translation that unfolds every occurrence of a fixed point operator j times and then replaces all further occurrences by ?, where (pred 0) is such a diverging expression, and thus there are diverging expressions for all types. Induction on the length of reductions shows that the condition of Theorem 4.3 holds, hence ◆ is fully abstract.

Criteria for Full Abstractness of Embeddings and Encodings

We now consider the case that there exists a translation T from the larger into the smaller calculus and we provide criteria to show full abstractness for the translation T in this case, thereby extending and generalizing Corollary 3.

:i f C A (p) is closed then C A (p) ,C B (p) ĥo lds.
Theorem 4.6 (full abstractness for extensions). Let K be an extension of K 0 , i.e. there is an embedding ◆ : K 0 ! K, and let the encoding T : K ! K 0 be an observationally correct translation such that T ◆ is the identity on T 0 and on O 0 , and for all types ⌧ 0 and all K 0 -programs p 0 of type ⌧ 0 : (T ◆)(p 0 ) ⇠ ⌧ 0 p 0 , and (T ◆)(p 0 ) ⇠ = cl p 0 . Then ◆ is fully abstract, i.e. a conservative embedding, and T is adequate. If in addition T is closedness reflecting and the following "surjectivity" condition ( †) holds:

( †) For all K-types ⌧ 1 , ⌧ 2 and C 0 2 C 0 T (⌧ 1 ),T (⌧ 2 ) , and every set M ✓ T (P ⌧ 1 ) of programs with |M |  2, there is a context C 2 C ⌧ 1 ,⌧ 2 with T (C) ⇡ M C 0 ; then T is also fully abstract.

Proof. Note that the conditions imply that ◆ is injective on the types, and on observation predicates, and that T is surjective on types, and on observation predicates. Adequacy of ◆ and T follows from Proposition 3.16.

First we show full abstractness of ◆. Let p 1 , p 2 be K 0 programs of type ⌧ , let p 1  0 ⌧ p 2 and let C be a K-context of the right type such that C(◆(p 1 )), C(◆(p 2 )) are closed and

C(◆(p 1 ))

.W e have to show that C(◆(p 2 ))

.S ince T is a translation, Lemma 3.7 implies that T (C(◆(p 1 ))), T (C(◆(p 1 ))), T (C)(T (◆(p 1 ))), and T (C)(T (◆(p 2 ))) are closed. The assumption of this theorem, . From p 1  ⌧ p 2 we now derive C(p 2 ) .A gain, observational correctness of T can be applied and shows that T (C)(T (p 2 ))

8p 0 : (T ◆)(p 0 ) ⇠ = cl p 0 , implies that T (C)(p 1 ), T (C)(p 2 ) are closed. Since T ◆ is the identity on T 0 , T (◆(p 1 )) has type ⌧ . Observational correctness of T implies T (C)(T (◆(p 1 ))) T . Since T (◆(p 1 )) ⇠ 0 ⌧ p 1 , ⇠ 0 ⌧ is a congruence,
T . This is equivalent to C 0 (T (p 2 )) T , again using C 0 ⇡ M T (C). Since the context C 0 2 C 0 ⌧,⌧ 0 was chosen arbitrarily, we have T (p 1 )  0 T (⌧ ) T (p 2 ). Surjectivity of T on contexts leads to an easy-to-check specialization of the conditions of Theorem 4.6: Corollary 4.7. If all preconditions of Theorem 4.6 hold, but ( †) is replaced by: For all

K-types ⌧ 1 , ⌧ 2 , T is a surjective mapping C ⌧ 1 ,⌧ 2 ! C T (⌧ 1 ),T (⌧ 2 )
, then the claims of Theorem 4.6 hold.

Injectivity of T on types is a special case of the condition in Theorem 4.6: Corollary 4.8 (full abstractness for extensions; injectivity). All claims of Theorem 4.6 also hold, if 1. ◆ is closedness reflecting; and 2. all preconditions of Theorem 4.6 hold, but ( †) is replaced by: T is injective (i.e. bijective) on types.

Proof. Assume injectivity of T on types. Given ⌧ 1 , ⌧ 2 and C 0 2 C T (⌧ 1 ),T (⌧ 2 ) , we define C := ◆(C 0 ) with ◆(C 0 ) 2 C ⌧ 1 ,⌧ 2 by the injectivity assumption, and have to show

C 0 ⇡ T (P⌧ 1 ) T (◆(C 0 )): Let p 0 2 T (P ⌧ 1 ) ✓ P T (⌧ 1 ) . It holds that C 0 (p 0 ) is closed i↵ (T ◆)(C 0 )(T ◆)(p 0 ) is closed i↵ (T ◆)(C 0 )(p 0
) is closed: The first equivalence follows since T and ◆ are closedness reflecting and property (3) of the definition of a translation, and the second equivalence follows from the precondition (T ◆)(p 00 ) ⇠ = cl p 00 for all p 00 . The precondition (T ◆)(p 0 ) ⇠ 0 T (⌧ 1 ) p 0 for all p 0 2 T (P ⌧ 1 ) ✓ P T (⌧ 1 ) and observational correctness of T and ◆ show that for all p 0 2 T (P

⌧ 1 ): if C 0 (p 0 ) is closed, then C 0 (p 0 ) , T (◆(C 0 ))(p 0 )
.H ence the relation C 0 ⇡ T (P⌧ 1 ) T (◆(C 0 )) holds. Remark 4.9. In general, Theorem 4.6 and Corollary 4.8 will not hold without assumption ( †) or the assumption that T is injective on types. To see this, let K 0 be the observational program calculus with one type A, four programs a 1 , a 2 , a 3 , a 4 of type A, the identity as well as a context

f 2 C A,A with f (a 1 ) = f (a 3 ) = a 3 , f (a 2 ) = f (a 4 ) = a 4 ,
.H ence b 1 ⇠ b 2 . Let T : K ! K 0 be defined by T (A) = T (B) = A, T (f ) = f , T (a i ) = a i , T (b 1 ) = a 1 , and
T (b 2 ) = a 2 . Note that T is not injective on the types, since T (A) = T (B) = A.
Then T is compositional and convergence equivalent, hence also observationally correct. Moreover, the embedding ◆ : K 0 ! K satisfies that T ◆ is the identity on K 0 . But T is not fully abstract, since b 1 ⇠ b 2 , but T (b 1 ) = a 1 and T (b 2 ) = a 2 , and a 1 6 ⇠ a 2 . Thus, we cannot omit the injectivity assumption in Corollary 4.8.

The example also shows that the condition ( †) is necessary in Theorem 4.6, since it does not satisfy this condition for the type B, elements a 1 , a 2 and context f 2 C A,A , there is no context C 2 C B,B , such that T (C) ⇡ a 2 f , since T (C) can only be Id , and a 2 ,b ut f (a 2 ) _ .

Remark 4.10. Note that closedness reflection does not follow from observational correctness of a translation, and that closedness reflection of T is a necessary condition for Theorem 4.6 and Corollary 4.8: Therefore consider the following example: Let K consist of four programs, p, q, p 0 , q 0 , where p, p 0 , q 0 are closed and q is open, and two contexts

C 1 , C 2 with C 1 (p) = q, C 1 (q) = q, C 1 (p 0 ) = q 0 , C 1 (q 0 ) = q 0 , and C 2 (p) = p, C 2 (q) = p, C 2 (q 0 ) = p 0 , C 2 (p 0 ) = p 0 . Assume that q 0
_ , but all other programs converge. Let K 0 be a subcalculus of K consisting only of p 0 , q 0 , C 1 , C 2 . Let T : K ! K 0 with T (p) = p 0 , T (q) = q 0 , T (p 0 ) = p 0 and T (q 0 ) = q 0 and T (C i ) = C i for i = 1, 2. Let ◆ : K 0 ! K be the identity. Then T and ◆ are observationally correct. However, T is not closedness reflecting, since

C 1 (p) is open, but T (C 1 )(T (p)) = T (C 1 (p)) = q 0 is closed.
Then T is also observationally correct, hence adequate, but not fully abstract, since p ⇠ q (only C 2 is closing and makes them equal), but p 0 6 ⇠ q 0 . All the assumptions of Corollary 4.8 are satisfied, with the exception that T is not closedness reflecting, and the conclusion of the corollary is not valid. Hence, closedness reflection of T is a required condition.

Example 4.11. Let pcf cbv ,let be the extension of pcf cbv (see Section 2.1) by strict letexpressions of the form (let x = p 1 in p 2 ). The reduction of pcf cbv ,let extends pcf cbvreduction by reducing first inside the binding of let-expressions and then applying the rule

(let x = v in p 2 ) ! p 2 [v/x] if v is a value. A translation T : pcf cbv ,let
! pcf cbv which removes the let-expressions can be defined as follows: T (let x = p 1 in p 2 ) := ( x.T (p 2 )) T (p 1 ) and for all other cases T translates the expressions homomorphically with respect to the term structure. T is the identity on types (and hence also injective on types) and can be extended to contexts in the obvious way. The embedding ◆ : pcf cbv ! pcf cbv ,let is the identity on types, expressions and contexts. Obviously, T ◆ is the identity on pcf cbv -expressions. Both translations T, ◆ are compositional and also convergence equivalent, since let-reductions exactly correspond to call-by-value beta-reductions and reductions inside let-bindings exactly correspond to reductions inside arguments of applications. Choosing C 0 = pcf cbv and C = pcf cbv ,let the first conditions of Theorem 4.6 hold and since T is injective on types, we can apply Corollary 4.8 and conclude that T and ◆ are fully abstract. Moreover, since T is surjective, T is also an isomorphism, and thus we can conclude that strict let-expressions are syntactic sugar. The following remark and example 4.13 shows that Corollary 4.8 may be inapplicable for showing full abstractness, and that the more complex preconditions of Theorem 4.6 have to be checked. (The translation T in the example is not injective on types.) This example highlights the fact that Corollary 4.8 cannot be applied to show full abstractness when the translation is given by an encoding of an abstract data type (such as products or lists in the lambda calculus) in terms of an implementation type in a subcalculus.

Remark 4.12. The Examples 3.3 and 3.9 exhibit a limitation for full abstractness of translations. The translation T in these examples which encodes the data type Boolean into non-negative integers is not fully abstract. We observe that this encoding is not really oneto-one on the respective types. The argument given in Example 3.3 and showing that T is not fully abstract, appears to be adaptable also to other similar situations.

If two data types are very similar, then Theorem 4.6 and in particular Corollary 4.7 can be applied to the encoding T : Example 4.13. Let us define pcf Two , which is pcf cbv extended by a copy of the Boolean data type. I.e., there is an extra data type Two of two logical constants true 0 , false 0 . The if-then-else is also permitted for this data type. Then the translation T : pcf ! b where b is a Boolean value. Let K be an extension of K 0 with n-ary functions, i.e., there are also n-ary function types (⌧ 1 , . . . , ⌧ n ) ! ⌧ , n-ary lambda-expressions, written as (x 1 , . . . , x n ).p, and n-ary applications p (p 1 , . . . , p n ). Lambda-reduction in K is permitted as ( (x 1 , . . . , x n ).p) (p 1 , . . . , p n ) ! p[p 1 /x 1 , . . . p n /x n ]. We assume that there are no explicit tuples and no variables of a tuple type. As above, we only observe convergence of Boolean expressions. It is not hard to see that the ⌘-axiom holds for all expressions of function type. That is, for p : ⌧ 1 ! ⌧ 2 and x not free in p, we have p ⇠ x.(p x) and for p : (⌧ 1 , . . . , ⌧ n ) ! ⌧ , the equivalence p ⇠ (x 1 , . . . , x n ).(p (x 1 , . . . , x n )) holds for fresh x 1 , . . . , x n . The embedding ◆ : K 0 ! K is defined as the identity on types, expressions and contexts, and the translation T translates types

Two ! pcf cbv with T (true 0 ) = true, T (false 0 ) = false, T (Two) = o
(⌧ 1 , . . . , ⌧ n ) ! ⌧ to ⌧ 1 ! . . . ⌧ n ! ⌧ , T ( (x 1 , . . . , x n ).p) = x 1 . . . . x n .T (p), T (p(p 1 , . . . , p n )) = (((T (p) T (p 1 )) . . .) T (p n ))
, and all other constructs homomorphically with respect to the term structure. The following properties hold: T ◆ is the identity, the embedding ◆ is compositional and also ( ce). The translation T is also compositional, since there are no special syntactic conditions. The translation is also ( ce), since reductions p 1 ⇤ ! p 2 for closed p 1 can be translated as T (p 1 ) ⇤ ! T (p 2 ). We argue that the condition ( †) of Theorem 4.6 holds. The main argument is that ⌘ holds, so that for given K-types ⌧ 1 , ⌧ 2 , finite set M of programs, and a context

C 0 2 C 0 T (⌧ 1 ),T (⌧ 2 ) , a context C 2 P ⌧ 1 ,⌧ 2 with T (C) ⇡ M C
0 can be found: for this (inductive) construction of C, eta-long normal forms are used. Since the cardinality of the set M that has to be covered is at most two, it is always possible to find fresh variable names when the eta-rule has to be applied to a context where the hole is in the scope of the fresh variable.

Remark 4.15. In contrast to the previous example, Theorem 4.6 cannot be applied to an extension of pcf cbv by n-ary functions, since the condition ( †) does not hold. It is su cient to show that T is not surjective on the programs of a fixed type: Let ⌧ := ((◆ ! ◆ ! ◆), ◆, ◆) ! ◆ and consider the "partial application"

p 1 := x 1 . x 2 .(x 1 x 2 ) of type T (⌧ ) = ((◆ ! ◆ ! ◆) ! ◆ ! ◆ ! ◆.
Then there is no p of type ((◆ ! ◆ ! ◆), ◆, ◆) ! ◆ such that T (p) ⇠ p 1 . For contradiction assume otherwise, then obviously T (p) cannot be ?. Hence p converges and we can assume that p is equivalent to a lambda-expression in the extension: (y 1 , y 2 , y 3 ).p 0 . Then T ( (y 1 , y 2 , y 3 ).p 0 ) p 0 1 p 0 2 = ( y 1 . y 2 . y 3 .T (p 0 )) p 0 1 p 0 2 always converges. However, p 1 ( x.?) 0 diverges, hence p 1 is not an image of an expression of type ⌧ under T . Note that the key to this counter-example is the failure of (⌘) in pcf cbv with respect to observational equivalence.

Applications and Specializations

In this section we first consider some specializations of our framework and discuss their consequences. Thereafter we present the example of Church's encoding of pairs in the callby-value lambda-calculus as a worked-out example for a translation between observational program calculi. Finally, we provide examples for more sophisticated translations which fit into our framework and whose correctness proofs were already given in other publications.

Specializations

We discuss specializations of program calculi and their consequences for reasoning about the correctness of translations in our framework.

No closedness:. If the distinction closed/nonclosed does not play a role in the specific application, then the following simplification of observational program calculi is possible: All programs are considered as closed, i.e. Clos is the set of all programs and the closing substitutions S can be chosen as only the empty context, perhaps for all type combinations. Then all prerequisites of lemmas, propositions, and theorems concerning closedness hold.

No types:. Those calculi can be modelled by a single type, thereby simplifying and trivializing the typing conditions.

No closedness and no types:. If a calculus is untyped, and closedness is irrelevant, then we combine the simplifications above. The only remaining condition in Definition 2.4 of translations is condition (4), which could be satisfied by requiring T ([.]) = [.], if only the empty context is chosen in the modeling as closing substitution.

Free variables instead of closedness:. We consider calculi where instead of the abstract notion of closedness, there is an explicit notion of free variables and the usual binding laws are valid: Assume there is a set V of variables and functions FV :

P ! V and FV : C ! V ⇥ V, where FV(C) = (V 1 , V 2 ) is written V 1 ! V 2 . Assume that FV(C(p)) = V 2 [ (V 3 \ V 1 ) for FV(p) = V 3 , and FV(C) = V 1 ! V 2 . Also, FV(C 1 C 2 ) = (V 2 [ V 3 ) ! (V 4 \ V 1 ) [ V 2 , where FV(C 1 ) = V 1 ! V 2 and FV(C 2 ) = V 3 ! V 4 .
We also say that p is closed i↵ FV(p) = ;. If for a considered translation T , we know that it maps V ! V 0 , and otherwise keeps the mapping behavior, i.e. T (FV(p)) = FV(T (p)) and

T (FV(C)) = T (V 1 ) ! T (V 2 ) for FV(C) = V 1 ! V 2 ,
then our methods and theorems are applicable, since following holds:

• T is closedness reflecting.

• In Theorem 4.3 the condition (3) is valid, and so it can be applied without further checking this condition.

• Theorem 4.6 can be applied without checking the closedness equivalence condition (T ◆)(p 0 ) ⇠ cl p 0 , since it holds automatically. • Corollary 4.8 is applicable without checking closedness conditions.

The same holds, if the translations are restricted in Definition 3.5, such that conditions (2) and ( 3) must be equivalences.

A Complete Example: Pair Encoding in the Typed Lambda Calculus

In this section we give a worked-out example for our framework of translations on observational program calculi. We recall the call-by-value lambda calculus with a fixed point operator and present its observational semantics on the basis of convergence. We illustrate that Church's encoding of pairs is observationally correct under typing restrictions and show why Church's encoding of pairs fails to be observationally correct in the untyped case.

The ) is the calculus without pairs and selectors and will be used as the target language. We use P cbv (Val cbv , resp.) for the set of cbv -expressions ( cbv -values, resp.). We assume that the distinct variable convention holds for all expressions, i.e. that the bound variables of an expression are all distinct and free variables are distinct from bound variables.

For both calculi we require call-by-value evaluation contexts E which are introduced in Fig. 2. The reduction rules for both calculi are defined in Fig. 3. The small step reduction ! pair of pair is the union of all four rules, and the small step reduction ! cbv of cbv is the union of the first two rules. We assume that reduction preserves the distinct variable convention by implicitly performing ↵-renaming if necessary.

The Removing Pairs. We will mainly investigate the translation enc of pair into cbv as defined in Fig. 4 under di↵erent restrictions. The translation performs the classical removal of pairs as given by Church. Note that conversely, it is trivial to encode cbv into pair via the identity translation inc(s) = s.

(sel-f) E[fst (w 1 ,w 2 )] ! E[w 1 ] (sel-s) E[snd (w 1 ,w 2 )] ! E[w 2 ]
Since abstractions are translated into abstractions and pairs and selectors are translated into abstractions, obviously the following holds: ). Nevertheless, we cannot prove reflection of convergence, since the following counterexample shows that the implementation of pairs is not correct in the untyped setting.

Example 5.3. Let t := fst( z.z). Then t" pair , since t is irreducible and not a value. However, the translation enc(t) results in the expression t 0 := ( p.p ( x. y.x)) ( z.z), which reduces by some ( -cbv)-reductions to x. y.x, hence enc(t)# cbv . This is clearly not a correct translation, since it removes an error. Therefore, the observations are not preserved by this translation. This example also shows that enc is not adequate, since it invalidates the pair p 2 , since enc(t 0 ) = t 0 , and hence enc(t 0 ) = t 0  cbv t 0 = enc(t), but t 0 6  pair t by the arguments above. One potential remedy to the failure of the untyped approach to correctness of translations is to distinguish divergence from typing errors. From a di↵erent point of view, this simply means that only correctly typed programs should be considered by a translation.

One solution to prevent the counter example 5. ⌧ for every type ⌧ . For typing, we treat pairs, projections, the unit value, and the operator fix as a family of constants which are indexed by their type, e.g. unit ⌧ , fix ⌧ , . . ., but in abuse of notation we omit these indexes in the following. However, for the sake of completeness, we present the type schemes of the constants in Fig. 5. This defines the typing-function type ⌧ pair . Type safety can be stated by a preservation theorem for all expressions and a progress theorem for closed expressions. The set Clos ⌧ pair are all typed closed expressions and O ⌧ pair = {# pair } where # pair is restricted to P ⌧ pair -expressions. The condition of observational program calculi in Definition 2.4 can easily be satisfied by defining S ⌧ pair to be the composition closure of the contexts of the form ( x. [.] ⌧ ) v, where v is a closed value. Note that for every type there is a closed value. Now it is easy to prove adequacy via observational correctness of the translations. Proposition 5.4. For ⌧ pair , the (correspondingly restricted) translation enc : ⌧ pair ! cbv where types ⌧ 2 T ⌧ pair are translated into the type Exp is compositional and convergence equivalent, and hence observationally correct and adequate.

Proof. Compositionality follows from the definition of enc (see Fig. 4). Lemma The extension situation could perhaps be regained by a System F-like type system, which we leave for future research. Here we just observe that the use of a simple type system for cbv is insu cient since the encoding of pairs with components of di↵erent types cannot be simply typed. (The same holds for Hindley-Milner polymorphic typing.) In [START_REF] Schmidt-Schauß | Adequacy of compositional translations for observational semantics[END_REF] we have shown that an adequacy result also holds if nondeterminism is added to both calculi, and if arbitrary expressions (instead of just values) are allowed as components of pairs.

Larger Examples for Translations

In this section we report on several examples of more complex translations, which fit into the framework presented in this paper (and also inspired us to work on this paper). Often the used methods are specializations of the presented techniques. The examples are far more complex than the one presented in the previous sections, so we only give an overview.

Comparing Concurrency Primitives. The call-by-value lambda calculus with futures [START_REF] Niehren | A concurrent lambda calculus with futures[END_REF][START_REF] Sabel | A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations[END_REF] is the core language of Alice ML [START_REF]The Alice Project[END_REF]. In its original formulation it has so-called handled futures as its basic synchronization primitive. These are variables whose value is initially not known, but it may become available in the future. From this view handled futures behave like single assignment variables, since the value of a future can only be assigned once. Synchronization between threads is possible by letting threads wait for the value of a handled future and synchronizing them by assigning a value to the future.

This motivated the question whether these handled futures are as expressive as other more common concurrency primitives, like concurrent bu↵ers, i.e. synchronizing memory cells (that are either filled or empty). In [START_REF] Schwinghammer | Correctly translating concurrency primitives[END_REF] this question is investigated. Starting from an implementation of concurrent bu↵ers using handled futures and memory cells, and an implementation of handled futures using bu↵ers, three languages L b , L h , and L bh (where L bh is the language containing both primitives) are defined, and then translations (in the sense of Definition 3.5) between them were analyzed by describing the embeddings and the encodings of one primitive by the other one. All calculi are observational program calculi, equipped with may-and should-convergence as observations. Our technique helped to show observational correctness of all the translations, and thus also all the translations are adequate. The proofs are split into showing compositionality and convergence equivalence, where hard parts are to show convergence equivalence: This required to analyze and compare the interplay between small-step reduction sequences of the di↵erent calculi. Moreover, almost all the translations are shown to be fully abstract in [START_REF] Schwinghammer | Correctly translating concurrency primitives[END_REF] where a similar technique like our Theorem 4.6 is used. Also the new Theorem 3.21 is applicable to these translations which further strengthens the results of [START_REF] Schwinghammer | Correctly translating concurrency primitives[END_REF] An exception is the translation that encodes bu↵ers by handles which is conjectured but not shown to be fully abstract. However, as in Example 4.12, the bu↵er type was encoded into another type so that the translation was not injective on types, and this prevented us from applying the extension theorem.

Proving Conservativity of Concurrent Haskell. Adding concurrency to a sequential programming language usually changes the semantics of the language, since e.g. nondeterminism is introduced, which cannot be expressed by the sequential language. I.e., there is no adequate translation from the concurrent extended language into the sequential one. The interesting question which arises in this setting is whether the new expressivity added by concurrency can distinguish programs of the sequential language. If this is not the case, then the sequential language can be conservatively embedded into the concurrent extension and all equations and correct transformations for the sequential programs still hold in the extension. This question is of practical interest, since for instance an optimizing compiler for the sequential language remains correct for the semantics of the extended language.

In [START_REF] Sabel | Conservative concurrency in Haskell[END_REF] this question was analyzed for the sequential, pure core language of Haskell and three extensions: The first extension is Concurrent Haskell [START_REF] Jones | Concurrent Haskell[END_REF] which adds concurrent threads and bu↵ers in Haskell's IO-monad (so-called MVars) to Haskell. The second one extends Concurrent Haskell by concurrent futures, i.e. the value of a concurrent computation in a thread can be accessed by a name reference. The first and the second extension are modeled by a process calculus called CHF [START_REF] Sabel | A contextual semantics for Concurrent Haskell with futures[END_REF] which is an observational program calculus, and uses may-and should-convergence as observations. For both extensions their conservativity was shown in [START_REF] Sabel | Conservative concurrency in Haskell[END_REF], i.e. the functional core language can be conservatively embedded into both extensions. The third extension adds so-called lazy futures to the calculus, which are concurrent futures whose computation only starts if their value is demanded by some other thread. A counter-example in [START_REF] Sabel | Conservative concurrency in Haskell[END_REF] disproves conservativity of this extension.

The used proof methods are custom tailored for the specific language CHF. However, the languages fit into our framework insofar as they are all observational program calculi and as convergence equivalence is used to prove the conservativity result.

Correctness of Abstract Machines. Proving correctness of an abstract machine w.r.t. a given program calculus fits into our framework, where the translation must map programs into machine states. For such a translation an obvious requirement is convergence equivalence, since this ensures that the machine is a correct evaluator for the programs. If the machine performs optimizations like e.g. garbage collection, then also observational correctness and hence adequacy of the translation is desirable.

In [START_REF] Sabel | Semantics of a Call-by-Need Lambda Calculus with McCarthy's amb for Program Equivalence[END_REF] correctness of an abstract machine for a non-deterministic call-by-need lambda calculus with McCarthy's amb-operator [START_REF] Mccarthy | A Basis for a Mathematical Theory of Computation[END_REF] was shown, by proving convergence equivalence and in [START_REF] Sabel | An abstract machine for Concurrent Haskell with futures[END_REF] correctness of an abstract machine for the CHF-calculus modelling Concurrent Haskell with futures [START_REF] Sabel | A contextual semantics for Concurrent Haskell with futures[END_REF] was shown. In both cases may-and should-convergence are the observations of the calculi and the machines. Also observational correctness of the translation holds where a compositional translation of the form T (e) = he, ;, . . . , ;i and T (C) = f where f he, . . .i = hC[e], ;, . . . , ;i must be used. Here he, ;, . . . , ;i means a machine state where all components (heap, stacks, etc.) are empty and e is the currently evaluated expression.

Correctness of an STM-Implementation. In [START_REF] Schmidt-Schauß | Correctness of an STM Haskell implementation[END_REF] an implementation of software transactional memory in Haskell was shown to be adequate by using the methods presented in this paper. As a specification a process calculus SHF was given which obviously ensures atomic execution of software transactions, by performing transactions by big-step rules isolated and in a sequential manner. Then a concurrent implementation was introduced as a modification of SHF, called CSHF, which allows concurrent execution of transactions and performs logging and roll-back in case of conflicting transactions. Both calculi are observational program calculi and use may-and should-convergence as observations. The translation from SHF to CSHF is the identity, since every SHF-process is also a CSHF-process (but not vice versa). After proving convergence equivalence of the translation (by analyzing and comparing both small-step reduction relations), observational correctness and adequacy follows, since the translation is obviously compositional. CIU Theorems. In [START_REF] Schmidt-Schauß | On generic context lemmas for higher-order calculi with sharing[END_REF] a framework for proving context lemmas and CIU-theorems for so-called sharing observational program calculi was presented, including may-, must-and should-convergence as possible observations. The generic proof of the context lemma requires that reduction in the underlying observational program calculus does not duplicate arbitrary expressions. However, also a variant of the context lemma for non-sharing calculi, like the lazy lambda calculus etc., was proved, which is a CIU-Theorem, i.e. all closing substitutions have to be considered. The generic proof of the CIU-Theorem uses the translation techniques presented in this paper: The non-sharing language is extended by a let-construct and reduction is modified to adapt it to sharing. Then a translation for removing the letconstruct is defined and shown to be observationally correct and thus adequate. This result finally allows to transfer the context lemma along this translation resulting in the CIU-Theorem. An analogous technique was also used in [START_REF] Sabel | A two-valued logic for properties of strict functional programs allowing partial functions[END_REF] for a higher-order, polymorphically typed call-by-value programming language which is used inside a logic for proving properties about programs.

The Lazy Lambda Calculus and the Call-by-Need Lambda Calculus. In [START_REF] Schmidt-Schauß | Simulation in the call-by-need lambda-calculus with letrec[END_REF] it was shown that the call-by-need lambda calculus with letrec-expressions (called L need ) is isomorphic with the lazy lambda calculus (called L lazy ), which are both observational program calculi. Since the calculi are deterministic, may-convergence is used as the observation. The technique to show isomorphism uses two translations W : L need ! L name and N : L name ! L lazy , where L name is the lazy lambda calculus with letrec-expressions using call-by-name reduction. The translation W is the identity translation and changes the evaluation strategy. Convergence equivalence of W is shown by using a further call-by-name calculus which unfolds all letrec-expressions by infinite trees. Since also the embedding An analogous result with similar techniques was obtained in [START_REF] Schmidt-Schauß | Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq[END_REF] for the extension of all calculi by data constructors, case-expressions and Haskell's seq-expressions.

(Non)conservative Embeddings. An investigation on embeddings among the extensions of the lazy lambda calculus, where the extension is by a seq or/and a case-construct together with data constructors and for the cases of untyped and typed calculi is undertaken in [START_REF] Schmidt-Schauß | Extending Abramsky's lazy lambda calculus: (non)conservativity of embeddings[END_REF][START_REF] Schmidt-Schauß | Extending Abramsky's lazy lambda calculus: (non)conservativity of embeddings[END_REF], where embeddings are analyzed for being conservative or not.

Related Work

In this section we discuss several related works where correctness of translations and compilations is taken into account. We first list some adequacy and full abstractness results for translations between program calculi with observational semantics. We then discuss further approaches concerning translation correctness. Due to the lot of work in this research area, this overview is not complete but rather a selection of works.

Fully-Abstract Translations. In [START_REF] Ritter | A fully abstract translation between a lambda-calculus with reference types and Standard ML[END_REF] translations from the core of Standard ML into a typed lambda calculus and vice versa are given and proved to be fully abstract. Both calculi are equipped with contextual equivalences and thus fit into the framework of observational program calculi. However, the proof uses bisimilarities to obtain full abstractness results, and thus uses calculus-specific methods.

In [START_REF] Mccusker | Full abstraction by translation[END_REF] a translation from the lazy lambda calculus into FPC is shown to be fully abstract, where a semantic model for FPC is used. Also the fact that adequate (and fully abstract) translations compose is exploited.

Sanjabi and Ong [START_REF] Sanjabi | Fully abstract semantics of additive aspects by translation[END_REF] develop a translation from an aspect-oriented language to an MLlike language. Both languages use contextual equivalence and their approach is similar to our suggested technique: They show observational correctness of the translation by proving convergence equivalence and compositionality, to obtain adequacy of the translation. Since full abstractness for the first proposed translation fails, they extend the source language such that full abstractness is finally obtained.

Another approach to obtain fully abstract translations is taken in [START_REF] Ahmed | Typed closure conversion preserves observational equivalence[END_REF][START_REF] Ahmed | An equivalence-preserving cps translation via multi-language semantics[END_REF] where the translations are modified such that the translation of types restricts the set of target contexts in such a way, that any translated program can only be plugged in those target contexts which can also be found as a translated source context. One drawback of this method is that a rich type system is necessary in the target calculus. In [START_REF] Ahmed | Typed closure conversion preserves observational equivalence[END_REF] it was shown that a typed closure conversion defined in [START_REF] Morrisett | From system F to typed assembly language[END_REF] for a System F like language is fully-abstract, while in [START_REF] Ahmed | An equivalence-preserving cps translation via multi-language semantics[END_REF] full abstractness of a translation from simply typed lambda calculus into System F is shown. Both full abstractness results are obtained using logical relations and thus do not use our techniques. Fournet et.al. [START_REF] Fournet | Fully abstract compilation to JavaScript[END_REF] use a similar approach for showing full abstractness of a translation from an ML-like language into JavaScript. Both languages are equipped with a contextual equivalence and fit into our framework of observational program calculi. The translation is performed in two steps, where the first step is a compositional translation. Full abstractness is ensured by using type-directed wrappers in the translation. In contrast to [START_REF] Ahmed | Typed closure conversion preserves observational equivalence[END_REF][START_REF] Ahmed | An equivalence-preserving cps translation via multi-language semantics[END_REF] no logical relations are used for the proof, but a bisimilarity in the ML-like language which coincides with contextual equivalence.

Adequate Translations. Adequate translations (with certain additional constraints) between call-by-name and call-by-value versions of PCF are considered in [START_REF] Riecke | Fully abstract translations between functional languages[END_REF] where observational semantics are used and thus all the calculi are observational program calculi. The proof technique uses denotational models which are fully abstract w.r.t. the observational equivalence. The adequacy results are then obtained by using logical relations between the denotational models. Also full abstractness is shown by extending the languages (thereby changing the semantics) by the addition of parallel constructs.

Milner [START_REF] Milner | Functions as processes[END_REF] shows that the call-by-name as well as the call-by-value lambda calculus can be encoded into the ⇡-calculus, by providing translations from the lambda calculi into the ⇡-calculus and showing adequacy of the translations. By providing counter examples full abstractness is disproved for both translations. All calculi are equipped with an observational equivalence and thus fit into the definition of observational program calculi. However, only may-convergence is considered as observation. For the proofs of adequacy first convergence equivalence of the translations is proved and adequacy is concluded by inspecting the translation similar to our proof of Proposition 3.16 but without abstracting from the concrete syntax and translation.

A similar result is obtained for the call-by-name lambda calculus with McCarthy's amboperator in [START_REF] Carayol | On the representation of McCarthy's amb in the pi-calculus[END_REF] where also adequacy of the translation is derived by first proving convergence equivalence (w.r.t. the observations of may-convergence and should-convergence) and then showing compositionality of the translation.

Convergence Equivalent and Convergence Preserving Translations. The CompCert project works on certified compilers of C [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] and uses also behavioral criteria for correctness. There are three kinds of observation predicates which are indexed with the input/output trace of the programs (and thus there are indeed infinitely many observation predicates). The three kinds are termination, divergence, and error, where the latter means that the program execution is going wrong (e.g. by accessing an array out of bounds). Let us denote the observation predicates by # (termination), " (divergence) and (error) indexed by the input/output trace . Let T : K ! K 0 be a translation, where we assume that the same observation predicates are available in K and K 0 and T translates them as the identity. Then the formalized criterion for correct compilation in [START_REF] Leroy | Formal verification of a realistic compiler[END_REF] is the following:

8p 2 K : ¬p =) (8 2{ # , " } : T (p) =) p )
This notion is weaker than convergence equivalence, since only error-free programs are taken into account. Also only reflection of the other observation predicates is shown, but since the investigated languages are deterministic, convergence equivalence should follow since in this case divergence is the negation of termination.

In a similar way, Chlipala [START_REF] Chlipala | A verified compiler for an impure functional language[END_REF] formalized a translation (compilation) from an untyped ML-like language into an assembly language, and formalized a proof of preservation of convergence and failing computations, but no adequacy result is included, and also nonterminating computations are excluded.

Work on Compositional Compiler Correctness. The recent work towards so-called "compositional compiler-correctness" [START_REF] Benton | Biorthogonality, step-indexing and compiler correctness[END_REF][START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF] also considers correctness of translations and provides results on correct compilations and translations, but focused on specific languages and thus does not propose general techniques. Benton and Hur [START_REF] Benton | Biorthogonality, step-indexing and compiler correctness[END_REF] investigate a translation from a simply-typed call-by-value PCF language into code for the SECD-machine, and Hur and Dreyer [START_REF] Hur | A Kripke logical relation between ML and assembly[END_REF] investigate a translation from an extended System F language into an assembly language. Both approaches are di↵erent from ours. Let us describe the approaches from a rough top level view: They define logical relations between the source language L S and the target language L T (or as in [START_REF] Benton | Biorthogonality, step-indexing and compiler correctness[END_REF] between target programs and the denotation of source programs), and prove properties about the relation, e.g. that any pair (p T , p S ) in the logical relation is convergence equivalent, i.e. target program p T converges i↵ source program p S converges. They also show compositionality results about the logical relations, e.g. that target level applications (p T,1 p T,2 ) and source level applications (p S,1 p S,2 ) (their denotation, resp.) are included in the logical relation if the functions p T,1 , p S,1 as well as the arguments p T,2 , p S,2 are already logically related. All these results are independent of a concrete translation from the source to the target language, so this step can be seen as relating the semantics of the source and the target language in general. An (application specific) compilation T : L S ! L T is shown to be included in the logical relation in a separate step, i.e., for any source level program p S , the pair (T (p S ), p S ) is in the logical relation (or (T (p S ), Jp S K) with J•K the denotation, resp.) where T translates source into target programs. A drawback of this method is that the definition of the logical relation is type-directed and thus requires typed languages. The most notable di↵erence between their approaches and our work is that they start by defining the logical relation then prove properties and finally show inclusion of the translation, while our approach starts with a general definition of translations and properties of the translation.

In assembly or machine languages, where runtime inspection and modification of the program are permitted, contextual semantics considering all contexts amounts to syntactic equality, which renders usual adequacy and full abstractness useless. Thus the works above do not show a (fully abstract or isomorphism) relation between the observational equivalences of the target and source language. However, Theorem 3.21 may provide a connection by restricting the contexts in assembly, perhaps to the images under the translation.

A further problem of this approach is discussed (and attacked by combining logical relations and bisimulations) in [START_REF] Hur | The marriage of bisimulations and Kripke logical relations[END_REF]: Logical relations do not compose well, and thus proving correctness of a composed translation by simply showing correctness of every single translation in the composition seems to be problematic. In contrast as shown in Proposition 3.13 the main correctness properties are closed under composition.

General Approaches. We discuss some general approaches on language translations and their correctness. Shapiro [START_REF] Shapiro | Separating concurrent languages with categories of language embeddings[END_REF] categorizes implementations and embeddings in concurrent scenarios, but does not provide concrete proof methods based on contextual equivalence.

For deterministic languages, frameworks similar to our proposal were considered by Felleisen [START_REF] Felleisen | On the expressive power of programming languages[END_REF] and Mitchell [START_REF] Mitchell | On abstraction and the expressive power of programming languages[END_REF]. Their focus is on comparing languages with respect to their expressive power; the non-deterministic case is only briefly mentioned by Mitchell.

Mitchell's work is concerned with (the impossibility of) translations that additionally preserve representation independence of ADTs, and consequently assumes, for the most part, source languages with expressive type systems. Felleisen's work is set in the context of a Scheme-like untyped language. Although the paper discusses the possibility of adding types to get stronger expressiveness statements, the theory of expressiveness is developed by abandoning principles similar to observational correctness and adequacy.

For parallel and concurrent languages, approaches to prove compiler correctness can be found in [START_REF] Wand | Compiler correctness for parallel languages[END_REF][START_REF] Gladstein | Compiler correctness for concurrent languages[END_REF]. While these results make use of a denotational semantics (and its domain is a common "intermediate language" for both the source and the target language), the recent [START_REF] Hu | Compiling Concurrency Correctly: Cutting out the Middle Man[END_REF] does not use a denotation, but shows correctness more directly. Nevertheless, the approach taken in [START_REF] Hu | Compiling Concurrency Correctly: Cutting out the Middle Man[END_REF] requires that the values of the source and the target language are comparable by a bisimulation equivalence.

Conclusions and Outlook

This paper clarifies the notions and the methods, and provides several tools for proving adequacy or full abstraction of translations. Since observational equivalence does not rely on denotational models (which are usually hard to find or even might not exist), our framework is applicable whenever an operational semantics, a notion of successful termination and a notion of contexts is available, which in general is the case and thus unifies a wide range of applications. It also shows that questions of adequacy, full abstractness or conservativeness of translations can be put into a general context and made rigorous.

In future research the framework will be used as a foundation to prove the correctness of various implementations, especially in concurrent settings where correctness of synchronization abstractions is often far from obvious.

  [.] o ) ⌦ o : the program C[true] reduces to true while C[if x then true else true] diverges. Thus, a surrounding context together with reduction may instantiate the free variables of an open program by any program, since pcf cbn has a call-by-name reduction. This is di↵erent under call-by-value strategies, for example pcf cbv , where the closing contexts are composed of contexts (( x.[.]

Example 3 . 3 .

 33 Simple examples for pre-translations are embeddings like the identity translation T incl from pcf cbv into pcf cbv ,

(

  C)(T (p)) T . Proof. (oc) =) (acooc): Let T be (oc), i.e., convergence equivalent and compositional up to observations; let C be a context and p be a program such that C(p) is closed. Then C(p) ^c e () T (C(p)) T cuo () T (C)(T (p)) T and thus the claim holds. (acooc) =) (oc): Let p be a closed program. According to Definition 2.4 there is a C 2 S, such that C(p) is also closed and C(p) () p .S ince T (C) 2 S 0 by condition (4) of Definition 3.5 and T (p) is closed, the following equivalence holds: == ) T (C)(T (p)) T () T (p) T . Hence T is (ce). It remains to show that T is (cuo): Assume C(p) is closed, then T (C(p)) T ce () C(p) ^a cooc ( == ) T (C)(T (p)) T

( 0 T 0 T 0 T 0 T 0 T

 00000 ce): Let 2O and p be closed. Then p () T (p) T , since T is (ce), also T (p) is closed and thus T (p) T () T 0 (T (p))T , since T 0 is (ce). In summary, this shows p : Let T, T 0 be observationally correct. Since this implies that T and T 0 are also convergence equivalent, the previous item already shows that T 0T is (ce). It remains to show that T 0 T is (cuo). Let C(p) be closed. Then T (C(p)) T () T (C)(T (p)) T holds, since T is (cuo). Since T (C)(T (p)) is closed and T 0 is (cuo), we also have T 0 (T (C)(T (p))) T 0 T () T 0 (T (C))(T 0 (T (p))) T . This shows T (C(p)) T () T 0 (T (C))(T 0 (T (p))) T . Since T 0 is convergence equivalent, we also have T (C(p)) T () T 0 (T (C(p))) T which implies T 0 (T (C(p))) , and thus T 0

  T , type, S) for i = 1, 2, 3 where Clos i = P i (all programs are closed), T = {unit} (a single type), type = {(p, unit) | p 2 P i }[{C, (unit, unit) | C 2 C}, S = {[.]} (all programs and contexts are typeable in the obvious way). We set P 1 = {a, b}, C 1 = {[.], C} with C(a) = a = C(b), and 1 = {a, b}; P 2 = {A, B}, C 2 = {[.]}, and 2 = ;; and P 3 = {↵, }, C 3 = {[•]} and 3 = {↵}. Let T 1,2 : K 1 ! K 2 be the translation with T 1,2 (a) = A, T 1,2 (b) = B, T 1,2 (C) = [.], T 1,2 (unit) = unit, and let T 2,3 :

Theorem 3 . 16 .

 316 If translation T : K ! K 0 is observationally correct, then T is also adequate. Proof. To show adequacy, let us assume that T (p 1 )  0 T (⌧ ) T (p 2 ). We must prove that p 1  ⌧ p 2 . Thus let C be such that C(p 1 ) and C(p 2 ) are closed and C(p 1 ) .B y the characterization of observational correctness in Lemma 3.12, this implies T (C)(T (p 1 )) T , where T (C)(T (p 1 )) and T (C)(T (p 2 )) are closed by Lemma 3.7. From T (p 1 )  0 T (⌧ ) T (p 2 ), we obtain T (C)(T (p 2 )) T . The other direction of the equivalence in the observational correctness condition implies C(p 2 )

4 .

 4 Convergence equivalence and full abstractness do not imply observational correctness.Proof.1. Let the observational program calculus K have three programs: a, b, c witha" K , b# K and c# K . Assume there are contexts C 1 , C 2 with C 1 = Id and C 2 (a) = a, C 2 (b) = a, C 2 (c) = c. Then b 6 ⇠ K c. The language K 0 has three programs A, B, C with A" K 0 , B# K 0 and C# K 0 .There is only the identity context Id 0 in K 0 . Then B ⇠ K 0 C. Let the translation be defined as T :K ! K 0 with T (a) = A, T (b) = B, T (c) = C, T (C 1 ) = T (C 2 ) = Id 0 , and T (# K ) = # K 0 . Then T is convergence equivalent, butneither adequate nor observationally correct. T is also not (cuo), since T (C 2 (b)) = A and thus T (C 2 (b))" K 0 while T (C 2 )(T (b)) = Id (B) = B and thus T (C 2 )(T (b))# K 0 .

4 .

 4 Let K have two programs a, b, the identity context, and one context C with C(a) = b and a# K , b" K . Let K 0 consists of A, B with A# K 0 , and B" K 0 , and the identity context. Let T : K ! K 0 be the translation defined by T (a) = A, T (b) = B, T (C) = Id 0 , and T (# K ) = # K 0 . Then T is -preserving and reflecting, since there are no relevant equalities. It is also convergence equivalent. But it is not observationally correct, since T (C(a)) = T (b) = B, i.e. T (C(a))" K 0 , and T (C)(T (a)) = A, i.e. T (C)(T (A))# K 0 .

3 :

 3 Definition 3.19. A translation T is closedness reflecting i↵ for all programs p and contexts C: C(p) is closed () T (C)(T (p)) is closed. Lemma 3.20. Let T : K ! K 0 and let T be closedness reflecting. Then T (C(p)) is closed provided C(p) is closed or T (C)(T (p)) is closed.

Proof. ( 1 )T hus p 1  ⌧ p 2 .Let p 1  ⌧ p 2

 11212 Let T (p 1 )  T,⌧ T (p 2 ) hold, and let C 2 C ⌧,⌧ 0 such that C(p 1 ), C(p 2 ) are closed and C(p 1 ) .T hen also T (C)(T (p 1 )) and T (C)(T (p 2 )) are closed (by Lemma 3.7). Observational correctness implies T (C)(T (p 1 )) T . The definition of  T,⌧ implies T (C)(T (p 2 )) T and by observational correctness, we obtain C(p 2 ) .and let C 2 C ⌧,⌧ 0 such that T (C)(T (p 1 )), T (C)(T (p 2 )) are closed, and let T (C)(T (p 1 )) T . We show that T (C)(T (p 2 )) T . By closedness reflection of T , C(p 1 ) and C(p 2 ) are closed. Observational correctness, the characterization in Lemma 3.12, p 1  ⌧ p 2 and Lemma 2.7 show T (C)(T (p 1 )) T =) C(p 1 ) ân d C(p 1 ) =) C(p 2 ) . Then C(p 2 ) în turn implies T (C)(T (p 2 )) T . Since this holds for all contexts T (C) satisfying the conditions, we have shown T (p 1 )  T,⌧ T (p 2 ). (2) Adequacy follows from Proposition 3.16 by applying it to the restricted translation T : K ! K 00 . Let p 1  ⌧ p 2 and let C 0 be a K 00 -context such that C 0 (T (p 1 )), C 0 (T (p 2 )) are closed and C 0 (T (p 1 ))

  false) in the extension of pcf cbn with por since (F true por) ⇠ true and (F false por) ⇠ false, but true 6 ⇠ false.

j 2 O 0 an observation predicate such that p 0 1  0 0 ,⌧ p 0 2

 2102 ◆)(p 0 ) ⇠ = cl p 0 . 4. for every context C 2 C⌧,⌧ 0 and program p 2 P ⌧ where C(p) is closed, there is some k 2 J, such that for all j 2 J with j k and for all înO: C(p) ,T j (C)(T j (p)) T .Then ◆ is fully abstract, i.e. ◆ is a conservative embedding.Proof. Proposition 3.16 implies that ◆ is adequate. In order to show full abstractness of ◆, let p 0 1 , p 0 2 2 P 0 be programs of type ⌧ and ^0 and let C be an arbitrary K-context such that C(◆(p 0 1 )), C(◆(p 0 2 )) are closed, and C(◆(p 0 1 )) ◆

Example 4 . 4 .

 44 We illustrate Theorem 4.3 by showing full abstractness of embeddings of restricted call-by-value PCF into call-by-value PCF. As in Example 3.24 let ◆ : pcf cbv , fix ! pcf

  and by Lemma 2.7, we obtain T (C)(p 1 ) T . Then p 1  0 ⌧ p 2 implies T (C)(p 2 ) T . By T (◆(p 2 )) ⇠ 0 ◆(⌧ ) p 2 we obtain T (C)(T (◆(p 2 ))) T . Observational correctness of T shows T (C(◆(p 2 ))) T , and thus C(◆(p 2 )) . It remains to show that T is fully abstract under the condition ( †). Let p 1 , p 2 be Kprograms of type ⌧ and assume p 1  ⌧ p 2 . We have to prove that T (p 1 )  0 T (⌧ ) T (p 2 ). Let C 0 be a K 0 -context such that C 0 (T (p 1 )) and C 0 (T (p 2 )) are closed and C 0 (T (p 1 )) ^0 i . Let C be the existing K-context with input type ⌧ for the set M := {T (p 1 ), T (p 2 )} due to the condition ( †) with T (C) ⇡ M C 0 . Then C(p 1 ) and C(p 2 ) are defined. Since T (C) ⇡ M C 0 , the programs T (C)(T (p 1 )) and T (C)(T (p 2 )) are closed and T (C)(T (p 1 )) ^0 . Since T is surjective on O, there is some ŝu ch that T ( )= ^0 . The assumption that T is closedness reflecting now implies that C(p 1 ) and C(p 2 ) are closed. Hence observational correctness of T implies C(p 1 )

Figure 3 :Figure 4 :

 34 Figure 3: Small-Step Reduction

(

  .,.) :: 8↵, .↵ ! ! (↵, ) fst :: 8↵, .(↵, ) ! ↵ snd :: 8↵, .(↵, ) ! unit :: unit fix :: 8↵, .((↵ ! ) ! (↵ ! )) ! (↵ ! )

Figure 5 :

 5 Figure 5: Types schemes for constants in ⌧ pair

W 1 :

 1 L name ! L need is convergence equivalent, and both W and W 1 are compositional translations, full abstractness of W, W 1 follows by Corollary 4.8. The translation N encodes letrec-expressions by multi-fixpoint combinators. It is shown that N is observationally correct (by proving compositionality and convergence equivalence) and thus adequate. The embedding of L lazy into L name is the identity translation which is also observationally correct. Applying Corollary 4.8 thus shows full abstractness of N . Finally, full abstractness of the translation (W N ) : L need ! L lazy follows by Lemma 3.13.

  T for the set of types of a program p and type(C) = {(⌧ 1 , ⌧ 2 ) | (C, ⌧ 1 , ⌧ 2 ) 2 type} ✓ 2 T ⇥T for the set of types of a context C. For all types ⌧, ⌧ 1 , ⌧ 2 we denote by P ⌧ the set of all programs of type ⌧ and by C ⌧ 1 ,⌧ 2 the set of all contexts of type (⌧ 1 , ⌧ 2 ). We assume that every program and context has at least one type, i.e., P = {p | p 2 P ⌧ , ⌧ 2 T }, andC = {C | C 2 C ⌧ 1 ,⌧ 2 , ⌧ 1 2 T , ⌧ 2 2 T }.We also assume that every context C 2 C is a partial function C : P ! P that is type-correct and closed under composition, i.e.:for all types ⌧ 1 , ⌧ 2 2 T , all contexts C 2 C ⌧ 1 ,⌧2 , and programs p 2 P ⌧ 1 : C(p) 2 P ⌧ 2 , and for all types ⌧ 1 , ⌧ 2 , ⌧ 3 2 T , and contexts

	Definition 2.1. An observational program pre-calculus is a tuple (P, Clos, C, O, T , type) where:
	P is a set of programs ranged over by p.
	Clos a subset of programs that are called closed.
	C is a set of contexts ranged over by C.
	O is a set of predicates we write p fo r the application of :P ! B called observation predicates. For convenience, to a program p. Furthermore, we write _ for its
	negation, i.e. p _	i↵ p do	es not hold.
	T is a set of types ranged over by ⌧ , and
	type is a relation with type ✓ (P ⇥ T ) [ (C ⇥ (T ⇥ T )).
	In the notation we will also use type as a set valued function, and write type(p) = {⌧ | (p, ⌧ ) 2 type} ✓ 2

  Definition 2.4. An observational program calculus is a tuple (P, Clos, C, O, T , type, S) such that (P, Clos, C, O, T , type) is an observational program pre-calculus and S ✓ C a subset of contexts, called generalized closing substitutions. We will write S . . . , n is closed. By condition 2.4.(3), also C 2 (C 1 (p 1 )) is closed. Now we apply condition 2.4.(1), which shows that C 2 C 1 2 S ⌧,⌧ 00 . Proposition 2.6. For any observational program calculus (P, Clos, C, O, T , type, S), type ⌧ in T and observation predicate în O, the relations 

	⌧,⌧ 0 for the set of generalized closing substitutions of type (⌧, ⌧ 0 ), and require that any observational program calculus
	satisfies the following properties for all types ⌧, ⌧ 0	, ⌧ 00 2 T :
	1. S is closed under typed function composition, i.e. for all C 2 S C 0 C 2 S ⌧,⌧ 00 , and	⌧,⌧ 0 , C 0 2 S	⌧ 0	,⌧ 00 :
	2. for all p 2 P such that C(p) is closed, and ⌧ there is some type ⌧ 0 and some generalized closing substitution C 2 S	⌧,⌧ 0 ,
	3. for all p 2 P C(p) is closed, and ⌧ and generalized closing substitutions C 2 S	⌧,⌧ 0 : if p is closed, then also
	4. for all closed programs p 2 P vation predicates în O: C(p) ⌧ , generalized closing substitutions C 2 S () p .	⌧,⌧ 0 , and obser-
	For call-by-value lambda calculi such as pcf	cbv , an appropriate choice of the set of
	generalized closing substitutions S would be compositions of all appropriately typed contexts ( x.[.] ⌧ ) v where v is a closed value. On the other hand, if S would be chosen as all closed contexts, then condition (4) of Definition 2.4 is in general false, since for example in pcf cbv :
	true#	pcfcbv , and for D := (⌦ o!o [.]
	and the relations ⇠ ,⌧	and ⇠	,⌧ ⌧ are typed congruences. That is: and 	⌧ are typed precongruences
	The relations  ,⌧	and 

o ), we have D(true)" pcfcbv . Note also that condition

[START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF]

implies that 8⌧.9⌧ 0 : S ⌧,⌧ 0 6 = ;. Lemma 2.5. For an observational program calculus K the following holds: For any type ⌧ and finite subset Q ✓ P ⌧ , there is some type ⌧ 0 and some generalized closing substitution

C 2 S ⌧,⌧ 0 , such that C(p) is closed for all p 2 Q. Proof.

The proof is by induction on |Q|. The base case where |Q| = 1 is condition 2 of Definition 2.4. Let Q = {p 1 , . . . , p n } ✓ P ⌧ where n 2. Then by condition 2.4.(2) there is C 1 2 S ⌧,⌧ 0 , such that C 1 (p 1 ) is closed. The induction hypothesis applied to {C 1 (p 2 ), . . . , C 1 (p n )} shows that there is a type ⌧ 00 and C 2 2 S ⌧,⌧ 00 , such that C 2 (C 1 (p i )) for i = 2, ⌧ are typed precongruences, i.e. they are preorders and for all programs p 1 , p 2 2 P ⌧ , all types

  further consequence of the restriction on observational program pre-calculi is that observationally equivalent, closed programs have the same observations: Lemma 2.7. Let p 1 , p 2 be two closed programs of an observational program calculus K of

the same type ⌧ and ân observation predicate of K. If p 1 ân d one of the following holds:

  (Example 3.3, cont.). We can extend the pre-translation T incl from pcf cbv into pcf cbv , to a translation, by defining: T . Obviously, this translation is convergence equivalent and compositional, so it is observationally correct.Also the pre-translation T B :: pcf cbv ! pcf cbv , B can easily be extended to contexts, which are translated like expressions and T ([.] ⌧ ) = [.] T (⌧ ) , and convergence is mapped to convergence. One can also prove that all other conditions on translations are satisfied. The translation T B is compositional and thus also cuo. For proving convergence equivalence, we first observe that values are translated into values, i.e. p 2 pcf cbv is a value i↵ T (p) 2 pcf cbv , B is a value. Also for any program p and context C one can observe that

	Example 3.9
	for all	2O	and all closed p: p ()	T (p)	, and
						T
	compositional up to observations (cuo) if the following condition holds: for all	2O	,
	all types ⌧, ⌧ 0 , all contexts C 2 C T (C(p)) T T () T (C)(T (p)) .	⌧,⌧ 0 , and all programs p 2 P	⌧ such that C(p) is closed:

incl (C) = C and T incl (# pcfcbv ) = # pcfcbv

22 .

 22 Definition 4.5. For an observational program calculus (P, Clos, C, O, T , type, S) and two contexts C A , C B 2 C ⌧ 1 ,⌧ 2 and a set M ✓ P ⌧ 1 of programs of type ⌧ 1 , we write C

A ⇡ M C B i↵ (i) for all p 2 M : C A (p) is closed i↵ C B (p)

is closed, and (ii) for all p 2 M and all

  a 1 6 ⇠ a 2 . Let K be an extension with additional type B and programs b 1 , b 2 of type B, with only the identity context, and such that b 1 ,b

		and a 1 ,a	2 ,
	a 3 ,b	ut a 4 _ . Thus, 2

  satisfies the preconditions of Theorem 4.6 and Corollary 4.7: It is observationally correct, and the embedding ◆ : pcf cbv ! pcf Two satisfies the assumptions of Theorem 4.6, and T as mapping of contexts (on respective types) is surjective. Application of Corollary 4.7 now shows that T is fully abstract. Corollary 4.8 is not applicable, since T is not injective on the types. Example 4.14. We give an example of an application of Theorem 4.6 using a slightly unusual contextual semantics for PCF. Let K 0 be pcf cbn,⌘ which is like pcf cbn where the observation predicate # pcfcbn,⌘ only tests convergence of Boolean expressions, i.e. p#

	i↵ p	⇤	pcfcbn,⌘

  ) is the usual untyped call-by-value lambda calculus extended by a call-by-value fixed point operator fix for recursion, pairs (w 1 ,w 2 ), selectors fst and snd, and a constant unit. Fixing a set of variables Var, the syntax of expressions (programs, resp.) P pair and values Val pair is shown in Fig.1. Note that only values are syntactically permitted as components of a pair.

	The subcalculus	cbv = (P	cbv , Clos	cbv , C	cbv , O	cbv , T	cbv , type	cbv , S	cbv

observational program calculus pair = (P pair , Clos pair , C pair , O pair , T pair , type pair , S pair

  sets of observation predicates are defined by O Exp and any context to (Exp ⇥ Exp). For the contextual preorders and equivalences for both calculi we subscript the relations with pair or cbv . s, t 2 P pair ::= w | t 1 t 2 v, w 2 Val pair ::= x | x.t | unit | fix | (w 1 ,w 2 ) | fst | snd

	pair = {# pair } and O pair i↵ 9v 2 Val pair : e ⇤ ! pair v, and for cbv = {# cbv } cbv cbv : e pair is defined as e# cbv is defined as e# where convergence # pair in convergence # cbv i↵ 9v 2 Val ⇤ ! cbv v. The sets of contexts C pair , C cbv contain all contexts of the respective calculus. For the closed expressions Clos pair , Clos cbv we use the closedness of expressions, and the generalized closing substitutions S pair , S cbv are the contexts of the form ( x.[.]) v, where v is a closed value, and their compositions. Since both calculi are untyped, but our framework requires types, we assume a single type Exp (i.e. T pair = T cbv = {Exp}) and the corresponding typing-functions type pair , type cbv map any E ::= [ ] | E t | w E Figure 2: Evaluation Contexts E expression to type Figure 1: Syntax of pair ( -cbv) E[( x.t) w] ! E[t[w/x]] (fix) E[fix x.t] ! E[t[( y.(fix x.t) y)/x]]

  Lemma 5.1. The translation enc preserves and reflects closedness, i.e. s 2 P We are able to show that convergence is preserved by the translation, i.e. We show by induction on n that enc(t 0 )# cbv . If n = 0 then t 0 is a value and enc(t 0 ) must be a value, too, by Lemma 5.1. For the induction step we assume the induction hypothesis enc(t 1 )# cbv . It su ces to show enc(t 0 ) enc(t 1 ). If t 0 ! pair t 1 by ( -cbv) or (fix), then the same reduction can be used in cbv , and enc(t 0 ) ! cbv enc(t 1 ). If t 0 ! pair t 1 by (sel-f) or (sel-s), then three ( -cbv) steps are necessary in cbv , i.e., enc(t 0 )

						pair is closed
	i↵ enc(s) is a closed i↵ enc(s) is a cbv -value. cbv -expression. For all closed expressions s 2 P	pair : s is a	pair -value
	Lemma 5.2. Let t 2 P	pair be closed with t# pair , then enc(t)# cbv .
	Proof. Let t = t 0 2 P	pair with t 0 #	pair so t 0 ! pair t 1 ! pair • • • ! pair t	n where t	n is a value.
						3 !	cbv enc(t 1

⇤ ! cbv

  3 is to consider a simply typed variant ::= unit | ⌧ ! ⌧ | (⌧, ⌧ ), P ⌧ pair consists only of typed expressions, C ⌧ pair consists only of typed contexts, where we assume a hole [•]

	⌧ pair = (P ⌧ pair , Clos ⌧ pair , C ⌧ pair , O ⌧ pair , T ⌧ pair , type ⌧ pair , S ⌧ pair ) of given by ⌧	pair are pair as follows. The types T ⌧

  5.1 also holds if enc is restricted to ⌧pair . We show convergence equivalence. Let t 2 P ⌧ : We use induction on the length of a reduction Red of enc(t) to a value to show that a corresponding reduction can be constructed. The base case is proved in Lemma 5.1. For the induction step closedness and typedness of t imply that t must either be a value or it is reducible. If t is a value, then we are finished. Otherwise, an inspection of the reductions shows that if a ⌧ pair -expression t 1 is reducible, then for every reduction Red of enc(t 1 ) to a value, there is some t 2 with t 1 ! pair t 2 and enc(t 1 ) enc(t 2 ) is a prefix of Red . Theorem 4.6 cannot be applied since ⌧ pair is not an extension of untyped cbv . Indeed full abstractness of enc does not hold: let s = p.(( y. z.(y,z)) (fst p) (snd p)), and t = p.p.

	pair ,(unit,unit)!(unit,unit) t holds in ⌧ pair , but after translation to cbv enc(t) which can be seen by the context C = ([•] unit), since C[enc(s)] is cbv , we Then the equation s ⇠ have enc(s) 6 ⇠ divergent while C[enc(t)] converges.
				pair be closed:
	1. t#	pair =) enc(t)#	cbv : Follows from Lemma 5.2.
	2. enc(t)#	cbv =) t#

pair + ! cbv

Note that should-convergence does not exclude weak-divergences. Sometimes it is also called mustconvergence. A di↵erent notion of must-convergence in the literature is obtained by defining p W pcfcbv such that there is no infinite reduction sequence starting from p and every reduction sequence ends in a value.

Another approach to obtain full abstractness to ensure security in connection with compilation can be found in[START_REF] Ahmed | Typed closure conversion preserves observational equivalence[END_REF][START_REF] Ahmed | An equivalence-preserving cps translation via multi-language semantics[END_REF], where a typed target language is used to ensure full abstractness. For the security issues this approach is reasonable, but for correctness of compilation one also has to consider target languages which are not typed.

Note that closedness reflection cannot be derived from observational correctness (see Remark

4.10).