Math. Struct. in Comp. Science (1991), vol. 1, pp. 1–20

Provable isomorphisms of types

Kim B. Bruce: ∗

Roberto Di Cosmo: ‡

Giuseppe Longo: §

Received 23 July 1990 Revised 12 December 1991

A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. By the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC’s. By the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having “invertible” proofs between the two terms. Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.

1. Introduction

There has been a great deal of interest over the years in constructing models of the various lambda calculi which satisfy various equations (isomorphisms) between types. One reason is that recursive definitions of data types are usually interpreted as equations to be solved over specific mathematical structures.

In previous work, Bruce and Longo [BL85], the first and third author showed that no such non-trivial isomorphism existed in either the simply typed or second-order lambda calculus. However, no extension of these results was known at that time for the lambda calculus with richer type disciplines. Products and higher order types, in particular, proved to be of special interest not only because of their common or increasing use in programming languages, but also because of the close connection between these calculi and relevant categorical structures and proof systems.

In this paper we characterize the isomorphisms which hold in all models of the simply typed lambda calculus with surjective pairing (and “terminal object”). Moreover we show that it is decidable whether two types (built from type variables) are isomorphic in

: ∗ Dept. Of Computer Science, Williams College, Williamstown, MA 01267 : ‡ Dip. di Informatica, Università di Pisa, Italy, and LIENS, 45, Rue d’Ulm, Paris, France : § LIENS (CNRS) - DMI, Ecole Normale Superieure, 45, Rue d’Ulm, Paris, France

all models of this calculus. It is well known that these models are exactly the Cartesian closed categories (CCC).

Once given the types which are isomorphic in every model of the lambda calculus (or equivalently, isomorphic in every CCC), there is, in principle, no reason to believe that there is a uniform way to witness these isomorphisms. Nevertheless it turns out that our proof of these results is based on a simple axiomatization of type equations and the notion of provable isomorphisms (those representable by closed terms of the lambda calculus). Moreover any proof of the equality of two types can be used to generate an isomorphism between the types (which holds in every model).

The axioms for our theory are given below:

Definition 1.1. T h_{×T}^{1} is a theory of equality plus the following axiom schemas, where T is a constant symbol: 1 A × B = B × A 2 A × (B × C) = (A × B) × C 3 (A × B) → C = A → (B → C) 4 A → (B × C) = (A → B) × (A → C) 5 A × T = A 6 A → T = T 7 T → A = A

The Main Theorem of this paper shows that two types A and B can be constructively proved to be isomorphic, by two programs which act one as the inverse of the other, iff T h_{×T}^{1}⊢ A = B.

In order to discuss the soundness of Th, and explain where it comes from, we hint here of its categorical meaning. Note, though, that no notion nor result from Category Theory is used in most of the paper.

Since models of the typed lambda calculus with surjective pairing are exactly the Cartesian closed categories (CCC), our results translate directly into theorems on when two generic objects are isomorphic in all CCC’s. In other words, T h_{×T}^{1} characterizes which are isomorphic just by the Cartesian closed structure of the category in which they are interpreted, no matter which particular CCC is chosen.

Observe first that T h_{×T}^{1} is realized in every Cartesian Closed Category, when “=” is interpreted as isomorphism. The first three axioms describe properties of the Cartesian product (associativity, commutativity, identity for ×), and the second three axioms can be seen as the properties of the three adjunctions of a CCC that relate product, exponent and the terminal object. The last equation (T → A = A) tells us that the arrows from the terminal object to A in a CCC are the points of A. Thus, the theory T h_{×T}^{1} is sound. A consequence of our main result is the completeness of T h_{×T}^{1} with respect to CCC’s. That is, no other isomorphism is valid in all CCC’s. (This is not obvious because there are categorical models of T h_{×T}^{1} which are not CCC’s: take a Cartesian Category with a bifunctor “ → ” such that A → B = B, say).

A further consequence of the work below in λ-calculus will be an insight into the composition of derivations in Proof Theory. The typed lambda calculus with surjective pairing is the language for proofs of IP C(True, ∧, →), the intuitionistic positive propositional calculus. In the proof theoretic framework we then characterize equivalent formulae, where two formulae A and B are considered equivalent if, given a proof f of the sequent A ⊢B, and a proof g of the sequent B ⊢ A, g f yields, after cut-elimination, the identity proof of the sequent A ⊢ A and vice-versa. The details of both the categorical and proof-theoretic applications are discussed in [DCL89].

As an example of the use of such results in computer science we note the two papers by Rittri ([Rit89], [Rit90]) in which the author discusses the problem of finding applicable functions in a program library. For example, one might be interested in looking up various search functions. As a result it might be useful to inspect all functions which take an element and a table and return an index to the table. Because trivial differences in argument order or Currying may lead one to ignore useful functions, it is important to be able to find all those functions whose type is isomorphic to that for which one is searching.

Rittri’s application of the result presented here settles on the same notion of provable isomorphism. He cites the paper by Solv’ev ([Sol83]), in which the author presents the same result as in our main theorem (Theorem 4.9), although by an entirely different proof which is based on taking the natural numbers as objects in a CCC (with × interpreted as multiplication and → as exponentiation) and then showing the equational completeness of the theory of (N, 1, ×, ↑). (Meyer and Statman, personal communication, suggested a similar proof for the exponential fragment only; also the abstract in Martin ([Mar72]) states the same fact). Solv’ev also provides a decision procedure similar to that given here.

We note that in a forthcoming paper, the second author extends these results to the second-order typed lambda calculus, with surjective pairings. We know no way of extending the proof given by Solv’ev to this more complex case.

The paper is organized as follows. Section 2 sets out the basic definitions leading up to the notion of a type normal form. Section 3 presents some rather technical lemmas which will be used in section 4 in order to characterize the set of provable isomorphisms. The third section also contains a discussion of the decidability of the theory and the connections with category and proof theory. The proofs of the important (but technically complex) lemmas in section 3 are put off into an appendix at the end of the paper.

2. Basic notions and facts

Definition 2.1. The collection Tp of type expressions, over a ground set At of atomic type symbols, is inductively defined by:

•At ⊆ Tp, where T ∈ At is a fixed constant type symbol

•if A, B ∈ Tp, then A → B ∈ Tp;

•if A, B ∈ Tp, then A × B ∈ Tp.

The intended meaning of T is the terminal object in the categorical sense; thus ∗_{A} below will stand for the unique map in A → T (as required of a terminal object).

Pure λ-terms are defined as usual. In particular, for every type A there exists a denumerable number of variables, ranged over by lower case letters near the end of the alphabet. We use upper case letters M, N, P, …, as meta-variables for terms. The fact that a term M has type A will be denoted with the expression “M : A”. Definition 2.2.

(i) The terms of λ^{1}βηπ∗, the typed λ-calculus with surjective pairing and terminal object, and their associated types, are defined according to the following formation rules:

•every variable x : A is a term;

•if x : A is a variable, and M : B is a term, then λx:A . M : A → B is a term; •if M : A → B is a term and N : A is a term, then MN : B is a term; •if M : A is a term and N : B is a term, then ⟨M, N⟩: A × B is a term; •p_{1} : A × B → A; •p_{2} : A × B → B; •∗A : A → T.

(ii) The equational theory of terms is the minimal congruence relation “=” which satisfies the following axiom schemas:

alpha-beta-eta-csi:

(α)  λx:A.M = λy:A.M[x:=y], if y is free for x in M
(→ β) (λx:A.M)N = M[x:=N], if N is free for x in M
(→ η) λx:A.(Mx) = M, if x ∉ F V (M)
(ξ)  if M=N then λx:A.M = λx:A.N

surjective pairing:

(×β_{1}) p_{1}(⟨M, N⟩) = M
(×β_{2}) p_{2}(⟨M, N⟩) = N
(×η) ⟨p_{1}(M), p_{2}(M)⟩ = M

terminal object:

(∗)  If M : A → T then M = ∗_{A}.

Notation 2.3. Given a sequence M_{1}, …,M_{n} of terms, and sequence x = x_{1}, …,x_{n} of variables, N[M⃗/x⃗] denotes the simultaneous substitution of every term M_{i} for the variable x_{i} in the term N (for simplicity, we always assume bound variables are renamed as necessary to avoid capture of free variables). We also use the notation N[M/x⃗] to express the simultaneous substitution of the term M for all the variables in x⃗. For application we follow the usual convention of associating to the left, i.e. N_{1} … N_{n} is to be parsed as (… (N_{1}N_{2})… N_{n}). In case a substitution is applied only to a subsequence of an application M_{1} … M_{n}, we will use the notation N_{1}N_{2}… {N_{i}… N_{k}[M⃗/x⃗]}… N_{n} to denote the term N_{1} … N_{n} with the substitution [M⃗/x⃗] applied only to the terms N_{i} … N_{k}.

We write ⟨M_{1},… M_{n}⟩ for ⟨… ⟨⟨M_{1}, M_{2}⟩, M_{3}⟩,… ⟩.

λ^{1}βηπ is the calculus without terminal object and related rules, λ^{1}βη is the classical typed calculus, and λ_{βη} the type-free calculus. Finally, let I_{A} = λx:A.x be the identity of type A.

Remark 2.4. Notion of reduction for λ^{1}βηπ∗. The notion of reduction associated with the equational theory of λ^{1}βηπ∗ obtained by just orienting the equalities in the axioms to the right is not Church-Rosser. It is possible, though, to derive for this equality theory another notion of reduction that has the Church-Rosser property; in the following we will refer to this latter one when talking about reduction, normal forms, and so on for λ^{1}βηπ∗ (see [Pot81], [CDC91]).

Definition 2.5. Let A, B ∈ Tp. Then A and B are provably isomorphic (A ≅_{p} B) iff there exist closed λ-terms M : A → B and N : B → A such that λ^{1}βηπ∗⊢ M N = I_{B} and λ^{1}βηπ∗⊢ N M = I_{A}. We then say that M and N are invertible terms, and that M is an inverse of N, in λ^{1}βηπ∗.

Note that, as usual, the inverse of a term M (if it exists) is unique up to “=.” Suppose that types A and B are provably isomorphic and consistently substitute arbitrary types for the common base types. Then the isomorphism still holds: just use the corresponding terms with updated types. Borrowing terminology from Statman (1983) we may say that the notion of provable isomorphism is typically ambiguous. Theorem 2.6. (Main Theorem (easy implication)) T h_{×T}^{1}⊢ A = B ⇒ A ≅_{p} B .

Proof. We give the terms associated to each axiom and rule. As T h_{×T}^{1} is a theory of equality, one has first to observe that the usual axioms and inference rules yield and preserve provable isomorphisms:

•λx:A.x proves A = A; •if M, with inverse N, proves A = B , then N proves B = A; •if an invertible M proves A = B and an invertible N proves B = C, then the term N∘M = λx:A.N (M x), that is clearly invertible, proves A = C ; •if an invertible term M proves A = B and an invertible term N proves C = D, then the invertible term λx:A × C.⟨M(p_{1}x), N(p_{2}x)⟩ proves A × C = B × D; •if an invertible M proves A = B and an invertible N proves C = D, then λy:A → C.λx:B.N (y (M^{−1} x)), where M^{−1} is the inverse of M, proves A → C = B → D and it is invertible (take λy:B → D.λx:A.N^{−1} (y (M x)) ). We next check the proper axioms: 1A × B = B × A is proved by λx:A × B.⟨p_{2}x, p_{1}x⟩; 2A × (B × C) = (A × B) × C is proved by λx: A × (B × C).⟨⟨p_{1}x, p_{1}(p_{2}x)⟩, p_{2}(p_{2}x)⟩, that is invertible; 3(A × B) → C = A → (B → C) is proved by λz:(A × B) → C.λx:A.λy:B.z⟨x, y⟩ with inverse λz:A → (B → C).λx:A × B.z (p_{1}x) (p_{2}x); 4A → (B × C) = (A → B) × (A → C) is proved by λz:A → (B × C).⟨λx : A.(p_{1}(zx)), λx : A.(p_{2}(zx))⟩ with inverse λz:(A → B) × (A → C).λx:A.⟨(p_{1}z)x, (p_{2}z)x⟩; 5A × T = A is proved by p_{1} with inverse λx:A.⟨x, ∗_{A}x⟩ (to check invertibility, notice that ∗_{A}∘p_{1} = ∗_{A→T} = p_{2}); 6A → T = T is proved by ∗_{(A→T)} with inverse λx:T.∗_{A}; 7T → A = A is proved by λz:T → A.z(∗_{(T→A)}z) with inverse λx:A.λy:T.x. The rest of this section, as well sections 3 and 4, are dedicated to the proof of the

other implication of the Main Theorem. The first steps are done by reducing types to a “type normal form”. The axioms of T h_{×T}^{1} suggest the following rewrite system R for types (essentially T h_{×T}^{1} without commutativity): Definition 2.7. [Type rewriting R] Let “⇝” be the transitive and substitutive type-reduction relation generated by:

1A × (B × C) ⇝ (A × B) × C 2(A × B) → C ⇝ A → (B → C) 3A → (B × C) ⇝ (A → B) × (A → C)

4A × T ⇝ A 5T × A ⇝ A 6A → T ⇝ T 7T → A ⇝ A

The system R yields an obvious notion of normal form for types (type-n.f.), i.e. when no type reduction is applicable. Note that 4, 5 and 6 “eliminate the T’s”, while 2 and 3 “bring the × outside”. It is then easy to observe that each type-n.f. is T or has the structure S_{1} × … × S_{n} where each S_{i} does not contain T or “ × ”. We write nf(S) for the normal form of S (there is exactly one, see 2.8), and say that a normal form is non-trivial if it is not T.

Proposition 2.8. Each type has a unique type normal form in R.

Proof. Notice that in any R-reduction, starting with a given type S:

(i) Rules 2 and 3 can be applied only finitely many times, as they strictly decrease the number of × ’s in the scope of an arrow of S and this number is finite and is not increased by any other rule.

(ii) Between an application of rule 2 or 3 (yielding type S’) and the next one, the remaining rules can be applied only finitely many times ( 4, 5, 7 and 6 simply throw away some subformula reducing by one the number of products or arrows, which is finite; rule 1 is just associativity to the left).

So, after a finite reduction path we get a type S” with no redex for rules 2 and 3, and then, again, the remaining rules can be applied only finitely many times (at most the length of S” plus the times required for associating S” to the left). The resulting type nf(S) has then no products in the scope of any arrow (otherwise 2 and 3 could be applied), and is either T or a type with no occurrence of T (otherwise 4, 5, 7 and 6 could be applied). Thus nf(S) is a product of types, each of which has no occurrence of ×.

It is easy to observe that R is Church-Rosser too and, thus, that nf(S) is unique. (Note also that we have actually proved that R strongly normalizes)

From the implication proved above of the Main Theorem, since R ⊢ S ⇝ R implies T h_{×T}^{1} ⊢ S = R , it is clear that any reduction R ⊢ S ⇝ R is witnessed (or, proved, in the “types-as-propositions” analogy) by an invertible term of type S → R. Moreover, one clearly has:

Corollary 2.9. T h_{×T}^{1} ⊢ S = nf(S) and, thus, T h_{×T}^{1} ⊢ S = R ⟺ T h_{×T}^{1} ⊢ nf(S) = nf(R)

In conclusion, when T h_{×T}^{1} ⊢ S = R, either we have nf(S) ≡ T ≡ nf(R), or T h_{×T}^{1} ⊢ nf(S) ≡ S_{1} × … × S_{n} = R_{1} × … × R_{m} ≡ nf(R). A crucial lemma below will prove that, in this case, one also has n = m.

The assertion in the corollary can be reformulated for invertible terms in a very convenient way:

Proposition 2.10. (Commuting diagram) Given types A and B, assume that the invertible terms F : A → nf(A) and G : B → nf(B) prove the reductions to typenormal-form. Then a term M : A → B is invertible iff there exist an invertible term M’ : nf(A) → nf(B), such that M = G^{−1}∘M’∘F.

Proof. (⇐) Set M^{−1} ≡ (G^{−1} ∘ M′ ∘ F)^{−1} ≡ F^{−1} ∘ M^{′−1} ∘ G , then M is invertible. (⇒) Just set M′ ≡ G^{∘}M^{∘}F^{−1}. Then M^{′−1} ≡ F ∘ M^{−1} ∘ G^{−1} and M’ is invertible. The diagram in the following Figure 1 represents the situation in the corollary.

[figure: (B_{1} ×… × B_{m}); (A_{1} ×… × A_{n}); M’ = G∘M∘F^{−1}; M; B; A; G; F]

Fig. 1. Reduction to a subclass of isomorphic types.

Thus we have reduced isomorphisms between arbitrary types to the same problems with respect to type normal forms. We examine next how this may affect the structure of the terms which prove the isomorphisms.

3. More Lemmas: From λ^{1}βηπ∗ to the Classical λ^{1}βη

This is a technical section, where we display the statements of some crucial lemmas. Their proofs are postponed to the appendix. Our aim is to reduce invertibility in λ^{1}βηπ∗ to invertibility in λ^{1}βη.

Recall first that, when T h_{×T}^{1} ⊢ S = R, one has nf(S) ≡ T ≡ nf(R), or T h_{×T}^{1} ⊢ nf(S) ≡ S_{1} × … × S_{n} = R_{1} × … × R_{m} ≡ nf(R). Notice now that, in the latter case, there cannot be any occurrence of T in either type. Indeed, a non trivial type-n.f. cannot be provably equated to T, as can be easily seen by taking a non-trivial model. Thus we restrict our attention to equations like S_{1} × … × S_{n} = R_{1} × … × R_{m} with no occurrence of T and, hence, to invertible terms with no occurrence of the type constant T in their types. We can show that these terms do not contain any occurrence of ∗_{A} either, for any type A, via the following lemmas. Lemma 3.1. (Form of the terms of a product type) Given a term M of λ^{1}βηπ∗ in normal form such that M: A × B, then either M ≡ ⟨M_{1}, M_{2}⟩, for some M_{1}, M_{2}, or there is a free variable x : C in M such that A × B is a type subexpression of C.

Proof. By induction on the length of the structure of M (see appendix). Lemma 3.2. (There are no ∗_{A} in a term in n.f. if its type does not contain T)

Assume that in a term M of λ^{1}βηπ∗ in normal form there is an occurrence of ∗_{A}, for some type A. Then there is some occurrence of the type constant T in the type of M or in the type of some free variable of M.

Proof. By induction on the structure of M (see appendix).

Proposition 3.3. (Isomorphisms between type-n.f.’s are given by terms in λ^{1}βηπ)

Assume that S and R are non trivial type-n.f.’s. If the closed terms M and N prove S≅_{p}R in λ^{1}βηπ∗, then their normal forms contain no occurrences of the constants ∗_{A}. (Thus, M and N are actually in λ^{1}βηπ).

Proof. By the previous lemma, as the terms are closed and no T occurs in their type.

So we have factored out the first class of constants ∗_{A}, and we have restricted ourselves to λ^{1}βηπ. In the next step we eliminate pairing as well, in a sense.

There is a problem though. Our aim is to reduce the investigation of invertible terms in λ^{1}βηπ∗ to that of terms in λ^{1}βηπ. This is done on the grounds of Proposition 2.10 by examining each component of the product, where the isomorphism will be given by terms of λ^{1}βη. However, in the notation of Proposition 2.10, consider the term M’ : nf(A) → nf(B). M’ is invertible in (the equational theory of) λ^{1}βηπ∗ and, thus, also the subterms yielding the isomorphism of the components (see 3.7 and 3.8 below) are, a priori, invertible in λ^{1}βηπ∗, while we need to know that they are actually invertible in λ^{1}βη. We get rid of the problem by the following remark.

Remark 3.4. (The equational theory of) λ^{1}βηπ∗ is a conservative extension of (the equational theory of) λ^{1}βη. Similarly for λ^{1}βηπ with respect to λ^{1}βη.

Indeed, both λ^{1}βηπ∗ and λ^{1}βηπ are Church-Rosser, where “the theory of reduction” for λ^{1}βηπ is given by orienting the equalities in the axioms from left to right (for the C-R property see the references in the remark before 2.5) . Consider now M and N in λ^{1}βηπ such that λ^{1}βηπ∗⊢ N = M and let P be the common reductum. Then λ^{1}βηπ∗⊢ N →→ P is actually a reduction λ^{1}βηπ⊢ N →→ P, as N contains no T-redex, and no T-redex can be created by the application of reduction rules. The same applies to λ^{1}βηπ∗⊢ M →→ P and, thus, λ^{1}βηπ⊢ N = M. Similarly for λ^{1}βηπ w.r.t λ^{1}βη.

Notation 3.5. Recall that by x⃗, y⃗, M⃗... we denote vectors of variables, terms, etc.

Lemma 3.6. (Terms of λ^{1}βηπ whose type is arrow-only belong to λ^{1}βη) Let M be a term of λ^{1}βηπ in normal form such that M : A, where A is a type with no occurrence of × in it. If no free variable of M has a type with occurrences of ×, then M is actually a term in λ^{1}βη.

Proof. By induction on the structure of M (see appendix).

Proposition 3.7. (Isolate the relevant ⟨M_{1},…, M_{n}⟩ in an isomorphism) Let S ≡ S_{1} × … × S_{m} and R ≡ R_{1} × … × R_{n} be type-n.f.’s where neither the S_{i}’s nor the R_{j}’s contain any occurrences of T or × . Then S ≅_{p} R iff there exist M_{1}, …,M_{n} and N_{1}, …,N_{m} such that

x_{1} : S_{1},…, x_{m} : S_{m} ⊢M_{1}, …,M_{n} M_{i}[N⃗/x⃗] =_{βη} y_{i}, for 1 ≤ i ≤ n
y_{1} : R_{1},…, y_{n} : R_{n} ⊢N_{1}, …,N_{m} N_{j}[M⃗/y⃗] =_{βη} x_{j}, for 1 ≤ i ≤ m

(where substitution of vectors of equal length is meant componentwise).

Proof. (See appendix: it is not obvious).

In conclusion, we have isolated some interesting terms from which every constant has been factored out. Next we prove that provably equal types in normal form have equal length.

Lemma 3.8. (Isomorphic type-n.f.’s have equal length) Assume that R_{1} × … × R_{n} and S_{1} × … × S_{m} are type-n.f.’s and M ≡ ⟨M_{1},…, M_{n}⟩ , N ≡ ⟨N_{1},…, N_{m}⟩ are terms in λ^{1}βηπ such that

x_{1} : S_{1},…, x_{m} : S_{m} ⊢M_{1}, …,M_{n} M_{i}[N⃗/x⃗] =_{βη} y_{i}, for 1 ≤ i ≤ n
y_{1} : R_{1},…, y_{n} : R_{n} ⊢N_{1}, …,N_{m} N_{j}[M⃗/y⃗] =_{βη} x_{j}, for 1 ≤ i ≤ m

then n = m and there exist permutations σ, π over n (and terms P_{i}, Q_{j}) such that

M_{i} = λu⃗_{i}.x_{σ_{i}} P⃗_{i}  and  N_{j} = λv⃗_{j}.x_{π_{i}} Q⃗_{j}

Proof. By lemma 3.6 (recall that we may assume that each M_{i} and N_{j} is in normal form) one has that M_{i} and N_{j} are in λ^{1}βη. Then,

M_{i} = λu⃗_{i}.s_{i}P⃗_{i}  and  N_{j} = λv⃗_{j}.t_{j}Q⃗_{j}

Note that s_{i} is a free variable (namely some x_{j}), since M_{i}[N⃗/x⃗] =_{βη}y_{i}. Indeed, if s_{i} is bound then M_{i} is λu_{1} … s_{i}… u_{k}.s_{i}P⃗_{i} and M_{i}[N⃗/x⃗] is λu_{1} … s_{i}… u_{k}.s_{i}P⃗_{i}[N⃗/x⃗] so that s_{i} would still be a bound head variable, and there would be no way to reduce it to a term without abstraction. Similarly t_{j} is some y_{i}.

So there are two functions σ : n → m, π: m → n such that

M_{i} = λu⃗_{i}.x_{σ(i)}P⃗_{i} for 1 ≤ i ≤ n, N_{j} = λv⃗_{j}.y_{π(j)}Q⃗_{j} for 1 ≤ i ≤ m

In conclusion, for 1 ≤ i ≤ n we obtain:

y_{i}=_{βη} M_{i}[N⃗/x⃗] =_{βη} (λu⃗_{i}.x_{σ(i)}P⃗_{i})[N⃗/x⃗]
=_{βη} λu⃗_{i}.N_{σ(i)}{P⃗_{i}[N⃗/x⃗]}
=_{βη} λu⃗_{i}.(λv⃗_{σ(i)}.y_{π(σ(i))}Q⃗_{σ(i)}){P⃗_{i}[N⃗/x⃗]}
=_{βη} if v⃗_{σ(i)} is longer than P⃗_{i}
then λu⃗_{i}.v⃗′_{σ(i)}.y_{π(σ(i))}Q⃗_{σ(i)}[(P⃗_{i}[N⃗/x⃗])/u⃗_{i}]
else λu⃗_{i}.y_{π(σ(i))}{Q⃗_{σ(i)}[(P⃗_{i}[N⃗/x⃗])/u⃗_{i}]}{P⃗′_{i}[N⃗/x⃗]}

In either case of the last equality, each term can reduce to y_{i} iff y_{i} = y_{π(σ(i))} and each of the Q’s and P’s left orderly reduce to one of the bound variables, so that one can apply η, several times, at the end. The same holds for N_{j}[M⃗/y⃗] for 1 ≤ j ≤ m.

Thus i = π(σ(i)) , for 1 ≤ i ≤ n, and j = σ(π(j)), for 1 ≤ j ≤ m and we can conclude that m = n, σ is a permutation and π is its inverse.

We are then reduced to examining componentwise the terms which prove an isomorphism. The next point is to show that each component, indeed a term of λ^{1}βη by lemma 3.6, yields an isomorphism.

4. Finite Hereditary Permutations

In order to prove that the isomorphism between two type-n.f.’s can be expressed componentwise, we use a theorem in [Dez76]. The same result will also be applied to obtain, at last, the remaining part of the proof of our Main Theorem.

Definition 4.1. [Finite Hereditary Permutations (f.h.p.)] Let M be an untyped term. Then M is a finite hereditary permutation (f.h.p.) iff either

•λ^{1}βη⊢ M = λx.x , or •λ^{1}βη⊢ M = λz.λx⃗.zN⃗_{σ}, where if ∥x⃗∥ = n then σ is a permutation over n and zN⃗_{σ} = (… (zN_{σ(1)}) … N_{σ(n)}), such that, for 1 ≤ i ≤ n, λx_{i}.N_{i} is a finite hereditary permutation. Thus λz.λx_{1}.λx_{2}.zx_{2}x_{1} and λz.λx_{1}.λx_{2}.zx_{2}λx_{3}.λx_{4}.x_{1}x_{4}x_{3} are f.h.p.’s. F.h.p.’s can

also be tidily described in terms of Böhm-trees. Recall that a Böhm-tree of a term M is (informally) given by:

BT(M) = Ω if M has no head normal form

BT(M) = λx_{1} … x_{n}.y  if M =_{β}λx_{1} … x_{n}.yM_{1} … M_{p} /...\ BT (M_{1}) … BT (M_{p})

Recall also that BT(M) is finite and Ω-free iff M has a normal form. Then one may look at f.h.p.’s as Böhm-trees, as follows:

λzx⃗.z
/… \
λy⃗_{1}.x_{σ(1)} … λy⃗_{n}.x_{σ(1)}
⋮  ⋮

and so on, up to a finite depth (note that y⃗_{i} may be an empty string of variables). Clearly f.h.p.’s are closed terms and they possess normal form. In particular, exactly the abstracted variables at level n + 1 appear at level n + 2 , modulo some permutation of the order (note the special case of z at level 0). The importance of f.h.p.’s arises from the following theorem. (Clearly, the notion of invertible term given in 2.5 easily translates to the untyped λ-calculus).

Theorem 4.2. (Dezani [Dez76]) Let M be an untyped term possessing normal form. Then M is λ_{βη}-invertible iff M is a f.h.p.

Remark 4.3. One may easily show that the f.h.p.’s are typable terms (Hint: Just follow the inductive definition and give z, for instance, type A_{1} → (A_{2} … → B), where the A_{i}’s are the types of the N_{σ(i)}.) By the usual abuse of language we may then speak of typed f.h.p.’s.

Recall now that all typed terms possess a (unique) normal form (see [Bar84]). As we now need an interplay between typed and type-free terms, we are going to be more explicit about which sort of terms we are dealing with, when needed. Let M be a typed λ-term. We write e(M) for the erasure of M, i.e. for M with all type labels on variables erased.

Remark 4.4. Observe that the erasures of all axioms and rules of the typed lambda calculus are themselves axioms and rules of the untyped lambda calculus. Then, in particular, if M and N are terms of λ^{1}βη and λ^{1}βη⊢ M = N, one has λ_{βη}⊢ e(M) = e(N).

Theorem 4.5. If M : A → B and N : B → A are invertible terms in λ^{1}βη, then e(M) and e(N) are f.h.p.’s.

Proof. e(N M) = e(N)∘e(M), and hence, by the remark, λ_{βη} ⊢ e(M)∘e(N) = e(I_{σ}) = I and λ_{βη} ⊢ e(N)∘e(M) = e(I_{σ}) = I. Thus by Theorem 4.2, e(M) and e(N) are f.h.p.’s.

The first application of 4.2 we need is the following.

Proposition 4.6. Let M_{1}, …,M_{n} and N_{1}, …,N_{n} and permutation σ satisfy all the assumptions in lemma 3.8. Then λx_{σ(i)}.M_{i}:S_{σ(i)} → R_{i} and λy_{i}.N_{σ(i)}:R_{i} → S_{σ(i)} are invertible terms.

Proof. For a suitable typing of the variables it is possible to build the following terms of λ^{1}βη :

M = λz.λx_{1} … x_{n}.zM_{1}… M_{n}, N = λz.λy_{1} … y_{n}.zN_{1}… N_{n}.

It is an easy computation to check, by the definition of the M_{i}’s and of the N_{i}’s, that M and N are invertible. Moreover, they are (by the construction given in the Appendix) in normal form, thus, by Dezani’s theorem, (the erasures of) M and N are f.h.p.’s. This is enough to show that every M_{i} has only one occurrence of the x_{i}’s (namely x_{σ(i)}); similarly for the N_{i}’s.

Thus we obtain M_{i}[N⃗/x⃗] ≡ M_{i}[N_{σ(i)}/x_{σ(i)}] =_{βη} y_{i}, for 1 ≤ i ≤ n, and N_{i}[M⃗/y⃗] ≡ N_{i}[M_{π(i)}/y_{π(i)}] =_{βη} x_{i}, for 1 ≤ i ≤ n,

Hence, for each i, λx_{σ(i)}.M_{i}:S_{σ(i)} → R_{i} and λy_{i}.N_{σ(i)}:R_{i} → S_{σ(i)} are invertible.

As a result of all the work done so far, we can then focus on invertible terms whose types contain only “ → ”, i.e. investigate componentwise the isomorphisms of type-n.f.’s. Of course, these isomorphisms will be given just by a fragment of the theory T h_{×T}^{1}.

Definition 4.7. Let Swap be the subtheory of T h_{×T}^{1} given by just the following proper axiom (plus the usual axioms and rules for “=”),

(swap) A → B → C = B → A → C.

Swap is a subtheory of T h_{×T}^{1} by axioms 1 and 3 of T h_{×T}^{1}.

Proposition 4.8. Let A, B be type expressions with no occurrences of T or ×. Then A ≅_{p} B ⇒ Swap ⊢ A = B.

Proof. Suppose A ≅_{p} B via M and N. As usual, we may assume without loss of generality that M and N are in normal form. By lemma 3.6, M and N actually live in λ^{1}βη and, by theorem 4.5, e(M) and e(N) are f.h.p.’s. We prove Swap ⊢ A = B by induction on the depth of the Böhm-tree of M.

Depth 1: M ≡ λz : C. z. Thus M : C → C. Now, Swap ⊢ C = C by reflexivity.

Depth n+1: M ≡ λz : E. λx⃗:D⃗. zN⃗_{σ}. Recall zN⃗_{σ} = (… (zN_{σ(1)}) … N_{σ(n)}) where if the ith abstraction in λx⃗:D⃗ is λx_{i}:D_{i} then the erasure of λx_{i}:D_{i}.N_{i} is a f.h.p. Let F_{i} be the type of N_{i}. In order to type check, we must have E = (F_{σ(1)} → … → F_{σ(n)} → B) for some B. Thus the type of M is (F_{σ(1)} → … → F_{σ(n)} → B) → (D_{σ(1)} → … → D_{σ(n)} → B). Since λx_{i}:D_{i}.N_{i} is a f.h.p, λx_{i}:D_{i}.N_{i} gives (half of) a provable isomorphism from _{i} to F_{i}. By induction, since the height of the Böhm tree of (of the erasure of) each λx_{i}:D_{i}.N_{i} is less than the height of the Böhm tree of M, one has Swap ⊢ D_{i} = F_{i} for 1 ≤ i ≤ n. By repeated use of the rules for “=”, we get

Swap ⊢ (F_{σ(1)} → … → F_{σ(n)} → B) = (D_{σ(1)} → … → D_{σ(n)} → B)

Hence it suffices to show

Swap ⊢ (D_{σ(1)} → … → D_{σ(n)} → B) = (D_{1} → … → D_{n} → B)

This is quite simple to show by repeated use of axiom (swap) above in conjunction with the rules for equality. Clearly, also the converse of proposition 4.8 holds, since the “⇐” part in 4.8 is provable

by a fragment of the proof in theorem 2.6. Thus one has:

Swap ⊢ A = B⟺ A ≅_{p} B by terms in λ^{1}βη.

The result we aim at is just the extension of this fact to T h_{×T}^{1} and λ^{1}βηπ∗. Theorem 4.9. (Main Theorem) S ≅_{p} R ⟺ T h_{×T}^{1} ⊢ S = R

Proof. In view of theorem 2.6, we only need to prove S ≅_{p} R ⇒ T h_{×T}^{1} ⊢ S = R. By proposition 2.10, this is equivalent to proving nf(S) ≅_{p} nf(R) ⇒ T h_{×T}^{1} ⊢ nf(S) = nf(R).

Now, for nf(S) ≡ S_{1} × … × S_{n} and R_{1} × … × R_{m} ≡ nf(R), we have shown, in lemmas 3.7, 3.8 and proposition 4.6, that nf(S) ≅_{p} nf(R) ⇒ n = m and there exist M_{1}, …,M_{n}, N_{1}, …,N_{n} and a permutation σ such that λx_{σ(i)}.M_{i}:S_{σ(i)} → R_{i} and λy_{i}.N_{σ(i)}:S_{i} → R_{σ(i)}.

By 4.6, these terms are invertible too, for each i. Thus, by 4.8, Swap ⊢ R_{i} = S_{σ(i)} and, hence, by the rules, T h_{×T}^{1} ⊢ S = R.

This concludes the proof of the main theorem. Here is an immediate consequence. Corollary 4.10. Given types A and B, it is decidable whether they are isomorphic in all models of λ^{1}βηπ∗. (And thus whether A and B name isomorphic objects in all CCC’s.)

Proof. Let the type-n.f. of A be R_{1} × … × R_{n} and that of B be S_{1} × … × S_{n} where neither the R_{i}’s nor the S_{j}’s contain any occurrences of T or × . (If one of A or B is T, the other must be as well if they are to be isomorphic.) By propositions 3.7 and 3.8, and theorem 4.9, A and B are isomorphic iff m = n and there is a permutation σ over n such that for 1 ≤ i ≤ n, R_{i} ≅_{p} S_{σ(i)}. By proposition 4.8, we know that Swap ⊢ R_{i} = S_{σ(i)}. Note that the axioms and rules of Swap do not change the length of type expressions. Hence if Swap ⊢ R_{i} = S_{σ(i)} , R_{i} and S_{σ(i)} have the same length. We provide a decision procedure to determine if Swap ⊢ R = S (and hence whether they are isomorphic in all models) by induction on the length of R (and hence S). We restrict ourselves to type expressions of the same length since otherwise they are not provably equal. If R and S are both type symbols then they are equal if and only if they are the same symbol. Suppose we have a decision procedure for all types of length less than n, and R and S have length n. Decompose R and S into terms of the form R_{1} → … → R_{k} and S_{1} → … → S_{m} where R_{k} and S_{m} are type symbols. If R_{k} and S_{m} are different or k ≠ m then it is not the case that Swap ⊢ R = S. Otherwise, for each R_{i} determine if there is a distinct S_{j} such that ⊢ R_{k} = S_{m}. Each of these tests is decidable by hypothesis. If each R_{i} can be paired with a distinct S_{j}, then Swap ⊢ S = R. Otherwise it fails. The proof of the correctness of this decision proceed follows the same lines as the proof of the (⇒) direction of proposition 4.8.

Indeed, more can be said about the connection to Category Theory. We also hint here of a simple application to Proof Theory, but refer to [DCL89] for more discussions on both topics.

Take the intuitionistic positive calculus, IPC, i.e. Intuitionistic Logic with only →, × (i.e. conjunction), and True, and consider the following notion of strong equivalence (see [Mar91], [LE85] and [AB91]). Definition 4.11. Two formulas A and B of IPC are strongly equivalent iff there are proofs f of the sequent A ⊢ B and g of the sequent B ⊢ A such that the proofs g∘f and f∘g obtained by composition reduce, by cut-elimination, to the one step deductions A ⊢ A and B ⊢ B.

Notice that this notion of equivalence is much stronger than the classical notion of logical equivalence: all tautologies of IPC are logically equivalent, for example, but only a few are strongly equivalent. Corollary 4.12. (Connection with deductive systems) Two formulas A and B of IPC are strongly equivalent iff T h_{×T}^{1} ⊢ A = B.

Appendix

We give here the proofs of the lemmas in section 3. The numbers refer to that section.

Lemma 3.1(Form of the terms of a product type) Given a term M of λ^{1}βηπ∗ in normal form such that M: A × B, then either M ≡ ⟨M_{1}, M_{2}⟩, for some M_{1}, M_{2}, or there is a free variable x : C in M such that A × B is a type subexpression of C.

Proof. By induction on the length of the structure of M. Basis of induction: if M is of length 1, then it can be only a free variable of type A×B. Inductive step: M ≡ λx⃗.rP⃗, as it is in normal form. Observe first that this case reduces

to M ≡ rP⃗, as its type is α × β, and we proceed by case analysis on r as follows: r is a variable: then r is free and has type type(P_{1}) → (... → (type(P_{n}) → A × B)...). r is ⟨M_{1}, M_{2}⟩: then M ≡ ⟨M_{1}, M_{2}⟩, in order to type check. r is p_{1} or p_{2}: then M ≡ (...(p_{i}M_{1})M_{2}...M_{k}) with M_{1}:S × U in normal form with

S or U ≡ type(M_{2}) → (... → (type(M_{k}) → A × B)...). By induction hypothesis either M_{1} is ⟨N_{1}, N_{2}⟩ or M_{1} has a free variable x : C with S × U (hence A × B too) a type subexpression of C. The first case is not possible, as p_{i}⟨N_{1}, N_{2}⟩ is a redex, so M has a free variable x : C with A × B a type subexpression of C.

r is a constant ∗_{A} for some type A: this is not possible as ∗_{A} has type A → T, which would prevent M from having type A × B.

Lemma 3.2(There are no ∗_{A} in a term in n.f. if its type does not contain T) Assume that in a term M of λ^{1}βηπ∗ in normal form there is an occurrence of ∗_{A}, for some type A. Then there is some occurrence of the type constant T in the type of M or in the type of some free variable of M.

Proof. By induction on the structure of M.

Basis for induction: ∗_{A} has type A → T. Inductive step: M ≡ λx⃗.rP⃗, as M is in normal form, and we proceed by case analysis

on r as follows:

r is a variable: then r has type type(P_{1}) → (... → (type(P_{n}) → C)...); by hypothesis, the P_{i}’s are in normal form and in some P_{j} there are occurrences of a constant ∗_{A}, so by induction hypothesis there are T’s in type(P_{j}), hence in the type of r. By this, either r is a free variable or (since r occurs among the x⃗) there are T’s in the type of M.

r is ⟨P, Q⟩: then M ≡ λx⃗.⟨P, Q⟩ where P and Q are in normal form. The type of M is D_{1} → ... → D_{n} → (A × B), with P : A and Q : B, and ∗_{A} occurs in P or Q. By inductive hypothesis, either T occurs in A × B (hence in the type of M, too) or in the type of some free variable y of P or Q. In either case, as above, some T’s occur in the type of M or in the type of y, which is free in M.

r is p_{1} or p_{2}: then M ≡ λx⃗.((p_{i}M_{1})M_{2}...M_{k}) where:

• M_{j} is in normal form, for each j.

• M_{1} : S × U with either S or U ≡ type(M_{2}) → (... → (type(M_{k}) → C)...).

• ∗_{A} occurs in M_{j} for some j; consider than

case j = 1: then T occurs in S × U, by induction hypothesis. By lemma 3.1, as M cannot be a redex, M_{1} is not a pair and has a free variable y : C with S × U a type subexpression of C. Notice that y is also free in ((p_{i}M_{1})M_{2}...M_{k}). Thus as in the earlier cases either y is free in M or some T’s occur in the type of M (because y is one of the variables in x⃗);

case j > 1: then by induction hypothesis either (a)there is a T occurring in the type of M_{j}, and, hence, in S × U or (b)there is a free variable y of M_{j} with type T occurring in its type. In case (a), we can conclude the proof as in the case for j = 1 above. In case (b), if y is free in M_{j} then it is also free in ((p_{i}M_{1})M_{2} … M_{k}). We can thus conclude the proof again as for i = 1.

r is ∗_{A}: then M ≡ λx⃗. ∗_{A} M_{1} or M ≡ λx⃗.∗_{A} and the type of M is D_{1} → ...D_{n} → T, for some D_{1},…, D_{n}.

Lemma 3.6(Terms of λ^{1}βηπ whose type is arrow-only belong to λ^{1}βη) Let M be a term of λ^{1}βηπ in normal form such that M : A, where A is a type with no occurrence of × in it. If no free variable of M has a type with occurrences of ×, then M is actually a term in λ^{1}βη.

Proof. By induction on the structure of M. Basis for induction: if M is of length 1, then it can be only a variable of type A, as

any constant has a type with occurrences of ×. Inductive step: M ≡ λx⃗.rP⃗, as M is in normal form, and we proceed by case analysis

on r as follows:

r is a variable: then r has type type(P_{1}) → (... → (type(P_{n}) → C)...) and no matter if r is free or bound, by hypothesis on the type of M and its free variables, the P_{i}’s (which are in normal form) have a type with no × ’s and free variables whose type have no ×’s, so by induction hypothesis they contain no constants nor pairs, hence M contains no constants or pairs either.

r is ⟨P, Q⟩: this is impossible, otherwise M ≡ λx⃗.⟨P, Q⟩ and the type of M would be

S_{1} → ... → S_{n} → (A × B), which contains ×. r is p_{1} or p_{2}: this cannot be either, since:

• M ≡ λx⃗.p_{i} must have a type containing ×,

• M ≡ λx⃗.((p_{i}M_{1})M_{2}...M_{k}) implies, by lemma 3.1, that either M_{1} is ⟨N_{1}, N_{2}⟩ or M_{1} has a free variable x : C with S × U a type subexpression of C. The first case is not possible, as p_{i}⟨N_{1}, N_{2}⟩ is a redex while M is in normal form. Thus M_{1} has a free variable x : C with S × U a type subexpression of C, and, hence, either x ∈ F V (M) or S × U is a type subexpression of the type of M, since the type of M includes the types of bound variables. Impossible.

Proposition 3.7(Isolate the relevant ⟨M_{1},…, M_{n}⟩ in an isomorphism) Let S ≡ S_{1} × … × S_{m} and R ≡ R_{1} × … × R_{n} be type-n.f.’s where neither the S_{i}’s nor the R_{j}’s contain any occurrences of T or ×. Then S ≅_{p} R iff there exist M_{1}, …,M_{n} and N_{1}, …,N_{m} such that

x_{1} : S_{1},…, x_{m} : S_{m} ⊢M_{1}, …,M_{n} M_{i}[N⃗/x⃗] =_{βη} y_{i}, for 1 ≤ i ≤ n
y_{1} : R_{1},…, y_{n} : R_{n} ⊢N_{1}, …,N_{m} N_{j}[M⃗/y⃗] =_{βη} x_{j}, for 1 ≤ i ≤ m

(where substitution of vectors of equal length is meant componentwise).

Proof. (⇒) Let M^{∘}: S → R and N^{∘} : R → S be closed terms (in normal form) of λ^{1}βηπ∗ such that M^{∘}∘N^{∘} = I_{R} and N^{∘}∘M^{∘} = I_{S}. Then by standard currying, consider the term λx_{1}...x_{m}.M < x_{1}, ...x_{m} >: (S_{1} → … → (S_{m} → (R_{1} ×… ×R_{n})...), and observe that the normal form M’ of M < x_{1}, ...x_{m} > : R_{1} × ... × R_{n}, by lemma 3.1, must be of the form < M_{1}, ..., M_{n} >, with FV(M’) = {x_{1} : S_{1}, ...x_{m} : S_{m}} (by assumption, the S_{i}’s contain no occurrences of ×). The same applies for N.

As for the other properties, let

M′′ ≡ λz.(λx_{1}...x_{m}.M^{∘} < x_{1}, ...x_{m} >)(p_{1}z)...(p_{m}z)

and

N′′ ≡ λz.(λy_{1}...y_{n}.N^{∘} < y_{1}, ...y_{n} >)(p_{1}z)...(p_{n}z),

where the x_{i}’s, y_{j}’s, and z are chosen to be distinct. Then

M′′ =_{β} λz.M^{∘} < p_{1}z, ...p_{m}z >=_{η} λz.M^{∘}z =_{η} M^{∘},

and similarly

N′′ =_{β} λz.N^{∘}z =_{η} N^{∘}.

Compute then

M^{∘}∘N^{∘} =_{βη} M′′∘N′′ ≡ λx.(M′′(N′′x)) for x a variable not occurring in M” or N”.
=_{βη} λx.(λz.(λx_{1}...x_{m}.M′)(p_{1}z)...(p_{m}z))(N′′x)
=_{βη} λx. < M_{1}[p⃗_{j}(N′′x)/x⃗_{j}], ..., M_{n}[p⃗_{j}(N′′x)/x⃗_{j}] >

where the substitution is done simultaneously for all 1 ≤ j ≤ m,

=_{βη} λx. < M_{1}[N⃗[p⃗_{i}x/y⃗]/x⃗],…, M_{n}[N⃗[p⃗_{i}x/y⃗]/x⃗] >
since \begin{aligned}N′′x & =_{βη} & λy_{1}...y_{n}.N′(p_{1}x) … (p_{n}x) \\ & =_{βη} & < N_{1}[p⃗_{i}x/y⃗], ..., N_{m}[p⃗_{i}x/y⃗] > \end{aligned}

where substitution is done simultaneously for all 1 ≤ i ≤ n,

=_{βη} λx. < M_{1}[N⃗/x⃗][p⃗_{i}x/y⃗_{i}],…, M_{n}[N⃗/x⃗][p⃗_{i}x/y⃗_{i}] >

by substitution properties, as noy_{i} is free in M′

=_{βη} λx. < p_{1}x, ..., p_{n}x >

since M^{∘}∘N^{∘} =_{βη} λx.x and x =_{βη}< p_{1}x, ..., p_{n}x > .

Observe now that the equality just proved implies, componentwise, that M_{k}[N⃗/x⃗][p⃗_{i}x/y⃗_{i}] =_{βη} p_{k}x. For the purpose of the final argument of the proof, we refer now to →→^{βηπ∗} as a “several steps reduction” in λ^{1}βηπ∗. In view of the Church-Rosser property for this calculus, the last equality is equivalent to

M_{k}[N⃗/x⃗][p⃗_{i}w/y⃗_{i}] →→^{βηπ∗}p_{k}w.

where w is a fresh variable (to avoid confusion between x⃗ and x; in other words, w is not free in M_{k} nor in any N_{i} and cannot be free in any reduct of M_{k}[N⃗/x⃗] either.)

Notice now that by hypothesis the terms M⃗ and N⃗ are in normal form and have no T or × involved in their types or in the types of their free variables (the S⃗_{i} and R⃗_{i}), so by lemma 3.6 they are actually terms of λ^{1}βη. This allows us to conclude that the substitution [p⃗_{i}w/y⃗_{i}] creates no new redexes: the p⃗_{i}w could only create new redexes for surjective pairing reductions, i.e. when they appear in < p_{1}w, ..., p_{n}w >. But VecM and N⃗ do not contain any pair, so surjective pairing reductions cannot apply.

This fact has an important consequence: the reductions are actually performed in-

side M_{k}[N⃗/x⃗], so if we have M_{k}[N⃗/x⃗][p⃗_{i}w/y⃗_{i}] →→^{βηπ∗}Q, then M_{k}[N⃗/x⃗] →→^{βηπ∗}Q′ with Q ≡

Q′[p⃗_{i}w/y⃗_{i}].

This implies, in the case of M_{k}[N⃗/x⃗][p⃗_{i}w/y⃗_{i}] →→^{βηπ∗}p_{k}w, the reduction M_{k}[N⃗/x⃗] →→^{βηπ∗}Q′ with p_{k}w ≡ Q′[p⃗_{i}w/y⃗_{i}], that is M_{k}[N⃗/x⃗] →→^{βηπ∗}p_{k}w. In conclusion, M_{k}[N⃗/x⃗] = y_{k}, as required.

Symmetrically, one obtains N_{j}[M⃗/y⃗] =_{βη} x_{j} from N^{∘}∘M^{∘} = λx.x.

(⇐) Just step through the above proof in reverse order, defining the required closed terms by

M ≡ λz.(λx_{1}...x_{m}. < M_{1}, ...M_{n} >)(p_{1}z)...(p_{m}z),
N ≡ λz.(λy_{1}...y_{n}. < N_{1}, ...N_{m} >)(p_{1}z)...(p_{n}z).

Acknowledgements

The authors would like to express their gratitude to Gregory Mints for pointing out to us the work of Soloviev, and Rittri for informing us of his own work in the topic. We would also like to thank Albert Meyer and John Mitchell for several helpful conversations on these matters.

REFERENCES

AB91 Franco Alessi and Franco Barbanera. Strong conjunction and intersection types. Diparti-

mento di Informatica, Universitá di Torino (Italy), manuscript., 1991. AL91 Andrea Asperti and Giuseppe Longo. Categories, Types, and Structures. MIT Press, 1991. Bar84 Henk Barendregt. The Lambda Calculus; Its syntax and Semantics (revised edition). North

Holland, 1984. BL85 Kim Bruce and Giuseppe Longo. Provable isomorphisms and domain equations in models

of typed languages. ACM Symposium on Theory of Computing (STOC 85), May 1985. BS82 A. A. Babaev and S. V. Soloviev. Coherence theorem for canonical maps in cartesian closed

categories. Journal of Soviet Mathematics, 20, 1982. CDC91 Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-

calculus with surjective pairing and terminal object. In Leach, Monien, and Artalejo, editors, ICALP, pages 291–302. Springer-Verlag, 1991.

DCL89 Roberto Di Cosmo and Giuseppe Longo. Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). Workshop on Logic for Computer Science - MSRI, Berkeley, November 1989.

Dez76 Mariangiola Dezani-Ciancaglini. Characterization of normal forms possessing an inverse

in the λβη calculus. Theoretical Computer Science, 2:323–337, 1976. LE85 E. G. K. Lopez-Escobar. Proof functional connectives. Lecture Notes in Mathematics,

1130:208–221, 1985. LS86 Joachim Lambek and Philip J. Scott. An introduction to higher order categorical logic.

Cambridge University Press, 1986. Mar72 C.F. Martin. Axiomatic bases for equational theories of natural numbers. Notices of the

Am. Math. Soc., 19(7):778, 1972. Mar91 Simone Martini. Strong equivalence in positive propositional logic: provable realizability

and type assignment. Dipartimento di Informatica, Universitá di Pisa (Italy), Internal Note., June 1991.

NPS89 Paliath Narendran, Frank Pfenning, and Rick Statman. On the unification problem for

cartesian closed categories. Hardware Verification Workshop, September 1989. Pot81 Garrel Pottinger. The Church Rosser Theorem for the Typed lambda-calculus with Sur-

jective Pairing. Notre Dame Journal of Formal Logic, 22(3):264–268, 1981. Rey84 J.C. Reynolds. Polymorphism is not set-theoretic. Lecture Notes in Computer Science,

173, 1984. Rit89 Mikael Rittri. Using types as search keys in function libraries. Journal of Functional

Programming, 1(1), 1989. Rit90 Mikael Rittri. Retrieving library identifiers by equational matching of types in 10th Int.

Conf. on Automated Deduction. Lecture Notes in Computer Science, 449, July 1990. Sol83 Serjey V. Soloviev. The category of finite sets and cartesian closed categories. Journal of

Soviet Mathematics, 22(3):1387–1400, 1983. Sta83 Rick Statman. λ-definable functionals and βη conversion. Arch. Math. Logik, 23:21–26,

1983.