BRICS

Basic Research in Computer Science

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

Kristian Støvring

BRICS Report Series RS-05-35 ISSN 0909-0878 November 2005 BRICS RS-05-35 K. Støvring: Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative Copyright \begin{matrix}c \\ ◯ \end{matrix} 2005, 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 Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
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/05/35/

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

Kristian Støvring

BRICS ^{∗}

Department of Computer Science University of Aarhus ^{†}

November 22, 2005

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 the first “syntactic” proof that the extensional lambda calculus with surjective pairing is consistent.

1 Introduction

The theory λ_{βηSP} is obtained from the (untyped) extensional lambda calculus λ_{βη} [2, p. 32], 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}

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 [7, 15] and featured as Problem 5 on the original RTA list of open problems [4]:

∗

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

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

In other words, we show that the theory λ_{βηSP} is a conservative extension of the theory λ_{βη}. As a byproduct we obtain the (as far as the author knows) first proof of consistency of λ_{βηSP} which uses purely syntactic methods.

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 on the preceding page) is definable in the lambda calculus [1], and the standard reduction relation for the lambda calculus with surjective pairing is not confluent [8]. Both results were shown for the extensional lambda calculus as well.

Klop [8] and Klop and de Vrijer [7] 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 [15]. 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}. A model-theoretic consistency proof for λ_{βηSP} (and hence for λ_{βSP}) can be given using the inverse limit model construction [12].

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

D ≅ D × D ≅ D → D,

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

1.2 Formalization

The author has formalized and verified the proof of the conservativity result using the Twelf system [11]. 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/∼kss/papers/SP/

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}; the relation =_{R} is a congruence in the usual sense. 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 a congruence =_{βη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 [8, p. 216]; its confluence would immediately imply the main result, namely that λ_{βηSP} is conservative over λ_{βη}.^{1}

In this article we instead define a further extension λ_{βηπ} of λ_{βηSP} and show that λ_{βηπ} is conservative over λ_{βη}. Since λ_{βηπ} is an extension of λ_{βηSP}, the main result follows.

The proof is structured in the following way:

• In Section 4 we define the extension λ_{βηπ} of λ_{βηSP} and show that it is generated by a confluent reduction relation ⟶_{βηπ}. In the relation ⟶_{βηπ} the axioms (η) and (SP) are oriented as expansion axioms (see, e.g., the work by Jay and Ghani [6]).

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

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

We first define the extension λ_{βηπ} of λ_{βηSP}. The relation ▷_{βηπ} is defined by the axioms in Figure 3. This relation generates the theory λ_{βηπ} and the reduction relation ⟶_{βηπ}. As discussed above, the axioms (η) and (SP) in ⟶_{βηπ} are oriented as expansion axioms.

Remark. The theory λ_{βηπ} and the associated reduction relation ⟶_{βηπ} have certain properties which might make them interesting in their own right:

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

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

Figure 3: The relation ▷_{βηπ}.

• From the point of view of semantics: The original model of λ_{βηSP} [9, 12] is also a model of λ_{βηπ}. Indeed, let D and E be complete partial orders such that E ≅ E × E and D ≅ [D → E]. Then D ≅ D × D ≅ [D → D], and it is easy to verify that the standard interpretation^{2} of λ-terms as elements of D gives rise to a model of λ_{βηπ}.

As an aside, if D is an arbitrary complete partial order satisfying that D ≅ D × D ≅ [D → D], then the standard interpretation using these isomorphisms makes D a model of (at least) λ_{βηSP}. Taking D = E in the above construction now gives an alternative pair of isomorphisms, and hence an alternative interpretation of λ-terms, resulting in a model of λ_{βηπ}.

• 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 ⟶_{βηπ} by virtue of the three new axioms.

In the rest of this section we prove that ⟶_{βηπ} is confluent. For that purpose we describe ⟶_{βηπ}^{∗} as the union of two relations: an “extensionality-free” part ⟶_{βπ}^{∗} and η/SP-expansion ⟶_{η}^{∗}.

• In Section 4.1 we define the relation ⟶_{βπ} and show that it is confluent.

• In Section 4.2 we define η/SP-expansion ⟶_{η} and show that it commutes with ⟶_{βπ} in the following sense: If N_{1} ⟵_{η}^{∗} M ⟶_{βπ}^{∗} N_{2}, then there is a P such that N_{1} ⟶_{βπ}^{∗} P ⟵_{η}^{∗} N_{2}.

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

• Finally, in Section 4.3 we use the Hindley-Rosen Lemma [2, p. 64] (and the well-known fact that ⟶_{η} is confluent) to conclude that ⟶_{βηπ} is confluent.

Earlier, van Oostrom used a similar approach to prove confluence of η-expansion (together with β-reduction) in the pure lambda calculus [10].

4.1 Confluence of an extensionality-free subrelation

In order to define the subrelation ⟶_{βπ} of ⟶_{βηπ}^{∗} we need the auxiliary notion of π-neutral terms:

Definition 1. The π-neutral terms are generated by the following (sub)grammar:

A ::= λx.M | π_{1} A | π_{2} A

In other words, the π-neutral terms are those of the form π_{i_{1}}(⋯ (π_{i_{n}}(λx.M)) ⋯) for some n ≥ 0.

The relation ▷_{βπ} is defined by the axioms in Figure 4. This relation generates the reduction relation ⟶_{βπ}.

(β) (λx.M) N ▷_{βπ} M[x := N]
(π_{1}) π_{1} ⟨M, N⟩ ▷_{βπ} M
(π_{2}) π_{2} ⟨M, N⟩ ▷_{βπ} N
(δπ) ⟨M, N⟩ P ▷_{βπ} ⟨M P , N P ⟩
(π_{1}λ) π_{1} (λx.M) ▷_{βπ} λx.π_{1} M
(π_{2}λ) π_{2} (λx.M) ▷_{βπ} λx.π_{2} M
(π_{1} ν) (π_{1} M) N ▷_{βπ} π_{1} (M N) (if M is π-neutral)
(π_{2} ν) (π_{2} M) N ▷_{βπ} π_{2} (M N) (if M is π-neutral)

Figure 4: The relation ▷_{βπ}.

Note that ⟶_{βπ} does not contain the “extensionality” axioms (η) and (SP). On the other hand, the new axioms (π_{1}ν) and (π_{2}ν) of ⟶_{βπ} are derivable in ⟶_{βηπ}^{∗}, using η-expansion:

(π_{i} M) N ⟶_{βηπ} (π_{i} (λx.M x)) N ⟶_{βηπ} (λx.π_{i} (M x)) N ⟶_{βηπ} π_{i} (M N)

Therefore, ⟶_{βπ} ⊆ ⟶_{βηπ}^{∗}.

The key property of π-neutral terms is that if a term M is π-neutral, then no substitution instance of M can βπ-reduce to a term of the form ⟨P, Q⟩:

Proposition 2.

(i) If M is π-neutral and M ⟶_{βπ} M′, then M′ is π-neutral. (ii) If M is π-neutral and N is an arbitrary term, then M[x := N] is π-neutral. (iii) No term of the form ⟨P, Q⟩ is π-neutral.

We now prove that ⟶_{βπ} is confluent. The proof follows the Tait/Martin-Löf proof of confluence of β-reduction in the pure lambda calculus [2, p. 60]: First we define a “parallel” [14] reduction relation ⟹_{βπ}, shown in Figure 5.

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

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

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

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

Figure 5: Parallel βπ-reduction ⟹_{βπ}.

Proposition 3.

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

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

(iii) If M ⟶_{βπ}^{∗} M′ and N ⟶_{βπ}^{∗} N′, then M[x := N] ⟶_{βπ}^{∗} 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. The relation ⟹_{βπ} satisfies the diamond property: If M ⟹_{βπ} N_{1} and M ⟹_{βπ} N_{2}, then there is a P such that N_{1} ⟹_{βπ} P and N_{2} ⟹_{βπ} P.

Proof. By induction on the derivations of M ⟹_{βπ} N_{1} and M ⟹_{βπ} N_{2} according to the rules in Figure 5. Many of the cases are well-known from the proof of confluence of β-reduction. We show the interesting new cases:

• (λx.π_{i} M_{1}) N_{1} ⟸_{βπ} (π_{i} (λx.M)) N ⟹_{βπ} π_{i} ((λx.M_{2}) N_{2}), where M ⟹_{βπ} M_{1}, M_{2} and N ⟹_{βπ} N_{1}, N_{2}.

By induction hypothesis, there are M_{3} and N_{3} such that M_{1}, M_{2} ⟹_{βπ} M_{3} and N_{1}, N_{2} ⟹_{βπ} N_{3}. Then π_{i} M_{1} ⟹_{βπ} π_{i} M_{3}, hence (λx.π_{i} M_{1}) N_{1} ⟹_{βπ} π_{i} (M_{3}[x := N_{3}]). Also, π_{i} ((λx.M_{2}) N_{2}) ⟹_{βπ} π_{i} (M_{3}[x := N_{3}]).

• (π_{i} M_{1}) N_{1} ⟸_{βπ} (π_{i} M) N ⟹_{βπ} π_{i} (M_{2} N_{2}), where M is π-neutral, M ⟹_{βπ} M_{1}, M_{2}, and N ⟹_{βπ} N_{1}, N_{2}.

By induction hypothesis, there are M_{3} and N_{3} such that M_{1}, M_{2} ⟹_{βπ} M_{3} and N_{1}, N_{2} ⟹_{βπ} N_{3}. By Proposition 2(i) and 3(i), M_{1} is π-neutral. Therefore, (π_{i} M_{1}) N_{1} ⟹_{βπ} π_{i} (M_{3} N_{3}) and π_{i} (M_{2} N_{2}) ⟹_{βπ} π_{i} (M_{3} N_{3}).

Corollary 5. The relation ⟶_{βπ} is confluent.

Remark. Without the restriction to π-neutral terms in two of the rules, ⟹_{βπ} would not satisfy the diamond property: Then we would have (π_{1} ⟨x, y⟩) z ⟹_{βπ} x z and (π_{1} ⟨x, y⟩) z ⟹_{βπ} π_{1} (⟨x, y⟩ z), but not π_{1} (⟨x, y⟩ z) ⟹_{βπ} x z.

4.2 Eta-expansion commutes with ⟶_{βπ}

We define ▷_{η} by the axioms in Figure 6. This relation generates the η/SPexpansion relation ⟶_{η}.

The purpose of this section is to show that ⟶_{βπ} commutes with ⟶_{η}: If N_{1} ⟵_{η}^{∗} M ⟶_{βπ}^{∗} N_{2}, then there is a P such that N_{1} ⟶_{βπ}^{∗} P ⟵_{η}^{∗} N_{2}. In order to prove this result we define “parallel” η/SP-expansion ⟹_{η} [6, 14], shown in Figure 7.

\begin{matrix}(η) & M & ▷_{η} & λx.M x & (if x ∉ FV(M)) \\ (SP) & M & ▷_{η} & ⟨π_{1} M, π_{2} M⟩ \end{matrix}

Figure 6: The relation ▷_{η}.

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

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

Proposition 6.

(i) ⟶_{η}^{∗} = ⟹_{η}^{∗}. (ii) ⟶_{η} is confluent. (iii) If M ⟹_{η} M′ and N ⟹_{η} N′, then M[x := N] ⟹_{η} M′[x := N′]. Proof. Standard [6]. The confluence of ⟶_{η} follows from the diamond property of ⟹_{η}.

We now aim to prove that if N_{1} ⟸_{η} M ⟶_{βπ} N_{2}, then there is a P such that N_{1} ⟶_{βπ}^{∗} P ⟸_{η} N_{2}. For most of the different cases (according to the axioms and congruence rules generating ⟶_{βπ}) this property can be shown using the following two lemmas. Lemma 7. If λx.M ⟹_{η} N, then

(i) there is a P such that N x ⟶_{βπ}^{∗} P ⟸_{η} M, and (ii) there is a Q such that for i ∈ {1, 2}: π_{i} N ⟶_{βπ}^{∗} λx.π_{i} Q and M ⟹_{η} Q. Proof. By induction on the definition of λx.M ⟹_{η} N. Lemma 8. If ⟨M_{1}, M_{2}⟩ ⟹_{η} N, then

(i) for i ∈ {1, 2} there is a P_{i} such that π_{i} N ⟶_{βπ}^{∗} P_{i} ⟸_{η} M_{i}, and (ii) there are Q_{1}, Q_{2} such that N x ⟶_{βπ}^{∗} ⟨Q_{1} x, Q_{2} x⟩ and also M_{1} ⟹_{η} Q_{1}

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

The most complicated case is N ⟸_{η} (π_{i} M_{1}) M_{2} ⟶_{βπ} π_{i} (M_{1} M_{2}) (where M_{1} is π-neutral). Here we use two additional lemmas. In the proof of Lemma 10 we need to perform induction on the height of derivations of “M ⟹_{η} N”, considering these derivations as finite trees constructed according to the rules in Figure 7. Lemma 9. If M ⟹_{η} N and M is π-neutral, then there is a π-neutral P such that

(i) for i ∈ {1, 2}, π_{i} N ⟶_{βπ}^{∗} π_{i} P, (ii) M ⟹_{η} P, and (iii) for any given derivation of M ⟹_{η} N of height n, one can find a derivation

of M ⟹_{η} P of height no greater than n.

Proof. By induction on the definition of M ⟹_{η} N. Since M is π-neutral there are only a few cases to consider.

Case 1: N is π-neutral. Then we choose P = N.

Case 2: N = π_{i} N′ and M = π_{i} M′ where M′ ⟹_{η} N′ and M′ is π-neutral. By the induction hypothesis there is a π-neutral P′ such that N = π_{i} N′ ⟶_{βπ}^{∗} π_{i} P′ and M′ ⟹_{η} P′. Now choose P = π_{i} P′.

Case 3: N = ⟨π_{1} N′, π_{2} N′⟩ where M ⟹_{η} N′. By the induction hypothesis there is a π-neutral P′ such that π_{1} N′ ⟶_{βπ}^{∗} π_{1} P′, π_{2} N′ ⟶_{βπ}^{∗} π_{2} P′, and M ⟹_{η} P′. Then π_{1} N ⟶_{βπ} π_{1} N′ ⟶_{βπ}^{∗} π_{1} P′, and similarly

π_{2} N ⟶_{βπ}^{∗} π_{2} P′. Now choose P = P′.

It is easy to verify that if the given derivation of M ⟹_{η} N has height n, then the above construction gives a derivation of M ⟹_{η} P of height no greater than n.

Lemma 10. If π_{i} M ⟹_{η} N and M is π-neutral, then there is a P such that N x ⟶_{βπ}^{∗} P ⟸_{η} π_{i} (M x).

Proof. By induction on the height of the derivation of π_{i} M ⟹_{η} N. We show the interesting case: Assume that N = ⟨π_{1} N′, π_{2} N′⟩ where π_{i} M ⟹_{η} N′. Let the height of the given derivation of π_{i} M ⟹_{η} N be n + 1; the height of the subderivation π_{i} M ⟹_{η} N′ is then n. By Lemma 9 there is a π-neutral Q such that π_{1} N′ ⟶_{βπ}^{∗} π_{1} Q, π_{2} N′ ⟶_{βπ}^{∗} π_{2} Q, and π_{i} M ⟹_{η} Q. Furthermore, the lemma gives a derivation of π_{i} M ⟹_{η} Q of height no greater than n. Therefore the induction hypothesis gives a P′ such that Q x ⟶_{βπ}^{∗} P′ ⟸_{η} π_{i} (M x). Hence,

N x = ⟨π_{1} N′, π_{2} N′⟩ x ⟶_{βπ}^{∗} ⟨π_{1} Q, π_{2} Q⟩ x
⟶_{βπ} ⟨(π_{1} Q) x, (π_{2} Q) x⟩
⟶_{βπ}^{∗} ⟨π_{1} (Q x), π_{2} (Q x)⟩
⟶_{βπ}^{∗} ⟨π_{1} P′, π_{2} P′⟩
⟸_{η} π_{i} (M x).

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

Lemma 11. If N ⟸_{η} M ⟶_{βπ} M′, then there is a P such that N ⟶_{βπ}^{∗} P ⟸_{η} M′.

Proof. Induction on the definition of M ⟹_{η} N, using Lemmas 7-10. We show some illustrative cases.

Case 1: ⟨π_{1} N′, π_{2} N′⟩ ⟸_{η} M ⟶_{βπ} M′ where N′ ⟸_{η} M. By the induction

hypothesis there is a P′ such that N′ ⟶_{βπ}^{∗} P′ ⟸_{η} M′. Then

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

Case 2: N_{1} N_{2} ⟸_{η} (λx.M_{1}) M_{2} ⟶_{βπ} M_{1}[x := M_{2}] where N_{1} ⟸_{η} λx.M_{1} and N_{2} ⟸_{η} M_{2}. Without loss of generality, x ∉ FV(N_{1}). By Lemma 7(i) there is a P′ such that N_{1} x ⟶_{βπ}^{∗} P′ ⟸_{η} M_{1}. Then by Propositions 3 and 6, N_{1} N_{2} ⟶_{βπ}^{∗} P′[x := N_{2}] ⟸_{η} M_{1}[x := M_{2}], so we choose P =

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

Case 3: N_{1} N_{2} ⟸_{η} (π_{i} M_{1}) M_{2} ⟶_{βπ} π_{i} (M_{1} M_{2}) where M_{1} is π-neutral, N_{1} ⟸_{η} π_{i} M_{1}, and N_{2} ⟸_{η} M_{2}. Choose x ∉ FV(N_{1}). Lemma 10 gives a P′ such that N_{1} x ⟶_{βπ}^{∗} P′ ⟸_{η} π_{i} (M_{1} x). Then by Propositions 3 and 6, N_{1} N_{2} ⟶_{βπ}^{∗} P′[x := N_{2}] ⟸_{η} π_{i} (M_{1} M_{2}), so we choose

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

Lemma 12.

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

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

(ii) By induction on the length of the reduction sequence M ⟹_{η}^{∗} N, using Part

(i). By Proposition 6(i), ⟶_{η}^{∗} = ⟹_{η}^{∗}. We therefore conclude from Lemma 12(ii)

that the relations ⟶_{βπ} and ⟶_{η} commute: Proposition 13. If N ⟵_{η}^{∗} M ⟶_{βπ}^{∗} M′, then there is a P such that N ⟶_{βπ}^{∗} P ⟵_{η}^{∗} M′.

4.3 Confluence of ⟶_{βηπ}

We now use the results of Sections 4.1 and 4.2 to prove the main result of Section 4: Proposition 14. The relation ⟶_{βηπ} is confluent.

Proof. Proposition 5 states that ⟶_{βπ} is confluent, Proposition 6(ii) states that ⟶_{η} is confluent, and Proposition 13 states that ⟶_{βπ} commutes with ⟶_{η}. By the Hindley-Rosen Lemma [5], the relation ⟶_{βηπ}^{∗} = ⟶_{βπ}^{∗} ∪ ⟶_{η}^{∗} is confluent. More specifically, by constructing the following diagram we see that the composition of ⟶_{βπ}^{∗} with ⟶_{η}^{∗} satisfies the diamond property:

[figure: M; ∗; βπ; ∗; βπ; ∗; βπ; ∗; η; ∗; βπ; ∗; η; N_{1}; ∗; βπ; ∗; η; ∗; η; N_{2}; ∗; βπ; ∗; η; ∗; η; P]

Corollary 15 (Church-Rosser property). If M =_{βηπ} N, then there is a P such that M ⟶_{βηπ}^{∗} P and N ⟶_{βηπ}^{∗} P.

Proof. Follows from confluence of ⟶_{βηπ} in the standard way [2, p. 54].

Remark. Orienting the axioms (SP) and (η) of ⟶_{βηπ} as contraction axioms does not give rise to a confluent reduction relation: With these axioms we would have ⟨y, z⟩ ⟵_{βηπ} λx.(⟨y, z⟩ x) ⟶_{βηπ} λx.⟨y x, z x⟩, but both ⟨y, z⟩ and λx.⟨y x, z x⟩ would be normal forms.

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 =_{βηπ} N, and by the Church-Rosser property (Corollary 15) there is a P such that M ⟶_{βηπ}^{∗} P and N ⟶_{βηπ}^{∗} P. However, since ⟶_{βηπ} contains SP-expansion, we cannot immediately conclude that P is a pure λ-term with M ⟶_{βη}^{∗} P and N ⟶_{βη}^{∗} P.

Definition 16 (π-erasure). 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 17. 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 18.

(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 19. If M is π-symmetric and M ⟶_{βηπ} N, then

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

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

M = |M| =_{βη} |P | =_{βη} |N| = N.

Corollary 21. The theory λ_{βηπ} is consistent. Proof. By Theorem 20 and consistency of λ_{βη} [2, p. 67].

Finally we turn to the main result of this article: Theorem 22. Let M, N be pure λ-terms. If M =_{βηSP} N, then M =_{βη} N. Proof. By Theorem 20 and the fact that λ_{βηπ} is an extension of λ_{βηSP}.

We have also obtained a new—syntactic—proof of consistency of λ_{βηSP}: Corollary 23. The theory λ_{βηSP} is consistent.

Remark. The question of conservativity was originally formulated in a slightly different setting [7]: 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 [15], i.e., a minor modification gives an alternative proof that λ_{βSP} is conservative over the lambda calculus λ_{β}. To this end, one should remove the axiom (η) from every definition and add the two (π_{i}ν) axioms to the definition of ⟶_{βηπ}. 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 [7]. The theory λ_{βηπ} does not seem useful in solving that problem.

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

Acknowledgements

The author is grateful to Olivier Danvy and Andrzej Filinski for their encouragement and insightful comments, 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 T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, Vol. 2, chapter 2, pages 118–309. Oxford University Press, Oxford, 1992.

[4] Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Open problems in rewriting. In Ronald V. Book, editor, 4th International Conference on Rewriting Techniques and Applications, volume 488 of Lecture Notes in Computer Science, pages 445–456, Como, Italy, April 1991. Springer-Verlag.

[5] J. R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic. PhD thesis, University of Newcastle-upon-Tyne, 1964.

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

[7] J. W. Klop and R. C. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80(2):97–113, 1989.

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

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

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

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

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

[13] 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.

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

[15] 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

%%% 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.
%%% 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'.
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'.
%%% Pure lambda-terms, i.e., no "pair", "p1", or "p2".
pterm : type.
^: pterm -> pterm -> pterm.  %infix left 10 ^.
lambda : (pterm -> pterm) -> pterm.
%block pvar : block {y : 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).

%%% 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)).
%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 easily
% follows by lambda-abstracting every free variable).

Recent BRICS Report Series Publications

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.

RS-05-33 Luca Aceto, Willem Jan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not Finitely Based over BPA with Interrupt. October 2005. 33 pp. This paper supersedes BRICS Report RS-04-24. An extended abstract of this paper appeared in Algebra and Coalgebra in Computer Science, 1st Conference, CALCO 2005, Swansea, Wales, 3–6 September 2005, Lecture Notes in Computer Science 3629, pp. 54–68, Springer-Verlag, 2005.

RS-05-32 Anders Møller, Mads Østerby Olesen, and Michael I. Schwartzbach. Static Validation of XSL Transformations. October 2005. 50 pp.

RS-05-31 Christian Kirkegaard and Anders Møller. Type Checking with XML Schema in Xact. September 2005. 20 pp.

RS-05-30 Karl Krukow. An Operational Semantics for Trust Policies. September 2005. 38 pp.

RS-05-29 Olivier Danvy and Henning Korsholm Rohde. On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation. September 2005. ii+9 pp. To appear in Information Processing Letters. This version supersedes BRICS RS-05-14.

RS-05-28 Jiří Srba. On Counting the Number of Consistent Genotype Assignments for Pedigrees. September 2005. 15 pp. To appear in FSTTCS ’05.

RS-05-27 Pascal Zimmer. A Calculus for Context-Awareness. August 2005. 21 pp.

RS-05-26 Henning Korsholm Rohde. Measuring the Propagation of Information in Partial Evaluation. August 2005. 39 pp.

RS-05-25 Dariusz Biernacki and Olivier Danvy. A Simple Proof of a Folklore Theorem about Delimited Control. August 2005. ii+11 pp. To appear in Journal of Functional Programming. This version supersedes BRICS RS-05-10.