An extended abstract of this paper appeared in the proceedings of FoSSaCS 2018 [35].

A Theory of Encodings and Expressiveness

Rob van Glabbeek

Data61, CSIRO, Sydney, Australia School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

                                       rvg@cs.stanford.edu

This paper proposes a definition of what it means for one system description language to encode another one, thereby enabling an ordering of system description languages with respect to expressive power. I compare the proposed definition with other definitions of encoding and expressiveness found in the literature, and illustrate it on a well-known case study: the encoding of the synchronous in the asynchronous π-calculus.

1 Introduction

This paper, like [39, 32], aims at answering the question what it means for one language to encode another one, and making the resulting definition applicable to order system description languages like CCS, CSP and the π-calculus with respect to their expressive power.

To this end it proposes a unifying concept of valid translation between two languages up to a semantic equivalence or preorder. It applies to languages whose semantics interprets the operators and recursion constructs as operations on a set of values, called a domain. Languages can be partially ordered by their expressiveness up to the chosen equivalence or preorder according to the existence of valid translations between them.

The concept of a [valid] translation between system description languages (or process calculi) was first formally defined by Boudol [9]. There, and in most other related work in this area, the domain in which a system description language is interpreted consists of the closed expressions from the language itself. In [30] I have reformulated Boudol’s definition, while dropping the requirement that the domain of interpretation is the set of closed terms. This allows (but does not enforce) a clear separation of syntax and semantics, in the tradition of universal algebra. Nevertheless, the definition employed in [30] only deals with the case that all (relevant) elements in the domain are denotable as the interpretations of closed terms. In [32] situations are described where such a restriction is undesirable. In addition, both [9] and [30] require the semantic equivalence ∼ under which two languages are compared to be a congruence for both of them. This is too severe a restriction to capture many recent encodings [8, 54, 56, 15, 4, 5, 58, 65].

In [32] I alleviated these two restrictions by proposing two notions of encoding: correct and valid translations up to ∼. Each of them generalises the proposals of [9] and [30]. The former drops the restriction on denotability as well as ∼ being a congruence for the whole target language, but it requires ∼ to be a congruence for the source language, as well as for the source’s image within the target. The latter drops both congruence requirements (and allows ∼ to be a preorder rather than an equivalence), but at the expense of requiring denotability by closed terms. In situations where ∼ is a congruence for the source language’s image within the target language and all semantic values are denotable, the two notions agree.

The current paper further generalises the work of [32] by proposing a new notion of a valid translation that incorporates the correct and valid translations of [32] as special cases. It drops the congruence requirements as well as the restriction on denotability.

As in [32], my aim is to generalise the concept of a valid translation as much as possible, so that it is uniformly applicable in many situations, and not just in the world of process calculi. Also, it needs to be equally applicable to encodability and separation results, the latter saying that an encoding of one language in another does not exists. At the same time, I try to derive this concept from a unifying principle, rather than collecting a set of criteria that justify a number of known encodability and separation results that are intuitively justified.

Overview of the paper Section 2 defines my new concept of a valid translation up to a semantic equivalence or preorder •∼ . Roughly, a valid translation up to •∼ of one language into another is a mapping from the expressions in the first language to those in the second that preserves their meaning, i.e. such that the meaning of the translation of an expression is semantically equivalent to the meaning of the expression being translated.

Section 3 shows that this concept generalises the notion of a correct translation from [32]: a translation is correct up to a semantic equivalence ∼ iff it is valid up to ∼ and ∼ is a congruence for the source language as well as for the image of the source language within the target language.

Likewise, Section 14 shows that my new concept of validity generalises the one of [32], and Section 15 establishes the coincidence of my new validity-based notion of expressiveness with the one from [32] when applying both to languages for which all semantic values are denotable by closed terms.

One language is said to be at least as expressive as another up to •∼ iff there exists a valid translation up to •∼ of the latter language into the former. Section 4 shows that the relation “being at least as expressive as” is a preorder on languages. This expressiveness preorder depends on the choice of •∼ , and a coarser choice (making less semantic distinctions) yields a richer preorder of expressiveness inclusions.

Section 5 presents the widely used class of closed-term languages, in which the distinction between syntax and semantic is effectively dropped by taking the domain of values where the language is interpreted in to consist of the closed terms of the language. Section 6 illustrates my approach on a wellknown case study: the encoding of the synchronous in the asynchronous π-calculus.

Section 7 discusses the congruence closure of a semantic equivalence for a given language, and remarks that in the presence of operators with infinite arity it is not always a congruence. Section 8 states a useful congruence closure property for valid translations: if a translation between two languages exists that is valid up a semantic equivalence ∼, then it is even valid up to an equivalence that

• on the source language coincides with the congruence closure of ∼

• on the image of the source within the target language also coincides with the congruence closure of ∼ • melts each equivalence class of the source with exactly one of the target, and vice versa.

Section 9 concludes that the framework established thus far is very suitable for comparing the expressiveness of languages, but falls short for the purpose of combining language features. This requires a congruence reflection theorem, provided in Section 13, for closed-term languages and preorders •∼ that satisfy some mild sanity requirements: the postulates formulated in Sections 10 and 11.

Section 12 defines when a translation is compositional, and shows that any valid translation up to •∼ can be modified into a compositional translation valid up to •∼ , provided the languages and preorders •∼ satisfy the sanity requirements of Sections 10 and 11. Hence, for the purpose of comparing the expressive power of languages, valid translations between them may be presumed compositional.

Section 16 contemplates a more general, and arguably also simpler, concept of a valid translation, than the one of Section 2. However, it lacks appealing properties of the latter.

Section 17 speculates on suitable choices for •∼ when comparing the expressiveness of process calculi. Sections 18–19 compare my approach with full abstraction, and with the approach of Gorla [39].

2 Languages, correct and valid translations, and expressiveness

A language consists of syntax and semantics. The syntax determines the valid expressions in the language. The semantics is given by a mapping ⟦ ⟧ that associates with each valid expression its meaning, which can for instance be an object, concept or statement.

Following [32], I represent a language L as a pair (𝕋_{L} ,⟦ ⟧_{L} ) of a set 𝕋_{L} of valid expressions in L and a mapping ⟦ ⟧_{L} : 𝕋_{L} → D_{L} from 𝕋_{L} in some set of meanings D_{L} .

Definition 1 ([32]) A translation from a language L into a language L′is a mapping T : 𝕋_{L} → 𝕋_{L′}.

In this paper, I consider single-sorted languages L in which expressions or terms are built from variables (taken from a set X ) by means of operators (including constants) and possibly recursion constructs. For such languages the meaning ⟦E⟧_{L} of an L -expression E is a function of type (X → V) → V for a given sets of values V. It associates a value ⟦E⟧_{L} (ρ) ∈ V to E that depends on the choice of a valuation ρ: X →V. The valuation associates a value from V with each variable.

Since normally the names of variables are irrelevant and the cardinality of the set of variables satisfies only the requirement that it is “sufficiently large”, no generality is lost by insisting that two (system description) languages whose expressiveness is being compared employ the same set of (process) variables. On the other hand, two languages L and L′may be interpreted in different domains of values V and V′.

Let L and L′be two languages of the type considered above, with semantic mappings

⟦ ⟧_{L} : 𝕋_{L} → ((X → V) → V)  and  ⟦ ⟧_{L′} : 𝕋_{L′} → ((X → V′) → V′).

In order to compare these languages w.r.t. their expressive power I need a semantic equivalence or preorder •∼ that is defined on a unifying domain of interpretation Z, with V,V′⊆ Z.^{1} Intuitively, v′ •∼ v with v ∈ V and v′∈ V′means that values v and v′are sufficiently alike for our purposes, so that one can accept a translation of an expression with meaning v into an expression with meaning v′.

Correct and a valid translations up to a semantic equivalence or preorder •∼ were introduced in [32]. Here I redefine these concepts in terms of a new concept of correctness w.r.t. a semantic translation.

Definition 2 Let V and V′be domains of values in which two languages L and L′are interpreted. A semantic translation from V into V′is a relation R ⊆ V′× V such that ∀v ∈ V.∃v′∈ V′.v′R v.

Thus every semantic value in V needs to have a counterpart in V′—possibly multiple ones. For valuations η : X → V′, ρ : X → V I write η R ρ iff η(X) R ρ(X) for each X ∈ X .

Definition 3 A translation T : 𝕋_{L} → 𝕋_{L′} is correct w.r.t. a semantic translation R if ⟦T (E)⟧_{L′}(η) R ⟦E⟧_{L} (ρ) for all expressions E ∈ 𝕋_{L} and all valuations η : X → V′and ρ : X → V with η R ρ. Thus T is correct iff the meaning of the translation of an expression E is a counterpart of the meaning of E, no matter what values are filled in for the variables, provided that the value filled in for a given variable X occurring in the translation T (E) is a counterpart of the value filled in for X in E.

Definition 4 A translation T : 𝕋_{L} → 𝕋_{L′} is correct up to •∼ iff •∼ is an equivalence, the restriction R of •∼ to V′× V is a semantic translation, and T is correct w.r.t. R.

Definition 5 A translation T is valid up to •∼ iff it is correct w.r.t. some semantic translation R ⊆ •∼ . Language L′is at least as expressive as L up to •∼ if a translation valid up to •∼ from L into L′exists.

1I will be chiefly interested in the case that •∼ is an equivalence—hence the choice of a symbol that looks like ∼. However, to establish Observation 2 and Theorem 2 below, it suffices to know that •∼ is reflexive and transitive. My convention is that the dotted end of •∼ points to a translation and the other end to an original—without offering an intuition for the possible asymmetry.

3 Correct = valid + congruence

In [32] the concept of a correct translation up to ∼ was defined, for ∼ a semantic equivalence on Z. Here two valuations η,ρ : X → Z are called ∼-equivalent, η ∼ ρ, if η(X) ∼ ρ(X) for each X ∈ X . In case there exists a v ∈ V for which there is no ∼-equivalent v′∈ V′, there is no correct translation from L into L′up to ∼. Namely, the semantics of L describes, among others, how any L -operator evaluates the argument value v, and this aspect of the language has no counterpart in L′. Therefore, [32] requires

∀v ∈ V. ∃v′∈ V′. v′∼ v.  (1)

This implies that for any valuation ρ : X → V there is a valuation η : X → V′with η ∼ ρ.

Definition 6 ([32]) A translation T from L into L′is correct up to ∼ iff (1) holds and ⟦T (E)⟧_{L′}(η) ∼ ⟦E⟧_{L} (ρ) for all E ∈ 𝕋_{L} and all valuations η : X → V′and ρ : X → V with η ∼ ρ.

Note that this definition agrees completely with Definition 4. Requirement (1) above corresponds to R being a semantic translation in Definition 4.

If a correct translation up to ∼ from L into L′exists, then ∼ must be a congruence for L.

Definition 7 An equivalence relation ∼ is a congruence for a language L interpreted in a semantic domain V if ⟦E⟧_{L} (ν) ∼ ⟦E⟧_{L} (ρ) for any L -expression E and any valuations ν,ρ: X → V with ν ∼ ρ.^{2}

Proposition 1 ([32]) If T is a correct translation up to ∼ from L into L′, then ∼ is a congruence for L.

The existence of a correct translation up to ∼ from L into L′does not imply that ∼ is a congruence for L′. However, ∼ has the properties of a congruence for those expressions of L′that arise as translations of expressions of L, when restricting attention to valuations into U := {v ∈ V′| ∃v ∈ V. v′∼ v}. In [32] this called a congruence for T (L).

Definition 8 Let T : 𝕋_{L} → 𝕋_{L′} be a translation from L into L′. An equivalence ∼ on V′ is a congruence for T (L) if ⟦T (E)⟧_{L′}(θ) ∼ ⟦T (E)⟧_{L′}(η) for any E ∈ 𝕋_{L} and θ,η:X →U with θ ∼ η.

Proposition 2 ([32]) If T is a correct translation up to ∼ from L into L′, then ∼ is a congruence for T (L).

The following theorem tells that the notion of validity proposed in Section 2 can be seen as a generalisation of the notion of correctness from [32] that applies to equivalences (and preorders) •∼ that are not necessarily congruences for L or T (L).

Theorem 1 A translation T from L into L′is correct up to a semantic equivalence ∼ iff it is valid up to ∼ and ∼ is a congruence for T (L).

Proof: By Definitions 4 and 5 any translation that is correct up to ∼ is surely valid up to ∼.

Suppose T is valid up to ∼ and ∼ is a congruence for T (L). Then there is a semantic translation R ⊆ V′×V such that R ⊆ ∼ and T is correct w.r.t. R. To establish that T is correct up to ∼, let E ∈ 𝕋_{L} and let η : X → V′and ρ : X → V be valuations with η ∼ ρ. Let θ : X → V′be a valuation with θ R ρ—it exists since R is a semantic translation. Now θ ∼ ρ ∼ η, using that R ⊆ ∼ , so θ,η : X → U and θ ∼ η. Hence ⟦T (E)⟧_{L′}(η) ∼ ⟦T (E)⟧_{L′}(θ) ∼ ⟦E⟧_{L} (ρ), using that ∼ is a congruence for T (L) and that T is correct w.r.t. R. □

2This is called a lean congruence in [33]; in the presence of recursion, stricter congruence requirements are common. Those are not needed in this paper.

4 A hierarchy of expressiveness preorders

An equivalence or preorder •∼ on a class Z is said to be finer, stronger, or more discriminating than another equivalence or preorder •≈ on Z if v •∼ w ⇒ v •≈ w for all v,w ∈ Z. Observation 1 Let T : 𝕋_{L} → 𝕋_{L′} be a translation from L into L′, and let •∼ be finer than •≈ . If T is valid up to •∼ , then it is also valid up to •≈ . The quality of a translation depends on the choice of the equivalence or preorder up to which it is valid. Any two languages are equally expressive up to the universal equivalence, relating any two processes. Hence, the equivalence or preorder needs to be chosen carefully to match the intended applications of the languages under comparison. In general, as shown by Observation 1, using a finer equivalence or preorder yields a stronger claim that one language can be encoded in another. On the other hand, when separating two languages L and L′by showing that L cannot be encoded in L′, a coarser equivalence or preorder yields a stronger claim.

Observation 2 The identity is a valid translation up to any preorder from any language into itself.

Theorem 2 If valid translations up to •∼ exists from L_{1} into L_{2} and from L_{2} into L_{3}, then there is a valid translation up to •∼ from L_{1} into L_{3}.

Proof: For i = 1,2,3 let ⟦ ⟧_{L_{i}} : 𝕋_{L_{i}} → ((X → V_{i}) → V_{i}), and for k = 1,2 let T_{k}: 𝕋_{L_{k}} → 𝕋_{L_{k+1}} be valid translations up to •∼ from L_{k} to L_{k+1}, based on semantic translations R_{k} ⊆ V_{L_{k+1}} ×V_{L_{k}}. I will show that the translation T_{2}∘T_{1} : 𝕋_{L_{1}} → 𝕋_{L_{3}} from L_{1} into L_{3}, given by T_{2}∘T_{1}(E) = T_{2}(T_{1}(E)), is valid up to •∼ . To this end, let R_{2} ∘ R_{1} ⊆ V_{3}×V_{1} be the relation given by v_{3} R_{2} ∘ R_{1} v_{1} iff ∃v_{2} : v_{3} R_{2} v_{2}∧ v_{2} R_{1} v_{1} — it is again a semantic translation, and satisfies R_{2} ∘ R_{1} ⊆ •∼ , using the transitivity of •∼ . Now let E ∈ 𝕋_{L_{1}} , ρ : X → V_{1} and θ : X → V_{3}, with θ R_{2} ∘ R_{1} ρ. Then there is a valuation η : X → V_{2} with θ R_{2} η R_{1} ρ. Hence ⟦T_{2}(T_{1}(E))⟧_{L_{3}} (θ) •∼ ⟦T_{1}(E)⟧_{L_{2}} (η) •∼ ⟦E⟧_{L_{1}} (ρ), so T_{2}∘ T_{1} is correct w.r.t. R_{2} ∘ R_{1}. □

Theorem 2 and Observation 2 show that the relation “being at least as expressive as up to •∼ ” is a preorder on languages.

5 Closed-term languages

The languages considered in this paper feature variables, operators of arity n ∈ ℕ, and/or other constructs. The set 𝕋_{L} of L -expressions is inductively defined by:

• X ∈ 𝕋_{L} for each variable X ∈ X ,

• f(E_{1},...,E_{n}) ∈ 𝕋_{L} for each n-ary operator f and expressions E_{i} ∈ 𝕋_{L} for i = 1,...,n,

• and clauses for the other constructs, if any. Examples of other constructs are the infinite summation operator ∑_{i∈I} E_{i} of CCS, which takes arbitrary many arguments, or the recursion construct μX.E, that has one argument, but binds all occurrences of X in that argument.

In general a construct has a number (possibly infinite) of argument expressions and it may bind certain variables within some of its arguments—the scope of the binding. An occurrence of a variable X in an expression is bound if it occurs within the scope of a construct that binds X, and free otherwise.

The semantics of such a language is given, in part, by a domain of values V, and an interpretation of each n-ary operator f of L as an n-ary operation f^{V} : V^{n} → V on V. Using the equations

⟦X⟧_{L} (ρ) = ρ(X) and ⟦f(E_{1},...,E_{n})⟧_{L} (ρ) = f^{V}(⟦E_{1}⟧_{L} (ρ),...,⟦E_{n}⟧_{L} (ρ))

this allows an inductive definition of the meaning ⟦E⟧_{L} of an L -expression E. Moreover, ⟦E⟧_{L} (ρ) only depends on the restriction of ρ to the set fv(E) of variables occurring free in E.

The set T_{L} ⊆ 𝕋_{L} of closed terms of L consists of those L -expressions E ∈ 𝕋_{L} with fv(E) = ∅. If P ∈ T_{L} and V ≠ ∅ then ⟦P⟧_{L} (ρ) is independent of the choice of ρ:X → V, and hence written ⟦P⟧_{L} .

Definition 9 A substitution in L is a partial function σ : X ⇀ 𝕋_{L} from the variables to the L - expressions. For a given L -expression E ∈ 𝕋_{L} , E[σ] ∈ 𝕋_{L} denotes the L -expression E in which each free occurrence of a variable X ∈ dom(σ) is replaced by σ(X), while renaming bound variables in E so as to avoid a free variable Y occurring in an expression σ(X) ending up being bound in E[σ].^{3} A substitution is closed if it has the form σ : X → T_{L} .

An important class of languages used in concurrency theory are the ones where the distinction between syntax and semantic is effectively dropped by taking V = T_{L} , i.e. where the domain of values where the language is interpreted in consists of the closed terms of the language. Here a valuation is the same as a closed substitution, and ⟦E⟧_{L} (ρ) for E ∈ 𝕋_{L} and ρ : X → T_{L} is defined to be E[ρ] ∈ T_{L} . I will call such languages closed-term languages.

6 Example: translating a synchronous into an asynchronous π-calculus

As an illustration of the concepts introduced above, consider the π-calculus as presented by Milner in [51], i.e., the one of Sangiorgi and Walker [76] without matching, τ-prefixing, and choice.

Given a set of names N , the set 𝕋_{π} of process expressions or terms E of the calculus is given by

E ::= X | 0 | x̄y.E | x(z).E | E|E′ | (νz)E | !E

with x,y,z ranging over N , and X over X , the set of process variables. Process variables are not considered in [76], although they are common in languages like CCS [50] that feature a recursion construct. Since process variables form a central part of my notion of a valid or correct translation, here they have simply been added. This works generally. In Section 12 I show that for the purpose of accessing whether one language is as expressive as another, translations between them can be assumed to be compositional. This important result would be lost if process variables were dropped from the language. In that case compositionality would need to be stated as a separate requirement for valid translations.

Closed process expressions are called processes. The π-calculus is usually presented as a closedterm language, in that the semantic value associated with a closed term is simply itself. Yet, the real semantics is given by a reduction relation between processes, defined below.

Definition 10 An occurrence of a name z in π-calculus process P ∈ T_{π} is bound if it occurs within a subexpression x(z).P′ or (νz)P′ of P; otherwise it is free. Let n(P) (resp. bn(P)) be the set of names occurring (bound) in P ∈ T_{π}.

Structural congruence, ≡, is the smallest congruence relation on processes satisfying

P_{1}|(P_{2}|P_{3}) ≡(P_{1}|P_{2})|P_{3}  !P ≡ P|!P  (νw)(P|Q) ≡ P|(νw)Q if w ∉ n(P) P_{1}|P_{2} ≡ P_{2}|P_{1}  (νz)0 ≡ 0  x(z).P ≡ x(w).P{w/z} if w ∉ n(P) P|0 ≡ P  (νz)(νw)P ≡ (νw)(νz)P  (νz)P ≡ (νw)P{w/z} if w ∉ n(P) .

Here P{w/z} denotes the process obtained by replacing each free occurrence of z in P by w.

3In languages with multiple kinds of binding, such as for process variables X ∈ X and for names x ∈ N in the π-calculus below, all types of bound variables may be renamed.

Definition 11 The reduction relation, → ⊆ T_{π} × T_{π}, is generated by the following rules.

\frac{z ∉ bn(Q)}{x̄z.P|x(y).Q → P|Q\{z/y\}} \frac{P → P′}{P|Q → P′|Q}  \frac{P → P′}{(νz)P → (νz)P′}  \frac{Q ≡ P P → P′ P′≡ Q′}{Q → Q′}

Let =⇒ be the reflexive and transitive closure of →. The observable behaviour of π-calculus processes is often stated in terms of the outputs they can produce (abstracting from the value communicated on an output channel).

Definition 12 Let x ∈ N . A process P has a strong output barb on x, notation P↓x̄, if P can perform an output action x̄z. This is defined inductively:

(x̄z.(P))↓x̄  \frac{P↓x̄}{(P|Q)↓x̄}  \frac{Q↓x̄}{(P|Q)↓x̄}  \frac{P↓x̄ x ≠ z}{((νz)P)↓x̄}  \frac{P↓x̄}{(!P)↓x̄}

A process P has a weak output barb on x, notation P⇓x̄, if there is a P′with P =⇒ P′⇓x̄.

A common semantic equivalence applied in the π-calculus is weak barbed congruence [52, 75, 76]. Definition 13 Weak (output) barbed bisimilarity is the largest symmetric relation ≈^{•} ⊆ T_{π} ×T_{π} such that

• P ≈^{•} Q and P↓x̄implies Q⇓x̄, and

• P ≈^{•} Q and P =⇒ P′implies Q =⇒ Q′for some Q′with P′ ≈^{•} Q′. Weak barbed congruence, ≅ ^{c}, is the largest congruence included in ≈^{•} . Often input barbs, defined similarly, are included in the definition of weak barbed bisimilarity [76]. This is known to induce the same notion of weak barbed congruence [76]. Another technique for defining weak barbed congruence is to use a barb, or set of barbs, external to the language under investigation, that are added to the language as constants, similar to the theory of testing of Hennessy and De Nicola [19]— see Section 17 for details. This method is useful for languages with a reduction semantics that do not feature a clear notion of barb, or where there is ambiguity in which barbs should be counted and which not, or for comparing languages with different kinds of barb.

Example 1 x̄z.0 ≅ ^{c̸} (νu)(x̄u.0|u(v).v̄z.0). For let E := X|x(u).ūv.0 with ζ(X) = (νu)(x̄u.0|u(v).v̄z.0) and ρ(X) = x̄z.0. Then E[ζ] → (νu)(u(v).v̄z.0|ūv.0) → (v̄z.0)↓v̄but (E[ρ])⇓̸v̄.

The asynchronous π-calculus, as introduced by Honda & Tokoro in [44] and by Boudol in [10], is the sublanguage aπ of the fragment π of the π-calculus presented above where all subexpressions x̄y.E have the form x̄y.0. Asynchronous barbed congruence, ≅ _{a}^{c}, is the largest congruence for the asynchronous π-calculus included in ≈^{•} . Since aπ is a sublanguage of π, ≅ _{a}^{c} is at least as coarse an equivalence as ≅ ^{c}, i.e. ≅ ^{c} ⊆ ≅ _{a}^{c}. The inclusion is strict, since !x(z).x̄z.0 ≅ _{a}^{c} 0, yet !x(z).x̄z.0 ≅ ^{c̸} 0 [76]. Since all expressions used in Example 1 belong to aπ, one even has x̄z.0 ≅ _{a̸}^{c} (νu)(x̄u.0|u(v).v̄z.0).

Boudol [10] defined a translation T from π to aπ inductively as follows:

T (X) = X  for X ∈ X
T (0) = 0
T (x̄z.P) = (u)(x̄u|u(v).(v̄z|T (P))) choosing u,v ∉ n(P), u ≠ v
T (x(y).P) = x(u).(v)(ūv|v(y).T (P)) choosing u,v ∉ n(P), u ≠ v
T (P|Q) = (T (P)|T (Q))
T (!P) = !T (P)
T ((νx)P) = (νx)T (P)

Example 1 shows that T is not valid up to ≅ ^{c}. In fact, it is not even valid up to ≅ _{a}^{c}. However, as shown in [47], it is valid up to ≈^{•} . Since ≈^{•} is not a congruence (for π or aπ) it is not correct up to ≈^{•} .

7 Congruence closure

Definition 14 An equivalence relation ∼ is a 1-hole congruence for a language L interpreted in a semantic domain V if ⟦E⟧_{L} (ν) ∼ ⟦E⟧_{L} (ρ) for any L -expression E and any valuations ν,ρ : X → V with ν ∼^{1} ρ. Here ν,ρ are ∼^{1}-equivalent, ν ∼^{1} ρ, if ν(X) ∼ ρ(X) for some X ∈ X and ν(Y) = ρ(Y) for all variables Y ≠ X.

An n-hole congruence for any finite n ∈ ℕ can be defined in the same vain, and it is well known and easy to check that a 1-hole congruence ∼ is also an n-hole congruence, for any n ∈ ℕ. However, in the presence of operators with infinitely many arguments, a 1-hole congruence need not be a congruence. Example 2 Let V be (ℕ × ℕ) ∪ {∞}, with the well-order ≤ on V inherited lexicographically from the default order on ℕ and ∞ the largest element. So (n,m) ≤ (n′,m′) iff n ≤ n′∨(n = m∧m ≤ m′). Consider the language L with constants 0, 1 and (1), interpreted in V as (0,0), (1,0) and (0,1), respectively, the binary operator +, interpreted by (n_{1},m_{1}) +^{V}(n_{2},m_{2}) = (n_{1}+n_{2},m_{1}+m_{2}) and ∞ + E = E + ∞ = ∞, and the construct sup(E_{i})_{i∈I} that takes any number of arguments (dependent on the set of the index sets I). The interpretation of supin V is to take the supremum of its arguments w.r.t. the well-order ≤. In case supis given finitely many arguments, it simply returns the largest. However sup((n,i))_{i∈ℕ} = (n+1,0).

Now let the equivalence relation ∼ on V be defined by (n,m) ∼ (n′,m′) iff n = n′, leaving ∞ in an equivalence class of its own. This relation is a 1-hole congruence on L. Hence, it is also a 2-hole congruence, so one has

((n_{1},m_{1}) ∼ (n′_{1},m′_{1}) ∧ (n_{2},m_{2}) ∼ (n′_{2},m′_{2})) ⇒ (n_{1},m_{1}) + (n_{2},m_{2}) ∼ (n′_{1},m′_{1}) + (n′_{2},m′_{2}).

Yet it fails to be a congruence: (n,i) ∼ (n,0) for all i ∈ ℕ, but

(n+1,0) = sup((n,i))_{i∈ℕ} ≁ sup((n,0))_{i∈ℕ} = (n,0).

It is well known and easy to check that the collection of equivalence relations on any domain V, ordered by inclusion, forms a complete lattice—namely the intersection of arbitrary many equivalence relations is again an equivalence relation. Likewise, the collection of 1-hole congruences for L is also a complete lattice, and moreover a complete sublattice of the complete lattice of equivalence relations on V. The latter implies that for any collection C of 1-hole congruence relations, the least equivalence relation that contains all elements of C (exists and) happens to be a 1-hole congruence relation. Again, this is a property that is well known [41] and easy to prove. It follows that for any equivalence relation ∼ there exists a largest 1-hole congruence for L contained in ∼. I will denote this 1-hole congruence by ∼_{L}^{1c}, and call it the congruence closure of ∼ w.r.t. L. One has v_{1} ∼_{L}^{1c} v_{2} for v_{1},v_{2} ∈ V iff ⟦E⟧_{L} (ν) ∼ ⟦E⟧_{L} (ρ) for any L -expression E and any valuations ν,ρ : X → V with ν(X) = v_{1} and ρ(X) = v_{2} for some X ∈ X and ν(Y) = ρ(Y) for all variables Y ≠ X. Such results do not generally hold for congruences. Example 3 Continue Example 2, but skipping the operator +. Let ∼_{k}be the equivalence on V defined by (n,m) ∼_{k}(n′,m′) iff n = n′∧(m = m′∨m,m′≤ k). It is easy to check that all ∼_{k}for k ∈ ℕ are congruences on the reduced L, and contained in ∼. Yet their least upper bound (in the lattice of equivalence relations on V) is ∼, which is not a congruence itself. In particular, there is no largest congruence contained in ∼. When dealing with languages L in which all operators and other constructs have a finite arity, so that each E ∈ 𝕋_{L} contains only finitely many variables, there is no difference between a congruence and a 1-hole congruence, and thus ∼_{L}^{1c} is a congruence relation for any equivalence ∼. I will apply the theory of expressiveness presented in this paper also to languages like CCS that have operators (such as ∑_{i∈I} E_{i}) of infinite arity. However, in all such cases I’m currently aware of, the relevant choices of L and ∼ have the property that ∼_{L}^{1c} is in fact a congruence relation. As an example, consider weak bisimilarity [50]. This equivalence relation fails to be a congruence for ∑. However, the coarsest 1-hole congruence contained in this relation, often called rooted weak bisimilarity, happens to be a congruence. In fact, when congruence-closing weak bisimilarity w.r.t. the binary sum, the result [31] is also a congruence for the infinitary sum, as well as for all other operators of CCS [50].

Definition 15 Let T be a translation from L into L′. A subset W of V′ is closed under T (L) if ⟦T (E)⟧(η) ∈ W for any expression E ∈ 𝕋_{L} and valuation η : X → W. An equivalence ∼ on W is a congruence (respectively 1-hole congruence) for T (L) on W if for any E ∈ 𝕋_{L} and θ,η : X → W with θ ∼ η (respectively θ ∼^{1} η) one has ⟦T (E)⟧_{L′}(θ) ∼ ⟦T (E)⟧_{L′}(η).

Proposition 3 Let T be a translation from L into L′that is correct w.r.t. a semantic translation R ⊆ V′× V. Let R(V) := {v′∈ V′| ∃v ∈ V. v′R v}. Then R(V) is closed under T (L).

Proof: Let E ∈ 𝕋_{L} and η : X → R(V). Take ρ : X → V with ρ R η. Then ⟦T (E)⟧_{L′}(η) R ⟦E⟧_{L} (ρ). Since ⟦E⟧_{L} (ρ) ∈ V one has ⟦T (E)⟧_{L′}(η) ∈ R(V). □

Proposition 4 Let the translation T from L into L′be correct w.r.t. the semantic translation R ⊆ ∼ . Then ∼ is a (1-hole) congruence for L iff it is a (1-hole) congruence for T (L) on R(V).

Proof: First suppose ∼ is a congruence for L. Let E ∈ 𝕋_{L} and θ,η : X → R(V) with θ ∼ η. By the definition of R(V) there are valuations ν,ρ : X → V with θ R ν and η R ρ. Now ν ∼ θ ∼ η ∼ ρ, so

⟦T (E)⟧_{L′}(θ) R ⟦E⟧_{L} (ν) ∼ ⟦E⟧_{L} (ρ) R^{−1} ⟦T (E)⟧_{L′}(η)

and hence ⟦T (E)⟧_{L′}(θ) ∼ ⟦T (E)⟧_{L′}(η). The other direction proceeds in the same way.

Now suppose ∼ is a 1-hole congruence for L. Let E ∈ 𝕋_{L} and θ,η : X → R(V) with θ ∼^{1} η. Then θ(X) ∼ η(X) for some X ∈ X and θ(Y) = η(Y) for all Y ≠ X. So there must be ν,ρ : X → V with θ R ν, η R ρ and ν(Y) = ρ(Y) for all Y ≠ X. Since ν(X) ∼ θ(X) ∼ η(X) ∼ ρ(X) it follows that ν ∼^{1} ρ. The conclusion proceeds as above, and the other direction goes likewise. □

The requirement of being a congruence for T (L) on R(V) is slightly weaker than that of being a congruence for T (L)—cf. Definition 8—for it proceeds by restricting attention to valuations into R(V) ⊆ U.

Example 4 Let L be a language with two constants Yes and No and a unary operator ¬. Its semantics is given by V = {0,1}, Yes^{V} = 1, No^{V} = 0 and ¬^{V}(b) = 1− b. Let L′be the extension of L with the constant ⊤ and the semantic value ⊤—so V′= {0,1,⊤}—with ⊤^{V′}= ⊤ and ¬^{V′}(⊤) = ⊤. Let ∼ be the semantic equivalence on V′⊇ V given by 0 ≁ 1 ∼ ⊤. Then the identity function I is a translation from L into L′that is valid up to ∼. This is witnessed by the semantic translation R := {(0,0),(1,1)} ⊆ ∼ . The relation ∼ is a congruence for L. In line with Proposition 4 it also is a congruence for I (L) on R(V) = {0,1}. However it fails to be a congruence for I (L) (on U = {0,1,⊤}). So by Proposition 2 the transition I is not correct up to ∼. Indeed, for ρ : X → V a valuation that sends X ∈ X to 1 and η : X → V′a valuation that sends X to ⊤, assuming ρ(Y) = η(Y) for other variables Y, one has ρ ∼ η, yet ⟦I (¬X)⟧_{L′}(η) = ⟦¬X⟧_{L′}(η) = ¬^{V′}(η(X)) = ⊤ ≁ 0 = ¬^{V}(ρ(X)) = ⟦¬X⟧_{L} (ρ).

8 A congruence closure property for valid translations

In many applications, semantic values in the domain of interpretation of a language L are only meaningful up to a semantic equivalence ∼^{c}, and the intended semantic domain could just as well be seen as the set of ∼^{c}-equivalence classes of values. For this purpose it is essential that ∼^{c} is a congruence for L.

Often ∼^{c} is the congruence closure of a coarser semantic equivalence ∼, so that two values end up being identified iff they are ∼-equivalent in every context. An example of this occurred in Section 6, with ≈^{•} in the rôle of ∼ and ≅ ^{c} in the rôle of ∼^{c}. Now Theorem 4, contributed in this section, says that if a translation from L into L′is valid up to ∼, then it is even valid up to an equivalence ∼_{L,R}^{1c} that extends ∼^{c} from V to a subdomain W of V′that suffices for the interpretation of translated expressions from L. This equivalence ∼_{L,R}^{1c} coincides with the congruence closure of ∼ on L, as well as on T (L), and melts each equivalence class of V with exactly one of W, and vice versa.

Let L and L′be languages with ⟦ ⟧_{L} : 𝕋_{L} → ((X → V) → V) and ⟦ ⟧_{L′} : 𝕋_{L′} → ((X → V′) → V′). In this section I assume that V ∩ V′= ∅. To apply the results to the general case, just adapt L′by using a copy of V′—any preorder •∼ on V ∪ V′extends to this copy by considering each copied element •∼ -equivalent to the original. Definition 16 Given any semantic translation R, let ≡_{R} ⊆ (V∪V′)^{2} be the smallest equivalence relation on V ∪ V′containing R. Theorem 3 If a translation T is correct w.r.t. the semantic translation R, then ≡_{R} is a 1-hole congruence for L. Proof: Let E ∈ 𝕋_{L} and ν,ρ : X → V with ν ≡_{R}^{1} ρ. I have to show that ⟦E⟧_{L} (ν) ≡_{R} ⟦E⟧_{L} (ρ).

Let X ∈ X be such that ν(X) ≡_{R} ρ(X) and ν(Y) = ρ(Y) for all Y ≠ X. Then, for some n ≥ 0 there are v_{0},...,v_{n} ∈ V and w_{1},...,w_{n} ∈ V′with ν(X) = v_{0} R^{−1} w_{1} R v_{1} R^{−1} w_{2} R v_{2} R^{−1} ... R v_{n} = ρ(X). For i = 0,...,n let ρ_{i} : X → V be given by ρ_{i}(X) = v_{i} and ρ_{i}(Y) = ρ(Y) for Y ≠ X, and for i = 1,...,n let η_{i} : X → V′be given by η_{i}(X) = w_{i} and η_{i}(Y) = η(Y) for Y ≠ X, for some η : X → V′with η R ρ. Then ν = ρ_{0} R^{−1} η_{1} R ρ_{1} R^{−1} η_{2} R ρ_{2} R^{−1} ... R ρ_{n} = ρ. Hence ⟦E⟧_{L} (ρ_{0}) R^{−1} ⟦T (E)⟧_{L′}(η_{1}) R ⟦E⟧_{L} (ρ_{1}) R^{−1} ⟦T (E)⟧_{L′}(η_{2}) R ⟦E⟧_{L} (ρ_{2}) R^{−1} ···R ⟦E⟧_{L} (ρ_{n}). Thus ⟦E⟧_{L} (ν) ≡_{R} ⟦E⟧_{L} (ρ). □ By Proposition 4 ≡_{R} also is a 1-hole congruence for T (L) on R(V). Only the subset R(V) of V′ matters for the purpose of translating L into L′. On V′\ R(V) the equivalence ≡_{R} is the identity. Theorem 4 Let T be a translation from a language L, with semantic domain V, into a language L′, with domain V′, that is valid up to a semantic equivalence ∼. Then T is even valid up to a semantic equivalence ∼_{L,R}^{1c} , contained in ∼, such that (1) the restriction of ∼_{L,R}^{1c} to V is the largest 1-hole congruence for L contained in ∼, (2) the set W := {v ∈ V′| ∃v ∈ V. v′∼_{L,R}^{1c} v} is closed under T (L), and (3) the restriction of ∼_{L,R}^{1c} to W is the largest 1-hole congruence for T (L) on W that is contained in ∼. Proof: By assumption the translation T from L into L′is correct w.r.t. a semantic translation R ⊆ ∼ . Let ∼_{L,R}^{1c} , the congruence closure of ∼ w.r.t. L and R, be the binary relation on V ∪ V′ defined by w_{1} ∼_{L,R}^{1c} w_{2} iff w_{1} ≡_{R} v_{1} ∼_{L}^{1c} v_{2} ≡_{R} w_{2} for some v_{1},v_{2} ∈ V. Here ∼_{L}^{1c} is the largest 1-hole congruence for L, defined on V, that is contained in ∼.

Since ≡_{R} is a 1-hole congruence for L contained in ∼ (by Theorem 3), and ∼_{L}^{1c} is the largest 1-hole congruence for L contained in ∼, one has v ≡_{R} w ⇒ v ∼_{L}^{1c} w for all v,w ∈ V. From this it follows that ∼_{L,R}^{1c} is transitive. As ≡_{R} and ∼_{L}^{1c} are reflexive and symmetric, so is ∼_{L,R}^{1c} . Thus, ∼_{L,R}^{1c} is an equivalence relation. Since ∼_{L}^{1c} and R, and hence also ≡_{R}, are contained in ∼, so is ∼_{L,R}^{1c} . Moreover, R ⊆ ≡_{R} ⊆ ∼_{L,R}^{1c} , so T is valid up to ∼_{L,R}^{1c} . It remains to check properties (1)–(3).

Let E ∈ 𝕋_{L} be an L -expression and ν,ρ : X → V be valuations with ν ∼^{1} ρ. Then there are valuations ν′,ρ′: X → V with ν ≡_{R}^{1} ν′(∼_{L}^{1c})^{1} ρ′≡_{R}^{1} ρ . Since ≡_{R} and ∼_{L}^{1c} are 1-hole congruences, it follows that ⟦E⟧_{L} (ν) ≡_{R} ⟦E⟧_{L} (ν′) ∼_{L}^{1c} ⟦E⟧_{L} (ρ′) ≡_{R} ⟦E⟧_{L} (ρ), so ⟦E⟧_{L} (ν) ∼_{L,R}^{1c} ⟦E⟧_{L} (ρ). Thus ∼_{L,R}^{1c} is a 1-hole congruence for L on V. Since ∼_{L}^{1c} is the largest 1-hole congruence for L contained in ∼, it follows that, restricted to V, ∼_{L,R}^{1c} ⊆ ∼_{L}^{1c} . By the reflexivity of ≡_{R} one moreover has ∼_{L}^{1c} ⊆ ∼_{L,R}^{1c} , so ∼_{L,R}^{1c} = ∼_{L}^{1c} , i.e. (1) holds.

Let W := {w ∈ V′| ∃v ∈ V. w ∼_{L,R}^{1c} v}. By definition, W = R(V). So by Proposition 3 W is closed under T (L), i.e. (2) holds.

By Proposition 4 ∼_{L,R}^{1c} is a 1-hole congruence for T (L) on W = R(V), contained in ∼. Let ≈ be any other 1-hole congruence on W contained in ∼. Define the relation ≈_{R} on V ∪ W by v_{1} ≈_{R} v_{2} iff v_{1} ≡_{R} w_{1} ≈ w_{2} ≡_{R} v_{2} for some w_{1},w_{2} ∈ W, and let ≈_{R}^{∗} be its transitive closure. Then ≈_{R}^{∗} is an equivalence relation on V ∪ W. Since ≡_{R} and ≈ are 1-hole congruences for T (L) on W, by the same reasoning as above also ≈_{R}^{∗} is a 1-hole congruence for T (L) on W. As R ⊆ ≡_{R} ⊆ ≈_{R}^{∗} , by Proposition 4, ≈_{R}^{∗} is a 1-hole congruence for L. Since ∼_{L}^{1c} is the largest 1-hole congruence for L contained in ∼, it follows that, restricted to V, ≈_{R}^{∗} ⊆ ∼_{L}^{1c} .

For each w_{1},w_{2} ∈ W with w_{1} ≈ w_{2} there are v_{1},v_{2} ∈ V with v_{1} ≡_{R} w_{1} ≈ w_{2} ≡_{R} v_{2} . So v_{1} ≈_{R} v_{2} and hence v_{1} ∼_{L}^{1c} v_{2}, and thus w_{1} ∼_{L,R}^{1c} w_{2} , by definition. So ≈ ⊆ ∼_{L,R}^{1c} and (3) holds. □

Note that each equivalence class of ∼_{L,R}^{1c} on V∪W melts an equivalence class of ∼_{L,R}^{1c} on V with one of ∼_{L,R}^{1c} on W. Moreover, on V the relation is completely determined by L and ∼. The following example shows that in general the whole relation ∼_{L,R}^{1c} is not completely determined by L and ∼.

Example 5 Let L be a language with two constants Yes and No and a binary operator same. Its semantics is given by V = {0,1,⊤,⊥}, Yes^{V} = 1, No^{V} = 0 and same^{V}(x,y) = 1 if x = y, while same^{V}(x,y) = 0 if x ≠ y. The semantic values ⊤ and ⊥ are not denotable as the interpretation of closed terms. Let L′ be an exact copy of L, except that the semantic values are primed. Let ∼ be the semantic equivalence on V ∪ V′ given by 0 ∼ 0′ ≁ 1 ∼ 1′ ≁ ⊤ ∼ ⊤′∼ ⊥ ∼ ⊥′. Then the identity function I is a translation from L into L′ that is valid up to ∼. This is witnessed by the semantic translation R^{†} := {(0′,0),(1′,1),(⊤′,⊥),(⊥′,⊤)} ⊆ ∼ , or, alternatively, by the semantic translation R := {(0′,0),(1′,1),(⊤′,⊤),(⊥′,⊥)} ⊆ ∼ . Upon taking the congruence closure ∼_{L}^{1} , the four semantic values of V become inequivalent. Yet, there are two candidates for ∼_{L,R}^{1c} , namely R^{†} and R.

Corollary 1 Let T be a translation from a language L, with semantic domain V, into a language L′, with domain V′, valid up to a semantic equivalence ∼, and suppose the congruence closure ∼_{L}^{1} of ∼ w.r.t. L is in fact a congruence. Then T is correct up to the equivalence ∼_{L,R}^{1c} described in Theorem 4.

Proof: By the proof of Theorem 4 T is correct w.r.t. the semantic translation R ⊆ ∼_{L,R}^{1c} , the restriction of ∼_{L,R}^{1c} to V equals ∼_{L}^{1} , and R(V) = W. Using that ∼_{L}^{1} is a congruence for L, by Proposition 4 ∼_{L,R}^{1c} is a congruence for T (L) on R(V). Since R(V) = W, which for ∼_{L,R}^{1c} is the U used in Definition 8, ∼_{L,R}^{1c} is a congruence for T (L). So by Theorem 1, T is correct up to ∼_{L,R}^{1c} . □

The languages π and aπ of Section 6 do not feature operators (or other constructs) of infinite arity. Hence the congruence closure ∼_{π}^{1c} or ∼_{aπ}^{1c} of an equivalence ∼ on π or aπ is always a congruence. So by Corollary 1 Boudol’s translation T is correct up to an equivalence ≈^{•} _{π,R}^{c}, defined on the disjoint union of the domains T_{π} and T_{aπ} on which the two languages are interpreted. This equivalence is contained in ≈^{•} , and on the source domain T_{π} coincides with ≅ ^{c}. By Theorem 4, the restriction of ≈^{•} _{π,R}^{c} to a subdomain W ⊆ T_{aπ} is the largest congruence for T (π) on W that is contained in ≈^{•} . As ≅ _{a}^{c} is a congruence for all of aπ on all of T_{aπ}, and contained in ≈^{•} , it is certainly a congruence for T (π) on W, and thus contained in ≈^{•} _{π,R}^{c}. This inclusion turns out to be strict. As an illustration of that, note that x̄z.0|x̄z.0 ≅ ^{c} x̄z.x̄z0. (This follows since these processes are strong (early) bisimilar [76] and thus strong full bisimilar by [76, Def. 2.2.2].) Consequently, their translations must be related by ≈^{•} _{π,R}^{c}. So, for distinct u,v,y,w,x,z ∈ N ,

(u)(x̄u|u(v).(v̄z|0))|(u)(x̄u|u(v).(v̄z|0)) ≈^{•} _{π,R}^{c} (y)(x̄y|u(w).(w̄z|(u)(x̄u|u(v).(v̄z|0)))).

Yet, these processes are not ≅ _{a}^{c}-equivalent, as can be seen by putting them in a context x(y).x(y).r̄(s)|X. In this context, only the left-hand side has a weak barb ⇓r̄.

9 Integrating language features through translations

The results of the previous section show how valid translations are satisfactory for comparing the expressiveness of languages. If there is a valid translation T from L to L′up to ∼, and (as usual) ∼_{L}^{1c} is a congruence, then all truths that can be expressed in terms of L can be mimicked in L′. For the congruence classes of ∼_{L}^{1c} translate bijectively to congruence classes of an induced equivalence relation on the domain of T (L) (within the domain of L′), and all operations on those congruence classes that can be performed by contexts of L have a perfect counterpart in terms of contexts of T (L). This state of affairs was illustrated on Boudol’s translation from a synchronous to an asynchronous π-calculus.

There is however one desirable property of translations between languages that has not yet been achieved, namely to combine the powers of two languages into one unified language. If both languages L_{1} and L_{2} have valid translations into a language L′, then all that can be done with L_{1} can be mimicked in a fragment of L′, and all that can be done with L_{2} can be mimicked in another fragment of L′. In order for these two fragments to combine, one would like to employ a single congruence relation on L′ that specialises to congruence relations for T_{1}(L_{1}) and T_{2}(L_{2}), which form the counterparts of relevant congruence relations for the source languages L_{1} and L_{2}.

In terms of the translation T from π to aπ, the equivalence ≅ _{a}^{c} on T_{aπ} would be the right congruence relation to consider for aπ. Ideally, this congruence would extend to an equivalence ≅ _{π,aπ}^{c} on the disjoint union T_{π} ⊎ T_{aπ}, such that the restriction of ≅ _{π,aπ}^{c} to T_{π} is a congruence for π. Necessarily, this congruence on T_{π} would have to distinguish the terms x̄z.0|x̄z.0 and x̄z.x̄z0, since their translations are distinguished by ≅ _{a}^{c}. One therefore expects ≅ _{π,aπ}^{c} on T_{π} to be strictly finer than ≅ ^{c}. Here it is important that the union of T_{π} and T_{aπ} on which this congruence is defined is required to be disjoint. For if one considers T_{aπ} as a subset of T_{π}, then we obtain that the restriction of ≅ _{π,aπ}^{c} to that subset (1) coincides with ≅ _{a}^{c} and (2) is strictly finer than ≅ ^{c}. This contradicts the fact that ≅ ^{c} is strictly finer than ≅ _{a}^{c}.

In Section 13 I will show that such a congruence ≅ _{π,aπ}^{c} indeed exists. In fact, under a few very mild conditions this result holds generally, provided that the source language L is a closed-term language. The following example illustrated why that restriction needs to be imposed.

Example 6 Let L be a language with three constants ⊤, Yes and No. Its semantics is given by V = {+,−}, ⊤^{V} = Yes^{V} = + and No^{V} = −. Let L′be a language with the same three constants and a unary operator next. Its semantics is given by V′= {0,1,2} with ⊤^{V′} = 2, Yes^{V′} = 1 and No^{V′} = 0, while next^{V′}(n) = (n + 1)mod3. Let ∼ be the semantic equivalence on V′∪ V given by − ∼ 0 ≁ 1 ∼ 2 ∼ +. Then the identity function I is a translation from L into L′that is valid up to ∼. This is witnessed by the semantic translation R := {(0,−),(1,+),(2,+)} ⊆ ∼ . The congruence closure of ∼ on V′is the identity relation. This relation cannot be extended to V ∪ V′in such a way that T remains valid. For 1 and 2 need to be different; yet to make T valid both need to be related to +.

10 A unique decomposition of terms

The results of Sections 12–16 apply only to languages that satisfy two postulates, and to preorders •∼ that “respect =^{α} ” (defined in Section 11). Below and in Section 11 I formulate these postulates.

Definition 17 α-conversion is the act of renaming all occurrences of a bound variable X within the scope of its binding into another variable, say Y, while avoiding capture of free variables. Here one speaks of capture when a free occurrence of Y turns into a bound one.

Write E =^{α} F if expression E can be converted into F by multiple acts of α-conversion.

In languages where there are multiple types of bound variables, =^{α} allows conversion of all of them. In a π-calculus with recursion, for instance, there could be bound process variables X ∈ X as well as bound names x ∈ N . The last two conversions in the right column of Definition 10 define α-conversion for π-calculus names.

The following notation and observation is used below and in Section 12.1.

Definition 18 Given two substitutions σ,ξ : X ⇀ 𝕋_{L} , their composition ξ • σ with dom(ξ • σ) = dom(σ) is given by (ξ • σ)(X) = σ(X)[ξ].

Observation 3 If dom(σ) = fv(E) then E[σ][ξ] =^{α} E[ξ • σ].

An expression E of the form f(E_{1},...,E_{n}) can be written as H[σ], where H is an expression f(X_{1},...,X_{n}) and σ : {X_{1},...,X_{n}} → 𝕋_{L} is the substitution with σ(X_{i}) = E_{i} for i = 1,...,n. Here H and σ are completely determined by E, except for the choice of the variables X_{1},...,X_{n}. The term H is called a head of E. In this paper, for the proofs of Section 12, I propose a unique decomposition of expressions E into H and σ, by making an arbitrary choice for the variables X_{1},...,X_{n}. Moreover, I extend this decomposition to all terms E that are not variables. This requires a postulate that says, in essence, that such a decomposition is always possible, and restricting attention to languages satisfying this postulate.

Definition 19 ([32]) A term E ∈ 𝕋_{L} is a prefix of a term F, written E ≤ F, if F =^{α} E[σ] for some substitution σ with dom(σ) = fv(E).

Note that E[id_{E}] = E, where id_{E} : fv(E) → 𝕋_{L} is the identity. Moreover, if dom(σ) = fv(E) then E[σ][ξ] =^{α} E[ξ • σ], by Observation 3. It follows that ≤ is reflexive and transitive, and hence a preorder. Write ≡ for the kernel of ≤, i.e. E ≡ F iff E ≤ F ∧ F ≤ E. Note that E =^{α} F implies E ≡ F. If E ≡ F then E can be converted into F by means of an injective renaming of its variables.

Definition 20 ([32]) A term H ∈ 𝕋_{L} is a head if H is not a single variable and E ≤ H implies that E is a single variable or E ≡ H. It is a head of another term F if it is a head, as well as a prefix of F.

Example 7 Let c be a constant, g a unary operator, f a binary operator, and μX.E the recursion construct of CCS. Then f(X,Y) is a head of the term f(c,g(c)), and μX.f(Y,g(g(X))) is a head of μX.f(g(c),g(g(X))). See [32] for further detail.

Postulate 1 ([32]) Each expression E, if not a variable, has a head, which is unique up to ≡.

This is easy to show for each common type of system description language, and I am not aware of any counterexamples. However, while striving for maximal generality, I consider languages with (recursionlike) constructs that are yet to be invented, and in view of those, this principle has to be postulated rather than derived. This means that in this section I consider only languages that satisfy this postulate.

Pick a representative from each ≡-equivalence class of heads, and call the chosen representatives standard heads. Likewise, pick a representative from each =^{α} -class of terms, and call a substitution σ where σ(X) is such a representative for each X ∈ dom(σ) a standard substitution. Now each expression E ∉ X can uniquely be written as E =^{α} H[σ], with H a standard head and σ a standard substitution with dom(σ) = fv(E). I will refer to the pair H,σ as the standard decomposition of E.

11 Invariance of meaning under α-conversion

Write v =^{α} _{L} w, with v,w ∈ V, iff there are terms E,F ∈ 𝕋_{L} with E =^{α} F, and a valuation ζ : X → V such that ⟦E⟧_{L} (ζ) = v and ⟦F ⟧_{L} (ζ) = w. This relation is reflexive and symmetric.

In [32] I limited attention to languages satisfying

if E =^{α} F then ⟦E⟧_{L} = ⟦F ⟧_{L} .  (2)

This postulate says that the meaning of an expression is invariant under α-conversion. It can be reformulated as the requirement that =^{α} _{L} is the identity relation. This postulate is satisfied by all my intended applications, except for the important class of closed-term languages. Languages like CCS and the πcalculus can be regarded as falling in this class (although it is also possible to declare the meaning of a term under a valuation to be an =^{α} -equivalence class of closed terms). To bring this type of application within the scope of my theory, here I weaken this postulate by requiring merely that =^{α}_{L} is an equivalence. Postulate 2 =^{α} _{L} is an equivalence relation. This postulate is needed for the results of Sections 12–16. I also need to restrict attention to preorders •∼ with =^{α} _{L} ⊆ •∼ . When that holds I say that the preorder •∼ respects =^{α} _{L} . If (2) holds—which strengthens of Postulate 2—then any preorder respects =^{α} _{L} .

12 Compositionality

An important property of translations, defined below, is compositionality. In this section show I that any valid translation up to a preorder •∼ can be modified into such a translation that moreover is compositional, provided one restricts attention to languages that satisfy Postulates 1 and 2, and preorders •∼ that

respect =^{α} .

Definition 21 A translation T from L into L′is compositional if

(1) T (E[σ]) =^{α} T (E)[T ∘ σ] for each E ∈ 𝕋_{L} and σ : fv(E) → 𝕋_{L} ,

(2) E =^{α} F implies T (E) =^{α} T (F) for all E,F ∈ 𝕋_{L} ,

(3) and moreover T (X) = X for each X ∈ X . In case E = f(t_{1},...,t_{n}) for certain t_{i} ∈ 𝕋_{L} this amounts to T (f(t_{1},...,t_{n})) =^{α} E_{f} (T (t_{1}),...,T (t_{n})), where E_{f} := T (f(X_{1},...,X_{n})) and E_{f} (u_{1},...,u_{n}) denotes the result of the simultaneous substitution in this expression of the terms u_{i} ∈ 𝕋_{L′} for the free variables X_{i}, for i = 1,...,n. The first requirement of Definition 21 is more general and covers language constructs other than functions, such as recursion. Requiring equality rather than =^{α} is too demanding, as the following example illustrates. Example 8 Take a source language L that features an unary replication operator !, as in the π-calculus, and a target language L′ that instead has a recursion construct μX.E, as in CCS; both languages have a constant 0. A suitable translation T satisfies T (!X_{1}) = μX.(X|X_{1}) and T (0) = 0. Applying Definition 21 with σ(X_{1}) = 0 gives T (!0) =^{α} μX.(X|0), whereas applying it with σ(X_{1}) = X gives T (!X) =^{α} μY.(Y |X). Here the bound variable X needed to be renamed (into Y) to avoid capture of the free variable X that is substituted for X_{1}. Furthermore, applying Definition 21 on T (!X) =^{α} μY.(Y |X) with σ(X) = 0 gives T (!0) =^{α} μY.(Y |0). Since X ≠ Y, this shows that =^{α} cannot consistently be replaced by =. Lemma 1 If T_{1} : 𝕋_{L_{1}} → 𝕋_{L_{2}} and T_{2} : 𝕋_{L_{2}} → 𝕋_{L_{3}} are compositional translations, then so is their composition T_{2}∘ T_{1} : 𝕋_{L_{1}} → 𝕋_{L_{3}} , defined by T_{2}∘ T_{1}(E) := T_{2}(T_{1}(E)) for all E ∈ L_{1}. Proof: (1) T_{2}(T_{1}(E[σ])) =^{α} T_{2}(T_{1}(E)[T_{1}∘σ]) =^{α} T_{2}(T_{1}(E))[T_{2}∘T_{1}∘σ]) for each σ : X ⇀ 𝕋_{L_{1}} and E ∈ 𝕋_{L_{1}} . Here the derivation of the first =^{α} uses Property (2) of Definition 21—and this is the reason for requiring that property.

(2) E =^{α} F implies T_{1}(E) =^{α} T_{1}(F) and hence T_{2}(T_{1}(E)) =^{α} T_{2}(T_{1}(F)) for all E,F ∈ 𝕋_{L} .

(3) T_{2}(T_{1}(X)) = T_{2}(X) = X for each X ∈ X . □

12.1 Translations that are compositional by construction

The following proposition shows that when verifying that a translation is compositional it suffices to check requirement (1) of Definition 21 for the case that the term E is a (standard) head only. In most applications (including the one of Section 6) a translation is defined inductively, in such a way that (1) for E a head, as well as (2) and (3), hold by definition; in such cases compositionality follows.

Proposition 5 Let L be a language satisfying Postulate 1. Any translation T from L into L′satisfying

T (X) = X  for X ∈ X , and
T (E) =^{α} T (H)[T ∘ σ] when E =^{α} H[σ] with H,σ the standard decomposition of E.

is compositional.

Proof: By assumption, this translation satisfies Properties (2) and (3) of Definition 21. Next, I show that T also satisfies Property (1), using induction on E/_{=^{α}}. So let E ∈𝕋_{L} and ξ: fv(E) → 𝕋_{L} . I have to show that T (E[ξ]) =^{α} T (E)[T ∘ ξ]. The case E ∈ X is trivial, so let E =^{α} H[σ], with H a standard head and σ a standard substitution with dom(σ) = fv(H). For each free variable X of H, σ(X) is a proper subterm of E up to =^{α} , so by the induction hypothesis T (σ(X)[ξ]) =^{α} T (σ(X))[T ∘ ξ]. Thus, for X ∈ fv(H),

(T ∘ (ξ • σ))(X)= T ((ξ • σ)(X))  by definition of functional composition ∘
= T (σ(X)[ξ])  by definition of the operation • on substitutions
=^{α} T (σ(X))[T ∘ ξ]  by induction, derived above
= ((T ∘ ξ) • (T ∘ σ))(X) by definition of the operations ∘ and •.

This shows that the substitutions T ∘(ξ •σ) and (T ∘ξ)•(T ∘σ)—both with domain fv(H)—are equal up to α-conversion, from which it follows that F [T ∘(ξ •σ)] =^{α} (F [T ∘σ])[T ∘ξ] for all terms F ∈ 𝕋_{L′}.

Hence T (E[ξ])=^{α} T (H[σ][ξ])  since E =^{α} H[σ], and thus E[ξ] =^{α} H[σ][ξ], using (2) =^{α} T (H[ξ • σ])  by Observation 3 =^{α} T (H[υ])  for a standard substitution υ =^{α} ξ • σ =^{α} T (H)[T ∘ υ]  by assumption =^{α} T (H)[T ∘ (ξ • σ)]  replacing υ by ξ • σ, using (2) =^{α} (T (H)[T ∘ σ])[T ∘ ξ] derived above =^{α} T (E)[T ∘ ξ]  by assumption. □

12.2 The denotation of a substitution

To obtain the compositionality of valid translations, I need the concept of the denotation of a substitution as a transformation of valuations. The semantic mapping ⟦ ⟧_{L} : 𝕋_{L} → ((X → V) → V) extends to substitutions σ by ⟦σ⟧_{L} (ρ)(X) := ⟦σ(X)⟧_{L} (ρ) for all X ∈ X and ρ : X → V—here σ is extended to a total function by σ(Y) := Y for all Y ∉ dom(σ). Thus ⟦σ⟧_{L} is of type (X → V) → (X → V), i.e. a map from valuations to valuations. The inductive nature of the semantic mapping ⟦ ⟧_{L} ensures that for each expression E ∈ 𝕋_{L} , substitution σ : X ⇀ 𝕋_{L} and valuation ρ : X → V there exists a term F with E =^{α} F such that ⟦E[σ]⟧_{L} (ρ) = ⟦F [σ]⟧_{L} (ρ) = ⟦F ⟧_{L} (⟦σ⟧_{L} (ρ)), and hence

⟦E[σ]⟧_{L} (ρ) =^{α} _{L} ⟦E⟧_{L} (⟦σ⟧_{L} (ρ)).  (3)

In case E is f(X_{1},...,X_{n}) this amounts to ⟦f(E_{1},...,E_{n})⟧_{L} (ρ) = f^{V}(⟦E_{1}⟧_{L} (ρ),...,⟦E_{n}⟧_{L} (ρ)), but the above is more general and anticipates language constructs other than functions, such as recursion.

12.3 Closing a semantic translation under α-conversion

The following lemma (assuming Postulate 2) says that =^{α} _{L} is a congruence.

Lemma 2 Let E ∈ 𝕋_{L} and ν,ρ : X → V. If ν =^{α} _{L} ρ then ⟦E⟧_{L} (ν) =^{α} _{L} ⟦E⟧_{L} (ρ).

Proof: Suppose ν =^{α} _{L} ρ. Then, for each X ∈ X , ν(X) =^{α} _{L} ρ(X), so there are terms E_{X},F_{X} ∈ 𝕋_{L} with E_{X} =^{α} F_{X} and a valuation ζ_{X}: X → V such that ⟦E_{X}⟧_{L} (ζ_{X}) = ν(X) and ⟦F_{X}⟧_{L} (ζ_{X}) = ρ(X). By renaming of variables one can assure that fv(E_{X}) ∩ fv(E_{Y}) = ∅ for any different X,Y ∈ fv(E). Here I assume that the set X of variables is sufficiently large. Note that fv(F_{X}) = fv(E_{X}) for all X ∈ fv(E). Let ζ : X → V be a valuation satisfying ζ(Z) = ζ_{X}(Z) for any Z ∈ fv(E_{X}) with X ∈ fv(E). Define the substitutions σ,ξ : fv(E) → 𝕋_{L} by σ(X) = E_{X} and ξ(X) = F_{X} for all X ∈ fv(E). Then ⟦σ(X)⟧_{L} (ζ) = ν(X) and ⟦ξ(X)⟧_{L} (ζ) = ρ(X) for all X ∈ fv(E). Hence, using (3), ⟦E⟧_{L} (ν) = ⟦E⟧_{L} (⟦σ⟧_{L} (ζ)) =^{α} _{L} ⟦E[σ]⟧_{L} (ζ)

and ⟦E⟧_{L} (ρ) = ⟦E⟧_{L} (⟦ξ⟧_{L} (ζ)) =^{α} _{L} ⟦E[ξ]⟧_{L} (ζ). As σ(X) =^{α} ξ(X) for all X ∈X one has E[σ] =^{α} E[ξ],

and thus ⟦E⟧_{L} (ν) =^{α} _{L} ⟦E[σ]⟧_{L} (ζ) =^{α} _{L} ⟦E[ξ]⟧_{L} (ζ) =^{α} _{L} ⟦E⟧_{L} (ρ). Hence ⟦E⟧_{L} (ν) =^{α} _{L} ⟦E⟧_{L} (ρ) with

Postulate 2. □ Given a relation R ⊆ V′× V, define R^{α} by w R v iff ∃w′,v′. w =^{α} _{L′} w′R v′ =^{α} _{L} v. Lemma 3 If a translation T between languages L and L′ that satisfy Postulate 2 is correct w.r.t. a semantic translation R, then it is also correct w.r.t. R^{α}. Proof: Let R ⊆ V′×V be a semantic translation, and T a translation that is correct w.r.t. R. Let E ∈ 𝕋_{L} , η : X → V′and ρ : X → V, with η R^{α} ρ. Then there must be valuations θ : X → V′and ν : X → V with η =^{α} _{L′} θ R ν =^{α} _{L} ρ. Since T is correct w.r.t. R one has ⟦T (E)⟧_{L′}(θ) R ⟦E⟧_{L} (ν). By Lemma 2

⟦T (E)⟧_{L′}(η) =^{α} _{L′} ⟦T (E)⟧_{L′}(θ) R ⟦E⟧_{L} (ν) =^{α} _{L} ⟦E⟧_{L} (ρ) and thus ⟦T (E)⟧_{L′}(η) R^{α} ⟦E⟧_{L} (ρ). □

12.4 Only the effect on standard heads matters

Proposition 6 Let L and L′ be languages that satisfy Postulates 1 and 2, and R ⊆ V′× V a semantic translation. A compositional translation T : 𝕋_{L} → 𝕋_{L′} is correct w.r.t. R^{α} iff ⟦T (H)⟧_{L′}(η) R^{α} ⟦H⟧_{L} (ρ) for all standard heads H ∈ 𝕋_{L} and all valuations η : X → V′and ρ : X → V with η R^{α} ρ. Proof: “Only if” follows immediately from Definition 3. So assume ⟦T (H)⟧_{L′}(η) R^{α} ⟦H⟧_{L} (ρ) for all standard heads H ∈ 𝕋_{L} and all η : X → V′and ρ : X → V with η R^{α} ρ. I have to show that T is correct w.r.t. R^{α}, i.e. that ⟦T (E)⟧_{L′}(η) R^{α} ⟦E⟧_{L} (ρ) for all terms E ∈ 𝕋_{L} and all η : X → V′and ρ : X → V with η R^{α} ρ. Let η and ρ be such valuations. I proceed with structural induction on E, up to =^{α} . When handling a term E =^{α} H[σ], σ(X) is, up to =^{α} , a proper subterm of E for each free variable X of H. So by induction ⟦T (σ(X))⟧_{L′}(η) R^{α} ⟦σ(X)⟧_{L} (ρ). The valuation ⟦σ⟧_{L} (ρ) is defined such that ⟦σ⟧_{L} (ρ)(X) = ⟦σ(X)⟧_{L} (ρ) for each X ∈ X . Likewise, ⟦T ∘σ⟧_{L′}(η)(X) = ⟦T (σ(X))⟧_{L′}(η) for each X ∈ X . Hence ⟦T ∘ σ⟧_{L′}(η) R^{α} ⟦σ⟧_{L} (ρ). (*)

• ⟦T (X)⟧_{L′}(η) = ⟦X⟧_{L′}(η) \begin{matrix}= η(X) & by definitions of T and ⟦ ⟧_{L′} \\ R^{α} ρ(X) & since η R^{α} ρ \\ = ⟦X⟧_{L} (ρ) & by definition of ⟦ ⟧_{L} . \end{matrix}

• ⟦T (E)⟧_{L′}(η) \begin{matrix}=^{α} _{L′} & ⟦T (H)[T ∘ σ]⟧_{L′}(η) & by the compositionality of T , since E =^{α} H[σ] \\ =^{α} _{L′} & ⟦T (H)⟧_{L′}(⟦T ∘ σ⟧_{L′}(η)) & by (3) \\ R^{α} & ⟦H⟧_{L} (⟦σ⟧_{L} (ρ)) & by assumption, using (*) above \\ =^{α} _{L} & ⟦H[σ]⟧_{L} (ρ) & by (3) \\ =^{α} _{L} & ⟦E⟧_{L} (ρ) & since E =^{α} H[σ]. □ \end{matrix}

12.5 Correct and valid transitions can be made compositional

Theorem 5 Let L and L′be languages satisfying Postulates 1 and 2. If any correct translation from L into L′w.r.t. R^{α} exists, then there is a compositional translation from L into L′that is correct w.r.t. R^{α}.

Proof: Given a translation T_{0} that is correct w.r.t. R^{α}, define the translation T inductively by

T (X) := X  for X ∈ X
T (E) := T_{0}(H)[T ∘ σ] when E =^{α} H[σ] with H,σ the standard decomposition of E.

By filling in H[id_{H}] for E, with H a standard head and id_{H} the identity substitution on fv(H), I obtain T (H) = T_{0}(H) for each standard head H. Hence, by Proposition 5, T is compositional. Moreover, since T_{0} is correct w.r.t. R^{α}, for all standard heads H ∈ 𝕋_{L} and all η : X → V′and ρ : X → V with η R^{α} ρ one has ⟦T (H)⟧_{L′}(η) = ⟦T_{0}(H)⟧_{L′}(η) R^{α} ⟦H⟧_{L} (ρ). Thus, by Proposition 6, T is correct w.r.t. R^{α}. □

Corollary 2 Let L and L′be languages that satisfy Postulates 1 and 2, and •∼ a preorder that respects =^{α} _{L} and =^{α} _{L′}. If any valid (or correct) translation from L into L′up to •∼ exists, then there exists a compositional translation that is valid (or correct) up to •∼ .

Proof: Let T : 𝕋_{L} → 𝕋_{L′} be valid up to •∼ . Then T is correct w.r.t. some semantic translation R ⊆ V′× V with R ⊆ •∼ . By Lemma 3 T is correct w.r.t. R^{α}. By Theorem 5 there exists a compositional translation T ′: 𝕋_{L} → 𝕋_{L′} that is correct w.r.t. R^{α}. Since •∼ respects =^{α} _{L} and =^{α} _{L′}, one has =^{α} _{L} ,=^{α} _{L′},R ⊆ •∼ , and thus R^{α} ⊆ •∼ . The statement about correct translations up to •∼ follows in the same way, or as a corollary by use of Theorem 1. □

Hence, for the purpose of comparing the expressive power of languages, valid translations between them can be assumed to be compositional. For correct translations this was already established in [32], but assuming (2), a stronger version of Postulate 2.

13 Translations from closed-term languages reflect target congruences

I can now establish the theorem promised in Section 9. In view of Corollary 2, no great sacrifices are made by assuming that the translation T is compositional. Additional “mild conditions” needed here are Postulate 2 for L′and ≈ respecting =^{α} _{L′}.

Theorem 6 Let L be a closed-term language and L′a language that satisfies Postulate 2. Let T be a compositional translation from L into L′ that is valid up to ∼. Let ≈ be any congruence for L′ containing =^{α} _{L′} and contained in ∼. Then T is correct up to an equivalence ≈_{T} on V∪V′, contained in ∼, that on V′coincides with ≈.

Proof: If V = ∅, the statement is trivial. Otherwise, pick a valuation ζ : X → V. By assumption, T is correct w.r.t. a semantic translation R ⊆ ∼ . Now pick a valuation θ : X → V′with θ R ζ. Let ≡_{T} be the smallest equivalence relation on V ∪ V′such that ⟦T (P)⟧_{L′}(θ) ≡_{T} ⟦P⟧_{L} for all P ∈ T_{L} . Since T is correct w.r.t. R, one has ⟦T (P)⟧_{L′}(θ) R ⟦P⟧_{L} (ζ) = ⟦P⟧_{L} for all P ∈ T_{L} . Hence ≡_{T} ⊆ ∼ .

Define ≈_{T} on V ∪ V′by v_{1} ≈_{T} v_{2} iff v_{1} ≡_{T} w_{1} ≈ w_{2} ≡_{T} v_{2} for some w_{1},w_{2} ∈ V′. Then ≈_{T} ⊆ ∼ . Since L is a closed-term language, for each v ∈ V there is exactly one P ∈ T_{L} with ⟦P⟧_{L} = v, namely P = v. Hence, each ≡_{T} -equivalence class on V ∪ V′contains exactly one element of V′. It follows that ≈_{T} is transitive, and hence an equivalence relation. Moreover, on V′it coincides with ≈. It remains to show that T is valid up to ≈_{T} . For then Theorem 1 implies that T is correct up to ≈_{T} .

Let R_{T} := {(w,v) | v ∈ T_{L} ∧w =^{α} _{L′} ⟦T (v)⟧_{L′}(θ)}. Then R_{T} is a semantic translation with R_{T} ⊆ ≈_{T} , using that =^{α} _{L′} ⊆ ≈ . To show validity of T up to ≈_{T} it suffices to establish that T is correct w.r.t. R_{T} . So let E ∈ 𝕋_{L} and let η: X → V′and ρ: X → V be valuations with η R_{T} ρ. I have to show that ⟦T (E)⟧_{L′}(η) R_{T} ⟦E⟧_{L} (ρ). Since L is a closed-term language, ρ also is a closed substitution, and ⟦E⟧_{L} (ρ) := E[ρ] =: ⟦E[ρ]⟧_{L} . Let T ∘ρ : X → T_{L′} be the substitution with (T ∘ρ)(X) = T (ρ(X)) for all X. Then—filling in (η(X),ρ(X)) for (w,v) in the definition of R_{T} —η(X) =^{α} _{L′} ⟦(T ∘ ρ)(X)⟧_{L′}(θ) for all X ∈ X , i.e., η =^{α} _{L′} ⟦T ∘ ρ⟧_{L′}(θ). So, using Lemma 2, (3) and compositionality,

⟦T (E)⟧_{L′}(η) =^{α} _{L′} ⟦T (E)⟧_{L′}(⟦T ∘ ρ⟧_{L′}(θ)) =^{α} _{L′} ⟦T (E)[T ∘ σ])⟧_{L′}(θ) =^{α} _{L′}

⟦T (E[σ])⟧_{L′}(θ) R_{T} ⟦E[σ]⟧_{L} = ⟦E⟧_{L} (ρ).

It follows that ⟦T (E)⟧_{L′}(η) R_{T} ⟦E⟧_{L} (ρ) using Postulate 2. □

Since by Theorem 6 T is correct up to ≈_{T} , by Proposition 1 ≈_{T} is a congruence for L, contained in ∼. Consequently, on V, ≈_{T} is contained in ∼_{L}^{c} , the coarsest 1-hole congruence for L contained in ∼. As remarked in Section 9, for the example of Section 6 this inclusion is strict.

14 Comparison with the definition of validity from [32]

An earlier definition of validity occurs in [32]. A shortcoming of that notion was that it only applied to languages for which all values in the domain of interpretation are denotable by closed terms. Here I show that the current notion of validity, which does not suffer from this limitation, generalises the one of [32]. Let L and L′be languages with ⟦ ⟧_{L} : 𝕋_{L} → ((X → V) → V) and ⟦ ⟧_{L′} : 𝕋_{L′} → ((X → V′) → V′). The property of a language that all values in the domain of interpretation are denotable by closed terms can be stated as

∀v ∈ V. ∃P ∈ T_{L} . ⟦P⟧_{L} = v .  (4)

Definition 22 ([32]) A translation T from L into L′respects •∼ if (1) holds and ⟦T (P)⟧_{L′}(η) •∼ ⟦P⟧_{L} for all closed L -expressions P ∈ T_{L} and all valuations η : X → U, with U := {v ∈ V′| ∃v ∈ V. v′•∼ v}.

In case V = ∅, then U = ∅, so by lack of any η : X → U each translation T from L into L′respects •∼ . When V ≠ ∅ the valuation η is needed because T (P) need not be a closed term, even if P is.

Definition 23 In [32], a translation from L into L′ is called valid up to •∼ if it is compositional and respects •∼ , while L satisfies (4).

Whereas (4) is an unwanted limitation, Example 2 in [32] shows that simply skipping requirement (4) in Definition 23 would yield a criterion that is too weak. The solution proposed by the current paper is to skip (4), while simultaneously strengthening or replacing the requirement of respecting •∼ by the one of being valid up to •∼ (Section 2). The following result state that, for languages L and L′that satisfy Postulate 2, and preorders •∼ that respects =^{α} _{L} and =^{α} _{L′}, any translation that is valid up to •∼ according to [32] is certainly valid according to Definition 5 of the current paper.

Theorem 7 Let L and L′satisfy Postulate 2, let L satisfy (4), and let T be a compositional translation from L into L′that respects •∼ , where •∼ respects =^{α} _{L} and =^{α} _{L′}. Then T is valid up to •∼ .

Proof: In case V = ∅, there is a unique semantic transition R ⊆ V′× V , namely ∅ ⊆ •∼ . Since there are no valuations ρ : X → V, T is correct w.r.t. R, and thus valid up to •∼ .

Otherwise, let θ : X → U := {v ∈ V′| ∃v ∈ V. v′ •∼ v}—it exists by (1)—and define the semantic translation R ⊆ V′× V by R := {(⟦T (P)⟧_{L′}(θ),⟦P⟧_{L} ) | P ∈ T_{L} }. Then R ⊆ •∼ , since T respects •∼ . Since •∼ respects =^{α} _{L} and =^{α} _{L′}, also R^{α} ⊆ •∼ . Hence it suffices to show that T is correct w.r.t. R^{α}. So let E ∈ 𝕋_{L} , ρ : X → V and η : X → V′with η R^{α} ρ. I need to show that ⟦T (E)⟧_{L′}(η) R^{α} ⟦E⟧_{L} (ρ).

Pick ρ̄:X → V and η̄:X → V′such that η =^{α} _{L′} η̄ R ρ̄ =^{α} _{L} ρ. Then there is a closed substitution σ : X → T_{L} such that ρ̄(X) = ⟦σ(X)⟧_{L} and η̄(X) = ⟦T (σ(X))⟧_{L′}(θ) for all X ∈ X, i.e., ρ̄= ⟦σ⟧_{L} and

η̄ = ⟦T ∘ σ⟧_{L′}(θ). Hence, ⟦T (E)⟧_{L′}(η) \begin{matrix}=^{α} _{L′} & ⟦T (E)⟧_{L′}(η̄) & by Lemma 2 \\ = & ⟦T (E)⟧_{L′}(⟦T ∘ σ⟧_{L′}(θ)) & derived above \\ =^{α} _{L′} & ⟦T (E)[T ∘ σ]⟧_{L′}(θ) & by (3) \\ =^{α} _{L′} & ⟦T (E[σ])⟧_{L′}(θ) & by compositionality of T \\ R & ⟦E[σ]⟧_{L} & by definition of R \\ =^{α} _{L} & ⟦E⟧_{L} (⟦σ⟧_{L} ) & by (3) \\ = & ⟦E⟧_{L} (ρ̄) & derived above \\ =^{α} _{L} & ⟦E⟧_{L} (ρ) & by Lemma 2. □ \end{matrix}

15 The case where all semantic values are denotable by closed terms

Here I show that the notion of validity from the current paper agrees with the one of [32] when applied to languages for which all values are denotable by closed terms.

Usually one employs translations T with the property that for any E ∈ 𝕋_{L} any free variable of T (E) is also a free variable of E—I call these free-variable respecting translations, or fvr-translations [32]. If T_{0} in the proof of Theorem 5 is an fvr-translation, then so is T . Hence, replaying the proof of Corollary 2, one obtains:

Observation 4 Let L and L′be languages that satisfy Postulates 1and 2, and •∼ a preorder that respects =^{α} _{L} and =^{α} _{L′}. If any valid (or correct) fvr-translation from L into L′up to •∼ exists, then there exists a compositional fvr-translation that is valid (or correct) up to •∼ .

An fvr-translation T from L into L′respects •∼ iff either V = ∅, or (1) holds and ⟦T (P)⟧_{L′} •∼ ⟦P⟧_{L} for all closed L -expressions P ∈ T_{L} .

Observation 5 Any fvr-translation that is valid up to •∼ respects •∼ .

Lemma 4 Let L′satisfy (4) and V ≠ ∅. If there is a translation from L into L′that is valid up to a preorder •∼ , then there is a fvr-translation from L into L′that is valid up to •∼ .

Proof: Let T be a translation from L into L′that is valid up to •∼ . Let R ⊆ •∼ be a semantic translation such that T is correct w.r.t. R. Let P ∈ T_{L′} be a closed L′-term with ⟦P⟧_{L′} R v for some v ∈ V—such a P exists by (4). Let the translation T ′be obtained from T by defining T ′(E) := T (E)[σ_{E}] for all E ∈ 𝕋_{L} —here σ_{E} is the substitution that (only) substitutes P for all variables X that occur in T (E) but not in E. Then T ′is a fvr-translation. It remains to show that T ′is correct w.r.t. R.

So let E ∈ 𝕋_{L} , η:X → V′and ρ:X → V with η Rρ. I aim to show that ⟦T ′(E)⟧_{L′}(η) R ⟦E⟧_{L} (ρ). Let η̄ : X → V′and ρ̄: X → V be substitutions with η̄(X) = η(X) and ρ̄(X) = ρ(X) for all X ∈ fv(E), such that η̄(Y) = ⟦P⟧_{L′} and ρ̄(Y) = v for all Y ∈ fv(T (E)) \ fv(E). Then η̄ R ρ̄. Consequently,

⟦T ′(E)⟧_{L′}(η) = ⟦T (E)[σ_{E}]⟧_{L′}(η) = ⟦T (E)⟧_{L′}(η̄) R ⟦E⟧_{L} (ρ̄) = ⟦E⟧_{L} (ρ). □

The following result states that in case both L and L′satisfy (4), as well as Postulates 1 and 2, and •∼ respects =^{α} _{L} and =^{α} _{L′}, the validity-based notion of expressiveness from [32] coincides with the one here.

Corollary 3 Let L and L′be languages satisfying Postulates 1 and 2, as well as (4), and •∼ a preorder respecting =^{α} _{L} and =^{α} _{L′}. There exists a valid translation from L into L′ up to •∼ iff there exists a compositional translation from L into L′that respects •∼ .

Proof: Suppose a valid translation up to •∼ exists. In case V = ∅, by Corollary 2 there exists a compositional translation T that is valid up to ∼, and by the remark following Definition 22 T respects •∼ .

In case V ≠ ∅, by Lemma 4 there exists an fvr-translation that is valid up to •∼ . By Observation 4, there exists a compositional fvr-translation T that is valid up to ∼. By Observation 5, T respects •∼ .

The converse direction follows from Theorem 7. □

16 A potential generalisation of the concept of a valid translation

In this section I consider a potentially more liberal concept of a valid transition up to a preorder •∼ , namely a translation that is compositional and preserves •∼ , as in Definition 24 below. Like correctness w.r.t. a semantic translation (Definition 3) and consequently also correctness and validity up to •∼ (Definitions 4, 5 and 6), the requirement of Definition 24 is that the translation preserves the meaning of expressions: the meaning of the translation of an expression E should be semantically equivalent to the meaning of E —see [32] for an elaboration. In fact, this should hold under any valuation of the variables occurring in E. The difference between Definitions 6 and 24 is that the former is based on universal quantification of all matching valuations in the target language, whereas the latter associates with any valuation in the source language a single matching valuation in the target language. This requires a translation T : 𝕋_{L} → 𝕋_{L′} to have a semantic counterpart T : V → V′that maps the possible meanings of L -expressions into the possible meanings of L′-expressions.

Definition 24 A translation T from L into L′preserves •∼ iff there exists a mapping T : V → V′such that T(v) •∼ v for all v ∈ V and ⟦T (E)⟧_{L′}(T ∘ ρ) •∼ ⟦E⟧_{L} (ρ) for all E ∈ 𝕋_{L} and all ρ : X → V.

Note that the existence of T implies (1) in Section 3.

Proposition 7 Any valid translation up to a preorder •∼ preserves •∼ .

Proof: Let T be correct w.r.t. the semantic translation R ⊆ •∼ . Take any T : V → V′with T ⊆ R. Then T∘ρ R ρ for any valuation ρ : X → V. Hence T preserves •∼ using the semantic counterpart T. □

Corollary 2 does not extend (from correct and valid translations up to •∼ ) to translations that preserve •∼ .

Example 9 Let L be a language with unary operators S and 2, and L′a language with unary operators S and G_{k} for each k > 0. Their semantics is given by V = V′= ℕ, S^{V}(n) = S^{V′}(n) = n + 1 for each n ∈ ℕ, 2^{V}(n) = 2n for each n ∈ ℕ, and G_{k}^{V′}(n) = 2^{k}n + 1 for each n ∈ ℕ and k > 0.

Let ∼ be the equivalence relation on ℕ defined by n ∼ m iff n and m differ only by a factor 2^{k} for some k ∈ ℕ, i.e., n = m = 0 or their prime factorisations, when leaving out the factors of 2, are the same.

Each term E ∈ 𝕋_{L} is obtained from a single variable X by applications of the operators S and 2. Using the equation 2SF = SS2F, each such term E can be rewritten into a unique normal form S^{i}2^{j}X for some i,j ∈ ℕ—notation E ↦ S^{i}2^{j}X. If E ↦ S^{i}2^{j}X then ⟦S^{i}2^{j}X⟧_{L} (ρ) = i+2^{j}ρ(X) = ⟦E⟧_{L} (ρ) for each valuation ρ : X → ℕ, and thus ⟦S^{i}2^{j}X⟧_{L} ∼ ⟦E⟧_{L} .

Let T : 𝕋_{L} → 𝕋_{L′} be the translation given by \{ \begin{matrix}T (E) = T (S^{i}2^{j}X) & if E ↦ S^{i}2^{j}X \\ T (2^{j}X) = X \\ T (S^{i+1} X) = S^{i+1} X \\ T (S^{i+1} 2^{j}X) = S^{i}G_{j}X. \end{matrix}

Then T preserves ∼, taking T to be the identity function on ℕ. Moreover, the preconditions of Corollary 2 are trivially satisfied. Yet, there is no compositional translation that preserves ∼.

For suppose T ′ is such a compositional translation, with semantic counterpart T. Then there is a term E_{2} such that T ′(2X) = E_{2}. Using that T ′ preserves ∼, one has ⟦E_{2}⟧_{L′}(T ∘ ρ) ∼ ⟦2X⟧_{L} (ρ) for each ρ : X → ℕ. Take ρ(X) = 0 and ρ(Y) = 7 for each Y ≠ X. Then T(ρ(Y)) ∼ 7, so T(ρ(Y)) ≥ 7, for each Y ≠ X. Since ⟦2X⟧_{L} (ρ_{0}) = 0, also ⟦E_{2}⟧_{L′}(T ∘ ρ_{0}) = 0. As the operators S and G_{k} are strictly increasing, it follows that E_{2} contains none of these operators, nor variables Y ≠ X. So E_{2} = X.

As T ′ is compositional, it follows that T ′(S2X) = T ′(SX). Thus, taking ρ(X) = 1, one obtains 2 = ⟦SX⟧_{L′}(ρ) ∼ ⟦T ′(SX)⟧_{L′}(T ∘ ρ) = ⟦T ′(S2X)⟧_{L′}(T ∘ ρ) ∼ ⟦S2X⟧_{L} (ρ) = 3, a contradiction.

For this reason, when using preservation of •∼ as a criterion like validity and correctness up to •∼ , compositionality has to be required separately.

By Observation 4 and Proposition 7, assuming that L and L′ satisfy Postulates 1 and 2 and •∼ respects =^{α} _{L} and =^{α} _{L′}, if a valid fvr-translation from L into L′ up to •∼ exists, then there exists a compositional fvr-translation that preserves •∼ . Below I establish the reverse, thereby showing that my concept of a valid translation is quite general.

Theorem 8 Let L and L′be languages that satisfy Postulate 2, and •∼ a preorder that respects =^{α} _{L} and =^{α} _{L′}. Any compositional fvr-translation T : 𝕋_{L} → 𝕋_{L′} that preserves •∼ is valid up to •∼ .

Proof: Let T be a compositional fvr-translation that preserves •∼ , say by means of the semantic counterpart T: V → V′. Let R ⊆ V′× V be the smallest relation containing T^{−1} such that T is correct w.r.t. R. By Lemma 3 T is correct w.r.t. R^{α}. I need to show that R^{α} ⊆ •∼ .

Claim: If v′R v then v′=^{α} _{L′} ⟦T (E)⟧_{L′}(T∘ν) and ⟦E⟧_{L} (ν) =^{α} _{L} v for some E ∈ 𝕋_{L} and ν : X → V. Establishing the validity of this claim is sufficient, because by Definition 24 and the transitivity of •∼ ,

using that =^{α} _{L} ,=^{α} _{L′} ⊆ •∼ , it immediately implies that R^{α} ⊆ •∼ .

I prove the claim with induction on the construction of R.

Induction base: If v′R v because v′= T(v) the claim holds by taking E := X and ν(X) = v.

Induction step: Let v′= ⟦T (E)⟧_{L′}(η) and v = ⟦E⟧_{L} (ρ) for some E ∈ 𝕋_{L} , η : X → V′ and ρ : X → V with η R ρ. By induction one may assume that for each X ∈ fv(E) there are E_{X} ∈ 𝕋_{L} and

ν_{X} : X → V such that η(X) =^{α} _{L′} ⟦T (E_{X})⟧_{L′}(T ∘ ν_{X}) and ⟦E_{X}⟧_{L} (ν_{X}) =^{α} _{L} ρ(X). Let (σ_{X})_{X∈fv(E)} be

a family of injective renamings of variables with dom(σ_{X}) = fv(E_{X}), such that the sets range(σ_{X}) := σ_{X}(fv(E_{X})) for X ∈ fv(E) are pairwise disjoint. Here I assume the pool of variables to draw from is large enough. Note that ⟦σ_{X}⟧_{L} (ν_{X}∘ σ_{X}^{−1} ) = ν_{X} and ⟦σ_{X}⟧_{L′}(T ∘ ν_{X}∘ σ_{X}^{−1} ) = T ∘ ν_{X}. Therefore, using (3),

⟦T (E_{X})⟧_{L′}(T ∘ ν_{X}) =^{α} _{L′} ⟦T (E_{X})[σ_{X}]⟧_{L′}(T ∘ ν_{X}∘ σ_{X}^{−1} ) and ⟦E_{X}[σ_{X}]⟧_{L} (ν_{X}∘ σ_{X}^{−1} ) =^{α} _{L} ⟦E_{X}⟧_{L} (ν_{X}). By

the compositionality of T , T (E_{X})[σ_{X}] =^{α} T (E_{X}[σ_{X}]), so η(X) =^{α} _{L′} ⟦T (E_{X}[σ_{X}])⟧_{L′}(T ∘ ν_{X}∘ σ_{X}^{−1} ).

Now let ν:X → V be a valuation such that ν(Y) = ν_{X}∘σ_{X}^{−1} (Y) if Y ∈ fv(E_{X}[σ_{X}]) for some X ∈ fv(E). Furthermore, define the substitution σ : fv(E) → 𝕋_{L} by σ(X) = E_{X}[σ_{X}]. Then ρ(X) =^{α} _{L} ⟦σ(X)⟧_{L} (ν) for all X ∈ fv(E), so v =^{α} _{L} ⟦E⟧_{L} (⟦σ⟧_{L} (ν)) by Lemma 2. Likewise, η(X) =^{α} _{L′} ⟦T (σ(X))⟧_{L′}(T∘ν) for all X ∈ fv(E) ⊇ fv(T (E)), so v′ =^{α} _{L′} ⟦T (E)⟧_{L′}(⟦T ∘ σ⟧_{L′}(T ∘ ν)). Now (3) yields v =^{α} _{L} ⟦E[σ]⟧_{L} (ν) and v′ =^{α} _{L′} ⟦T (E)[T ∘ σ]⟧_{L′}(T ∘ ν). By compositionality, T (E)[T ∘ σ] =^{α} T (E[σ]), from which it follows that v′ =^{α} _{L′} ⟦T (E[σ])⟧_{L′}(T ∘ ν). □

Corollary 4 Let L and L′be languages satisfying Postulates 1 and 2, and •∼ a preorder respecting =^{α} _{L} and =^{α} _{L′}. There exists a valid fvr-translation from L into L′up to •∼ iff there exists a compositional fvr-translation from L into L′that preserves •∼ .

There exist translations that are compositional and preserve •∼ but are not fvr-translations and not valid in the sense of Definition 5. Examples are hard to find and do not appear very natural. Moreover, major results I establish about valid translations (Theorems 4 and 6) do not generalise to such examples. For these reasons I prefer to exclude them from my definition of a valid translation.

Example 10 Let L be a language with constants 0 and 1, and a semantics given by V = {a,b}, 0^{V}= a and 1^{V} = b. Let L′be a language with a unary operator f, and a semantics given by V′= {1,2,3,4} and f^{V′}(n) = n+ 1(mod4). Finally, let ∼ be the equivalence on V ∪ V′given by a ∼ 1 ∼ 2 ≁ 3 ∼ 4 ∼ b.

The translation T : 𝕋_{L} → 𝕋_{L′} given by T (0)=f(X_{0}) and T (1)=f(f(f(X_{0}))) for some X_{0} ∈ X , and T (X) = X for all X ∈ X , is compositional by construction, and preserves •∼ . This is witnessed by its semantic counterpart T : V → V′given by T(a) = 1 and T(b) = 4.

Since T_{L′} = ∅, there do not exists fvr-translations from L to L′. Up to symmetry, T is in fact the only translation from L to L′ that preserves •∼ . For considering that f^{4}(n) = n and the choice of X_{0} is immaterial, any such translation T_{k,ℓ} must satisfy T (0) = f^{k}(X_{0}) and T (1) = f^{ℓ}(X_{0}), where k,ℓ ∈ {0,1,2,3}. The only choices for T(a) are 1 or 2, and by symmetry one can pick T(a) = 1. Hence, to satisfy ⟦T_{k,ℓ}(a)⟧_{L′}(T ∘ ρ) •∼ ⟦a⟧_{L} (ρ) when ρ(X_{0}) = a, one must take k ∈ {0,1}. To also satisfy this formula when ρ(X_{0}) = b, one must take k=1 and T(b)=4. This forces ℓ ∈ {2,3}∩{3,0}, so T_{k,ℓ}=T_{1,3}.

However, there does not exists a translation from L to L′that is valid up to •∼ . For by symmetry, using Proposition 7, T is the only candidate for such a translation. Suppose R is a semantic translation w.r.t. which T is correct. Then 1 R a or 2 R a. Suppose 1 R a. Take valuations ρ,η with η R ρ, such that ρ(X_{0}) = a and η(X_{0}) = 1. As T is correct w.r.t. R, one has

2 = f^{V′}(1) = ⟦f(X_{0})⟧_{L′}(η) = ⟦T (0)⟧_{L′}(η) R ⟦0⟧_{L} (ρ) = a.

So one must have 2 R a. Now take valuations ρ,η with η R ρ, such that ρ(X_{0}) = a and η(X_{0}) = 2. As T is correct w.r.t. R, one has

3 = f^{V′}(2) = ⟦f(X_{0})⟧_{L′}(η) = ⟦T (0)⟧_{L′}(η) R ⟦0⟧_{L} (ρ) = a.

This contradicts the requirement that R ⊆ ∼ .

Theorem 6 does not extend to this translation. For L is a closed-term language and L′ trivially satisfies Postulate 2 (for by lack of bound variables =^{α} _{L′} is the identity). Any congruence ≈ for L′ contained in ∼ must distinguish all four semantic values. Suppose T would preserve an equivalence ≈_{T} on V ∪ V′, contained in ≈, that on V′ coincides with ≈. Let T′ be a semantic counterpart of T . Then T′(a) = 1 or T′(a) = 2. Suppose T′(a) = 1. Take a valuation ρ with ρ(X_{0}) = a. Then

2 = f^{V′}(1) = ⟦f(X_{0})⟧_{L′}(T′∘ ρ) = ⟦T (0)⟧_{L′}(T′∘ ρ) ≈_{T} ⟦0⟧_{L} (ρ) = a.

So one has 2 ≈_{T} a ≈_{T} 1, a contradiction. The case T′(a) = 2 leads to a contradiction in the same way. Hence T does not preserve such an equivalence ≈_{T} .

17 Validity up to barbed bisimilarity for process calculi

In this paper I defined a notion of a valid translation op to a semantic equivalence ∼ between general system description languages, dealing in Section 5 with the special case of closed-term languages. In this section I zoom in further on process calculi such as CCS [50] and the π-calculus [76], and ask which equivalences ∼ to use in studying their relative expressiveness. These languages have in common that their semantics can be given in terms of labelled transition systems, whose states, called processes, are the closed expressions in the language, and whose transitions are given by an operational semantics in the style of Plotkin [71].

For a wide class of process calculi without name-binding, the finest equivalence in regular employ is strong bisimilarity [50]. In proving that process calculus L′is at least as expressive as process calculus L up to a semantic equivalence ∼, the choice of strong bisimilarity for ∼ thus yields the strongest result. Accordingly, Robert de Simone [79] showed that a wide class of process calculi, including CCS [50], CSP [11], ACP [6] and SCCS [49], are expressible up to strong bisimilarity in Meije [3].

However, strong bisimilarity is not suitable for comparing any two process calculi. As an example, consider the π-calculus with the early operational semantics versus the π-calculus with the late operational semantics [76]. Both operational semantics are meant to convey the same idea on how π-calculus processes interact. Consequently, one would hope and expect that the identity function between these versions of the π-calculus is a valid translation. However, it is not valid up to strong bisimilarity. The late semantics has transitions labelled x(y), where the name y is a variable in which a value received on channel x will be stored, whereas the early semantics has transitions labelled xy, where the name y is a particular value received on channel x. Since these labels have a different shape, and strong bisimilarity requires matching labels, validity up to strong bisimilarity fails. Moreover, the problem cannot be resolved by simply renaming the labels, for the entire meaning of input transitions is different.

In the π-calculus, strong early bisimilarity [76] is a much more canonical semantic equivalence than strong bisimilarity, and the identity function is a valid transition between the early and late π-calculi up to strong early bisimilarity. However, the definition of early bisimilarity for the π-calculus with the late operational semantics [76] has a very different form than the definition of early bisimilarity for the early π-calculus [76]. The reason is that the same idea needs to be phrased in terms of rather different transition relations. Consequently, taking strong early bisimilarity as a unifying equivalence for comparing the late and early π-calculus appears to be somewhat ad hoc. Moreover, neither strong bisimilarity nor strong early bisimilarity would be suitable to compare, say, the π-calculus with CCS.

A canonical semantic equivalence that can be defined in a uniform way on CCS as well as on the late and early π-calculi is strong barbed bisimilarity, originally proposed by Milner and Sangiorgi in [52]. It is based on the idea that a τ-transition of a process P describes an actual reaction of the process P, whereas a translation labelled a ≠ τ merely indicates a potential reaction of P when synchronising with a communication partner that is willing to engage in the complementary transition ā. (Likewise, in CSP [11] a transition P −→^{a} P′can be regarded as a potential; one that is not realised when putting the process in a parallel composition involving synchronisation on the action a when the other component cannot partake in such a synchronisation. The only way to be sure that the CSP action a cannot be inhibited by any synchronisation context is to conceal it from the environment, using the CSP concealment operator \a, renaming the action a into τ.) From this perspective, it appears natural to formulate semantic equivalences entirely in terms of the τ-transitions processes can do, and capture the communication potentials (manifested by the other transitions) merely by studying the behaviour of processes in contexts. Accordingly, (strong) reduction bisimilarity was defined in [52] as the version of strong bisimilarity that requires the transfer property for τ-transitions only, i.e., strong barbed bisimilarity as defined below, without the first clause, and reading −→^{τ} for →. Naturally, reduction bisimilarity is not a congruence: the CCS processes a.0 and 0 are reduction equivalent (for neither can do a τ-transition), yet a.0|ā.0 and 0|ā.0 are not. The purpose of the relation is to define a reasonable semantic equivalence as its congruence closure. Indeed, for divergence-free CCS processes strong bisimilarity turned out to be the congruence closure of reduction bisimilarity [52]. Unfortunately, this failed for processes with divergences (infinitesequences of τ-transitions) [52], and when lifted to the weak case, weak reduction congruence turned out to be the universal relation, and thus useless [52]. For this reason, reduction bisimilarity needed to be strengthened. The main idea is that processes like a.0 and 0 can be told apart by placing them in a context |ā.ω, where ω denotes a success state that might be reached by the environment in which a process is placed. The process a.0|ā.ω can reach this success state by performing a τ-transition, whereas 0|ā.ω can not. Writing P↓_{ω} to indicate that a process P has reached this success state, reduction bisimilarity can be strengthened by requiring that if P↓_{ω} then any process Q equivalent to P should also satisfy Q↓_{ω}. This yields the notion of strong barbed bisimilarity. The predicate ↓_{ω} is called a barb. In general, one can use a collection of barbs.

Barbed bisimilarity is defined on closed-term languages L that are equipped with a binary reduction relation → ⊆ T_{L} ×T_{L} between processes and with a collection {↓_{ω} ⊆ T_{L} | ω ∈ Ω} of unary predicates on processes, called barbs.

Definition 25 Strong barbed bisimilarity is the largest symmetric relation ∼^{•} ⊆ T_{L} × T_{L} such that • P ∼^{•} Q and P↓_{ω} with b ∈ Ω implies Q↓_{ω}, and

• P ∼^{•} Q and P → P′implies Q → Q′for some Q′with P′ ∼^{•} Q′. Strong barbed congruence, ∼^{•} _{L}^{1c}, is the congruence closure of ∼^{•} w.r.t. the language L.

For process calculi equipped with a labelled transition system semantics, the reductions P → P′are simply the τ-transitions. However, for many languages it is possible to give a reduction semantics that generates the reductions directly, without first constricting a labelled transition system. Some languages, such as the λ-calculus, come with a natural reduction semantics, even when they have no labelled transition semantics at all.

The definition of the barbs on various process calculi is somewhat ad hoc. In [52] only one barb was used, and a process has this barb when it can perform an observable action, i.e., P↓ iff P −→^{a} P′for some process P′and action a ≠ τ. An alternative is to introduce a barb a for each action a ≠ τ, taking P↓_{a} iff P −→^{a} P′for some P′. Both forms of barbs lead to the same notion of strong barbed congruence. In the π-calculus, x and x̄for x ∈ N are taken to be barbs (or just x̄), with P↓_{ω} iff P −→^{ω(y)} P′or P −→^{ωy} P′for some P′—cf. Section 6. Again, including barbs x ∈ N or not makes no difference in the resulting notion of strong barbed congruence. In fact, it does not matter at all how the barbs are defined, but only whether there are enough barbs, and how they propagate upwards through a context (that is, how the validity of C[P]↓_{ω} is determined by the validity of P↓_{ω}). This is because in determining whether two processes P and Q are strongly barbed congruent, the barbs that help in this determination appear in contexts in which the processes P and Q are placed, rather than in P and Q themselves. For this reason, aiming for a fairly language-independent definition of barbed congruence, I propose the use of external barbs instead, defined as follows. Postulate a sufficiently large collection Ω of barbs and add each of them as a fresh constant to the language under consideration. Require them to propagate upwards through a context in the same way as τ-transitions or reduction steps. Thus, whenever the structural operational semantics of the language has a rule

\frac{P_{i} → Q}{f(P_{1},...,P_{n}) → R}

for some n-ary operator f, possibly with −→^{τ} in the rôle of →, then postulate a rule

P_{i}↓_{ω}
f(P_{1},...,P_{n})↓_{ω}

for each barb ω ∈ Ω. Note that this agrees exactly with Definition 12 of (strong) output barbs in the π-calculus. It turns out that for CCS, the π-calculus, and in fact any language with a definition of strong barbed congruence that I am aware of, the above use of external barbs yields the same notion of strong barbed congruence as the original approach. It may be felt as a drawback that in defining strong barbed congruence on a language L, L needs to be extended, namely by the added constants ω ∈ Ω. However, as a tool to define strong barbed congruence on L this is not a big problem, as the definition on the extended language naturally restricts to L.

The treatment of barbs proposed above is strongly inspired by the success action ω in the treatment of testing equivalences by De Nicola & Hennessy [19], and by the criterion of success sensitiveness imposed by Gorla [39] on translations between process calculi. Both [19] and [39] use only a single success predicate (barb). In [39] P↓_{ω} is defined to hold iff P has a “top-level unguarded occurrence” of ω. Gorla defines the latter concept only for languages that are equipped with a notion of structural congruence ≡ as well as a parallel composition |. In that case P has a top-level unguarded occurrence of ω iff P ≡ Q|ω, for some Q [39]. Specialised to the π-calculus, a (top-level) unguarded occurrence is one that not lays strictly within a subterm α.Q, where α is τ, x̄y or x(z). As far as I know, for all languages where Gorla’s definition of P↓_{ω} as well as mine apply, they yield the same result.

On CCS strong barbed congruence coincides with strong bisimilarity [52]. On the π-calculus strong barbed congruence coincides with strong early congruence, the congruence closure of strong early bisimilarity [76]. This testifies to the success of the barbed bisimilarity approach to defining canonical semantic equivalences for different process calculi in a uniform way. For many other calculi, strong barbed congruence is the primary proposal for a canonical semantic equivalence, and its explicit characterisation in a manner that does not involve quantification over all context is a task that merely follows.

This makes strong barbed bisimilarity an attractive candidate for the equivalence relation ∼ up to which translations between process calculi are proven valid. Theorem 4 says that if a translation between two process calculi is valid up to strong barbed bisimilarity, then it is also valid up an equivalence that on the source language coincides with strong barbed congruence, and on the image of the source language within the target language is also the congruence closure of strong barbed bisimilarity.

For “nonprompt encodings” [56], that “allow administrative (or book-keeping) steps to precede a committing step”, strong (barbed) bisimilarity is too fine an equivalence to relate source processes and their translations. Here an appealing alternative is weak barbed bisimilarity, cf. Definition 13. On CCS weak barbed congruence coincides with weak bisimilarity as defined in [50]. On the π-calculus weak barbed congruence coincides with weak early congruence as used in [76], at least for image finite processes, or in general when allowing infinite sums in the π-calculus [75]. Section 6 mentioned Boudol’s encoding of π into aπ as an example of a transition valid up to weak barbed bisimilarity.

In many situations one would reject translations between process calculi, that introduce (or eliminate) divergences. This can be captured in my framework by requiring validity op to weak (barbed) bisimilarity with explicit divergence [7]. It adds to Definition 13 the clause

• P ≈^{•} Q and P⇑ implies Q⇑. Here P⇑ denotes that there are P_{i} for i ≥ 0 such that P = P_{0} and P_{i} → P_{i+1} (or P_{i} −→^{τ} P_{i+1} ) for all i ≥ 0. Using Remark 1, Theorem 2, Observation 3 and Corollary 3 in [34], the proof of Theorem 2 in [47] shows that Boudol’s encoding of π into aπ is even valid up to weak barbed bisimilarity with explicit divergence.

In most industrial applications of process calculi the rôle once played by weak bisimilarity has largely been taken over by branching bisimilarity [37]—cf. [24, 18]—of which both a default version and two versions with explicit divergence are in use [36, 22]. The following proposal captures these through the barbed bisimilarity methodology:

Definition 26 Divergence-preserving branching barbed bisimilarity is the largest symmetric relation \underline{↔}^{•} _{b}^{Δ} ⊆ T_{L} × T_{L} such that

• P \underline{↔}^{•} _{b}^{Δ} Q and P↓_{ω} with ω ∈ Ω implies Q =⇒ Q^{†} for some Q^{†} with P \underline{↔}^{•} _{b}^{Δ} Q^{†} and Q^{†}↓_{ω},

• P \underline{↔}^{•} _{b}^{Δ} Q and P → P′implies Q =⇒ Q^{†} (→ ) Q′for some Q^{†},Q′with P \underline{↔}^{•} _{b}^{Δ} Q^{†} and P′\underline{↔}^{•} _{b}^{Δ} Q′, and

• P \underline{↔}^{•} _{b}^{Δ} Q and P → P_{1} → P_{2} → ... implies Q → Q′for some Q′with P_{k} \underline{↔}^{•} _{b}^{Δ} Q′for some k ≥ 0.

Here P (→ ) Q abbreviates (P = Q) ∨ (P → Q). See [36] for a number of equivalent versions of the last clause, i.e. with Q =⇒→ Q′. For weakly divergence-preserving branching barbed bisimilarity the last clause is weakened to “P \underline{↔}^{•} _{b}^{Δ} Q and P⇑ implies Q⇑”, just as for weak barbed bisimilarity with explicit divergence above. Skipping the last clause altogether yields branching barbed bisimilarity. On CCS, the congruence closures of these equivalences yield ((weakly) divergence-preserving) branching bisimilarity, as defined in the literature [22]; the proofs are not essentially different from the ones for strong and weak barbed bisimilarity. Using the remark below Observation 3 in [34], the proof of Theorem 2 in [47] can be adapted to show that Boudol’s encoding of π into aπ is even valid up to divergence-preserving branching barbed bisimilarity.

18 Related work: full abstraction

The concept of full abstraction stems from Milner [48]. It indicates a particularly nice connection between a denotational and an operational semantics of a language L. Here a denotational semantics is a function ⟦ ⟧_{L} as introduced in Section 2, whereas an operational semantics is given by an evaluation function E : T_{L} → 𝕆 from the closed terms, there called programs, to a set 𝕆 of observations. Evaluation determines an equivalence relation on programs: P ∼_{E} Q iff E (P) = E (P). Let ∼_{E}^{1c} be the congruence closure of ∼_{E} for the language L, as defined in Section 7.

Definition 27 ([48]) The semantic function ⟦ ⟧_{L} for L is fully abstract w.r.t. E iff for all P,Q ∈ T_{L}

⟦P⟧_{L} = ⟦Q⟧_{L} ⇔ P ∼_{E}^{1c} Q.

A semantic function ⟦ ⟧_{L} always induces an equivalence relation on T_{L} by P ≈_{L} Q iff ⟦P⟧_{L} = ⟦Q⟧_{L} . When this semantics is defined inductively as indicated in Section 5, ≈_{L} must be a congruence. Now ⟦ ⟧_{L} is fully abstract w.r.t. E iff ≈_{L} = ∼_{E}^{1c} .

Note that any equivalence relation ∼_{E} can be extracted from an evaluation function E : T_{L} → 𝕆, namely by taking 𝕆 to be the set of ∼_{E}-equivalence classes of closed terms, with E mapping each p ∈ T_{L} to its own equivalence class. Likewise, each congruence relation ≈ on T_{L} can be obtained from a semantics ⟦ ⟧_{L} : take V to be the set of ≈-equivalence classes of closed terms, and for E ∈ 𝕋_{L} and ρ : L → V define ⟦E⟧_{L} (ρ) by to be the ≈-equivalence class of E[σ], where σ : X → T_{L} is a closed substitution that maps each variable X to a member of the ≈-equivalence class of closed terms ρ(X). Since ≈ is a congruence, this definition is independent of the choice of σ.

Consequently, full abstraction can equally well be stated as a relation between two equivalence relations ≈ and ∼ on T_{L} :

≈ is fully abstract w.r.t. L and ∼ iff ≈ = ∼_{L}^{1c} .

It is in this spirit that full abstraction has been employed in [29] and subsequent papers.

Riecke [73] and Shapiro [77] extend the notion of full abstraction to translations between languages. Riecke [73] compares languages L_{S} and L_{T} with a shared evaluation function E : T_{L_{S}} ∪ T_{L_{T}} → 2^{𝕆}, associating with each closed expression a set of observations. Write P ⊑^{E} Q, for P,Q ∈ T_{L_{S}} ∪ T_{L_{T}} , if E (P) ⊆ E (Q), and let ⊑_{L_{i}}^{E} be the congruence closure of ⊑^{E} w.r.t. L_{i}, for i = S,T (source and target). He calls a translation T : 𝕋_{L_{S}} → 𝕋_{L_{T}} fully abstract iff, for all P,Q ∈ T_{L_{S}} ,

P ⊑_{L_{S}}^{E} Q ⇔ T (P) ⊑_{L_{T}}^{E} T (Q).

The same notion occurs earlier in Mitchell [53], although not under the name “full abstraction”, and using equivalence relations instead of preorders—taking P ∼^{E} Q iff E (P) = E (Q). He compares the expressive power of programming languages in terms of abstraction preserving reductions between them. These are translations that are compositional as well as fully abstract in the above sense. Later work abstracts from the evaluation function E, and casts full abstraction directly in terms of equivalences ∼^{S} and ∼^{T} on the source and target languages [74].

Felleisen [21] compares the expressive power of programming languages through a notion of eliminability of language constructs. With some effort, this approach can be seen to have significant similarities with the approach of Mitchell [53], although it allows certain degenerate reductions [53].

Whereas most work on expressiveness deals with closed-term languages, allowing a focus on syntax over semantics, Shapiro [77] works entirely on the semantic side, leaving the syntax largely implicit. His languages are triples (V,L ,∼), consisting of a semantic domain V, a collection L of partial operators on V, and a semantic equivalence ∼ on V. A language embedding of one such language (V_{S},L_{S},∼^{S}) into another (V_{T},L_{T},∼^{T}) is defined to be a homomorphism of the partial algebra (V_{S},L_{S}) into the partial algebra (V_{T},L_{T}). Recasting this definition in terms of my framework, this is a function R: V_{S} → V_{T} such that there exists a compositional translation T : L_{1} → L_{2} correct w.r.t. R (as in Definition 3). For i = S,T let ∼_{L_{i}}^{i} be the congruence closure of ∼^{i} w.r.t. L_{i}—Shapiro calls this the fully-abstract congruence of L_{i}. Then a language embedding is deemed fully abstract iff, for all v,w ∈ V_{S},

v ∼_{L_{S}}^{S} w ⇔ T (v) ∼_{L_{T}}^{T} T (w).

In [78] these fully abstract language embeddings are used to classify a number of concurrent programming languages on expressive power.

In Nestmann & Pierce [56] the notion of full abstraction was generalised by dropping the requirement that the source and target equivalences being compared need to be congruence closures.

Definition 28 A translation T : 𝕋_{L_{S}} → 𝕋_{L_{T}} is fully abstract w.r.t. the equivalences ∼_{S} ⊆ T_{L_{S}}^{2} and ∼_{T} ⊆ T_{L_{T}}^{2} if, for all P,Q ∈ T_{L_{S}} ,

P ∼_{S} Q ⇔ T (P) ∼_{T}T (Q).

In this form, full abstraction has found widespread applications [54, 5]. Fu [23], for instance, bases a theory of expressiveness on full abstraction, with divergence-preserving branching barbed bisimilarity in the rôle of ∼_{S} and ∼_{T}.

As stressed in [40, 62], the notion of full abstraction is meaningful only in relation to a well-chosen pair of source and target equivalences, and only in combination with a criterion like compositionality. In particular, for each encoding T and each target equivalence ∼_{T} there exits a source term equivalence ∼_{S}, namely {(P,Q) | T (P) ∼_{T}T (Q)}, such that T is fully abstract w.r.t. ∼_{S} and ∼_{T}. For each injective encoding T and each source term relation ∼_{S}, there exits ∼_{T} ⊆ T_{L_{T}}^{2} , namely {(T (P),T (Q)) | P ∼_{S} Q}, such that T is fully abstract w.r.t. ∼_{S} and ∼_{T}. Finally, for each pair ∼_{S} and ∼_{T} such that the cardinality of T_{L_{T}} /_{∼_{T}} greater than or equal to the cardinality of T_{L_{S}} /_{∼_{S}} there exists a translation from L_{S} to L_{T} that is fully abstract w.r.t. ∼_{S} and ∼_{T}.

Naturally, any translation that is valid up to an equivalence ∼ as in Definition 5 of the current paper is also fully abstract, namely w.r.t. the same equivalence ∼ in the rôle of both ∼_{S} and ∼_{T}. Furthermore, validity entails compositionality through Corollary 2. Both full abstraction and validity imply an injective translation from the ∼_{S}-equivalence classes of closed source terms to the ∼_{T}-equivalence classes of closed target terms. However, validity demands that this link between source and target terms is again governed by ∼, whereas full abstraction implies no counterpart to this crucial requirement.

A typical example of a valid transition is the encoding of the synchronous into the asynchronous πcalculus described in Section 6. This encoding is valid up to weak barbed bisimilarity ≈^{•} . Consequently is it also fully abstract w.r.t. ≈^{•} and ≈^{•} according to Definition 28. However, it is not fully abstract w.r.t. ≈^{•} and ≈^{•} in the more original sense of Shapiro [77] and others, due to the fact that ≈^{•} is not a congruence for either the source or the target language. By Theorem 4 the same translation is also fully abstract w.r.t the congruence closure of ≈^{•} on the source language, and a somewhat artificial equivalence on the target language that is the congruence closure of ≈^{•} under translated source contexts. Although closer, this is still not a full-abstraction result according to Shapiro, as the latter equivalence fails to be a congruence for all of the target language. Finally, by Theorem 6, the same encoding is furthermore fully abstract w.r.t. the congruence closure of ≈^{•} on the target language, and an artificial congruence on the source language that is strictly finer than the congruence closure of ≈^{•} on the source language. This is a full abstraction result in the framework of [77]. However, in line with the observations of [40, 62], the latter two full abstraction results should not be regarded as lending additional credibility to this particular encoding of the synchronous into the asynchronous π-calculus. Since Theorems 4 and 6 hold in great generality, these full abstraction results are merely consequences of the validity of the encoding up to ≈^{•} .

It is well known that Boudol’s encoding—described in Section 6—of the synchronous into the asynchronous π-calculus fails to be fully abstract w.r.t. ≅ ^{c} and ≅ _{a}^{c}. Here ≅ ^{c} is the congruence closure of ≈^{•} on the source language, and ≅ _{a}^{c} the congruence closure of ≈^{•} on the target language. A counterexample was given at the end of Section 8. The same analysis applies to a similar encoding proposed by Honda & Tokoro [44]. In [20] this problem is addressed by proposing a strict subcalculus SAπ of the target language that contains the image of the source language under of a version Honda & Tokoro’s encoding, such that this encoding is fully abstract w.r.t. ≅ ^{c} and the congruence closure of ≈^{•} w.r.t. SAπ. In [72] a similar solution to the same problem was found earlier, but for a variant of Boudol’s encoding from the polyadic π-calculus to the (monadic) asynchronous π-calculus. They defined a class of well-typed expressions in the asynchronous π-calculus, such that the well-typed expressions constitute a subcalculus of the target language that contains the image of the source language under the encoding. Again, the encoding is fully abstract w.r.t. ≅ ^{c} and the congruence closure of ≈^{•} w.r.t. that sublanguage. By Theorem 4 such results can always be achieved, namely by taking as target language exactly the image of the source language under the encoding. What the results of [72, 20] add is that the sublanguage may be strictly larger than the image of the source language, and that its definition is not phrased in terms of the encoding.

19 Related work: validity of encodings according to Gorla

In the last twenty years, a great number of encodability and separation results have appeared, comparing CCS, Mobile Ambients, and several versions of the π-calculus (with and without recursion; with mixed choice, separated choice or asynchronous) [74, 45, 8, 60, 56, 57, 54, 17, 16, 12, 15, 4, 5, 59, 58, 69, 14, 81, 13, 42, 70, 80, 1, 43, 66, 2]; see [38, 39] for an overview. Many of these results employ different and somewhat ad hoc criteria on what constitutes a valid encoding, and thus are hard to compare with each other. Several of these criteria are discussed and compared in [55], [61] and [63]. Gorla [39] collected some essential features of these approaches and integrated them in a proposal for a valid encoding that justifies most encodings and some separation results from the literature. Since then, several authors have used Gorla’s framework as a basis for establishing new valid encodings and separation results [38, 46, 68, 65, 67, 25, 26, 27, 28].

R.J. van Glabbeek 29

Like Boudol [9] and the present paper, Gorla requires a compositionality condition for encodings. However, his criterion differs on two counts from mine. It is stronger in that the expression E_{f} encoding an operator f may use each variable corresponding to an argument of f only once. A translation defined (in part) by T (f(P)) = g(T (P)∥T (P)) for instance can be compositional according to Definition 21, but not according to Gorla’s definition. It is weaker than mine in that the expression E_{f} encoding an operator f may be dependent on the set of names occurring freely in the expressions given as arguments of f. This issue is further discussed in [32]. It is an interesting topic for future research to see if there are any valid encodability results à la [39] that suffer from my proposed strengthening of compositionality.

The second criterion of [39] is a form of invariance under name-substitution. It serves to partially undo the effect of making the compositionality requirement name-dependent. In my setting I have not yet found the need for such a condition. In [32] I argue that this criterion as formalised in [39] is too restrictive.

The remaining three requirements of Gorla (the ‘semantic’ requirements) are very close to an instantiation of mine with a particular preorder •∼ . If one takes •∼ to be weak barbed bisimilarity with explicit divergence (i.e. relating divergent states with divergent states only—see Section 17), using external barbs as defined in Section 17, then any valid translation in my sense satisfies Gorla’s semantic criteria, provided that the equivalence ≍ on the target language that acts as a parameter in Gorla’s third criterion is also taken to be weak barbed bisimilarity with explicit divergence. The precise relationships between the proposals of [32] and [39] are further discussed in [64].

Further work is needed to sort out to what extent the two approaches have relevant differences when evaluating encoding and separation results from the literature. Another topic for future work is to sort out how dependent known encoding and separation results are on the chosen equivalence or preorder.

References

[1] J. Åman Pohjola & J. Parrow (2014): Priorities Without Priorities: Representing Preemption in Psi-Calculi. In J. Borgström & S. Crafa, editors: Proceedings Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics, Rome, Italy, 1st September 2014, Electronic Proceedings in Theoretical Computer Science 160, Open Publishing Association, pp. 2–15,

doi:10.4204/EPTCS.160.2.

[2] J. Åman Pohjola & J. Parrow (2016): The Expressive Power of Monotonic Parallel Composition. In P. Thiemann, editor: Programming Languages and Systems: Proceedings 25th European Symposium on Programming, ESOP’16, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’16, Eindhoven, The Netherlands, April 2016, LNCS 9632, Springer, pp. 780–803, doi:10.1007/

978-3-662-49498-1_30.

[3] D. Austry & G. Boudol (1984): Algèbre de processus et synchronisations. Theoretical Computer Science

30(1), pp. 91–131, doi:10.1016/0304-3975(84)90067-7.

[4] M. Baldamus, J. Parrow & B. Victor (2004): Spi Calculus Translated to π-Calculus Preserving May-Tests. In: Proceedings 19th IEEE Symposium on Logic in Computer Science, LICS’04, July 2004, Turku, Finland, IEEE Computer Society Press, pp. 22–31, doi:10.1109/LICS.2004.1319597.

[5] M. Baldamus, J. Parrow & B. Victor (2005): A Fully Abstract Encoding of the pi-Calculus with Data Terms. In L. Caires, G.F. Italiano, L. Monteiro, C. Palamidessi & M. Yung, editors: Proceedings 32nd International Colloquium on Automata, Languages and Programming, ICALP’05, Lisbon, Portugal, July 2005, LNCS 3580, Springer, pp. 1202–1213, doi:10.1007/11523468_97.

[6] J.A. Bergstra & J.W. Klop (1986): Algebra of communicating processes. In J.W. de Bakker, M. Hazewinkel & J.K. Lenstra, editors: Mathematics and Computer Science, CWI Monograph 1, North-Holland, Amsterdam, pp. 89–138.

[7] J.A. Bergstra, J.W. Klop & E.-R. Olderog (1987): Failures without chaos: a new process semantics for fair abstraction. In M. Wirsing, editor: Formal Description of Programming Concepts – III, Proceedings of the 3^{th}IFIP WG 2.2 working conference, Ebberup 1986, North-Holland, Amsterdam, pp. 77–103.

[8] M. Boreale (1998): On the Expressiveness of Internal Mobility in Name-Passing Calculi. Theoretical Computer Science 195(2), pp. 205–226, doi:10.1016/S0304-3975(97)00220-X.

[9] G. Boudol (1985): Notes on algebraic calculi of processes. In K. Apt, editor: Logics and Models of Concurrent Systems, Springer, pp. 261–303, doi:10.1007/978-3-642-82453-1_9. NATO ASI Series F13.

[10] G. Boudol (1992): Asynchrony and the π-calculus (Note). Technical Report 1702, INRIA.

[11] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): A theory of communicating sequential processes. Journal of the ACM 31(3), pp. 560–599, doi:10.1145/828.833.

[12] N. Busi, M. Gabbrielli & G. Zavattaro (2009): On the expressive power of recursion, replication and iteration in process calculi. Mathematical Structures in Computer Science 19(6), pp. 1191–1222, doi:10.1017/

S096012950999017X.

[13] D. Cacciagrano, F. Corradini, J. Aranda & F.D. Valencia (2008): Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus. Electronic Notes in Theoretical Computer Science 194(2), pp. 59–84,

doi:10.1016/j.entcs.2007.11.006.

[14] D. Cacciagrano, F. Corradini & C. Palamidessi (2007): Separation of synchronous and asynchronous communication via testing. Theoretical Computer Science 386(3), pp. 218–235, doi:10.1016/j.tcs.2007.07.

009.

[15] M. Carbone & S. Maffeis (2003): On the Expressive Power of Polyadic Synchronisation in pi-calculus. Nordic Journal of Computing 10(2), pp. 70–98.

[16] L. Cardelli, G. Ghelli & A.D. Gordon (2002): Types for the Ambient Calculus. Information and Computation 177(2), pp. 160–194, doi:10.1006/inco.2001.3121.

[17] L. Cardelli & A.D. Gordon (2000): Mobile ambients. Theoretical Computer Science 240(1), pp. 177–213,

doi:10.1016/S0304-3975(99)00231-5.

[18] S. Cranen, J. F. Groote, J. J. A. Keiren, F. P. M. Stappers, E. P. de Vink, W. Wesselink & T. A. C. Willemse (2013): An Overview of the mCRL2 Toolset and Its Recent Advances. In Nir Piterman & Scott A. Smolka, editors: Proceedings Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’13, LNCS 7795, Springer, pp. 199–213, doi:10.1007/978-3-642-36742-7_15.

[19] R. De Nicola & M. Hennessy (1984): Testing equivalences for processes. Theoretical Computer Science 34,

pp. 83–133, doi:10.1016/0304-3975(84)90113-0.

[20] W. Du, Z. Yang & H. Zhu (2018): A Fully Abstract Encoding for Sub Asynchronous Pi Calculus. In J. Pang & C. Zhang, editors: 12th International Symposium on Theoretical Aspects of Software Engineering, IEEE. To appear.

[21] M. Felleisen (1991): On the Expressive Power of Programming Languages. Science of Computer Program-

ming 17(1-3), pp. 35–75, doi:10.1016/0167-6423(91)90036-W.

[22] W.J. Fokkink, R.J. van Glabbeek & B. Luttik (2017): Divide and Congruence III: Stability & Divergence. In R. Meyer & U. Nestmann, editors: Proceedings 28th International Conference on Concurrency Theory, CONCUR 2017, Leibniz International Proceedings in Informatics (LIPIcs) 85, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, pp. 15:1–15:16, doi:10.4230/LIPIcs.CONCUR.2017.15.

[23] Y. Fu (2016): Theory of interaction. Theoretical Computer Science 611, pp. 1–49, doi:10.1016/j.tcs.

2015.07.043.

[24] H. Garavel, F. Lang, R. Mateescu & W. Serwe (2011): CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes. In P.A. Abdulla & K.R.M. Leino, editors: Proceedings Tools and Algorithms for the Construction and Analysis of Systems, TACAS ’11, LNCS 6605, Springer, pp. 372–387,

doi:10.1007/978-3-642-19835-9_33.

[25] T. Given-Wilson (2014): Expressiveness via Intensionality and Concurrency. In G. Ciobanu & D. Méry, editors: Proceedings 11th International Colloquium on Theoretical Aspects of Computing, ICTAC’14, Bucharest, Romania, 2014, LNCS 8687, Springer, pp. 206–223, doi:10.1007/978-3-319-10882-7_13.

[26] T. Given-Wilson (2014): On the Expressiveness of Intensional Communication. In J. Borgström & S. Crafa, editors: Proceedings Combined 21st International Workshop on Expressiveness in Concurrency and 11th Workshop on Structural Operational Semantics, Rome, Italy, 1st September 2014, Electronic Proceedings in Theoretical Computer Science 160, Open Publishing Association, pp. 30–46, doi:10.4204/EPTCS.160.4.

[27] T. Given-Wilson & A. Legay (2015): On the Expressiveness of Joining. In S. Knight, I. Lanese, A. Lluch Lafuente & H. Torres Vieira, editors: Proceedings 8th Interaction and Concurrency Experience, Grenoble, France, 4-5th June 2015, Electronic Proceedings in Theoretical Computer Science 189, Open Publishing Association, pp. 99–113, doi:10.4204/EPTCS.189.9.

[28] T. Given-Wilson & A. Legay (2016): On the Expressiveness of Symmetric Communication. In A. Sampaio & F. Wang, editors: Proceedings 13th International Colloquium on Theoretical Aspects of Computing, ICTAC’16, Taipei, Taiwan, October 2016, LNCS 9965, Springer, pp. 139–157, doi:10.1007/

978-3-319-46750-4_9.

[29] R.J. van Glabbeek (1993): Full Abstraction in Structural Operational Semantics (extended abstract). In M. Nivat, C. Rattray, T. Rus & G. Scollo, editors: Proceedings of the 3^{rd} International Conference on Algebraic Methodology and Software Technology, AMAST’93, Twente, The Netherlands, June l993, Workshops

in Computing, Springer, pp. 75–82. Available at http://theory.stanford.edu/~rvg/abstracts.
html#28.

[30] R.J. van Glabbeek (1994): On the expressiveness of ACP (extended abstract). In A. Ponse, C. Verhoef & S.F.M. van Vlijmen, editors: Proceedings First Workshop on the Algebra of Communicating Processes, ACP’94, Utrecht, The Netherlands, May 1994, Workshops in Computing, Springer, pp. 188–217, doi:10.

1007/978-1-4471-2120-6_8.

[31] R.J. van Glabbeek (2005): A Characterisation of Weak Bisimulation Congruence. In A. Middeldorp, V. van Oostrom, F. van Raamsdonk & R. de Vrijer, editors: Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday, LNCS 3838, Springer,

pp. 26–39, doi:10.1007/11601548_4.

[32] R.J. van Glabbeek (2012): Musings on Encodings and Expressiveness. In B. Luttik & M.A. Reniers, editors: Proceedings Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structured Operational Semantics, Newcastle upon Tyne, UK, September 3, 2012, Electronic Proceedings in Theoretical Computer Science 89, Open Publishing Association, pp. 81–98, doi:10.4204/EPTCS.89.7.

[33] R.J. van Glabbeek (2017): Lean and Full Congruence Formats for Recursion. In: Proceedings 32^{nd} Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’17, Reykjavik, Iceland, June 2017, IEEE Computer Society Press, doi:10.1109/LICS.2017.8005142.

[34] R.J. van Glabbeek (2018): On the Validity of Encodings of the Synchronous in the Asynchronous π-calculus. Information Processing Letters 137, p. 1725, doi:10.1016/j.ipl.2018.04.015.

[35] R.J. van Glabbeek (2018): A Theory of Encodings and Expressiveness (extended abstract). In C. Baier & U. Dal Lago, editors: Proceeding 21st International Conference on Foundations of Software Science and Computational Structures, FoSSaCS 2018; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, hessaloniki, Greece, April 2018, LNCS 10803, Springer, pp. 183–202,

doi:10.1007/978-3-319-89366-2_10.

[36] R.J. van Glabbeek, B. Luttik & N. Trčka (2009): Branching Bisimilarity with Explicit Divergence. Fundamenta Informaticae 93(4), pp. 371–392, doi:10.3233/FI-2009-109.

[37] R.J. van Glabbeek & W.P. Weijland (1996): Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), pp. 555–600, doi:10.1145/233551.233556.

[38] D. Gorla (2010): A taxonomy of process calculi for distribution and mobility. Distributed Computing 23(4),

pp. 273–299, doi:10.1007/s00446-010-0120-6.

[39] D. Gorla (2010): Towards a unified approach to encodability and separation results for process calculi. Information and Computation 208(9), pp. 1031–1053, doi:10.1016/j.ic.2010.05.002.

[40] D. Gorla & U. Nestmann (2016): Full abstraction for expressiveness: history, myths and facts. Mathematical Structures in Computer Science 26(4), pp. 639–654, doi:10.1017/S0960129514000279.

[41] G. Grätzer (2010): Lattice Theory: Foundation. Springer, doi:10.1007/978-3-0348-0018-1.

[42] B. Haagensen, S. Maffeis & I. Phillips (2008): Matching Systems for Concurrent Calculi. Electronic Notes in Theoretical Computer Science 194(2), pp. 85–99, doi:10.1016/j.entcs.2007.11.004.

[43] M. Hatzel, C. Wagner, K. Peters & U. Nestmann (2015): Encoding CSP into CCS. In S. Crafa & D.E. Gebler, editors: Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, Madrid, Spain, August 2015, Electronic Proceedings in Theoretical Computer Science 190, Open Publishing Association, pp. 61–75, doi:10.4204/EPTCS.190.5.

[44] K. Honda & M. Tokoro (1991): An Object Calculus for Asynchronous Communication. In Pierre America, editor: Proc. European Conference on Object-Oriented Programming, ECOOP’91, LNCS 512, Springer, pp.

133–147, doi:10.1007/BFb0057019.

[45] C.T. Jensen (1994): Interpreting Broadcast Communication in CCS with Priority Choice. In: Proceedings of the 6th Nordic Workshop on Programming Theory, pp. 49–70.

[46] I. Lanese, J.A. Pérez, D. Sangiorgi & A. Schmitt (2010): On the Expressiveness of Polyadic and Synchronous Communication in Higher-Order Process Calculi. In S. Abramsky, C. Gavoille, C. Kirchner, F. Meyer auf der Heide & P.G. Spirakis, editors: Proceedings 37th International Colloquium on Automata, Languages and Programming, ICALP’10, Bordeaux, France, July 2010, Part II, LNCS 6199, Springer, pp. 442–453, doi:10.

1007/978-3-642-14162-1_37.

[47] C. Lippert, S. Mennicke, R.J. van Glabbeek & U. Goltz (2018): A Case Study on Evaluating Encodings

Between Process Calculi. Available at http://theory.stanford.edu/~rvg/abstracts.html#129.

[48] R. Milner (1975): Processes: A Mathematical Model for Computing Agents. In H.E. Rose & J.C. Shepherdson, editors: Logic Colloquium ’73, Studies in Logic and the Foundations of Mathematics 50, Elsevier, pp.

157–173, doi:10.1016/S0049-237X(08)71948-7.

[49] R. Milner (1983): Calculi for synchrony and asynchrony. Theoretical Computer Science 25, pp. 267–310,

doi:10.1016/0304-3975(83)90114-7.

[50] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242. Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980.

[51] R. Milner (1992): Functions as Processes. Mathematical Structures in Computer Science 2(2), pp. 119–141,

doi:10.1017/S0960129500001407.

[52] R. Milner & D. Sangiorgi (1992): Barbed Bisimulation. In W. Kuich, editor: Proceedings 19th International Colloquium on Automata, Languages and Programming, ICALP’92, Vienna, Austria, July 1992, LNCS 623,

Springer, pp. 685–695, doi:10.1007/3-540-55719-9_114.

[53] J.C. Mitchell (1993): On Abstraction and the Expressive Power of Programming Languages. Science of Computer Programming 21(2), pp. 141–163, doi:10.1016/0167-6423(93)90004-9. A earlier version was circulated in 1986 under the name Lisp is not universal.

[54] U. Nestmann (2000): What is a “Good” Encoding of Guarded Choice? Information and Computation 156(1-2), pp. 287–319, doi:10.1006/inco.1999.2822.

[55] U. Nestmann (2006): Welcome to the Jungle: A Subjective Guide to Mobile Process Calculi. In C. Baier & H. Hermanns, editors: Proceedings 17th International Conference on Concurrency Theory, CONCUR 2006, Bonn, Germany, August 2006, LNCS 4137, Springer, pp. 52–63, doi:10.1007/11817949_4.

[56] U. Nestmann & B.C. Pierce (2000): Decoding Choice Encodings. Information and Computation 163(1), pp. 1–59, doi:10.1006/inco.2000.2868. An earlier version appeared in Proc. CONCUR’96.

[57] C. Palamidessi (2003): Comparing The Expressive Power Of The Synchronous And Asynchronous Pi-Calculi. Mathematical Structures in Computer Science 13(5), pp. 685–719, doi:10.1017/S0960129503004043.

[58] C. Palamidessi, V.A. Saraswat, F.D. Valencia & B Victor (2006): On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus. In: Proceedings 21th IEEE Symposium on Logic in Computer Science, LICS’06, August 2006, Seattle, WA, USA, IEEE Computer Society Press, pp. 59–68, doi:10.1109/

LICS.2006.39.

[59] C. Palamidessi & F.D. Valencia (2005): Recursion vs Replication in Process Calculi: Expressiveness. Bulletin of the EATCS 87, pp. 105–125.

[60] J. Parrow (2000): Trios in concert. In G.D. Plotkin, C. Stirling & M. Tofte, editors: Proof, Language, and Interaction, Essays in Honour of Robin Milner, The MIT Press, pp. 623–638.

[61] J. Parrow (2008): Expressiveness of Process Algebras. Electronic Notes in Theoretical Computer Science

209, pp. 173–186, doi:10.1016/j.entcs.2008.04.011.

[62] J. Parrow (2016): General conditions for full abstraction. Mathematical Structures in Computer Science

26(4), pp. 655–657, doi:10.1017/S0960129514000280.

[63] K. Peters (2012): Translational Expressiveness. Comparing Process Calculi using Encodings. Ph.D. thesis,

TU Berlin, doi:10.14279/depositonce-3416.

[64] K. Peters & R.J. van Glabbeek (2015): Analysing and Comparing Encodability Criteria. In S. Crafa & D.E. Gebler, editors: Proceedings of the Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics, Madrid, Spain, 31st August 2015, Electronic Proceedings in Theoretical Computer Science 190, Open Publishing Association, pp. 46–60, doi:10.4204/

EPTCS.190.4.

[65] K. Peters & U. Nestmann (2012): Is It a “Good” Encoding of Mixed Choice? In L. Birkedal, editor: Proceeding 15th International Conference on Foundations of Software Science and Computational Structures, FoSSaCS’12; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’12, Tallinn, Estonia, March/April 2012, LNCS 7213, Springer, pp. 210–224, doi:10.1007/

978-3-642-28729-9_14.

[66] K. Peters & U. Nestmann (2016): Breaking symmetries. Mathematical Structures in Computer Science 26(6),

pp. 1054–1106, doi:10.1017/S0960129514000346.

[67] K. Peters, U. Nestmann & U. Goltz (2013): On Distributability in Process Calculi. In M. Felleisen & Ph. Gardner, editors: Programming Languages and Systems: Proceedings 22nd European Symposium on Programming, ESOP’13, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’13, Rome, Italy, March 2013, LNCS 7792, Springer, pp. 310–329, doi:10.1007/

978-3-642-37036-6_18.

[68] K. Peters, J.-W. Schicke & U. Nestmann (2011): Synchrony vs Causality in the Asynchronous Pi-Calculus. In B. Luttik & F. Valencia, editors: Proceedings 18th International Workshop on Expressiveness in Concurrency, EPTCS 64, pp. 89–103, doi:10.4204/EPTCS.64.7.

[69] I. Phillips & M.G. Vigliotti (2006): Leader election in rings of ambient processes. Theoretical Computer Science 356(3), pp. 468–494, doi:10.1016/j.tcs.2006.02.004.

[70] I. Phillips & M.G. Vigliotti (2008): Symmetric electoral systems for ambient calculi. Information and Computation 206(1), pp. 34–72, doi:10.1016/j.ic.2007.08.005.

[71] G.D. Plotkin (2004): A Structural Approach to Operational Semantics. The Journal of Logic and Algebraic Programming 60–61, pp. 17–139, doi:10.1016/j.jlap.2004.05.001. Originally appeared in 1981.

[72] P. Quaglia & D. Walker (2000): On Synchronous and Asynchronous Mobile Processes. In J. Tiuryn, editor: Proceedings Third International Conference on Foundations of Software Science and Computation Structures, FoSSaCS’00, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS’00, Berlin, Germany, March/April 2000, LNCS 1784, Springer, pp. 283–296, doi:10.1007/

3-540-46432-8_19.

[73] J.G. Riecke (1991): Fully Abstract Translations between Functional Languages. In D.S. Wise, editor: Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, POPL’91, Orlando, Florida, USA, January 1991, ACM Press, pp. 245–254, doi:10.1145/99583.99617.

[74] D. Sangiorgi (1993): From π-calculus to Higher-Order π-calculus — and back. In M.-C. Gaudel & J.-P. Jouannaud, editors: Proceedings Theory and Practice of Software Development, TAPSOFT’93, International Joint Conference CAAP/FASE, Orsay, France, April 1993, LNCS 668, Springer, pp. 151–166, doi:10.1007/

3-540-56610-4_62.

[75] D. Sangiorgi & D. Walker (2001): On Barbed Equivalences in π-Calculus. In K.G. Larsen & M. Nielsen, editors: Proceeding 12th International Conference on Concurrency Theory, CONCUR’01, Aalborg, Denmark, August 2001, LNCS 2154, Springer, pp. 292–304, doi:10.1007/3-540-44685-0_20.

[76] D. Sangiorgi & D. Walker (2001): The π-calculus: A Theory of Mobile Processes. Cambridge University Press.

[77] E.Y. Shapiro (1991): Separating Concurrent Languages with Categories of Language Embeddings (Extended Abstract). In C. Koutsougeras & J.S. Vitter, editors: Proceedings 23rd Annual ACM Symposium on Theory of Computing, STOC’91, May 1991, New Orleans, Louisiana, USA, ACM, pp. 198–208, doi:10.1145/

103418.103423.

[78] E.Y. Shapiro (1992): Embeddings Among Concurrent Programming Languages (Preliminary Version). In R. Cleaveland, editor: Proceedings Third International Conference on Concurrency Theory, CONCUR ’92, Stony Brook, NY, USA, August 1992, LNCS 630, Springer, pp. 486–503, doi:10.1007/BFb0084811.

[79] R. de Simone (1985): Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science

37, pp. 245–267, doi:10.1016/0304-3975(85)90093-3.

[80] C. Versari, N. Busi & R. Gorrieri (2009): An expressiveness study of priority in process calculi. Mathematical Structures in Computer Science 19(6), pp. 1161–1189, doi:10.1017/S0960129509990168.

[81] M.G. Vigliotti, I. Phillips & C. Palamidessi (2007): Tutorial on separation results in process calculi via leader election problems. Theoretical Computer Science 388(1-3), pp. 267–289, doi:10.1016/j.tcs.2007.09.