BRICS

Basic Research in Computer Science

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

Kristian Støvring

BRICS Report Series RS-06-5 ISSN 0909-0878 March 2006 BRICS RS-06-5 K. Støvring: Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative Copyright \begin{matrix}c \\ ◯ \end{matrix} 2006, Kristian Støvring.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/06/5/

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative^{∗}

Kristian Støvring

BRICS ^{†}

Department of Computer Science University of Aarhus ^{‡}

March 1, 2006

Abstract

We answer Klop and de Vrijer’s question whether adding surjectivepairing axioms to the extensional lambda calculus yields a conservative extension. The answer is positive. As a byproduct we obtain a “syntactic” proof that the extensional lambda calculus with surjective pairing is consistent.

∗To appear in Logical Methods in Computer Science.

† Basic Research in Computer Science (www.brics.dk), funded by the Danish National Research Foundation.

‡ IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark E-mail: kss@brics.dk

1 Introduction

The theory λ_{βηSP} is obtained from the untyped extensional lambda calculus λ_{βη} [2] by adding three surjective-pairing axioms:

\begin{aligned}(π_{1}) & π_{1} ⟨M, N⟩ & = & M \\ (π_{2}) & π_{2} ⟨M, N⟩ & = & N \\ (sp) & ⟨π_{1} M, π_{2} M⟩ & = & M \end{aligned}

These axioms are said to define a surjective pairing since the axiom (sp) implies that every term is equal to a pair.

A λ-term is called pure if it does not contain any of the new constructs π_{i} and ⟨·, ·⟩. In this article we give a positive answer to the following question, asked by Klop and de Vrijer in 1989 [10, 23] and featured as Problem 5 in the original RTA list of open problems [6]:

Suppose that M and N are pure λ-terms. Does M =_{βηSP} N imply that M =_{βη} N?

In other words, we show that the theory λ_{βηSP} is a conservative extension of the theory λ_{βη}. As a byproduct we obtain a proof of consistency of λ_{βηSP} that uses purely syntactic methods.^{1}

1.1 Background of the problem

The two perhaps most obvious attempts at showing conservativity of λ_{βηSP} fail because of two negative results: no surjective-pairing function (that is, no pairing function satisfying the three axioms above) is definable in the lambda calculus [1], and the standard reduction relation for the lambda calculus with surjective pairing is not confluent [9]. Both results were shown for the extensional lambda calculus as well.

Klop [9] and Klop and de Vrijer [10] have considered a number of properties of the (non-extensional) lambda calculus with surjective pairing, λ_{βSP}, which would have trivially followed from confluence of the standard reduction relation. In particular, de Vrijer has shown that λ_{βSP} is a conservative extension of the lambda calculus [23]. This result motivated the question answered here: whether surjective pairing also conservatively extends the extensional lambda calculus.

The proof of conservativity by de Vrijer is furthermore the first known “syntactic” consistency proof for λ_{βSP}. One of Scott’s model-theoretic consistency proofs for λ_{βη} [20] can be easily adapted to show consistency of λ_{βηSP} (and hence also λ_{βSP}) as well.

The theory λ_{βηSP} has also been investigated from a categorical point of view. If C is a cartesian closed category with an object U such that

U ≅ U × U ≅ U → U,

then there are various ways of interpreting λ-terms as morphisms of C [2, 11]. Moreover, every extension of the theory λ_{βηSP} is the theory of a model arising in this way [11, 21].

1The author only knows of one other such “syntactic” consistency proof for λ_{βηSP} , namely one based on recent work on operationally defined bisimulations [12].

1.2 Formalization

The author has formalized and verified the proof of the conservativity result using the Twelf system [16]. The formalized proof additionally serves as an implementation of a procedure transforming a formal derivation of M =_{βηSP} N into a formal derivation of M =_{βη} N (for pure terms M and N). It is available from

                http://www.brics.dk/RS/06/5/Proof/

The formalized statement of the main result is presented in Appendix A.

2 Background and notation

The reader is assumed to be familiar with basic properties of the untyped lambda calculus, as presented for example in the first three chapters of Barendregt’s book [2].

The syntax of λ-terms is extended with constructs for pairing and projection:

M ::= x | λx.M | M M | ⟨M, M⟩ | π_{1} M | π_{2} M

(where x ranges over an infinite set of variables). The pure terms are the usual λ-terms, i.e., terms with no occurrences of π_{i} or ⟨·, ·⟩. The set of free variables of a term M is denoted FV(M). We follow practice and identify α-equivalent terms.

We use the following notation and definitions for relations on λ-terms: For any binary relation ▷_{R} on λ-terms, ⟶_{R} denotes the compatible closure of ▷_{R} as defined in Figure 1. The relation ⟶_{R} is called a reduction relation. The reflexive–transitive closure of ⟶_{R} is written ⟶_{R}^{∗}, and the reflexive-transitive-symmetric closure of ⟶_{R} is written =_{R}. We write λ_{R} for the equational theory of λ-terms corresponding to =_{R}, i.e., λ_{R} is the set of formal equations “M = N” such that M =_{R} N.

\begin{matrix}\begin{matrix}M ▷_{R} M′ \\ M ⟶_{R} M′ \end{matrix} & \begin{matrix}M ⟶_{R} M′ \\ λx.M ⟶_{R} λx.M′ \end{matrix} \\ \begin{matrix}M ⟶_{R} M′ \\ M N ⟶_{R} M′ N \end{matrix} & \begin{matrix}N ⟶_{R} N′ \\ M N ⟶_{R} M N′ \end{matrix} \\ \begin{matrix}M ⟶_{R} M′ \\ ⟨M, N⟩ ⟶_{R} ⟨M′, N⟩ \end{matrix} & \begin{matrix}N ⟶_{R} N′ \\ ⟨M, N⟩ ⟶_{R} ⟨M, N′⟩ \end{matrix} \\ \begin{matrix}M ⟶_{R} M′ \\ π_{1} M ⟶_{R} π_{1} M′ \end{matrix} & \begin{matrix}M ⟶_{R} M′ \\ π_{2} M ⟶_{R} π_{2} M′ \end{matrix} \end{matrix}

Figure 1: The compatible closure of ▷_{R}.

The relation ▷_{βηSP} is defined by the axioms in Figure 2. This relation generates a reduction relation ⟶_{βηSP} and an equality relation =_{βηSP}. The extensional lambda calculus with surjective pairing is defined as the theory λ_{βηSP}.

(β)  (λx.M) N ▷_{βηSP} M[x := N]
(η) λx.M x ▷_{βηSP} M (if x ∉ FV(M))
(π_{1})  π_{1} ⟨M, N⟩ ▷_{βηSP} M
(π_{2})  π_{2} ⟨M, N⟩ ▷_{βηSP} N
(sp) ⟨π_{1} M, π_{2} M⟩ ▷_{βηSP} M

Figure 2: The relation ▷_{βηSP}.

3 Overview of the proof

The relation ⟶_{βηSP} is the standard reduction relation generating =_{βηSP}. This reduction relation is, however, not confluent [5] [9, p. 216]; its confluence would immediately imply the main result, namely that λ_{βηSP} is conservative over λ_{βη}.^{2} In this article we instead consider a further extension λ_{FP} of λ_{βηSP} and show that λ_{FP} is conservative over λ_{βη}. Since λ_{FP} is an extension of λ_{βηSP}, the main result follows. The proof is structured in the following way:

• In Section 4 we present the extension λ_{FP} of λ_{βηSP} and show that it is generated by a confluent reduction relation ⟶_{FP}. In the relation ⟶_{FP} the orientation of the axioms (η) and (sp) is reversed; in other words, the extensionality axioms are oriented as expansion axioms (see, e.g., the work by Jay and Ghani [8]).

• In Section 5 we show that λ_{FP} is conservative over λ_{βη} on pure λ-terms. This result does not immediately follow from confluence of ⟶_{FP} since ⟶_{FP} contains (sp) oriented as an expansion axiom.

4 An extension of the theory λ_{βηSP}

We first present the extension λ_{FP} of λ_{βηSP}; the name fp is intended to be a mnemonic for “functional pairing”. The relation ▷_{FP} is defined by the axioms in Figure 3. This relation generates the theory λ_{FP} and the reduction relation ⟶_{FP}. For convenience, we refer to the axioms (δπ), (π_{1}λ), and (π_{2}λ) as the commutation axioms; intuitively, these axioms express how a function behaves as a pair and vice versa. As discussed above, the axioms (\overline{η}) and (\overline{sp}) are oriented as expansion axioms.

2The non-confluent reduction relation considered by Klop [9] is slightly different from ⟶_{βηSP} . It is simple to construct a counter-example to confluence similar to Klop’s.

The theory λ_{FP} it not new, although is does not appear to have been explicitly named before. Axioms similar to the commutation axioms (δπ), (π_{1}λ), and (π_{2}λ) were first considered in work on products and lists in the lambda calculus [18] and in work on categorical combinators [19]: adding the surjectivepairing axiom (sp) to Révész’s theory λ_{p} gives the theory λ_{FP}, except for a minor syntactic difference. Durfee gave a model for the full theory λ_{FP} [7] (see the remark below). Axioms equivalent to the commutation axioms play an indirect, but important, role in recent work on solvability for λ-terms with pairs [12].

The reduction relation ⟶_{FP} (with its combination of commutation axioms and expansion axioms) appears to be new.

(β) (λx.M) N ▷_{FP} M[x := N]
(\overline{η}) M ▷_{FP} λx.M x (if x ∉ FV(M))
(π_{1}) π_{1} ⟨M, N⟩ ▷_{FP} M
(π_{2}) π_{2} ⟨M, N⟩ ▷_{FP} N
(\overline{sp})  M ▷_{FP} ⟨π_{1} M, π_{2} M⟩
(δπ) ⟨M, N⟩ P ▷_{FP} ⟨M P , N P ⟩
(π_{1}λ) π_{1} (λx.M) ▷_{FP} λx.π_{1} M
(π_{2}λ) π_{2} (λx.M) ▷_{FP} λx.π_{2} M

Figure 3: The relation ▷_{FP}.

Remark. In this article, the theory λ_{FP} and the associated reduction relation ⟶_{FP} are used to prove a specific result about a different theory. However, λ_{FP} and ⟶_{FP} can be justified semantically and syntactically:

• From the point of view of semantics: The original model of λ_{βηSP} [11, 20] is also a model of λ_{FP} [7]. Indeed, let U and V be complete partial orders such that V ≅ V × V and U ≅ [U → V]. Then by calculations valid in any cartesian closed category [20], U ≅ U × U ≅ [U → U], and one can verify that the standard interpretation^{3} of λ-terms as elements of U gives rise to a model of λ_{FP}. As an aside, if U is an arbitrary complete partial order satisfying that U ≅ U × U ≅ [U → U], then the standard interpretation using these isomorphisms makes U a model of (at least) λ_{βηSP}. Taking U = V in the above construction now gives an alternative pair of isomorphisms, and hence an alternative interpretation of λ-terms, resulting in a model of λ_{FP}.

• From the point of view of term rewriting: In the simply-typed lambda calculus, term constructs can be proof-theoretically classified as either introduction forms (λx.M and ⟨M, N⟩) or elimination forms (M N and π_{i} M), using the Curry-Howard isomorphism [3]. The simply-typed counterparts of the axioms (β), (π_{1}), and (π_{2}) of Figure 3 then imply that, when constructing a term bottom-up, “an introduction form followed by an elimination form is a redex.” This property is preserved in the untyped reduction relation ⟶_{FP} by virtue of the commutation axioms (δπ), (π_{1}λ) and (π_{2}λ).

3See also Exercise 18.4.19 in Barendregt’s book [2].

In the rest of this section we prove that ⟶_{FP} is confluent. For that purpose we describe ⟶_{FP} as the union of two relations: a part ⟶_{E} generated from the η/sp-expansion axioms (\overline{η}) and (\overline{sp}), and an “extensionality-free” part ⟶_{R} generated from all the remaining axioms.

• In Section 4.1 we show that the extensionality-free part ⟶_{R} is confluent.

• In Section 4.2 we briefly review the well-known fact that η/sp-expansion ⟶_{E} is confluent, and then show that ⟶_{E} commutes with ⟶_{R}: if N_{1} ⟵_{E}^{∗} M ⟶_{R}^{∗} N_{2}, then there is a P such that N_{1} ⟶_{R}^{∗} P ⟵_{E}^{∗} N_{2}.

We conclude by the Hindley–Rosen Lemma [2, p. 64] that the union ⟶_{FP} = ⟶_{R} ∪ ⟶_{E} is confluent. Earlier, van Oostrom used a similar approach to prove confluence of η-expansion (together with β-reduction) in the pure lambda calculus [14].

From a technical point of view, the proof that ⟶_{E} commutes with ⟶_{R} is the novel part of the confluence proof: the commutation proof highlights the role of the axioms (δπ), (π_{1}λ), and (π_{2}λ).

4.1 Confluence of an extensionality-free subrelation

The relation ▷_{R} is defined by all the axioms of ▷_{FP} except (\overline{η}) and (\overline{sp}); for convenience the remaining axioms are shown in Figure 4. The relation ▷_{R} generates the reduction relation ⟶_{R}.

\begin{matrix}(β) & (λx.M) N & ▷_{R} & M[x := N] \\ (π_{1}) & π_{1} ⟨M, N⟩ & ▷_{R} & M \\ (π_{2}) & π_{2} ⟨M, N⟩ & ▷_{R} & N \\ (δπ) & ⟨M, N⟩ P & ▷_{R} & ⟨M P , N P ⟩ \\ (π_{1}λ) & π_{1} (λx.M) & ▷_{R} & λx.π_{1} M \\ (π_{2}λ) & π_{2} (λx.M) & ▷_{R} & λx.π_{2} M \end{matrix}

Figure 4: The relation ▷_{R}.

We now aim to prove that ⟶_{R} is confluent. In fact, this follows from general higher-order rewriting theory, since ⟶_{R} can be formulated as an orthogonal pattern higher-order rewriting system [13, 17], and such systems are confluent [13]. However, in order to keep the presentation self-contained, we give a direct confluence proof. This direct proof, which follows the method of the Tait/Martin-Löf proof of confluence of β-reduction [2, p. 60], can be viewed as a specialized version of Nipkow’s confluence proof [13].

First, define a parallel [22] reduction relation ⟹_{R}, shown in Figure 5.^{4}

4The notion that ⟹_{R} is the parallel reduction relation generated from the axioms of ▷_{R}

\begin{matrix}M ⟹_{R} M′ & N ⟹_{R} N′ \\ (λx.M) N ⟹_{R} M′[x := N′] \end{matrix}

\begin{matrix}M ⟹_{R} M′ \\ π_{1} ⟨M, N⟩ ⟹_{R} M′ \end{matrix}  \begin{matrix}N ⟹_{R} N′ \\ π_{2} ⟨M, N⟩ ⟹_{R} N′ \end{matrix}

\begin{matrix}M ⟹_{R} M′ & N ⟹_{R} N′ & P ⟹_{R} P′ \\ ⟨M, N⟩ P ⟹_{R} ⟨M′ P′, N′ P′⟩ \end{matrix}

\begin{matrix}M ⟹_{R} M′ \\ π_{1} (λx.M) ⟹_{R} λx.π_{1} M′ \end{matrix}  \begin{matrix}M ⟹_{R} M′ \\ π_{2} (λx.M) ⟹_{R} λx.π_{2} M′ \end{matrix}
M ⟹_{R} M  \begin{matrix}M ⟹_{R} M′ \\ λx.M ⟹_{R} λx.M′ \end{matrix}
\begin{matrix}M ⟹_{R} M′ & N ⟹_{R} N′ \\ M N ⟹_{R} M′ N′ \end{matrix}  \begin{matrix}M ⟹_{R} M′ & N ⟹_{R} N′ \\ ⟨M, N⟩ ⟹_{R} ⟨M′, N′⟩ \end{matrix}
\begin{matrix}M ⟹_{R} M′ \\ π_{1} M ⟹_{R} π_{1} M′ \end{matrix}  \begin{matrix}M ⟹_{R} M′ \\ π_{2} M ⟹_{R} π_{2} M′ \end{matrix}

Figure 5: Parallel R-reduction ⟹_{R}.

Proposition 4.1.

(i) ⟶_{R}^{∗} = ⟹_{R}^{∗}.

(ii) If M ⟹_{R} M′ and N ⟹_{R} N′, then M[x := N] ⟹_{R} M′[x := N′].

(iii) If M ⟶_{R}^{∗} M′ and N ⟶_{R}^{∗} N′, then M[x := N] ⟶_{R}^{∗} M′[x := N′].

Proof. Standard [2, p. 60]. Part (iii) follows from the first two parts and will be used in the next section.

Proposition 4.2. The relation ⟹_{R} satisfies the diamond property: If both M ⟹_{R} N_{1} and M ⟹_{R} N_{2}, then there is a P such that N_{1} ⟹_{R} P and N_{2} ⟹_{R} P.

Proof. By induction on the derivations of M ⟹_{R} N_{1} and M ⟹_{R} N_{2} according to the rules in Figure 5. Many of the cases are well-known from the proof of confluence of β-reduction. There are no interesting new cases (which is another way of saying that ⟶_{R} can naturally be defined as an orthogonal higher-order term rewriting system).

Corollary 4.3. The relation ⟶_{R} is confluent.

4.2 The relation ⟶_{R} commutes with η/sp-expansion

We define the relation ▷_{E} by the axioms (\overline{η}) and (\overline{sp}), for convenience shown in Figure 6. This relation generates the η/sp-expansion relation ⟶_{E}.

(\overline{η}) M ▷_{E} λx.M x  (if x ∉ FV(M))
(\overline{sp}) M ▷_{E} ⟨π_{1} M, π_{2} M⟩

Figure 6: The relation ▷_{E}.

The purpose of this section is to show that ⟶_{E} commutes with ⟶_{R}, that is, if N_{1} ⟵_{E}^{∗} M ⟶_{R}^{∗} N_{2}, then there is a P such that N_{1} ⟶_{R}^{∗} P ⟵_{E}^{∗} N_{2}. Before proceeding with the proof of commutation, we consider some of the critical pairs [13] between ⟶_{E} and ⟶_{R}. The first two cases are well-known:

1. (λx.(λx.M) x) N ⟵\overline{η} (λx.M) N ⟶_{β} M[x := N]. Solution: (λx.(λx.M) x) N ⟶_{β} (λx.M) N ⟶_{β} M[x := N].

2. π_{i} ⟨π_{1} ⟨M_{1}, M_{2}⟩, π_{2} ⟨M_{1}, M_{2}⟩⟩ ⟵\overline{sp} π_{i} ⟨M_{1}, M_{2}⟩ ⟶_{π_{i}} M_{i}. Solution: π_{i} ⟨π_{1} ⟨M_{1}, M_{2}⟩, π_{2} ⟨M_{1}, M_{2}⟩⟩ ⟶_{π_{i}} π_{i} ⟨M_{1}, M_{2}⟩ ⟶_{π_{i}} M_{i}.

On the other hand, to resolve the next two kinds of critical pairs, one needs the commutation axioms (δπ), (π_{1}λ), and (π_{2}λ):

can be made precise [13, Section 4].

3. π_{1} (λx.⟨M_{1}, M_{2}⟩ x) ⟵\overline{η} π_{i} ⟨M_{1}, M_{2}⟩ ⟶_{π_{i}} M_{i}.

Solution:

π_{i} (λx.⟨M_{1}, M_{2}⟩ x) ⟶_{δπ} π_{i} (λx.⟨M_{1} x, M_{2} x⟩)
⟶_{π_{i}λ} λx.π_{i} ⟨M_{1} x, M_{2} x⟩
⟶_{π_{i}} λx.M_{i} x
⟵\overline{η} M_{i}.

4. ⟨π_{1} (λx.M), π_{2} (λx.M)⟩ N ⟵\overline{sp} (λx.M) N ⟶_{β} M[x := N]. Solution:

⟨π_{1} (λx.M), π_{2} (λx.M)⟩ N ⟶_{π_{1}λ,π_{2}λ}^{∗} ⟨λx.π_{1} M, λx.π_{2} M⟩ N
⟶_{δπ}  ⟨(λx.π_{1} M) N, (λx.π_{2} M) N⟩
⟶_{β}^{∗}  ⟨π_{1} (M[x := N]), π_{2} (M[x := N])⟩
⟵\overline{sp}  M[x := N].

These are all the kinds of critical pairs between ⟶_{E} and ⟶_{R} in which the R-step uses one of the axioms (β), (π_{1}), or (π_{2}). The cases where the R-step is one of the remaining axioms can be resolved similarly to the simple cases 1 and 2.

We now turn to the actual proof of commutation. Define a parallel η/spexpansion relation ⟹_{E} [8, 22] by the rules in Figure 7.

\begin{aligned}M ⟹_{E} M′ \\ & (x ∉ FV(M)) \\ M ⟹_{E} λx.M′ x \end{aligned}  \begin{matrix}M ⟹_{E} M′ \\ M ⟹_{E} ⟨π_{1} M′, π_{2} M′⟩ \end{matrix}

M ⟹_{E} M  \begin{matrix}M ⟹_{E} M′ \\ λx.M ⟹_{E} λx.M′ \end{matrix}

\begin{matrix}M ⟹_{E} M′ & N ⟹_{E} N′ \\ M N ⟹_{E} M′ N′ \end{matrix}  \begin{matrix}M ⟹_{E} M′ & N ⟹_{E} N′ \\ ⟨M, N⟩ ⟹_{E} ⟨M′, N′⟩ \end{matrix}

\begin{matrix}M ⟹_{E} M′ \\ π_{1} M ⟹_{E} π_{1} M′ \end{matrix}  \begin{matrix}M ⟹_{E} M′ \\ π_{2} M ⟹_{E} π_{2} M′ \end{matrix}

Figure 7: Parallel η/sp-expansion ⟹_{E}.

First, some simple facts about parallel η/sp-expansion:

Proposition 4.4.

(i) ⟶_{E}^{∗} = ⟹_{E}^{∗}.

(ii) ⟶_{E} is confluent.

(iii) If M ⟹_{E} M′ and N ⟹_{E} N′, then M[x := N] ⟹_{E} M′[x := N′].

Proof. Standard [8]. The confluence of ⟶_{E} follows from the diamond property of ⟹_{E}.

We now aim to prove that if N_{1} ⟸_{E} M ⟶_{R} N_{2}, then there exists a P such that N_{1} ⟶_{R}^{∗} P ⟸_{E} N_{2}. Consider for example the case

N Q ⟸_{E} (λx.M) Q ⟶_{β} M[x := Q]

where N ⟸_{E} λx.M. Then N results from λx.M by a number of η/spexpansions, and in order to show commutation we intuitively need to iterate cases 1 and 4 of the critical pair calculations shown in the beginning of this section. Similar examples exist for the other axioms of ⟶_{R}. The properties which are needed are shown in the following two lemmas:

Lemma 4.5. If λx.M ⟹_{E} N, then

(i) there is a P such that N x ⟶_{R}^{∗} P ⟸_{E} M, and

(ii) there is a Q such that for i ∈ {1, 2}: π_{i} N ⟶_{R}^{∗} λx.π_{i} Q and M ⟹_{E} Q.

Proof. By induction on the definition of λx.M ⟹_{E} N.

Lemma 4.6. If ⟨M_{1}, M_{2}⟩ ⟹_{E} N, then

(i) for i ∈ {1, 2} there is a P_{i} such that π_{i} N ⟶_{R}^{∗} P_{i} ⟸_{E} M_{i}, and

(ii) there are Q_{1}, Q_{2} such that N x ⟶_{R}^{∗} ⟨Q_{1} x, Q_{2} x⟩ and M_{1} ⟹_{E} Q_{1} and M_{2} ⟹_{E} Q_{2}.

Proof. By induction on the definition of ⟨M_{1}, M_{2}⟩ ⟹_{E} N.

We now prove the main lemma needed in the commutation proof:

Lemma 4.7. If N ⟸_{E} M ⟶_{R} M′, then there is a P such that

N ⟶_{R}^{∗} P ⟸_{E} M′.

Proof. Induction on the definition of M ⟹_{E} N, using Lemmas 4.5 and 4.6. We show some illustrative cases.

Case 1: ⟨π_{1} N′, π_{2} N′⟩ ⟸_{E} M ⟶_{R} M′ where N′ ⟸_{E} M. By the induction hypothesis there is a P′ such that N′ ⟶_{R}^{∗} P′ ⟸_{E} M′. Then

⟨π_{1} N′, π_{2} N′⟩ ⟶_{R}^{∗} ⟨π_{1} P′, π_{2} P′⟩ ⟸_{E} M′
so choose P = ⟨π_{1} P′, π_{2} P′⟩.

Case 2: N_{1} N_{2} ⟸_{E} (λx.M_{1}) M_{2} ⟶_{R} M_{1}[x := M_{2}] where N_{1} ⟸_{E} λx.M_{1} and where N_{2} ⟸_{E} M_{2}. By Lemma 4.5(i) there is a P′ such that N_{1} x ⟶_{R}^{∗} P′ ⟸_{E} M_{1}. It is easy to see from the definition of ⟹_{E} that x is not free in N_{1}. Therefore, by Propositions 4.1 and 4.4,

N_{1} N_{2} ⟶_{R}^{∗} P′[x := N_{2}] ⟸_{E} M_{1}[x := M_{2}]

so choose P = P′[x := N_{2}].

Lemma 4.8.

(i) If N ⟸_{E} M ⟶_{R}^{∗} M′, then there is a P such that N ⟶_{R}^{∗} P ⟸_{E} M′. (ii) If N ⟸_{E}^{∗} M ⟶_{R}^{∗} M′, then there is a P such that N ⟶_{R}^{∗} P ⟸_{E}^{∗} M′. Proof.

(i) By induction on the length of the reduction sequence M ⟶_{R}^{∗} M′, using Lemma 4.7.

(ii) By induction on the length of the reduction sequence M ⟹_{E}^{∗} N, using Part (i). Now, by Proposition 4.4(i), ⟶_{E}^{∗} = ⟹_{E}^{∗}. Therefore Lemma 4.8(ii) implies

that the relations ⟶_{E} and ⟶_{R} commute: Proposition 4.9. If N ⟵_{E}^{∗} M ⟶_{R}^{∗} M′, then there is a P such that

N ⟶_{R}^{∗} P ⟵_{E}^{∗} M′.

4.3 Confluence of ⟶_{FP}

We now use the results of Sections 4.1 and 4.2 to prove the main result of Section 4: Proposition 4.10. The relation ⟶_{FP} is confluent. Proof. Proposition 4.3 states that ⟶_{R} is confluent, Proposition 4.4(ii) states that ⟶_{E} is confluent, and Proposition 4.9 states that ⟶_{R} commutes with ⟶_{E}. By the Hindley–Rosen Lemma [2, p. 64], the relation ⟶_{FP} = ⟶_{R} ∪ ⟶_{E} is confluent. Corollary 4.11 (Church–Rosser property). If M =_{FP} N, then there is a P such that M ⟶_{FP}^{∗} P and N ⟶_{FP}^{∗} P. Proof. Follows from confluence of ⟶_{FP} [2, p. 54]. Remarks.

(i) Orienting the axioms (\overline{sp}) and (\overline{η}) of ⟶_{FP} as contraction axioms does not give rise to a confluent reduction relation: with these axioms we would have the reductions λx.x ⟵_{FP} ⟨π_{1} (λx.x), π_{2} (λx.x)⟩ ⟶_{FP}^{∗} ⟨λx.π_{1} x,λx.π_{2} x⟩, but the two terms λx.x and ⟨λx.π_{1} x, λx.π_{2} x⟩ would be normal forms.

(ii) The commutation axioms of λ_{FP} depend on the fact that the calculus is untyped, such that, intuitively, every function is also a pair and vice versa. A different line of work concerns reduction relations in typed calculi, with product and unit types, containing (sp) oriented as a contraction axiom [4].

5 Main result

We are now almost in a position to prove the main result: Suppose M and N are pure λ-terms such that M =_{βηSP} N. Then M =_{FP} N, and by the Church–Rosser property (Corollary 4.11) there is a P such that M ⟶_{FP}^{∗} P and N ⟶_{FP}^{∗} P. However, since ⟶_{FP} contains sp-expansion, we cannot immediately conclude that P is a pure λ-term with M ⟶_{βη}^{∗} P and N ⟶_{βη}^{∗} P. Definition 5.1. The π-erasure of a λ-term M is the pure λ-term |M| defined inductively as follows:

\begin{aligned}|x| & = & x \\ |M N| & = & |M| |N| \\ |λx.M| & = & λx.|M| \\ |⟨M, N⟩| & = & |M| \\ |π_{1} M| & = & |M| \\ |π_{2} M| & = & |M| \end{aligned}

We could just as well have defined |⟨M, N⟩| as |N|, since we are only interested in |P | when P is π-symmetric: Definition 5.2. A λ-term M is π-symmetric if for every subterm of M of the form ⟨P, Q⟩, the π-erasures of P and Q are βη-equivalent: |P | =_{βη} |Q|.

In particular, every pure λ-term is π-symmetric. Proposition 5.3.

(i) |M[x := N]| = |M|[x := |N|] (ii) If M and N are π-symmetric, then M[x := N] is π-symmetric. Proof. By induction on M. Proposition 5.4. If M is π-symmetric and M ⟶_{FP} N, then

(i) |M| =_{βη} |N|, and (ii) N is π-symmetric. Proof. By induction on the definition of M ⟶_{FP} N, using Proposition 5.3.

Now we are ready to prove that λ_{FP} is a conservative extension of λ_{βη}: Theorem 5.5. Let M, N be pure λ-terms. If M =_{FP} N, then M =_{βη} N. Proof. Suppose M and N are pure λ-terms such that M =_{FP} N. By the Church–Rosser property (Corollary 4.11) there is a P such that M ⟶_{FP}^{∗} P and N ⟶_{FP}^{∗} P. Since M and N are pure, they are in particular π-symmetric; it follows from Proposition 5.4 that P is π-symmetric and that |M| =_{βη} |P | =_{βη} |N|. Hence M = |M| =_{βη} |N| = N. Corollary 5.6. The theory λ_{FP} is consistent.

Proof. By Theorem 5.5 and consistency of λ_{βη} [2, p. 67].

Finally we turn to the main result of this article:

Theorem 5.7. Let M, N be pure λ-terms. If M =_{βηSP} N, then M =_{βη} N.

Proof. By Theorem 5.5 and the fact that λ_{FP} is an extension of λ_{βηSP}.

We have also obtained a new—syntactic—proof of consistency of λ_{βηSP}:

Corollary 5.8. The theory λ_{βηSP} is consistent.

Remark. The question of conservativity was originally formulated in a slightly different setting [10]: let D, D_{1} and D_{2} be three new constants, and add the following axioms to the pure λ_{βη}-calculus:

\begin{aligned}D_{1} (D M N) & =_{βηD} & M \\ D_{2} (D M N) & =_{βηD} & N \\ D (D_{1} M) (D_{2} M) & =_{βηD} & M \end{aligned}

To see that the resulting theory λ_{βηD} is conservative over λ_{βη}, one can simulate λ_{βηD} in λ_{βηSP} by defining D as λx.λy.⟨x, y⟩, D_{1} as λx.π_{1} x, and D_{2} as λx.π_{2} x.

6 Related problems

The conservativity proof presented here can be adapted to the non-extensional case settled by de Vrijer [23], i.e., a minor modification gives an alternative proof that λ_{βSP} is conservative over the lambda calculus λ_{β}. To this end, one should simply remove the axiom (η) from every definition and proof. The electronic, formalized version of the proof allows for a straightforward verification that the modification is correct.

Another related problem posed by Klop and de Vrijer is still open: whether the reduction relation ⟶_{βηSP} has the unique normal-form property [10]. The theory λ_{FP} does not seem useful in solving that problem.

Meyer asked whether any lambda theory can be conservatively extended with surjective pairing [6]. That problem also remains open.

Acknowledgements

The author is grateful to Olivier Danvy, Andrzej Filinski, and the anonymous referees for their insightful comments. Vincent van Oostrom pointed out a substantial simplification of the confluence proof in Section 4. Thanks are also due to Pierre-Louis Curien and Soren Lassen for discussions on this work, and to Karl Crary for his lectures on LF and the Twelf system in the fall of 2004 at CMU.

References

[1] Henk Barendregt. Pairing without conventional restraints. Z. Math. Logik Grundlag. Math., 20:289–306, 1974.

[2] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, revised edition, 1984.

[3] Henk Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 2, chapter 2, pages 118–309. Oxford University Press, Oxford, 1992.

[4] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the lambda-calculus with surjective pairing and terminal object. Journal of Functional Programming, 6(2):299–327, 1996.

[5] Pierre-Louis Curien and Thérèse Hardin. Yet yet a counterexample for λ+SP. Journal of Functional Programming, 4(1):113–115, 1994.

[6] Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Open problems in rewriting. In Ronald V. Book, editor, Rewriting Techniques and Applications, 4th International Conference, RTA-91, volume 488 of Lecture Notes in Computer Science, pages 445–456. Springer-Verlag, 1991. The RTA list of open problems is currently maintained at

http://www.lsv.ens-cachan.fr/rtaloop/.

[7] Glenn Durfee. A model for a list-oriented extension of the lambda calculus. Master’s thesis, School of Computer Science, Carnegie Mellon University, 1997.

[8] C. Barry Jay and Neil Ghani. The virtues of eta-expansion. Journal of Functional Programming, 5(2):135–154, 1995.

[9] Jan Willem Klop. Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980.

[10] Jan Willem Klop and Roel de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80(2):97– 113, 1989.

[11] Joachim Lambek and Philip J. Scott. Introduction to Higher Order Categorical Logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

[12] Soren B. Lassen. Head normal form bisimulation for pairs and the λμ-calculus. Manuscript, 2006.

[13] Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, TLCA ’93, volume 664 of Lecture Notes in Computer Science, pages 306–317. Springer-Verlag, 1993.

[14] Vincent van Oostrom. Developing developments. Theoretical Computer Science, 175(1):159–181, 1997.

[15] Frank Pfenning. A proof of the Church–Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, School of Computer Science, Carnegie Mellon University, 1992.

[16] Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Harald Ganzinger, editor, Automated Deduction—CADE-16, 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Computer Science, pages 202–206. Springer-Verlag, 1999.

[17] Femke van Raamsdonk. Confluence and Normalization for higher-order rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1996.

[18] György E. Révész. A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem. Theoretical Computer Science, 93:75–89, 1992.

[19] György E. Révész. Categorical combinators with explicit products. Fundamenta Informaticae, 22:153–166, 1995.

[20] Dana S. Scott. Logic and programming languages. Communications of the ACM, 20:634–641, 1977.

[21] Dana S. Scott. Relating theories of the lambda calculus. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 403–450. Academic Press, 1980.

[22] Masako Takahashi. Parallel reductions in λ-calculus. Information and Computation, 118:120–127, 1995.

[23] Roel de Vrijer. Extending the lambda calculus with surjective pairing is conservative. In Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science, pages 204–215, Pacific Grove, California, June 1989. IEEE Computer Society Press.

A Formalized statement of the main result

Below is the formalized statement of the conservativity theorem. The full formal proof consists of 2670 lines of Twelf code. It was developed using version 1.5R1 of the Twelf system.^{5} The encoding technique is based on a formal proof of the Church–Rosser theorem for β-reduction that is distributed along with earlier versions of the Twelf system [15].

%%% Terms of the untyped lambda calculus with surjective pairing.
term : type.
@ : term -> term -> term.  %infix left 10 @.
lam : (term -> term) -> term.
p1 : term -> term.
p2 : term -> term.
pair : term -> term -> term.
%freeze term.
%%% Lambda calculus with the extensionality rules eta and SP.
==SP : term -> term -> type.  %infix none 5 ==SP.
sp_beta : (lam F) @ N ==SP F N.
sp_eta : lam ([x] M @ x) ==SP M.
sp_proj1 : p1 (pair M N) ==SP M.
sp_proj2 : p2 (pair M N) ==SP N.
sp_SP : pair (p1 M) (p2 M) ==SP M.
% Congruence rules.
sp_refl : M ==SP M.
sp_sym : M ==SP N -> N ==SP M.
sp_trans : M ==SP N -> N ==SP P -> M ==SP P.
sp_c-app : M @ N ==SP M' @ N'
            <- M ==SP M'
            <- N ==SP N'.
sp_c-lam : lam F ==SP lam F'
            <- ({x} F x ==SP F' x).
sp_c-p1 : p1 M ==SP p1 M'
           <- M ==SP M'.

5The Twelf system can be obtained from http://www.cs.cmu.edu/∼twelf/

sp_c-p2 : p2 M ==SP p2 M'
           <- M ==SP M'.
sp_c-pair : pair M N ==SP pair M' N'
             <- M ==SP M'
             <- N ==SP N'.
%freeze ==SP.
%%% Pure lambda-terms, i.e., no "pair", "p1", or "p2".
pterm : type.
^: pterm -> pterm -> pterm.  %infix left 10 ^.
lambda : (pterm -> pterm) -> pterm.
%freeze pterm.
%%% Beta-eta equality on pure terms.
==be : pterm -> pterm -> type.  %infix none 5 ==be.
be_beta : (lambda F) ^N ==be F N.
be_eta : lambda ([x] M ^x) ==be M.
% Congruence rules.
be_refl : M ==be M.
be_sym : M ==be N -> N ==be M.
be_trans : M ==be N -> N ==be P -> M ==be P.
be_c-app : M ^N ==be M' ^N'
           <- M ==be M'
           <- N ==be N'.
be_c-lam : lambda F ==be lambda F'
           <- ({x} F x ==be F' x).
%freeze ==be.
%%% Injecting pure terms into the general terms.
inject : pterm -> term -> type.
%mode inject +P -T.
inj_app : inject (P1 ^P2) (M1 @ M2)
           <- inject P1 M1
           <- inject P2 M2.

inj_lam : inject (lambda P) (lam M)
           <- ({x} {y} inject x y -> inject (P x) (M y)).
%freeze inject.
%block inj : block {x : pterm} {y : term} {thm : inject x y}.
%worlds (inj) (inject __).
%total P (inject P _).

%%% The main theorem: ==SP is conservative over ==be.
conservative : inject M M' -> inject N N'
                           -> M' ==SP N'
                           -> M ==be N
                           -> type.
%mode conservative +I1 +I2 +E1 -E2.
% [The proof is omitted.]
%worlds () (conservative ____).
%total I1 (conservative I1 ___).
% With empty "worlds", the main theorem is actually only shown
% for closed terms. (The generalization to open terms is more
% complicated to express, but it follows easily by
% lambda-abstracting every free variable.)

Recent BRICS Report Series Publications

RS-06-5 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. March 2006. 18 pp. To appear in Logical Methods in Computer Science. Supersedes RS-05-35.

RS-06-4 Olivier Danvy and Kevin Millikin. A Rational Deconstruction of Landin’s J Operator. 2006.

RS-06-3 Ma�gorzata Biernacka and Olivier Danvy. A Concrete Framework for Environment Machines. February 2006. ii+29 pp. To appear in the ACM Transactions on Computational Logic. Supersedes BRICS RS-05-15.

RS-06-2 Mikkel Baun Kjærgaard and Jonathan Bunde-Pedersen. A Formal Model for Context-Awareness. February 2006. 26 pp.

RS-06-1 Luca Aceto, Taolue Chen, Willem Jan Fokkink, and Anna Ingólfsdóttir. On the Axiomatizability of Priority. January 2006. 25 pp.

RS-05-38 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. December 2005. iii+39 pp. Revised version of BRICS RS-05-22.

RS-05-37 Gerth Stølting Brodal, Kanela Kaligosi, Irit Katriel, and Martin Kutz. Faster Algorithms for Computing Longest Common Increasing Subsequences. December 2005. 16 pp.

RS-05-36 Dariusz Biernacki, Olivier Danvy, and Chung-chieh Shan. On the Static and Dynamic Extents of Delimited Continuations. December 2005. ii+33 pp. To appear in the journal Science of Computer Programming. Supersedes BRICS RS-05-13.

RS-05-35 Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. November 2005. 19 pp.

RS-05-34 Henning Korsholm Rohde. Formal Aspects of Polyvariant Specialization. November 2005. 27 pp.