A Third-Order Representation of the λμ-Calculus

Andreas Abel^{⋆}

Carnegie Mellon University, Department of Computer Science 5000 Forbes Avenue, Pittsburgh, PA 15213, USA phone: +1(412)268-2582, email: abel@cs.cmu.edu

Abstract. Higher-order logical frameworks provide a powerful technology to reason about object languages with binders. This will be demonstrated for the case of the λμ-calculus with two different binders which can most elegantly be represented using a third-order constant. Since cases of third- and higher-order encodings are very rare in comparison with those of second order, a second-order representation is given as well and equivalence to the third-order representation is proven formally.

1 Introduction

The λμ-calculus [Par92,OS97,Bie98], a proof theory for the implicational fragment of classical logic, has been established as a general tool to reason about functional programming languages with control, e.g. continuations and exceptions. It is basically an extension of the λ-calculus by a second binder. Some of its properties like strong normalization and confluence are very fundamental for its use in functional programming and proof systems; a formal verification of these basic properties is therefore desirable. Human proofs are error-prone; even these which have undergone the scientific review process. For instance, the first published proof of confluence for the λμ-calculus contained a flaw that was only recently corrected [BHF01].

When reasoning about programming languages and logics with binders— like the λ-calculus—the use of a higher-order logical framework can greatly reduce the size formalized proofs require. This is due to its built-in notions of α-equivalence and substitution which make several technical lemmata obsolete if a clever representation of the object language is chosen.

To our knowledge, properties of the λμ-calculus have not been verified mechanically so far. This article intends to provide a working point by giving two possible encodings of the λμ-calculus in a higher-order abstract syntax. As it will be seen, the λμ-calculus is one of the rare examples that can best be represented in a way that involves a third-order constructor. This representation will enable a natural implementation of the structural or mixed substitution that has been discussed controversially in the literature [OS97,SR98,dG98,Bie98].

⋆ This work was supported by the Graduiertenkolleg Logik in der Informatik (GKLI), Munich, and the Office of Technology in Education, Carnegie Mellon University.

The remainder of this article is organized as follows: In Sect. 2 we will introduce the λμ-calculus in its original formulation by Parigot [Par92]. We will proceed to interpret it computationally in Sect. 3 by giving a small-step semantics and an application in exception handling. Sect. 4 contains a development of a third-order representation for the untyped and the typed λμ-calculus together with the formalization of the small-step semantics. We will point out a difficulty with the representation and give an alternative, second-order encoding and prove equivalence of both representations in Sect. 5. An outlook on further work will conclude this article.

2 Parigot’s λμ-Calculus

In his seminal 1992 paper Parigot [Par92] introduced the λμ-calculus as a proof theory for classical logic. In the following we will present the first-order fragment which, in its computational interpretation, provides a general tool to model control in functional programming.

The raw terms are given by this grammar:

M ::= x | λx.M | M M | μa.N (Unnamed) terms
N ::= [a]M  Named terms

It is basically the untyped λ-calculus plus a second binder μ and μ-application [a]M. Furthermore there is a second class of variables which we call μ-variables and denote by a, b and c, in contrast to the λ-variables denoted by x, y and z. The constructor μ binds a μ-variable in the following term; as for λ-variables, α-equivalence can be defined. In the following we will not distinguish between α-equivalent terms.

The raw terms can be typed by the following rules which we present in natural deduction style:

x : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : B ; \overline{→I^{x}} ; λx.M : A → B  M_{1} : A → B  M_{2} : A ; \overline{→E} ; M_{1} M_{2} : B ; a : \overline{A}  M : A ; \overline{contra} ; [a]M : −  a : \overline{A} ; \begin{matrix}· \\ · \\ · \end{matrix} ; N : − ; \overline{raa^{a}} ; μa.N : A

In the rule raa the judgment N : − means that the term N has no type. The symbol − denotes the absurdity, which is not considered to be a type. The formula \overline{A} denotes the cotype of A; in the realm of logic \overline{A} would be the negated proposition A. Thus the μ-introduction is isomorphic to the reductio ad absurdum rule in classical logic, which states that A holds if ¬A leads to a contradiction.

The contra rule is analogous to the fact in logic that ¬A and A entail a contradiction. Note that there is no rule which constructs an inhabitant of a cotype. Thus, if C : \overline{A} holds, C must be a μ-variable a. The term [a]M resulting from the application of a μ-variable a to a term M has no type, but it is said to be named by a and hence is called a named term.

As closed λ-terms inhabit types that are isomorphic to tautologies in the implicational fragment of intuitionistic logic, closed λμ-terms inhabit types that are isomorphic to tautologies in the implicational fragment of classical logic. The primary example is the Pierce-type ((A → B) → A) → A which is inhabited by the λμ-term

λx^{(A→B)→A}.μa\overline{A}.[a](x λy^{A}.μb\overline{B}.[a]y)

but empty in the λ-calculus. (For better readability we have annotated the abstracted variables with their type.)

2.1 Reductions

In the simply-typed λ-calculus each normal term M has the subformula property: if x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ M : A then each subterm of M is an inhabitant of a type given by a subformula of A or A_{i} for some i. Each term M has a normal form which can be obtained by a finite number of β-reductions. The reduction relation is given by the compatible closure of the β-axiom.

(λx.M_{1})M_{2} ⟶_{β} [M_{2}/x]M_{1}

In the λμ-calculus, we ignore negation when determining subformulas, that is, \overline{A} is considered a subformula of A. Then we can define a reduction relation that computes normal forms which have the subformula property as in the λcalculus. Besides β-reduction we need permutative conversions induced by the following axiom:

(μa.N) M ⟶_{π} μb.[λ^{∘}z.[b](z M)/a]N

This involves a new kind of substitution [λ^{∘}z.[b](z M)/a]N, Parigot’s structural substitution, which has the following effect: In N, replace every subterm of the form [a]M′ by [b](M′ M) for any term M′. Our presentation of the structural substitution follows de Groote [dG98], who introduces internal extensions of the syntax:

M ::= x | λx.M | M M | μa.N  Terms
N ::= [C]M  Named terms
C ::= a | λ^{∘}z.N (z appears exactly once in N) Contexts

Structural substitution is generalized to a substitution of contexts [C/a]M. After a context is substituted for a μ-variable, appearances of λ^{∘} are eliminated silently by linear β-reductions:

[λ^{∘}z.N]M ⟶_{β^{∘}} [M/z]N.

The effect of the π-reduction is to uncover hidden β-redices; it is best explained in an example. Consider the following open term of type A:

y:A ⊢ (μa\overline{A→A}.[a]λx^{A}.x) y : A

Because it contains the subterm λx.x of type A → A, this term does not fulfill the subformula property. It is destroyed by a β-redex (λx.x) y which is separated by a μ-abstraction. This hidden redex can be uncovered by a permutation:

(μa\overline{A→A}.[a]λx^{A}.x) y ⟶_{π} μb\overline{A}.[λ^{∘}z^{A→A}.[b](z y)/a]([a]λx^{A}.x)
= μb\overline{A}.[λ^{∘}z^{A→A}.[b](z y)]λx^{A}.x
⟶_{β^{∘}} μb\overline{A}.[λx^{A}.x/z]([b](z y))
= μb\overline{A}.[b](λx^{A}.x) y
⟶_{β} μb\overline{A}.[b]y

Note that the ⟶_{β^{∘}}-reduction step counts as part of the structural substitution.

Finally, we introduce a third kind of reduction which is analogous to βreduction:

[a]μb.N ⟶_{μβ} [a/b]N

Parigot calls this reduction “renaming” of named terms. It requires a third kind of substitution—μ-variables for μ-variables—as Ong and Steward point out [OS97]. However, in our formulation it is just a special case of context substitution.

The reduction relation induced by the three axioms β, π and μβ is confluent. However, a straightforward adaption of the Tait and Martin-Löf parallel reduction method fails. This was overlooked in the original confluence proof [Par92], and only after years a correct proof was given by Baba, Hirokawa and Fujita [BHF01]. They found that in its straightforward definition parallel reduction does not have the diamond property. This is due to the twofold effect of πreduction: It may create a β-redex but at the same time disrupt a μβ-redex. For example,

\xymatrix{ & (μa.[a]μb.[a](λx.x)) y \ar[dr]^{π} \ar[dl]_{μβ} \\ (μa.[a](λx.x)) y \ar[dr]_{π} &  & μa.[a](μb.[a](λx.x) y) y \ar@{.>}[dl]^{?} \\  & μa.[a](λx.x) y}

The μβ-redex [a]μb... is hidden after the π-reduction step. Another π-reduction is required to restore it.

3 A Computational Interpretation

Since the pioneering work of Griffin [Gri90] it is known that control constructs for functional programming like call/cc or Felleisen’s C [FFKD87] can be typed by classical tautologies. Therefore we expect that the λμ-calculus can be interpreted operationally such that known control constructs can be encoded as λμ-terms. This is indeed the case—as demonstrated by Ong and Stewart [OS97] and Bierman [Bie98]. In the following we present Ong and Stewart’s call-by-value λμ-calculus, Bierman’s small step semantics and an encoding of de Groote’s exception handling calculus [dG95] into the λμ-calculus.

3.1 Call-by-Value λμ-Calculus

The λμ-calculus can be extended by datatypes, case-distinction and recursion to form the core of a programming language. This has been done by Ong and Stewart who named the resulting toy language μPCFv^{−}. We will stick to its core λμ_{v} which is the λμ-calculus with a call-by-value reduction strategy.

A value v is simply a λ-abstraction. We obtain a call-by-value strategy by adding two rules and restricting the β-axiom to values.

(λx.M) v ⟶_{β_{v}} [v/x]M
v (μa.N) ⟶_{π_{v}} μb.[λ^{∘}z.[b](v z)/a]N
μa.[a]M ⟶_{μη} M  (a ∉ μFV(M))

A deterministic evaluation strategy for λμ_{v} is given by the following small-step semantics.

3.2 A Small-Step Semantics

Bierman [Bie98] gives a simple call-by-value small-step semantics that sheds some light on the meaning of μ-abstraction and μ-application. Before we present it, we define redices and evaluation contexts with a single hole •:

E ::= • | E M | v E Evaluation context
R ::= v v | μa.N  Redex

Lemma 1 (Decomposition). Every λ-closed unnamed term M is either a value or can be uniquely decomposed into an evaluation context E[•] and a redex R such that M = E[R].

Furthermore, named terms N are always of the form [a]M. Hence, using an environment E which maps μ-variables into evaluation contexts, we can spell out the small-step semantics ⇒ by three axioms:

\begin{aligned}(E[(λx.M) v], & E) & ⇒ & (E[[v/x]M], & E) \\ (E[μa.N], & E) & ⇒ & (N, & E ⊎ \{a ↦ E[•]\}) \\ ([a]M, & E ⊎ \{a ↦ E[•]\}) & ⇒ & (E[M], & E ⊎ \{a ↦ E[•]\}) \end{aligned}

Note the invariant that the environment E binds all free μ-variables in M or N.

This semantics suggests that, in the same way as λ-variables are placeholder for terms, μ-variables stand for contexts or continuations. Binding a μ-variable a means saving the current context in a, and applying a to a term M means restoring the context denoted by a and continuing the evaluation of M in this context. This insight will be critical in finding the best higher-order representation later in this article.

3.3 de Groote’s Exception Handling Calculus

To demonstrate the capability of the λμ-calculus to model control we present an SML-like exception handling mechanism given by de Groote [dG95]. Exceptions are added to the λ-calculus via two constructs: one that declares a new exception and provides a handler for it; another one that raises the exception. They are typed as follows:

e : \overline{A} ; \begin{matrix}· \\ · \\ · \end{matrix} ; M : B  x : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; M_{e} : B

\overline{Handle}

(exception e in M handle e(x).M_{e}) : B

e : \overline{A} M : A

\overline{Raise}

raise e(M) : B

We sketch the desired computational behavior by two examples:

exception e in E[raise e(v)] handle e(x).M_{e} ⇝ [v/x]M_{e}
exception e in v handle e(x).M_{e}  ⇝ v

Bierman gives the following translation of the two constructs into λμ-terms. Note that the encoding of raise introduces a β-redex to ensure call-by-value evaluation.

⌜raise e(M)⌝  = (λy.μ .[e]y) ⌜M⌝
⌜exception e in M handle e(x).M_{e}⌝ = μa.[a](λx.⌜M_{e}⌝) (μe.[a]⌜M⌝)

The reader is invited to convince himself that this translation has the stipulated evaluation behavior, e.g. by verifying that

(⌜exception e in raise e(v) handle e(x).x⌝ , E) ⇒^{∗} (v, E′).

Assuming the reader has gained some familiarity with the λμ-calculus by now, in the next section we shall proceed by discussing its formal representation in a reasoning framework.

4 A Third-Order Representation

Formal reasoning about logics and programming languages, in the following called object theories, must take place in a framework, the meta theory. A possible choice for such a logical framework is predicate logic: first-order terms, made up from function symbols and variables, encode the syntactic entities of the object theory, and predicates represent properties of these entities, for example the wellformedness of a formula or the validity of a proof. However, reasoning about languages with binders in a first-order representation is a tedious business and requires numerous technical lemmata concerning variable renaming, substitution etc. (see e.g. [Sha88], [Alt93]). More suitable is a logical framework with a higher-order term language which has binders itself. Then object variables can be encoded by meta variables and substitution in the object theory can be expressed by substitution in the logical framework.

The primary candidate for a higher-order logical framework is the simplytyped λ-calculus λ^{→} with βη-equality, in which object languages with binders can be encoded in a direct way. For example, the untyped λ-calculus can be represented by the following signature.

Base types tm  Terms
Constants  lam : (tm → tm) → tm Abstraction
app : tm → tm → tm  Application

The representation function ⌜·⌝ maps any untyped λ-term M into a term t of the logical framework. It is defined by recursion over M as follows:

⌜x⌝  = x
⌜λx.M⌝ = lam λx:tm. ⌜M⌝
⌜M_{1} M_{2}⌝ = app ⌜M_{1}⌝ ⌜M_{2}⌝

The given representation is adequate, that is, there exists a one-to-one correspondence between untyped λ-terms and their canonical representation in the logical framework.

Theorem 1 (Adequacy). Let Γ = x_{1} :tm, …, x_{n}:tm be a context. Then

1. for every untyped λ-term M with free variables in {x_{1}, …, x_{n}} it holds that Γ ⊢ ⌜M⌝ : tm,

2. for every canonical (i.e. β-normal η-long) term t with Γ ⊢ t : tm there exists an untyped λ-term M s.th. ⌜M⌝ = t, and

3. the representation function is compositional in the sense that ⌜[M_{1}/x]M_{2}⌝ = [⌜M_{1}⌝ /x] ⌜M_{2}⌝.

Proof. By induction on (1.) M, (2.) t canonical, and (3.) M_{2}. The cases for abstraction λx … refer to the induction hypothesis with an extended context (Γ, x:tm).

We observe these benefits of representing the untyped λ-calculus in a higherorder logical framework like λ^{→}: (i) α-equivalent object terms M_{1} and M_{2} translate into equivalent terms of the logical framework and, (ii) substitution does not have to be implemented. More on logical frameworks can be found in [Pfe01b].

4.1 Untyped λμ-Calculus

The untyped λμ-calculus extends the untyped λ-calculus by μ-abstraction and μ-application. How shall we represent the new binder? Let us analyse the general structure of a binder bind:

bind : (ρ → σ) → τ

The binder bind generates an expression of type τ from a context of type σ with a free variable of type ρ. We know that the binder μ takes a named term N with a free μ-variable a and returns a term. Thus we add the following constants to our signature.

Base type nam  Named terms
Constant  mu : (ρ → nam) → tm μ-abstraction

In this signature ρ has to be replaced by the type of the variables that are bound by mu. In the case of lam we had ρ = tm since λ-variables just stand for terms. The crucial question is: “What do μ-variables stand for?” The small-step semantics suggested that they are placeholder for evaluation contexts. This is confirmed by the nature of the structural substitution which replaces contexts with contexts. We make use of the fact that contexts can be represented directly in λ^{→} as functions from terms to terms and set ρ = tm → nam. Hence, the type of the constant mu is third-order:

mu : ((tm → nam) → nam) → tm

Surprisingly, we do not have to add a constant for μ-application; it is represented by application in λ^{→}. The translation function for λμ-terms M, N and contexts C is an extension of ⌜·⌝ by the following definitions:

⌜μa.N⌝ = mu λa:tm → nam. ⌜N⌝ : tm
⌜[C]M⌝ =  ⌜C⌝ ⌜M⌝ : nam
⌜a⌝ = a : tm → nam
⌜λ^{∘}z.N⌝ =  λz:tm. ⌜N⌝ : tm → nam

Theorem 2 (Adequacy). Let Γ = x_{1} : tm, …, x_{n}: tm, a_{1} : tm → nam, …, a_{m}: tm → nam. Additionally to an adaption of Thm. 1 for λμ it holds that

4. for every named term N with free variables in Γ it holds that Γ ⊢ ⌜N⌝ : nam,

5. for every canonical term s with Γ ⊢ s : nam there exists a named term N s.th. ⌜N⌝ = s,

6. for every (not necessarily linear) context C with free variables in Γ it holds that Γ ⊢ ⌜C⌝ : tm → nam,

7. for every canonical term r with Γ ⊢ r : tm → nam there exists a (not necessarily linear) context C s.th. ⌜C⌝ = r, and,

8. the representation is compositional for context substitution, that is,

⌜[C/a]M⌝ = [⌜C⌝ /a] ⌜M⌝ .

Proof. We prove 1., 4. and 6. simultaneously by induction on M/N/C, 2., 5. and 7. by induction on the canonical forms of tm, nam and tm → nam, and 8. by induction on M.

Note that we only represented general contexts adequately, not linear contexts C. However, all contexts we de facto write down in the encoding of reduction rules and small-step semantics will actually be of the required form. In the given encoding the structural substitution, which looks complicated in the literature (e.g. [OS97]), is just λ^{→}-substitution for μ-variables (see 8.). For example,

⌜[λ^{∘}z.[b](z y)/a]([a]x)⌝ = ⌜[b](xy)⌝ = b (app x y) = (λz:tm .b (app z y)) x

= [λz:tm .b (app z y)/a](a x) = [⌜λ^{∘}z.[b](z y)⌝ /a] ⌜[a]x⌝ .

Well-typed terms:

ty  : type  Types
tm  : ty → type  Typed terms
nam : type  Named terms
i  : ty  Base type
⇒  : ty → ty → ty  Function space
lam : (tm A → tm B) → tm(A ⇒ B)  λ-abstraction
app : tm(A ⇒ B) → tm A → tm B  Application
mu : ((tm A → nam) → nam) → tm A  μ-abstraction

Reduction:

⟶ : tm A → tm A → type  Red. for typed terms
⟶_{n} : nam → nam → type  Red. for named terms
⟶_{β} : ΠM:tm A → tm B. ΠN:tm A.
app (lam M) N ⟶ M N  β-axiom
⟶_{π} : ΠM:(tm(A ⇒ B) → nam) → nam. ΠN:tm A.

app (mu M) N ⟶ mu λa:tm B → nam.

M (λz:tm(A ⇒ B).a (app z N))  π-axiom
⟶_{lam}, ⟶_{app1}, ⟶_{app2} : …  lam- and app-congruences

(i) Direct representation (not adequate):

⟶_{μβ} : Πa:tm A → nam. ΠM:(tm A → nam) → nam.
a (mu M) ⟶_{n} M a  μβ-axiom
⟶_{nam} : Πa:tm A → nam. M ⟶ M′
→ a M ⟶_{n} a M′  nam-congruence
⟶_{mu} : (Πa:tm A → nam. N a ⟶_{n} N′a)
→ mu N ⟶ mu N′  mu-congruence

(ii) Representation with local rules (adequate):

⟶_{mu} : (Πa:tm A → nam.

Π⟶_{μβ} : (ΠM:(tm A → nam) → nam. a (mu M) ⟶_{n} M a). Π⟶_{nam} : (ΠM, M′:tm A. M ⟶ M′ → a M ⟶_{n} a M′). → N a ⟶_{n} N′a)

→ mu N ⟶ mu N′  mu-congruence

Table 1. The Signature Σ^{3rd}: Well-Typed Terms and Reduction.

4.2 Typed λμ-calculus

Table 1 lists the signature Σ^{3rd} which encodes the well-typed λμ-terms in the dependently typed λ-calculus λ^{Π}—the core of logical frameworks like LF [HHP93]. To represent terms of type A we instantiate the type family tm : ty → type to tm A. Note that in the constant declarations A and B are considered to be implicitly quantified. For example, the full type of the constant lam would be ΠA:ty.ΠB:ty.(tm A → tm B) → tm(A ⇒ B).

Reduction is represented by a pair of type families, ⟶ and ⟶_{n}. In part (i), the representation of the two rules ⟶_{μβ} and ⟶_{nam} is not adequate yet, since context C could be instantiated for a, but only μ-variables should be allowed. This problem can be circumvented by removing these rules and making them local: Whenever a new parameter a:tm A → nam is introduced, add these rules dynamically for this specific a. The only rule that introduces such parameters is ⟶_{mu}; we replace it by the version in part (ii). Adequacy of our representation can be stated and proven in a similar way to Thm. 2.

4.3 Small-Step Semantics

In the following we will refine and encode the small-step semantics (M, E) ⇒ (M′, E′) given in Sect. 3.2. The original formulation has a little flaw: during the process of evaluation the environment E grows monotonically and accumulates contexts that will never be used again. We give a modification that uses substitution instead of environments and includes the decomposition of the subject M into evaluation context C and redex R. The μ-constant eval denotes the top level evaluation context.

Values  val : tm A → type
v ::= λx.M  vlam : ΠM:tm A → tm B. val (lam M)

Evaluation Contexts

C ::= λ^{∘}z.[eval]z  eval : tm A → nam
| λ^{∘}z.[C](z M)  λz. ⌜C⌝ (app z ⌜M⌝)
| λ^{∘}z.[C](v z)  λz. ⌜C⌝ (app ⌜v⌝ z)

Again not each inhabitant of tm A → nam stands for a valid evaluation context. However, a judgment ecxt : (tm A → nam) → type which singles out the evaluation contexts can be defined easily.

The small-step semantics can be defined by the four rules given below. Formally, it maps one named term into another. We say a term M evaluates to a value v iff [eval]M ⇒^{∗} [eval]v.

⇒_{β} [C]((λx.M) v) ⇒ [C]([v/x]M)  ⇒_{μβ} [C](μa.N) ⇒ [C/a]N

⇒_{appl} {[λ^{∘}z.[C](z M_{2})]M_{1} ⇒ N \atop [C](M_{1} M_{2}) ⇒ N}  ⇒_{appr} {[λ^{∘}z.[C](v z)]M ⇒ N \atop [C](v M) ⇒ N}

On the left hand side of ⇒ an occurrence of [C]M is to be read as “term M in context C” but on the right hand side it is just the named term [C]M. After each step we decompose the reduct N afresh into [eval]M. This is possible since the following invariant holds: If C and M are closed and [C]M ⇒ N, then N = [eval]M′ for a closed term M′. Obviously it holds for the rules ⇒_{β}, ⇒_{appl} and ⇒_{appr}. To justify it for the rule ⇒_{μβ} we first notice that the right hand side [C/a]N is a closed named term. Hence, it must be equal to [c]M′ for some μ-constant c, which can only be eval.

The representation of “⇒” maps a context-term pair C M into another context-term pair C′ M′. The decomposition of a named term into context and term we did silently in the informal treatment is performed by the auxiliary judgment “⇒_{n}”.

⇒ : (tm A → nam) → tm A → (tm A′ → nam) → tm A′ → type
⇒_{n} : nam → (tm A′ → nam) → tm A′ → type
⇒_{eval} : ΠM:tm A′. (eval M) ⇒_{n} eval M

The four computation rules for “⇒” are given in the following. Note that “⇒” is written infix and appears after two of its arguments.

⇒_{β} : ΠC:tm B → nam. ΠM:tm A → tm B. ΠV :tm A. val V →
(C (M V)) ⇒_{n} C′ M′ → C (app (lam M) V) ⇒ C′ M′
⇒_{μβ} : ΠN:(tm A → nam) → nam. ΠC:tm A → nam.
(NC) ⇒_{n} C′ M′ → C (mu N) ⇒ C′ M′
⇒_{appl} : (λz.C(app z M_{2})) M_{1} ⇒ C′ M′
→ C (app M_{1} M_{2}) ⇒ C′ M′
⇒_{appr} : (λz.C(app V z)) M ⇒ C′ M′ → val V
→ C (app V M) ⇒ C′ M′

5 A Second-Order Representation

Even though we managed to show that the third-order representation of the λμ-calculus is elegant and adequate, it is not without pitfalls: As we have seen in Sect. 4.2, the direct representation of the reduction relation is not adequate; the rules for named terms have to be locally introduced for a new parameter a: tm T → nam. This works for ordinary reduction, but cannot be applied to a representation of parallel reduction. Consider the rule ⟹_{μβ}:

⟹_{μβ} : Πa:tm T → nam. (Πb:tm T → nam.M b ⟹_{n} M′b)
→ a(mu λb.M b) ⟹_{n} M′ a

An application of this rule has the following effect: [a]μb.M is reduced by the μβrule, and additional reductions may occur within M. The hypothesis introduces a new parameter b since we step under the binder μ. To make this rule local, it has to be added for each μ-variable that is introduced as a parameter and

Adequacy of the second-order representation of λμ-terms:

\xymatrix{Calc. & λμ \ar[d]_{⌜·⌝}^{≅} \ar@{=>}[r]^{≅} \ar@{.>}[dr]_{⌜·⌝}^{≅} & Cont_{can} \ar[d]_{⌜·⌝}^{≅} \ar[r]_{⊆} & Cont \ar[d]_{⌜·⌝}^{≅} \ar[l]_{≪} \\ Rep. & λ^{Π} + Σ^{3rd} \ar@{=>}[r]^{≅} & (λ^{Π} + Σ^{2nd})/≫ \ar@{.>}[r]_{⊆} & λ^{Π} + Σ^{2nd} \ar@{.>}[l]_{≪}}

Adequacy of the second-order representation of reduction ⟶ (Bisimulation):

\xymatrix{λμ & Cont_{can} & Cont \\ L \ar@{=>}[r]^{≅} \ar[dd] & H \ar[dd] \ar@{.>}[dr] \\  &  & H^{0} \ar@{.>}[dl]_{≪} \\ L′ \ar@{=>}[r]^{≅} & H′}

Fig. 1. Overview: Adequacy of the Second-Order Representation

therefore also for b. Thus, ⟹_{μβ} has to be inserted into itself. This leads to an infinite chain of local rules and cannot be implemented.

These problems do not occur with a second-order representation, which we present in this section. We define the representation function indirectly and also prove adequacy indirectly as outlined in Fig. 1. First, we define the calculus of continuations Cont, a modification of the λμ-calculus which allows general continuation terms K in a μ-application, now called throw K E. In principle, we make λ^{∘} an explicit constructor klam and do not treat ⟶_{β^{∘}} silently any more. Furthermore, in the representation Σ^{2nd} we add a base type cont for continuations. Then, we define the canonical expressions H ∈ Cont_{can} as those which only contain continuation variables, that is, no klam. Every expression H ∈ Cont can be made canonical by applying normalization H ≫ H′.

For the three representations of these calculi we can show adequacy in a straightforward manner. Hence, in each case a one-to-one correspondence exists, and we can restrict ourselves to reason about the original calculi to obtain analogous results for their representations. Particularly, if we construct a bijection between λμ and Cont_{can}, we implicitly define an adequate second-order representation of λμ.

As a second part, we define reduction in Cont_{can} and prove that it is the second-order representation of the reduction in λμ. It is sufficient to show bisimulation of reduction in λμ (L ⟶ L′) and reduction in Cont_{can} (H ⟶ H′) as sketched in Fig. 1. The only case where we have to be careful is H ⟶_{π} H′ because applying structural substitution on H temporarily creates a non-canonical expression H^{0} on which we have to apply normalization. Thus, we incorporate normalization into π-reduction.

In the following we will sketch the proof of adequacy of the second-order representation of λμ. The whole proof has been carried out in Twelf [PS98] and is available electronically [Abe01]. We consider it as a case study for formal reasoning about a system by a third-order representation. To my knowledge, this is the first formal proof in a representation of order strictly greater than two. This may be because cases are rare where third- or higher-order representations can be applied.

Raw expressions:

E ::= x | λx.E | E E | catch k.F Expressions
F ::= throw K E  Responses
K ::= k | klam x.F  Continuations
H ::= E | F | K  Any Cont-term

Typing:

k : \overline{A} ; \begin{matrix}· \\ · \\ · \end{matrix} ; F : − ; catch k.F : A  {K : \overline{A}  E : A \atop throw K E : −}  x : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; F : − ; klam x.F : \overline{A}

Signature Σ^{2nd}:

exp : ty → type
resp : type
cont : ty → type
lm : (exp A → exp B) → exp(A ⇒ B)
ap : exp(A ⇒ B) → exp A → exp B
catch : (cont A → resp) → exp A
throw : cont A → exp A → resp
klam : (exp A → resp) → cont A

Canonical raw expressions can H:

can x ; \begin{matrix}· \\ · \\ · \end{matrix} ; can E ; can λx.E

can E_{1} can E_{2}

can E_{1} E_{2} can K can E can throw K E

can k ; \begin{matrix}· \\ · \\ · \end{matrix} ; can F

can catch k.F

Normalization H ≫ H′:

[E/x]F ≫ F′ throw (klam x.F) E ≫ F′

x ≫ y ; \begin{matrix}· \\ · \\ · \end{matrix} ; E ≫ E′ ; λx.E ≫ λy.E′ {E_{1} ≫ E′_{1} E_{2} ≫ E′_{2} \atop E_{1} E_{2} ≫ E′_{1} E′_{2}}

K ≫ K′ E ≫ E′ throw K E ≫ throw K′ E′

k ≫ l ; \begin{matrix}· \\ · \\ · \end{matrix} ; F ≫ F′

catch k.F ≫ catch l.F′

Translation L = ; = ; > ; = H from λμ into Cont_{can}:

x = ; = ; > ; = y ; \begin{matrix}· \\ · \\ · \end{matrix} ; M = ; = ; > ; = E ; λx.M = ; = ; > ; = λy.E  {M_{1} = ; = ; > ; = E_{1}  M_{2} = ; = ; > ; = E_{2} \atop M_{1} M_{2} = ; = ; > ; = E_{1} E_{2}} ; {a = ; = ; > ; = K  M = ; = ; > ; = E \atop [a]M = ; = ; > ; = throw K E}  a = ; = ; > ; = k ; \begin{matrix}· \\ · \\ · \end{matrix} ; N = ; = ; > ; = F ; μa.N = ; = ; > ; = catch k.F

Reductions H ⟶ H′ in Cont_{can}:

(λx.E_{1})E_{2}  ⟶_{β} [E_{2}/x]E_{1}
throw k (catch l.F) ⟶_{μβ} [k/l]F

[klam z.throw l (z E)/k]F ≫ F′ (catch k.F)E ⟶_{π} catch l.F′

Table 2. Calculus of Continuations Cont and Canonical Fragment Cont_{can}

5.1 The Calculus of Continuations Cont

Table 2 defines expressions, continuations and responses (name due to Streicher and Reus [SR98]) of Cont all of which we will refer to as raw expressions H.

Canonical raw expressions H are those which do not contain a klam. The judgment can H is established by recursion on H; there are congruence rules for all constructs except klam. Cont_{can} is the quotient of Cont w.r.t. the equality induced by the axiom throw (klam x.F) E = [E/x]F. We obtain the canonical representative H′ of a Cont-term H by applying the big-step call-by-name normalization procedure H ≫ H′.

Lemma 2 (Properties of ≫).

1. If H_{1} ≫ H_{2} then can H_{2}.

2. If H_{1} ≫ H_{2} and can H then [H/x]H_{1} ≫ [H/x]H_{2}.

Proof (of both assertions). By induction on H_{1} ≫ H_{2}. ⊓ ⊔

5.2 Bisimulation

The relation L = ; = ; > ; = H constitutes a bijective translation between terms of the λμ-calculus L and Cont_{can}-expressions H. The following rectangle theorem (cf. Fig. 1) states that λμ-reductions can be simulated by Cont_{can}-reductions.

Theorem 3 (Simulation). If L = ; = ; > ; = H and L ⟶ L′ then L′ = ; = ; > ; = H′ and H ⟶ H′ for some H′.

Proof. By induction on L ⟶ L′. The only difficult case is ⟶_{π} for which we need Lemma 3. ⊓ ⊔

Lemma 3 (Substitution). If

a = ; = ; > ; = k ; \begin{matrix}· \\ · \\ · \end{matrix} ; L = ; = ; > ; = H  and  x = ; = ; > ; = z ≪ y ; \begin{matrix}· \\ · \\ · \end{matrix} ; C = ; = ; > ; = D′ ≪ D

then

[λ^{∘}x.C/a]L = ; = ; > ; = H′ ≪ [klam y.D/k]H

Proof. By induction on L. We spell out the hard case L = [a]M.

[a]M = ; = ; > ; = throw k E  by ass. and def. of = ; = ; > ; =
M = ; = ; > ; = E  by inversion
[λ^{∘}x.C/a]M = ; = ; > ; = E′  by induction hypothesis
[λ^{∘}x.C/a]([a]M) = [[λ^{∘}x.C/a]M/x]C = ; = ; > ; = [E′/z]D′  by assumption
E′ ≪ [klam y.D/k]E  by induction hypothesis
[E′/z]D′ ≪ [[klam y.D/k]E/y]D  by assumption
[E′/z]D′ ≪ throw (klam y.D) ([klam y.D/k]E)  by def. of ≫
= [klam y.D/k](throw k E)  ⊓ ⊔

Note that the proof makes use of substitution of deductions. For example, we show [[λ^{∘}x.C/a]M/x]C = ; = ; > ; = [E′/z]D′ by instantiating the deduction x = ; = ; > ; = z of

the assumption C = ; = ; > ; = D′ with [λ^{∘}x.C/a]M = ; = ; > ; = E′.

Analogously, it can be shown that the reduction in Cont_{can} simulates the reduction in the λμ-calculus which gives us bisimulation.

6 Conclusion

We have presented the λμ-calculus with an application and discussed two different encodings. The third-order representation seems to fit the λμ-calculus best since all three kinds of substitutions are reduced to substitution of the logical framework. Furthermore, we could formalize the small-step semantics economically. However, a direct representation of parallel reduction fails. The second-order representation is unaffected by these problems but requires auxiliary notions like canonical term and normalization which blow up the proofs considerably in practice.

Two further directions of research open up from here: On the side of the third-order representation, alternative formulations of parallel reduction have to be investigated. A concrete idea is to introduce an auxiliary judgment “C is a μ-variable” which makes the localizations of rules superfluous.

To improve support of the second-order representation, the logical framework could be extended to allow type refinement. The type of canonical expressions would be a refinement (a subtype) of the type of expressions. The fact whether a term H is canonical could be decided and the proof of can H would be irrelevant and could be hidden. The theoretical foundations for such an extension of the logical framework have been laid by Pfenning [Pfe01a].

The third-order representation can be used to prove many properties of the λμ-calculus. For a start, I have formally shown soundness of the big-step semantics given by Ong and Stewart [OS97] wrt. to an evaluation-frames-stack small-step semantics. I expect more applications of the encoding in the future.

Acknowledgments. It was Ralph Matthes who first interested me in the λμcalculus. Frank Pfenning and Brigitte Pientka deserve my gratitude for many discussions and ideas. For comments on the draft I thank Ralph, Frank and the two anonymous referees. Last but not least, I thank the Creator for the framework in which human life and thinking can take place.

References

[Abe01] Andreas Abel. A third-order representation of the λμ-calculus. Twelf code, available under http://www.cs.cmu.edu/˜ abel/merlin01.tar.gz, 2001.

[Alt93] Thorsten Altenkirch. A formalization of the strong normalization proof for System F in LEGO. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, TLCA’93, volume 664 of Lecture Notes in Computer Science, pages 13–28. Springer-Verlag, 1993.

[BHF01] Kensuke Baba, Sachio Hirokawa, and Ken-etsu Fujita. Parallel reduction in type free λμ-calculus. In Proceedings of CATS 2001 (Computing: the Australasian Theory Symposium), volume 42 of Electronic Notes in Theoretical Computer Science. Elsevier Science B. V., 2001. Also appeared as Technical Report DOI-TR-177, Kyushu University, Fukuoka, Japan.

[Bie98] Gavin M. Bierman. A computational interpretation of the λμ-calculus. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lecture Notes in Computer Science, pages 336–345, Brno, Czech Republic, August 1998.

[dG95] Philippe de Groote. A simple calculus of exception handling. In M. Dezani and G. Plotkin, editors, Second International Conference on Typed Lambda Calculi and Applications, TLCA’95, volume 902 of Lecture Notes in Computer Science, pages 201–215. Springer, 1995.

[dG98] Philippe de Groote. An environment machine for the λμ-calculus. To appear in MSCS, 1998.

[FFKD87] Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker, and Bruce F. Duba. A syntactic theory of sequential control. Theoretical Computer Science, 52:205–237, 1987.

[Gri90] Timothy G. Griffin. A formulæ-as-types notion of control. In Proceedings of the Seventeenth ACM/SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM Press, January 1990.

[HHP93] Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. Journal of the Association of Computing Machinery, 40(1):143– 184, January 1993.

[OS97] C.-H. L. Ong and C. A. Stewart. A Curry-Howard foundation for functional computation with control. In Proceedings of ACM SIGPLAN-SIGACT Symposium on Principle of Programming Languages, pages 215–227, Paris, Januar 1997. ACM Press.

[Par92] M. Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Logic Programming and Automated Reasoning: Proc. of the International Conference LPAR’92, pages 190–201. Springer, Berlin, Heidelberg, 1992.

[Pfe01a] Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In LICS 2001: IEEE Symposium on Logic in Computer Science, June 2001.

[Pfe01b] Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers B.V. and MIT Press, 2001. In preparation. Draft available from http://www.cs.cmu.edu/˜ fp.

[PS98] Frank Pfenning and Carsten Schürmann. Twelf user’s guide. Technical report, Carnegie Mellon University, 1998.

[Sha88] Natarajan Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475–522, July 1988.

[SR98] Thomas Streicher and Bernhard Reus. Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6):543– 572, 1998.