Factoring an Adequacy Proof (Preliminary Report)

Roy L. Crole^{∗}

Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, United Kingdom.

                    rlc@doc.ic.ac.uk

Andrew D. Gordon^{∗}

University of Cambridge Computer Laboratory, New Museums Site, Cambridge CB2 3QG, United Kingdom.

                    adg@cl.cam.ac.uk

To appear in Functional Programming: Proceedings of the 1993 Glasgow Workshop, July 5–7 1993, Ayr, Scotland. Springer Workshops in Computing, 1994.

Abstract

This paper contributes to the methodology of using metalogics for reasoning about programming languages. As a concrete example we consider a fragment of ML corresponding to call-by-value PCF and translate it into a metalogic which contains (amongst other types) computation types and a fixpoint type. The main result is a soundness property (⋆): if the denotations of two programs are provably equal in the metalogic, they have the same operationally observable behaviour. As usual, this follows from a computational adequacy result. In early notes, Plotkin showed how such proofs could be factored into two stages, the first non-trivial and the second (essentially) routine; our contribution is to rework his suggestion within a new framework. We define a metalogic, which incorporates computation and fixpoint types, and specify a modular translation of the ML fragment. Our proof of (⋆) factors into two parts. First, the term language of the metalogic is equipped with an operational semantics and a (generic) computational adequacy result obtained. Second, a simple syntactic argument establishes a correspondence between the operational behaviour of an object program and of its denotation. The first part is not routine but is proved once and for all. The second is a detailed but essentially trivial calculation that is easily adaptable to other object languages. Such a factored proof is important because it promises to scale up more easily than a monolithic one. We show that it may be adapted to an object language with call-by-name functions and one with a simple exception mechanism.

1 Motivation and Background

The motivation for this work is to contribute to the long term project of using denotational semantics to prove properties of programs written in realistic languages like Standard ML or Haskell.

Our contribution is to the methodology of expressing and reasoning about denotational semantics using what we term metalogics. By metalogic we mean a formal system (such as a type theory or logic) intended to express denotational semantics, that is implementable in a theorem-prover, and which is equipped with general proof principles, such as natural number induction or fixpoint induction. The intention is that the general proof infrastructure of the metalogic can be applied to a particular object language via a translation into the metalogic. We shall define a metalogic (called M) which has a basic syntax of types and terms, and is equipped with both an equational and an operational semantics. M is closely allied to Crole and Pitts’ FIX-logic [3, 4], a metalogic based on ideas from Moggi’s computational let-calculus [10, 11] and a precursor of Pitts’ evaluation logic [15]. An important principle underlying each of these metalogics is to distinguish simple data values from computations; more precisely, each uses computation types, of the form T σ, to represent computations that may return data values of type σ. Each of these metalogics is monadic in the sense that a computation type is modelled by a strong monad.

We consider the general problem of how to prove soundness of metalogical reasoning about an object language. The object language we use as a vehicle for this problem is O, a small fragment of ML corresponding to call-by-value PCF. We give a translation into M and prove its soundness: if the denotations of two programs are provably equal in the metalogic, then the two are in fact observationally equivalent. Given that ML is defined operationally, the result justifies use of the metalogic to derive properties of the object language.

It is standard to derive such a soundness result from a proof that the denotational semantics respects evaluation in a sense known as computational adequacy [8]. Proofs of computational adequacy are, usually, directly linked to the denotational semantics of the object language in question. In his CSLI notes [17], Plotkin showed how such proofs can be factored in two, via an operational semantics for the metalogic. Our contribution is to rework (the idea of) such a factorisation in the setting of a metalogic endowed with computation and fixpoint types. First, we prove a (non-routine) adequacy result which relates the equational and operational semantics of M. Second, we obtain soundness of metalogical reasoning for O via a simple but detailed proof of a correspondence between the operational behaviour of each O program and its denotation, which utilises the adequacy result for M. The computational adequacy of M is generic in the sense that a computational adequacy result for a new programming language will only require a reworking of the second (and simpler) proof stage. We present two variants of O as evidence for this genericity: one with call-by-name functions and another with a simple exception mechanism. The use of computation types gives an elegant structure to the form of O’s denotational semantics. This factored proof is important as it is likely to scale up more easily than a monolithic one, and the monadic presentation ought to be of use as monadic metalogics are mechanised and applied to more realistic object languages.

2 An Equational Metalogic M

We now present a Martin-Löf style (simple) type theory M which will be viewed as a programming metalogic. This is based on the term language of the FIXlogic [3, 4], though M has a few crucial differences. The term language of M is well known, except, perhaps, for the fragment associated with the fixpoint

{Γ ⊢ M : σ \atop Γ ⊢ ValL(M) : σ_{⊥}} Γ ⊢ M : σ

\overline{(σ total)}
Γ ⊢ EvalL(M) : σ_{⊥}

Γ ⊢ E : σ_{⊥} Γ, x:σ ⊢ F : τ_{⊥}
Γ ⊢ LetL x ⇐ E in F : τ_{⊥}

{Γ, e:σ_{⊥} ⊢ F : σ Γ ⊢ N : fix \atop Γ ⊢ It(e. F, N) : σ}

Γ ⊢ ω : fix_{⊥}

Γ ⊢ E : fix_{⊥}
Γ ⊢ Inc(E) : fix

Table 1: Type assignment for M

type and lifted types σ_{⊥}. Let us summarise the types and (raw) terms:

σ ::= unit | nat | fix | σ × σ | σ + σ | σ → σ | σ_{⊥}
M ::= x | ⟨⟩ | Z | S(M) | (x.M)^{M}(M) | ω | Inc(M) | It(x. M, M) |

⟨M, M⟩ | Split(M, x. x. M) | Inl(M) | Inr(M) | Case(M, x. M, x. M) |

λx. M | M M | ValL(M) | EvalL(M) | LetL x ⇐ M in M

The types are given by a unit type, natural numbers, fixpoint type, (co)products, exponentials, and lifted types. In the cases of the unit type, natural numbers, products, coproducts and exponentials, the raw terms are the usual ones of Martin-Löf’s (simple) type theory—for background see Nordström et al [12]. The raw terms of the fixpoint type are described elsewhere [3, 4].

The type σ_{⊥} is thought of as the type of partial computations with values of type σ. If M is any term, then ValL(M) is a computation which evaluates immediately yielding result M. EvalL(M) is similar, but M is never a partial computation. If E and F are both partial computations, then LetL x ⇐ E in F can be thought of as the computation F [M/x] provided that the partial computation E is defined and evaluates with result M, and is undefined if E is undefined. Up to provable equality EvalL(M) is the same as ValL(M); the two will be distinguished by their operational semantics. Evaluation of the former forces evaluation of M but evaluation of the latter does not. EvalL will be vital later on in obtaining precise relationships between operational and denotational semantics.

We give a type assignment system for M. This will consist of rules for deriving judgments of the form Γ ⊢ M : σ where the environment Γ is a finite list of (variable, type) pairs. We shall refer to σ as the type assigned to the raw term M in the environment Γ. Well formed judgments of the form Γ ⊢ M : σ are generated by the rules for simply typed lambda-calculus with unit, natural numbers, products and coproducts, plus the additional rules in Table 1. We write σ ⇀ τ for σ → τ_{⊥}. We refer to a type σ, where σ ≢ τ_{⊥} for any τ, as a total type.

We can use the syntax of M as the basis for a pure equational type theory [4] in which theorems take the form Γ ⊢ M = M′:σ; in this abstract we omit the rules for proving such judgments.

We can give a categorical semantics to M in the usual way. We shall interpret M in the FIX-category [3, 4] ωCPO of ωcpos and Scott continuous functions, equipped with the lifting monad, and topped vertical natural numbers with the successor structure map as FPO. We shall write D_{⊥} =^{def} {⊥} ∪ {[d] | d ∈ D} for (the underlying set of) the lift of the ωcpo D, with unit η_{D} =^{def} λd ∈ D.[d]:D → D_{⊥}. We denote the FPO by (ℕ^{∞}, ∞, s) (using an obvious notation). If f:C × D_{⊥} → D is a Scott continuous function, then the mediating morphism of the (indexed) FPO will be written it(f):C × ℕ^{∞} → D. We summarise the semantics of the less well known fragment of M:

• [[σ_{⊥}]] =^{def} [[σ]]_{⊥}, [[fix]] =^{def} ℕ^{∞},

• [[Γ ⊢ EvalL(M):σ_{⊥}]] = [[Γ ⊢ ValL(M):σ_{⊥}]] =^{def} η_{[[σ]]} ∘ [[Γ ⊢ M:σ]],

• [[Γ ⊢ LetL x ⇐ E in F:τ_{⊥}]] =^{def} [[Γ, x:σ ⊢ F:σ_{⊥}]]_{⊥} ∘ ⟨id_{[[Γ]]}, [[Γ ⊢ E:σ_{⊥}]]⟩, where f_{⊥} is the indexed Kliesli lifting of f in ωCPO,

• [[Γ ⊢ ω:fix_{⊥}]] =^{def} ∞∘!, where we have [[Γ]] ⟶^{!} 1 ⟶^{∗↦∞} ℕ_{⊥}^{∞}, 1 terminal in ωCPO,

• [[Γ ⊢ Inc(E):fix_{⊥}]] =^{def} s ∘ [[Γ ⊢ E:fix_{⊥}]],

• [[Γ ⊢ It(e.F, N):σ]] =^{def} it([[Γ, e:σ_{⊥} ⊢ F:σ]]) ∘ ⟨id_{[[Γ]]}, [[Γ ⊢ N:fix]]⟩.

3 Computation Types and the Let-Calculus

Moggi [10, 11] introduced a (simple) type theory which is now often referred to as the computational let-calculus. His calculus captures the following intuitions about (many) programming languages. First, it is sensible to separate out the notions of computations of values from values themselves; second that any value may be regarded as a “trivial” computation yielding itself as its value; and third, that computations may be composed sequentially. In fact this type theory corresponds with the notion of a category (with finite products) equipped with a strong monad. For these reasons an instance of the computional let-calculus is often referred to as a computational monad. More precisely, a computational monad is specified by a triple (T, Val, Let) where T is a type constructor and Val and Let are term constructors, that satisfy the following type assignment rules,

{Γ ⊢ M : σ \atop Γ ⊢ Val(M) : T σ} Γ ⊢ M : T σ Γ, x:σ ⊢ N : T σ′

Γ ⊢ Let x ⇐ M in N : T σ′

and the following rules for deducing equational theorems.

Γ ⊢ M : σ Γ, x:σ ⊢ N : T τ
Γ ⊢ Let x ⇐ Val(M) in N = N[M/x] : T σ′
Γ ⊢ M : T σ
Γ ⊢ Let x ⇐ M in Val(x) = M : T σ
Γ ⊢ M : T σ  Γ, x:σ ⊢ N : T σ′  Γ, y:σ′ ⊢ P : T σ′′

Γ ⊢ Let x ⇐ M in (Let y ⇐ N in P) = Let y ⇐ (Let x ⇐ M in N) in P : T σ′′

As expected, the triple ((−)_{⊥}, ValL, LetL) is a computational monad, usually known as the lifting monad. The equational logic of M must be omitted here for the sake of brevity, but (the appropriate instance of) the three (equational) rules above are indeed present in M [3, 4]. We include a small example at the end of the paper in Section 8 to illustrate the use of a monad other than the lifting monad.

4 An Operational Semantics for M

Let us specify an operational semantics for (the term language of) M, as done for a similar metalogic by Gordon [5]. We shall need a few auxiliary definitions. The canonical raw terms are given by the grammar

V ::= ⟨⟩ | Z | S(V) | ⟨M, M⟩ | Inl(M) | Inr(M) | λx.M | ValL(M) | Inc(M).

We write M_{σ} for the set of M-programs, that is, raw terms M for which ⊢ M:σ is provable, and M_{σ}^{can} ⊆ M_{σ} for the subset of canonical terms. We specify an operational semantics in two equivalent ways: as a ‘big step’ evaluation relation, M ⇓ V, and a ‘small step’ reduction relation, M → N, where M, N and V are programs and V is canonical. The two relations are generated in the usual way, except for the syntax involving lifted types and the fixpoint type; the rules for the evaluation and reduction relations appear in Table 2. It is straightforward to prove that M ⇓ V if and only if M →^{∗} V (where →^{∗} means reflexive, transitive closure of →). The semantics is deterministic and call-by-name. If M ∈ M_{σ} and M → N then N ∈ M_{σ} too. It is easy to prove the following result by rule induction.

Proposition 1 If M ∈ M_{σ} and also M ⇓V, then V ∈ M_{σ}^{can} and ⊢ M = V:σ, where the latter judgment holds in the equational metalogic.

Our principal aim here is to prove the following (generic) adequacy theorem.

Theorem 2 (Generic Adequacy) The equational metalogic is computationally adequate for the operational semantics in the following sense. If E ∈ M_{σ_{⊥}} and M ∈ M_{σ} are such that ⊢ E = ValL(M) : σ_{⊥} is provable, then there is V ∈ M_{σ_{⊥}}^{can} for which E ⇓ V.

We also prove a normalisation result at total types.

Theorem 3 (Normalisation) If M ∈ M_{σ} with σ total, then evaluation of M converges, that is, ∃V. M ⇓ V.

To prove this we need some technical machinery. Let [[−]]:M → ωCPO refer to the semantics of M in the FIX-category ωCPO. We now define a logical relation which takes the form ◁_{σ}⊆ [[σ]] × M_{σ} for all types σ, and is defined through certain inductive clauses of which we give just a few examples:

• e ◁_{σ_{⊥}} E iff whenever e = [d] for d ∈ [[σ]] then ∃M. E ⇓ ValL(M) and d ◁_{σ} M.

• ∞ ◁_{fix} N iff ∀n ∈ ℕ^{∞} \ {∞} we have n ◁_{fix} N.

• n + 1 ◁_{fix} N iff ∃E_{n}. N ⇓ Inc(E_{n}), ∃N_{n}. E_{n} ⇓ ValL(N_{n}) and also for 1 ≤ i ≤ n we have ∃E_{i−1}. N_{i} ⇓ Inc(E_{i−1}), ∃N_{i−1}. E_{i−1} ⇓ ValL(N_{i−1}) and ∃E. N_{0} ⇓ Inc(E).

• 0 ◁_{fix} N iff ∃E. N ⇓ Inc(E).

V ⇓ V
{M ⇓ V \atop S(M) ⇓ S(V)}  {N ⇓ Z  M ⇓ V \atop (x. F)^{N}(M) ⇓ V}  {N ⇓ S(U)  F [(x. F)^{U}(M)/x] ⇓ V \atop (x. F)^{N}(M) ⇓ V}

{P ⇓ ⟨M, N⟩ F [M, N/x, y] ⇓ V \atop Split(P, x. y. F) ⇓ V}

{C ⇓ Inl(M)  F [M/x] ⇓ V \atop Case(C, x. F, x. G) ⇓ V}  {C ⇓ Inr(M)  G[M/x] ⇓ V \atop Case(C, x. F, x. G) ⇓ V}

{F ⇓ λx. N N[M/x] ⇓ V \atop F M ⇓ V}

M ⇓ V

EvalL(M) ⇓ ValL(V)

E ⇓ ValL(M) F [M/x] ⇓ V
LetL x ⇐ E in F ⇓ V

N ⇓ Inc(E) M[LetL y ⇐ E in ValL(It(e. M, y))/e] ⇓ V It(e. M, N) ⇓ V

ω ⇓ ValL(Inc(ω))
(x.F)^{Z}(M) → M
(x.F)^{S(V )}(M) → F [(x.F)^{V} (M)/x]
Split(⟨M, N⟩, x. y. F) → F [M, N/x, y]
Case(Inl(M), x. F, x. G) → F [M/x]
Case(Inr(M), x. F, x. G) → G[M/x]
(λx. N)M → N[M/x]
LetL x ⇐ ValL(M) in F → F [M/x]

It(e. M, Inc(E)) → M[LetL y ⇐ E in ValL(It(e. M, y))/e] ω → ValL(Inc(ω)) EvalL(V) → ValL(V)

{M → N \atop E[M] → E[N]}

where E[−] ::= S(−) | (x.F)^{−}(M) | Split(−, x. y. F) | Case(−, x. F, x. G) | (− M) | LetL x ⇐ − in E | It(e. M, −) | EvalL(−)

Table 2: Operational semantics for M We shall also need the following lemmas and proposition, for which we sketch the proof of the latter:

Lemma 4 Suppose that d ◁_{σ} M and also M′ →^{∗} M; then d ◁_{σ} M′.

Lemma 5 Let (d_{i} | i ∈ ω) be an ω-chain in [[σ]] for any σ. If d_{i} ◁_{σ} M for some M and each i ∈ ω, then ⋁_{i∈ω} d_{i} ◁_{σ} M.

Proposition 6 Let x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : σ be provable, let M_{i} ∈ M_{σ_{i}} for 1 ≤ i ≤ n, and let d_{i} ∈ [[σ_{i}]] for 1 ≤ i ≤ n with d_{i} ◁_{σ_{i}} M_{i}. Then it is the case that

[[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ M : σ]](d⃗) ◁_{σ} M[M^{1}, …, M^{n}/x_{1}, …, x_{n}]

where d⃗ =^{def} (d_{1}, …, d_{n}) ∈ Π_{1}^{n}[[σ_{i}]].

Proof The proof proceeds by induction on the structure of M, and uses Lemma 4 and Lemma 5. We just give some example cases. We shall adopt the following convention: if (for example) Γ ⊢ M:σ is provable, we write m:[[Γ]] → [[σ]] for the morphism (here continuous function) [[Γ ⊢ M:σ]]. We shall also write (for example) M̃ for M[M^{1}, …, M^{n}/x_{1}, …, x_{n}]. We give two inductive cases:

(Case M is It(e.F, N)): We need to prove that

[[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ It(e.F, N):σ]] = it(f)(d⃗, n(d⃗)) ◁_{σ} It(e.F̃, Ñ),

where f:Π_{1}^{n}[[σ_{i}]]×[[σ]]_{⊥} → [[σ]] and thus it(f):Π_{1}^{n}[[σ_{i}]]×ℕ^{∞} → [[σ]]. By induction we know that n(d⃗) ◁_{fix} Ñ (1) and

e ◁_{σ_{⊥}} E implies f(d⃗, e) ◁_{σ} F̃[E/e]. (2)

We consider the case when n(d⃗) is ň + 1 ∈ ℕ^{∞} \ {∞}. We have ň + 1 ◁_{fix} Ñ from (1), and so Ñ ⇓ Inc(Eň), Eň ⇓ ValL(Nň) and so on to N_{0} ⇓ Inc(E). It can be shown that

it(f)(d⃗, 0) ◁_{σ} It(e.F̃, N_{0}).

Now let 0 ≤ r ≤ ň. Write N_{ň+1} =^{def} Ñ; we prove that if

it(f)(d⃗, r) ◁_{σ} It(e.F̃, N_{r}) (3)

then it(f)(d⃗, r + 1) ◁_{σ} It(e.F̃, N_{r+1}). From (3) and that E_{r} ⇓ ValL(N_{r}) we may deduce

it(f)(d⃗, r + 1) ◁_{σ} F̃[LetL y ⇐ E^{r} in ValL(It(e.F̃, y))/e].

But N_{r+1} →^{∗} Inc(E_{r}) and hence It(e.F̃, N_{r+1}) →^{∗} F̃[LetL E^{r} in ValL(It(e.F̃, y))/e], so we are done by appeal to Lemma 4.

(Case M is EvalL(M)): We wish to prove that

[[x_{1}:σ_{1}, …, x_{n}:σ_{n} ⊢ EvalL(M):σ_{⊥}]](d⃗) = [m(d⃗)] ◁_{σ_{⊥}} EvalL(M̃)

and so we need to show that there is V ∈ M_{σ}^{can} for which EvalL(M̃) ⇓ ValL(V) with m(d⃗) ◁_{σ} V. By the induction hypothesis we have m(d⃗) ◁_{σ} M̃, and by inspecting the clauses of the logical relation one can deduce that M̃ ⇓ V for some V with m(d⃗) ◁_{σ} V and so we are done. ■

Proof [of Theorem 2 ] Follows because the categorical semantics of M is sound, together with the application of Proposition 6 with i = 1 and d_{1} ≡ ∗ ◁_{unit} ⟨⟩ ≡ M_{1}. More precisely, we may deduce

[[x:unit ⊢ E:σ_{⊥}]](∗) = [[[x:unit ⊢ M:σ]](∗)] ◁_{σ_{⊥}} E[⟨⟩/x] ≡ E

and so ∃V.E ⇓ V by inspecting the clause defining the logical relation at lifted types. ■

Proof [of Theorem 3 ] Just as in the last proof, apply Proposition 6 to deduce that the relation [[⊢ M:σ]](∗) ◁_{σ} M. By inspection of the clauses defining relation ◁_{σ} it will follow that evaluation of M converges. ■

5 The Object Language O

The object language O is essentially a call-by-value form of PCF. Syntactically it is a tiny fragment of Standard ML. The O-types, denoted by σ or τ, are generated from ground types bool of Booleans, int of numbers, by forming function types σ -> τ. Let metavariable ℓ range over a set, ℕ ∪ {tt, ff}, of literals, and metavariable ⊕ over a set of operators, {+, −, ×, =, <}. The Oterms, e, are generated by the following BNF grammar, which also defines canonical O-terms, c.

e ::= c | e\underline{⊕}e | if e then e else e | e e

           c ::= x | () | \underline{ℓ} | fn x => e | letfun f x = e in f end

The last canonical term is a form of SML notation for a recursively defined function, named f and with argument x, which are both bound in e.

The type assignment system for O consists of a collection of rules for proving judgments of the form Γ ⊢ e : σ where Γ is a finite list of (variable, type) pairs; we shall write x_{1}:σ_{1}, …, x_{n}:σ_{n} for Γ. The typing rules for O are a straightforward extension of those for simply typed lambda-calculus; we omit them all apart from the rule for recursively defined functions.

Γ, f:σ -> τ, x:σ ⊢ e : τ

    Γ ⊢ letfun f x = e in f end : σ -> τ

For each O-type σ, let O_{σ} be the set of O-terms e for which ⊢ e : σ is provable; such a term is known as a program. Let O_{σ}^{can} be the set of all programs from O_{σ} that are canonical.

The operational semantics of O is specified as an evaluation relation, consisting of ‘big step’ judgments of the form e ⇓ c, where e and c are programs, the latter canonical. One should think of the canonical terms as values which are returned by (non-divergent) programs. The relation is given inductively by the rules in Table 3. One can deduce from the rules for forming such judgments that evaluation is deterministic and that if e ∈ O_{σ} and e ⇓ c, then c ∈ O_{σ}^{can}. If e is a program, write e⇓ to mean ∃c. e⇓c, in which case we say that program c converges.

The evaluation relation induces a Morris-style contextual equivalence between O-terms: two terms are equivalent if each can replace the other in any

c ⇓ c

{e_{1} ⇓ \underline{ℓ_{1}} e_{2} ⇓ \underline{ℓ_{2}} \atop e_{1}\underline{⊕}e_{2} ⇓ \underline{ℓ_{1} ⊕ ℓ_{2}}} e_{1} ⇓ \underline{tt} e_{2} ⇓ c

                           if e_{1} then e_{2} else e_{3} ⇓ c

e_{1} ⇓ \underline{ff} e_{3} ⇓ c

                                                 if e_{1} then e_{2} else e_{3} ⇓ c

{e_{1} ⇓ fn x => e  e_{2} ⇓ c_{2}  e[c^{2}/x] ⇓ c \atop e_{1} e_{2} ⇓ c}

e_{1} ⇓ letfun f x = e in f end e_{2} ⇓ c_{2} e[letfun f x = e in f end, c^{2}/f, x] ⇓ c

e_{1} e_{2} ⇓ c

Table 3: Operational semantics for O

program without changing its convergence behaviour. Informally, let a context, C[−], be a term some of whose subterms have been replaced by a hole, −, and let C[e] be the term obtained by filling each hole with the term e. Suppose that e_{1} and e_{2} are both members of one of the sets O_{σ}. Write e_{1} ≈ e_{2} to mean that C[e_{1}]⇓ iff C[e_{2}]⇓ whenever C[e_{1}], C[e_{2}] are both members of O_{τ} for some type τ. In this case we say the two terms are observationally equivalent.

6 Translation of O into M

In this section we give a denotational semantics for O using M. The intention is that via this semantics, the metalogic can be applied to prove observational equivalences between O-terms. This intention is vindicated by Theorem 12, the main result of the paper, which says that if the denotations of two O-terms are provably equal in the metalogic, then in fact the two terms are observationally equivalent.

We adopt the usual inductive definition of numerals, ⌊0⌋ =^{def} Z and ⌊n+1⌋ =^{def} S(⌊n⌋). Booleans are represented by terms of type unit + unit; let ⌊tt⌋ =^{def} Inl(⟨⟩) and ⌊ff⌋ =^{def} Inr(⟨⟩). For each arithmetic or relational operator, ⊕ ∈ {+, −, ×, =, <}, we need an encoding (M⌊+⌋N) in M such that suitably typed (⌊ℓ⌋⌊⊕⌋⌊ℓ′⌋) evaluates to ⌊ℓ⊕ℓ′⌋. Given the iteration on nat in M, it is routine to do so; for instance, (M⌊+⌋N) is (x.S(x))^{N}(M).

Using iterations on the fix type we can define an operation Fix(−), that we will need for recursively defining partial functions of the form σ ⇀ τ.

Lemma 7 There is a term-former Fix(−) that satisfies the typing rule

{Γ ⊢ M : (σ ⇀ τ) → (σ ⇀ τ) \atop Γ ⊢ Fix(M) : σ ⇀ τ}

and for any M and N, Fix(M) N →^{∗} M (Fix(M)) N.

Proof Let Fix′(M, N) =^{def} It(e. λx. LetL y ⇐ e in M y x, N) and then set Fix(M) =^{def} Fix′(M, Inc(ω)). It is straightforward to check that Fix(M) has the expected type. From the calculation,

Fix(M) N ≡ It(e. λx. LetL y ⇐ e in M y x, Inc(ω)) N
→ (λx. LetL y ⇐ (LetL z ⇐ ω in ValL(Fix′(M, z))) in M y x) N
→ LetL y ⇐ (LetL z ⇐ ω in ValL(Fix′(M, z))) in M y N
→ LetL y ⇐ (LetL z ⇐ ValL(Inc(ω)) in ValL(Fix′(M, z))) in M y N
→ LetL y ⇐ ValL(Fix′(M, Inc(ω))) in M y N
≡ LetL y ⇐ ValL(Fix(M)) in M y N
→ M (Fix(M)) N

one sees that Fix(M) has the expected reduction behaviour too. ■

We give the translation of O into M in terms of an arbitrary computational monad (T, Val, Let). In this section and the next this computational monad will be an instance of the lifting monad, ((−)_{⊥}, ValL, LetL). In Section 8 we will use a different monad to admit the possibility of an exception being raised.

The translation of O into M follows the pattern set by Pitts [15]. Map each O-type σ to an M-type [[σ]] inductively as follows: ground types bool and int are mapped to unit + unit and nat respectively, while σ -> τ is mapped inductively to [[σ]] → T [[τ]]. Each O-environment Γ = x_{1}:σ_{1}, …, x_{n}:σ_{n} is mapped to [[Γ]] =^{def} x_{1}:[[σ_{1}]], …, x_{n}:[[σ_{n}]]. To begin the translation of O terms into M, to each canonical O-term c we assign a canonical M-term |c| as follows.

|x| =^{def} x
|\underline{ℓ}| =^{def} ⌊ℓ⌋
|fn x => e| =^{def} λx. [[e]]
|letfun f x = e in f end| =^{def} Fix(λf. λx. [[e]])

In keeping with the intuition that arbitrary O-terms express computations rather than simple values, we assign to each O-term e an M-term [[e]] of computation type.

[[c]] =^{def} Val(|c|)
[[e_{1}\underline{⊕}e_{2}]] =^{def} Let x_{1} ⇐ [[e_{1}]] in (Let x_{2} ⇐ [[e_{2}]] in EvalL(x_{1}⌊⊕⌋x_{2}))
[[if e_{1} then e_{2} else e_{3}]] =^{def} Let b ⇐ [[e_{1}]] in Case(b, u. [[e_{1}]], u. [[e_{1}]])
[[e_{1} e_{2}]] =^{def} Let f ⇐ [[e_{1}]] in (Let x ⇐ [[e_{2}]] in f x)

The translation respects the type systems of O and M in the following sense, easily proved by structural induction.

Proposition 8 (Static Adequacy)

(1) Whenever Γ ⊢ e : σ is provable in O, [[Γ]] ⊢ [[e]] : T [[σ]] is provable in M.

(2) Furthermore, if e is canonical, then [[e]] is canonical and [[Γ]] ⊢ |e| : [[σ]] is provable in M.

Since the translation is compositional it is straightforward to prove the congruence and substitution parts of the following lemma by structural induction.

Lemma 9

(1) If Γ ⊢ [[e_{1}]] = [[e_{2}]] : σ, Γ′ ⊢ [[C[e_{1}]]] : τ and Γ′ ⊢ [[C[e_{2}]]] : τ are provable in M, then Γ′ ⊢ [[C[e_{1}]]] = [[C[e_{2}]]] : τ is provable in M too.

(2) For any O-term e and canonical O-term c, [[e]][|c|/x] ≡ [[e[c/x]]].

We can establish the following exact correspondence between evaluation of any configuration and its translation by rule inductions and appeal to Lemmas 7 and 9.

Lemma 10 Suppose e ∈ O_{σ}.

(1) Whenever e ⇓ c for some c ∈ O_{σ}^{can}, then [[e]] ⇓ [[c]].

(2) Whenever [[e]] ⇓ V for some V ∈ M_{T [[σ]]}^{can}, there is c with e ⇓ c and V ≡ [[c]].

Now we can prove adequacy for O. This is the crux of the factorisation, where adequacy for M—obtained from a domain-theoretic logical relations argument—is combined with the previous correspondence lemma—obtained by comparatively routine albeit detailed syntactic calculations.

Proposition 11 (Dynamic Adequacy) Suppose e ∈ O_{σ} and c ∈ O_{σ}^{can}.

(1) Whenever e ⇓ c then ⊢ [[e]] = [[c]] : T [[σ]] is provable.

(2) Whenever ⊢ [[e]] = [[c]] : T [[σ]] is provable, then e⇓.

Proof (1) Suppose e ⇓ c. By Lemma 10(1) we have [[e]] ⇓ [[c]]. Hence we have ⊢ [[e]] = [[c]] : T [[σ]] by Proposition 1. (2) Suppose ⊢ [[e]] = [[c]] : T [[σ]]. From Proposition 8(2) we know that [[c]] is canonical, so by Theorem 2, there is V such that [[e]] ⇓ V. Then by Lemma 10(2) there is c such that that e ⇓ c as required. ■

We now obtain soundness from adequacy as usual [8].

Theorem 12 (Soundness) If e_{1}, e_{2} ∈ O_{σ} and ⊢ [[e_{1}]] = [[e_{2}]] : T [[σ]] then e_{1} ≈ e_{2}.

Proof Suppose ⊢ [[e_{1}]] = [[e_{2}]] : T [[σ]]. We are to show for all contexts C[−] such that C[e_{1}] and C[e_{2}] are both O-programs of some type τ, that C[e_{1}]⇓ iff C[e_{2}]⇓. We show the forwards direction; the reverse follows by symmetry. Suppose then that each C[e_{i}] ∈ O_{τ}, and that C[e_{1}]⇓c for some canonical c ∈ O_{τ}. By Proposition 11(1), we have ⊢ [[C[e_{1}]]] = [[c]] : T [[τ]]. By Lemma 9(1) we have ⊢ [[C[e_{1}]]] = [[C[e_{2}]]] : T [[τ]]. By transitivity and symmetry, ⊢ [[C[e_{2}]]] = [[c]], and then since c is canonical C[e_{2}]⇓ by Proposition 11(2), as required. ■

7 Variant 1: call-by-name O

In this and the following section we show how our modular proof of adequacy can easily be modified to apply to two variants of the object language O.

The first of these is a form of O in which functions are applied using a callby-name instead of a call-by-value strategy. The syntax and type system of O is unchanged except that variables are no longer included among the canonical O-terms.

{e_{1} ⇓ fn x => e e[e^{2}/x] ⇓ c \atop e_{1} e_{2} ⇓ c}

e_{1} ⇓ letfun f x = e in f end e[letfun f x = e in f end, e^{2}/f, x] ⇓ c

e_{1} e_{2} ⇓ c

Table 4: Rules for call-by-name function application in O

             c ::= \underline{ℓ} | fn x => e | letfun f x = e in f end.

The evaluation relation, e ⇓ c, is given inductively by the original rules from Table 3, except that the two rules for the two kinds of function application are replaced by call-by-name forms in Table 4. One can easily deduce that evaluation is deterministic and preserves types as before. We adopt the same notions of program convergence and observational equivalence as before.

We must also modify the translation of O into M. As before, ground types bool and int are mapped to unit + unit and nat respectively, but this time each (call-by-name) function type σ -> τ is mapped to T [[σ]] -> T [[τ]] (instead of [[σ]]->T [[τ]] in the call-by-value case). A call-by-name strategy applies functions to computations rather than values. Each O-environment Γ = x_{1}:σ_{1}, …, x_{n}:σ_{n} is mapped to M-environment [[Γ]] =^{def} x_{1}:T [[σ_{1}]], …, x_{n}:T [[σ_{n}]]. The mapping of environments reflects a change in denotation of object variables—in the callby-value setting they denoted values; here they denote computations. The translations of terms are the same as before except for the following changes. The rules for recursive functions and applications are changed, the rule for canonical variables is dropped, and a new one for non-canonical variables is introduced.

|letfun f x = e in f end| =^{def} Fix(λg. λx. (λf. [[e]])(Val(g)))
[[x]] =^{def} x
[[e_{1} e_{2}]] =^{def} Let f ⇐ [[e_{1}]] in f [[e_{2}]]

The third of these equations effects the call-by-name strategy, while the remaining two reflect the change in denotation of object variables—from values to computations.

Given the change in translation of environments, the following static adequacy result is easily proved.

Proposition 13 (Static Adequacy)

(1) Whenever Γ ⊢ e : σ is provable in O, [[Γ]] ⊢ [[e]] : T [[σ]] is provable in M.

(2) Furthermore, if e is canonical, then [[e]] is canonical and [[Γ]] ⊢ |e| : [[σ]] is provable in M.

The congruence lemma is stated and proved as before, but the substitution lemma this time concerns the substitution of arbitrary O-terms, rather than simply canonical ones.

           e_{1} ⇓ wrong

e_{1}\underline{⊕}e_{2} ⇓ wrong

                         e_{1} ⇓ wrong ; e_{1} e_{2} ⇓ wrong

                                                e_{1} ⇓ wrong
                                        if e_{1} then e_{2} else e_{3} ⇓ wrong

e_{1} ⇓ \underline{ℓ} e_{2} ⇓ wrong

e_{1}\underline{⊕}e_{2} ⇓ wrong

                                 e_{1} ⇓ c  c ≢ wrong  e_{2} ⇓ wrong
                                          e_{1} e_{2} ⇓ wrong

Table 5: Rules for a single exception in O

Lemma 14

(1) If Γ ⊢ [[e_{1}]] = [[e_{2}]] : σ, Γ′ ⊢ [[C[e_{1}]]] : τ and Γ′ ⊢ [[C[e_{2}]]] : τ are provable in M, then Γ′ ⊢ [[C[e_{1}]]] = [[C[e_{2}]]] : τ is provable in M too.

(2) For any O-terms e and e′, [[e]][[[e′]]/x] ≡ [[e[e′/x]]].

The correspondence between evaluation of an O-program and its denotation is proved much as before, by a detailed but routine rule induction and appeal to the previous lemmas.

Lemma 15 Suppose e ∈ O_{σ}.

(1) Whenever e ⇓ c for some c ∈ O_{σ}^{can}, then [[e]] ⇓ [[c]].

(2) Whenever [[e]] ⇓ V for some V ∈ M_{[[σ]]}^{can}, there is c with e ⇓ c and V ≡ [[c]].

Once these detailed calculations are complete the soundness theorem follows exactly as before.

Theorem 16 (Soundness) If e_{1}, e_{2} ∈ O_{σ} and ⊢ [[e_{1}]] = [[e_{2}]] : T [[σ]] then e_{1} ≈ e_{2}.

Proof From Lemma 15 by the same arguments that established Proposition 11 and Theorem 12 in the call-by-value case. ■

8 Variant 2: O plus an exception

Our second variant consists in adding a single exception, wrong, to the original call-by-value O. The point of this variant is that our methods work for computational monads other than the lifting monad.

We introduce a new canonical expression, wrong, and extend the typing relation so that judgment Γ ⊢ wrong : σ is provable for any type σ and (wellformed) environment Γ. The evaluation relation is generated from the original call-by-value rules in Table 3—amended with the side-condition on both rules for function application that c_{2} ≢ wrong—together with the new rules in Table 5. Convergence and observational equivalence are defined as before.

To give the translation of O into M, we shall need a new computational monad (T, Val, Let). Intuitively, computations may either converge to a value, diverge, or go wrong, that is, converge to the exceptional value wrong. To model such computations set T σ =^{def} (σ + 1)_{⊥}. A computation that goes wrong will be modelled by Wrong =^{def} ValL(Inr(⟨⟩)). The terms of the computational monad are defined by

Val(M) =^{def} ValL(Inl(M))
Let x ⇐ M in N =^{def} LetL y ⇐ M in Case(y, x. M, u. Wrong).

Given the metalogic’s coproduct rules [3, 4], it is routine to check that this is indeed a well defined computational monad in the sense given earlier.

Apart from the re-interpretation of the triple (T, Val, Let) there are two other changes needed to the translation of O into M. First, we need to change the translation of canonical terms, [[c]], to the following.

[[c]] =^{def} \{ \begin{matrix}Wrong & if c ≡ wrong \\ Val(|c|) & otherwise \end{matrix}

Note that the interpretation of each canonical term c ∈ O_{σ} as a value |c| ∈ O_{[[σ]]} does not need to be extended to wrong—and in fact would not make sense. Second, we need to change the translation of [[e_{1}\underline{⊕}e_{2}]] to the following,

[[e_{1}\underline{⊕}e_{2}]] =^{def} Let x_{1} ⇐ [[e_{1}]] in (Let x_{2} ⇐ [[e_{2}]] in Eval(x_{1}\underline{⊕}x_{2}))

where Eval(M) =^{def} LetL y ⇐ EvalL(M) in Val(y) for any M. There is no need to re-interpret the definition of recursive functions using Fix because although the definition of T σ is different, the interpretation of an O-function σ -> τ is still a partial function, this time [[σ]] ⇀ [[τ]] + 1.

Given these modifications to the denotational semantics, the soundness argument goes through much as before. Static adequacy (Proposition 8) holds as before, except that the judgment in part (2) holds only when e ≢ wrong. Compositionality, Lemma 9(1) holds as before, and so does the second part, substitution, except again for a side-condition that c ≢ wrong—but the sidecondition on function applications ensures that wrong is never substituted for a variable in the operational semantics. The correspondence between the evaluation of each O-program and its denotation, Lemma 10, holds as before. The proof requires the easily verified facts that

Let x ⇐ Val(M) in N →^{+} N[M/x]
Let x ⇐ Wrong in M →^{+} Wrong
Eval(⌊ℓ⌋⌊⊕⌋⌊ℓ′⌋) →^{+} Val(⌊ℓ ⊕ ℓ⌋)

for suitably-typed terms M, N and literals ℓ and ℓ′ (where →^{+} is the transitive closure of →). Given these lemmas, dynamic adequacy and soundness (Proposition 11 and Theorem 12) follow exactly as before.

9 Related and Future Work

This paper has shown how adequacy (and hence soundness) for a call-by-value object language O may be factored into two parts: a (non-routine) adequacy proof for a metalogic coupled with a comparatively routine proof of correspondence between the evaluation of each object program and its denotation in the metalogic. The factorisation is of interest because the second part can easily be adapted to other object languages without needing to repeat the first part. Variants of O with call-by-name functions and with a simple exception mechanism illustrated this genericity.

Apart from the unpublished notes [17, Chapter 3] that inspired this reworking, the only previous work to factor an adequacy proof via a metalogic is in Gordon’s dissertation [5]. There the meaning of the metalogic was given using Abramsky’s applicative bisimulation rather than domain theoretically. Others have equipped a metalogic with an operational semantics [1, 6, 7, 8, 9, 14, 21] but none has reworked Plotkin’s original factorisation. Crole presents unfactored adequacy proofs for two PCF style languages mapped into the FIX-logic [2]. Apart from their application to denotational semantics, monads have been popularised by Wadler and others as a way to incorporate imperative features into lazy functional programming [13, 19, 20].

The key feature of this paper is the reworking of Plotkin’s idea for factoring adequacy, but within a more structured and foundational framework; nonetheless the absence of recursive types from M prohibits modelling of many object language features. Hence in future work we intend to extend M with recursive types; Pitts’ recent advances [16] will be highly relevant to extending Theorem 2. A further goal is to mechanise some form of M in a theorem-prover, and hence take advantage of this paper’s soundness result to prove operational equivalences of O-programs mechanically. The operational semantics of M itself induces an observational equivalence on M-terms. It is of interest to consider the relationship between the direct observational equivalence on O-terms and the indirect equivalence induced by the translation into M and observational equivalence on M-terms; Riecke pursues a related investigation [18]. Although space has prevented its full exposition here, application of M to verification of functional programs was the specific motivation for the theory in this paper.

Acknowledgements We wish to thank everyone at the Ayr workshop who discussed this work, and to the referees for their detailed comments. Roy Crole holds a SERC Research Fellowship at Imperial College. During this work Andrew Gordon was a member of the Programming Methodology Group at Chalmers University of Technology, Gothenburg. The work was begun while we were visitors at the University of Cambridge Computer Laboratory. We thank Andrew Pitts, our host, and everyone else at the Lab for their hospitality. Roy Crole thanks the SERC and the CEC CLICS project for providing funding to visit Cambridge and Gothenburg. Andrew Gordon thanks Mary Sheeran for arranging his visit to the PMG.

References

[1] Peter Nicholas Benton. Strictness Analysis of Lazy Functional Programs. PhD thesis, University of Cambridge Computer Laboratory, August 1993. Available as Technical Report 309.

[2] R. L. Crole. Computational adequacy for the FIX-Logic. Theoretical Computer Science. Accepted. (To appear in 1994.)

[3] R. L. Crole and A. M. Pitts. New foundations for fixpoint computations: FIX hyperdoctrines and the FIX-logic. Information and Control, 98:171– 210, 1992. Earlier version in LICS’90.

[4] Roy L. Crole. Programming Metalogics with a Fixpoint Type. PhD thesis, University of Cambridge Computer Laboratory, February 1992. Available as Technical Report 247.

[5] Andrew D. Gordon. Functional Programming and Input/Output. PhD thesis, University of Cambridge, August 1992. To appear in Cambridge University Press’ series Distinguished Dissertations in Computer Science.

[6] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, Mass., 1992.

[7] Claire Jones. Probabilistic Non-determinism. PhD thesis, University of Edinburgh, 1990. Available as Technical Report CST–63–90, Computer Science Department, University of Edinburgh.

[8] Albert R. Meyer and Stavros S. Cosmadakis. Semantical paradigms: Notes for an invited lecture. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science, pages 236–253, July 1988.

[9] Eugenio Moggi. The Partial Lambda-Calculus. PhD thesis, Department of Computer Science, University of Edinburgh, August 1988. Available as Technical report CST–53–88.

[10] Eugenio Moggi. Computational lambda calculus and monads. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, June 1989.

[11] Eugenio Moggi. Notions of computation and monads. Theoretical Computer Science, 93:55–92, 1989.

[12] Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf’s Type Theory, volume 7 of The International Series of Monographs in Computer Science. Clarendon Press, Oxford, 1990.

[13] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Proceedings 20th ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993. ACM Press, 1993.

[14] Andrew M. Pitts. Notes on the call-by-value and call-by-name translation of the simply typed lambda-calculus into the computational lambdacalculus. Manuscript, October 1990.

[15] Andrew M. Pitts. Evaluation logic. In G. Birtwistle, editor, IVth Higher Order Workshop, Banff 1990, Workshops in Computing, pages 162–189. Springer-Verlag, 1991. Available as University of Cambridge Computer Laboratory Technical Report 198, August 1990.

[16] Andrew M. Pitts. Computational adequacy via ‘mixed’ inductive definitions. In MFPS IX, New Orleans, 1993.

[17] Gordon D. Plotkin. Denotational semantics with partial functions. Unpublished lecture notes, CSLI, Stanford University, July 1985.

[18] Jon G. Riecke. Fully abstract translations between functional languages. To appear in Mathematical Structures in Computer Science, December 1992.

[19] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2:461–493, 1992.

[20] Philip Wadler. The essence of functional programming. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, 1992.

[21] Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, Mass., 1993.