Eta

A Syntactic Approach to Eta Equality in Type Theory Healfdene Goguen AT&T Labs 180 Park Ave. Florham Park NJ 07932 USA

[email protected]

ABSTRACT This paper outlines an elementary approach for showing the decidability of type checking for type theories with βηequality, relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic translation mapping terms in the βη presentation into their full η-expansions in the β presentation. Decidability of type checking is lifted from the target β presentation to the βη presentation. The approach extends to other inductive kinds with a single constructor, and is demonstrated for singletons and dependent pairs.

Categories and Subject Descriptors F.4.1 [Theory of Computation]: Lambda calculus and related systems

General Terms Theory, Languages

Keywords Logical frameworks, type checking, decidability, beta-eta equality

1.

INTRODUCTION

In this article we introduce an elementary approach to the metatheory of type theories with βη-style equalities. These weakly extensional equational theories have applications to programming languages, especially for understanding modules systems like that of Standard ML [20], to categorical combinators [18] and systems of explicit substitution [1], and to the foundations of type theory-based proof assistants [19]. Our intention in this article is to justify the weakly extensional η rules by translating them into a system with only the traditional β-style computation rules. Practically, our approach provides a short and direct proof of the decidability

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. POPL’05, January 12–14, 2005, Long Beach, California, USA. Copyright 2005 ACM 1-58113-830-X/05/0001 ...$5.00.

of type theories with the additional equality rules. This contrasts with other approaches to η-reduction by not requiring extensive redevelopment for a βη-system given existing results for the β-system. Philosophically, our approach explains uniqueness rules without a clear computational justification in terms of the well-understood computational rules. We begin by studying Martin-L¨ of’s Logical Framework with Π-kinds and βη equality. In this case βη reduction is strongly normalizing and Church–Rosser, and so we could use this relation directly to implement an algorithm for testing conversion. We follow by studying the extension of the Logical Framework with singletons and dependent pairs at the level of kinds, similar to that of Stone and Harper [22], although our singletons include explicit term constructors and elimination constants. This language has the key difficulties that the equalities are type-directed and that the η-equalities directed as reductions do not have the Church–Rosser property, and so conversion must be implemented by a customized algorithm, as done by Stone and Harper, or by conversion in the target language as we do here. Our development of the metatheory begins by defining the source language with the additional η-style equalities over fully decorated terms, as introduced by Streicher [23] but with full labels for variables and abstraction. Each term constructor contains explicit labels allowing the reconstruction of the premises in the rule of inference; for example, the application constructor AppB x:A (M, N ) allows us to infer that M must have kind Πx : A.B and N must have kind A, even from a judgement Γ ` AppB x:A (M, N ) : C. Because of this explicit information in the term structure, we are able to define a total translation from terms in the source language into the target language, without reference to derivations of well-kindedness. We reuse the basic definition of type-directed η-expansion, like that used in defining η-long normal forms [6, 9]. The new approach taken here is to apply that expansion to every subterm of the source term. The labels in the fully decorated terms are used to provide the kind information for the η-expansion of each term constructor. We give a simple proof that the translation function preserves substitution, and the soundness of the translation follows by induction on derivations of the source language. The target language of the interpretation is formed from β-equality over unlabeled terms, i.e. the terms of the untyped λ-calculus. This is necessary because β-reduction under the translation does not preserve the kind labels of ηreduction: writing ηA (M ) for the η-expansion of M at kind

B A A, we only have that ηΠx:C.D (AppD x:C (λx:A (M ), x )) reduces D B to λx:C (M ), not to λx:A (M ) as would be required by a fully decorated term language.

extend the proofs to singletons and dependent pairs, and in Section 8 we summarize and outline future work.

1.1

2.

Related Work

Deciding βη-equality is a long-standing problem in type theory. While various approaches have been studied extensively, including interpreting the η-style equality rules as either reduction rules [10, 12, 21] or expansion rules [11], each of these approaches suffers from deficiencies. The systems arising from interpreting η-equality rules as reductions can fail to be confluent [17, 18], invalidating the primary advantage of the reduction approach. Interpreting the η-equality rules as expansions appears natural for simple type systems, but it becomes increasingly unnatural for more complex type theories: for example, Ghani’s treatment of η-expansions for the Calculus of Constructions [11] requires kinds of expanded abstractions to be in normal form. Barthe [2] and Joachimski [16] study strong normalization for η expansions given the strong normalization of βη reduction for the type theory with βη equality, and so their results will also follow for type theories with β equality where our approach applies. Salvesen [21] gives a syntactic proof of Church–Rosser for βη-reduction, but this proof makes the much stronger assumption that βη-reduction is strongly normalizing, instead of just β-reduction. In practice this assumption is difficult to establish without Church–Rosser for most systems. Geuvers [10] also relates systems with βη-reduction to those with βreduction, but his proof is much more complex and relies on properties of untyped conversion. Di Cosmo and Kesner [8] also use η-expansions in a translation to a target language, where a simply-typed source language with η expansions is shown confluent and strongly normalizing; since the article treats simple types it is not clear whether it would extend to dependent types, since the system with βη equality has different valid judgements than the system with β equality. Coquand, Pollack and Takeyama [6] use partial equivalence relations to show that weakly extensional equality in a type theory can be modeled by untyped β-equality, and they show the correctness and decidability of type checking for a Logical Framework with singletons and dependent pairs. Coquand [5] and Harper and Pfenning [15] treat the decidability of type checking by defining logical relations directly over specific choices of algorithms for type checking. This article only treats the decidability of type checking for βη equality, as opposed to studying particular algorithms for type checking. A subsequent article [14] begins to study justifying algorithms for type checking more sophisticated than simple reduction to common normal form, including Coquand’s and Harper and Pfenning’s for the Logical Framework, on the basis of βη normalization.

1.2

SYNTAX

The term language of the Logical Framework is given by the following grammar: A, B, C, D ∈ M, N, P, Q ∈ Γ, ∆, Φ ∈

::= ::= ::=

Type | El(M ) | Πx : A.B B xA | λB x:A (M ) | Appx:A (M, N ) () | Γ, x : A

We identify terms and kinds that are equivalent up to the renaming of bound variables, and we write M ≡ N if M and N are equal in this way. We write FV(M ) for the free variables in a term M , those variables not bound by abstractions. We write [N/x]M for the usual capture-free substitution of N for occurrences of the variable x in M . Each of these operations is lifted to kinds and contexts in the natural way. As we have mentioned earlier, in this article we consider two versions of Martin-L¨ of’s Logical Framework, with judgements Γ `+ M =β N : A and Γ `+ M =βη N : A. We write Γ `+ M = N : A for the remainder of this section, with the understanding that the rules of inference presented here define =βη , and that =β is defined by the same rules without the rule of inference η. The Logical Framework has several judgements: • `+ Γ valid, meaning Γ is a valid context, • Γ `+ A kind, meaning A is a valid kind in context Γ, • Γ `+ M : A, meaning M is a valid term of kind A in context Γ, • Γ `+ A = B kind, meaning A and B are equal in context Γ, and • Γ `+ M = N : A, meaning M and N are equal and of kind A in context Γ. The derivations are given by the following rules of inference. (Emp) `+ () valid (Ext)

Γ `+ A kind x 6∈ FV(Γ) `+ Γ, x : A valid

(Type)

Overview

In Section 2 we introduce the judgements for the Logical Framework over two separate term languages, fully decorated and unlabeled terms. In Section 3 we introduce the basic metatheory, primarily for the target language. In Sections 4 and 5 we show the soundness and completeness of βequality on unlabeled λ-terms for the fully decorated terms under βη-equality, and in Section 6 we show that type checking for the full source language is decidable. In Section 7 we

Kind Term Ctxt

(El)

(Π)

`+ Γ valid Γ `+ Type kind

Γ `+ M : Type Γ `+ El(M ) kind

Γ `+ A kind Γ, x : A `+ B kind Γ `+ Πx : A.B kind

Figure 1: Contexts and Kinds

(Type)

Γ

`+

`+ Γ valid Type = Type kind

Γ `+ M = N : Type (El) Γ `+ El(M ) = El(N ) kind (Π)

(Var)

Γ `+ A = C kind Γ, x : A `+ B = D kind + Γ, x : A ` M = N : B (λ) D Γ `+ λB x:A (M ) = λx:C (N ) : Πx : A.B

Γ `+ A = C kind Γ, x : A `+ B = D kind + Γ ` Πx : A.B = Πx : C.D kind (App) Figure 2: Kind Equality `+ Γ valid x : A ∈ Γ (Var) Γ `+ xA : A Γ `+ A kind Γ, x : A `+ B kind Γ, x : A `+ M : B (λ) Γ `+ λB x:A (M ) : Πx : A.B

(App)

Γ `+ A kind Γ, x : A `+ B kind + Γ ` M : Πx : A.B Γ `+ N : A

x:A∈Γ Γ `+ xA = xA : A

(β)

Γ `+ A = C kind Γ, x : A `+ B = D kind + Γ ` M = P : Πx : A.B Γ `+ N = Q : A D Γ `+ AppB x:A (M, N ) = Appx:C (P, Q) : [P/x]B

Γ, x : A `+ M : B Γ `+ N : A + Γ ` [N/x]M : [N/x]B B Γ `+ AppB x:A (λx:A (M ), N ) = [N/x]M : [N/x]B

(η)

Γ

`+

(Eq)

Γ `+ M : Πx : A.B = M : Πx : A.B

B A λB x:A (Appx:A (M, x ))

Γ `+ M = N : A Γ `+ A = B kind + Γ` M =N :B

Γ `+ AppB x:A (M, N ) : [N/x]B (Refl)

(Eq)

Γ `+ M : A Γ `+ A = B kind Γ `+ M : B

Γ `+ M : A Γ `+ M = M : A

(Sym)

Γ `+ M = N : A Γ `+ N = M : A

Figure 3: Terms (Trans)

2.1

Unlabeled Terms

Finally, our development also requires a type system for unlabeled terms, i.e. the terms of the untyped λ-calculus. The reduction relation β is exactly the reduction of the untyped λ-calculus. As mentioned in the introduction, we translate the source language to unlabeled λ-terms because the labels in η-reduction are not preserved by the translation. The judgement forms for the unlabeled target language are the same as those for the fully decorated target language. We distinguish by annotating the turnstile `− β . The rules of inference are also identical: the distinction between the labeled and unlabeled systems lies in the information that can be extracted from terms, not derivations.

3.

Properties of the Source Language

Definition 1. Define the principal kind P(M ) by case analysis on M : P(xA )

=

P(λB x:A (M )) = P(AppB x:A (M, N )) =

Figure 4: Term Equality

The following notation x : A ∈ M means that A ≡ B for all free occurrences of xB in M . Definition 2. Define x : A ∈ M inductively as follows: • x : A ∈ xA . • x : A ∈ y B if x 6= y. • x : A ∈ λC x:B (M ). • x : A ∈ λC y:B (M ) if x 6= y, x : A ∈ B, x : A ∈ C and x : A ∈ M.

BASIC METATHEORY

3.1

Γ `+ M = N : A Γ `+ N = P : A + Γ` M =P :A

A Πx : A.B [N/x]B

+ Lemma 1. If Γ `+ βη M : A then Γ `βη M : P(M ) as a subderivation, and either P(M ) ≡ A or Γ `+ P(M ) =βη A kind as a subderivation.

Proof. By induction on derivations.

• x : A ∈ AppC x:B (M, N ). • x : A ∈ AppC y:B (M, N ) if x 6= y, x : A ∈ B, x : A ∈ C, x : A ∈ M , and x : A ∈ N . The extension to kinds x : A ∈ B is straightforward. Lemma 2. • If Γ `+ βη B kind and x : A ∈ Γ then x : A ∈ B. • If Γ `+ βη M : B and x : A ∈ Γ then x : A ∈ M . Proof. By induction on derivations.

3.2

Properties of the Target Language

We assume that the standard properties hold for the target language, the Logical Framework with fully decorated terms and β-equality. We also take β to be the usual compatible closure of β-reduction with no restrictions on the labels, that is: B AppD x:C (λx:A (M ), N )

β

[N/x]M

ηType (M ) ηEl(P ) (M )

= =

M M

ηΠx:A.B (M )

=

λx.η[ηA (x)/x]B (M (ηA (x)))

Lemma 3.

Proposition 1.

− 1. If Γ `− β M : A then Γ `β ηA (M ) : A.

1. If Γ `+ β M : A then FV(M ) ∪ FV(A) ⊆ dom(Γ).

− 2. If Γ `− β M = N : A then Γ `β ηA (M ) = ηA (N ) : A.

+ 0 2. If Γ, Γ0 `+ β J, x 6∈ dom(Γ) ∪ dom(Γ ) and Γ `β A kind 0 + then Γ, x : A, Γ `β J. + 0 + 3. If Γ, x : A, Γ0 `+ β J and Γ `β N : A then Γ, [N/x]Γ `β [N/x]J. + 4. If Γ `+ β M : A then Γ `β A kind. + + 5. If Γ `+ β M : A and Γ `β M : B then Γ `β A = B kind. + 6. If Γ `+ β Πx : A.B =β Πx : C.D kind then Γ `β A =β + C kind and Γ, x : A `β B =β D kind.

7. If Γ `+ M =β N : A then M =β N . Proof. This is largely standard, following Streicher [23]. One subtlety of our presentation is that the rule β has a premise that Γ `+ β [N/x]M : [N/x]B. The equivalence with the usual presentation can be demonstrated by first proving Cases 2 and 3 for our presentation, and then showing the equivalence of the two presentations by induction on derivations of each system. Alternatively, the properties listed here can be shown directly for our presentation using a Kripke-style model construction [3, 13].

3.3

The Unlabeled Target Language

The judgements in the unlabeled system have the properties of Proposition 1, as well as the following standard properties. Proposition 2. − 1. If Γ `− β M : A and M β N then Γ `β N : A.

2. If Γ `− β M : A then M is strongly normalizing under β . 3. Typechecking for `− β is decidable.

4.

Definition 3. Define ηA (M ), for M an unlabeled λ-term, by induction on A:

SOUNDNESS

We now show that the η-expansions of terms typable in the βη-system are typable in the β-system. We begin by defining two maps on terms, ηA (−) and H(−). Intuitively, ηA (M ) represents the η-expansion of M at kind A, and H(M ) replaces all subterms of M with their η-expansions at their principal kinds. This translation inserting η-expansions through all subterms clearly models η D E equality, since the subterm M in an η-redex λB x:A (Appx:C (M, x )) will be translated to a λ-abstraction, and so the translation of the η-redex is β-equal to the translation of its reduct.

Proof. Each follows by induction on the length of A. Lemma 4. 1. [N/x](ηA (M )) ≡ η[N/x]A ([N/x]M ). 2. If A β B then ηA (M ) ≡ ηB (M ). 3. ηA (ηA (M )) ∗β ηA (M ) and ηΠx:A.B (ηΠx:A.B (M )) + β ηΠx:A.B (M ). Proof. Case 1 follows by induction on A, and Case 2 follows by induction on derivations of A β B and inversion of the definition of ηA (M ). Case 3 follows by induction on A. We consider Πx : A.B, where we assume x 6∈ FV(M ): ≡

ηΠx:A.B (ηΠx:A.B (M )) λx.η[ηA (x)/x]B (ηΠx:A.B (M )(ηA (x)))

≡ β

λx.η[ηA (x)/x]B ((λx.η[ηA (x)/x]B (M (ηA (x))))(ηA (x))) λx.η[ηA (x)/x]B (η[ηA (x)/x]B (M (ηA (ηA (x)))))

∗β

λx.η[ηA (x)/x]B (M (ηA (x)))

≡

ηΠx:A.B (M )

Definition 4. Define H(A) and H(M ) by structural induction: H(Type) = H(El(P )) = H(Πx : A.B) =

Type El(H(P )) Πx : H(A).H(B)

H(xA )

=

ηH(A) (x)

H(λB x:A (M ))

=

ηΠx:H(A).H(B) (λx.H(M ))

H(AppB x:A (M, N ))

=

η[H(N )/x]H(B) (H(M )(H(N )))

The H(−) map extends to contexts in the obvious way. Lemma 5. ηH(P(M )) (H(M )) ∗β H(M ). Furthermore, if P(M ) ≡ Πx : A.B then ηH(Πx:A.B) (H(M )) + β H(M ). Proof. By induction on M , using Lemma 4 Case 3 directly for each term constructor. The following lemma is similar to typical substitution lemmas. We need to include the side condition that x not occur free in its kind because the definition of H(−) is for arbitrary terms and kinds, not only well-formed ones, and so imposes no conditions on subterms of its argument. The side condition will always hold for terms and kinds in well-formed judgements.

Lemma 6.

by Lemma 3, and H(Γ) `− [H(N )/x]H(B) =β H([N/x]B) kind

1. If x : C ∈ A, H(C) =β H(P(P )) and x 6∈ FV(H(C)) then [H(P )/x]H(A) ∗β H([P/x]A).

by Lemma 6, Proposition 1 Case 4 (for `− ) and Subject Reduction (Proposition 2 Case 1), so H(Γ) `− β H(AppB x:A (M, N )) : H([N/x]B) by Eq.

2. If x : C ∈ M , H(C) =β H(P(P )) and x 6∈ FV(H(C)) then [H(P )/x]H(M ) ∗β H([P/x]M ). Proof. By induction on A and M . We consider several cases.

• β. By induction hypothesis H(Γ) `− H(λB x:A (M )) : H(Πx : A.B) and H(Γ) `− H(N ) : H(A), so H(Γ) `− B H(AppB x:A (λx:A (M ), N )) ≡ η[H(N )/x]H(B) (H(M )(H(N ))) : [H(N )/x]H(B) =β H([N/x]B) by Lemma 3 and reasoning similar to App for the kind equality. Furthermore, by inversion Γ, x : A `+ M : B, so x : A ∈ M by Lemma 2. By Lemma 1, there either exists a subderivation of Γ `+ P(N ) =βη A, in which case by induction hypothesis H(Γ) `− H(P(N )) =β H(A) kind, or P(N ) ≡ A, in which case H(Γ) `− H(P(N )) =β H(A) kind by Proposition 1 Case 4 and Refl; furthermore, in either case x 6∈ FV(H(A)) by Proposition 1 Case 1. Similarly, H(Γ) `− H(P([N/x]M )) =β H([N/x]B) and x 6∈ FV(H([N/x]B)).

• xA . Then: ≡

[H(P )/x]ηH(A) (x) η[H(P )/x]H(A) (H(P ))

≡ ≡

ηH(A) (H(P )) ηH(P(P )) (H(P ))

∗β

H(P )

by Lemma 5, since x 6∈ FV(H(C)) and x : C ∈ xA implies C ≡ A by inversion. • y B . Then [H(P )/x]ηH(B) (y) ≡ η[H(P )/x]H(B) (y) ≡ ηH([P/x]B) (y), by Lemma 4 Case 2 since [H(P )/x]H(B)∗β H([P/x]B) by induction hypothesis.

Therefore, by Lemma 4 Cases 2 and 3 and Lemma 6:

• λB y:A (M ). Then, by definition, Lemma 4 Cases 1 and 2 and induction hypothesis:

≡ ≡

[H(P )/x]H(λB y:A (M ))

β

≡

[H(P )/x]ηΠy:H(A).H(B) (λy.H(M ))

≡ ≡

ηΠy:[H(P )/x]H(A).[H(P )/x]H(B) ([H(P )/x]λy.H(M )) ηΠy:H([P/x]A).H([P/x]B) ([H(P )/x]λy.H(M ))

≡

≡ ∗β

ηΠy:H([P/x]A).H([P/x]B) (λy.[H(P )/x]H(M )) ηΠy:H([P/x]A).H([P/x]B) (λy.H([P/x]M ))

∗β

≡

H(λy:[P/x]A ([P/x]M ))

≡

H([P/x](λB y:A (M )))

β ∗β ≡ ≡ ∗β

[P/x]B

Theorem 1

B H(AppB x:A (λx:A (M ), N )) η[H(N )/x]H(B) (ηH(Πx:A.B) (λx.H(M ))(H(N ))) η[H(N )/x]H(B) (λx.η[ηH(A) (x)/x]H(B) ( (λx.H(M ))(ηH(A) (x)))(H(N ))) η[H(N )/x]H(B) (η[ηH(A) (H(N ))/x]H(B) ( (λx.H(M ))(ηH(A) (H(N ))))) η[H(N )/x]H(B) (η[ηH(P(N )) (H(N ))/x]H(B) ( (λx.H(M ))(ηH(P(N )) (H(N ))))) η[H(N )/x]H(B) (η[H(N )/x]H(B) ( (λx.H(M ))(H(N )))) η[H(N )/x]H(B) (η[H(N )/x]H(B) ([H(N )/x]H(M ))) η[H(N )/x]H(B) (H([N/x]M )) ηH([N/x]B) (H([N/x]M )) ηH(P([N/x]M )) (H([N/x]M )) H([N/x]M )

• η. By Lemma 1 either Γ `+ P(M ) =βη Πx : A.B as a subderivation, in which case by induction hypothesis H(Γ) `− H(M ) : H(Πx : A.B), or P(M ) ≡ Πx : A.B; in either case H(Γ) `− H(P(M )) =β H(Πx : A.B). Therefore:

(Soundness).

− • If Γ `+ βη A kind then H(Γ) `β H(A) kind.

• If Γ `+ A =βη B kind then H(Γ) `− H(A) =β H(B) kind. − • If Γ `+ βη M : A then H(Γ) `β H(M ) : H(A).

≡

• If Γ `+ M =βη N : A then H(Γ) `− H(M ) =β H(N ) : H(A).

≡ + β ≡ ∗β

Proof. By induction on derivations. We consider several cases.

B A H(λB x:A (Appx:A (M, x ))) ηH(Πx:A.B) (λx.η[ηH(A) (x)/x]H(B) ( H(M )(ηH(A) (x)))) ηH(Πx:A.B) (ηH(Πx:A.B) (H(M )) ηH(Πx:A.B) (H(M )) ηH(P(M )) (H(M )) H(M )

• Var. H(Γ) `− H(xA ) ≡ ηH(A) (x) : H(A) by Var and Lemma 3. • App. By induction hypothesis H(Γ) `− β H(M ) : H(Πx : A.B) ≡ Πx : H(A).H(B) and H(Γ) `− β H(N ) : H(A), so H(Γ) `− H(M )(H(N )) : [H(N )/x]H(B) by App. β Then: H(Γ) `− β ≡ :

H(AppB x:A (M, N )) η[H(N )/x]H(B) (H(M )(H(N ))) [H(N )/x]H(B)

5.

COMPLETENESS

This section shows that the judgements in the target language can be lifted to judgements in the source language: that is, judgements under the η-expansion translation H(−) in the system with unlabeled terms and β equality can be lifted to the system with decorated terms and βη equality. First, we show that lifting equality over unlabeled terms to the fully decorated terms is possible: this is because the

derivations of well-formedness of unlabeled terms contain all of the kind information necessary to assign kinds in the decorated terms. Our presentation relating fully decorated terms and unlabeled terms is strongly influenced by Streicher [23]. Then we define an η-expansion translation with fully decorated terms as the target, and show that all terms are βηequal to themselves under the translation. The composition of these two operations is equivalent to the original translation from fully decorated terms to unlabeled terms, and so Completeness follows from the properties of each component of the translation. We begin by defining the stripping function from fully decorated terms to unlabeled terms. Definition 5. Define the stripping function |M | by induction on M : |Type| = |El(P )| = |Πx : A.B| = A

|x | = |λB x:A (M )| B |Appx:A (M, N )|

Type El(|P |) Πx : |A|.|B| x

=

λx.|M |

=

|M |(|N |)

`+ β

Lemma 7. If Γ M : A, Γ then Γ `+ M =β N : A.

`+ β

N : A and |M | ≡ |N |

Proof. As in [23]. Lemma 8. + 1. If Γ `− β M : A then there is a P such that Γ `β P : A and |P | ≡ M .

2. If Γ `− M =β N : A then there are P and Q such that Γ `+ P =β Q : A, |P | ≡ M and |Q| ≡ N . Proof. As in [23]. The following map H + (M ) differs from H(M ) only by mapping to fully decorated terms instead of unlabeled terms. + Definition 6. Define ηA (M ) by induction on A: + (M ) ηType

=

M

+ ηEl(P ) (M )

=

M

ηΠx:A.B (M )

=

B A λB x:A (Appx:A (M, x ))

= Type = El(H + (P )) = Πx : H + (A).H + (B) + A = ηH + (A) (x ) = H + (B)

+ + ηΠx:H + (A).H + (B) (λx:H + (A) (H (M ))) + B H (Appx:A (M, N )) = H + (B)

+ + + η[H + (N )/x]H + (B) (Appx:H + (A) (H (M ), H (N )))

The H + (−) map extends to contexts in the obvious way. Lemma 9. |H + (M )| ≡ H(M ). Proof. Induction on M .

A. Proof. By induction on M , using Lemma 1 and the simple lemma that Γ `+ M =βη ηA (M ) : A. Theorem 2

(Completeness of Equality).

1. If Γ M, N : A and H(Γ) `− H(M ) =β H(N ) : H(A) then Γ `+ M =βη N : A. `+ βη

− 2. If Γ `+ βη A, B kind and H(Γ) ` H(A) =β H(B) kind + then Γ ` A =βη B kind.

Proof. We show Case 1, where Case 2 is similar. We know by Lemma 9 that H(Γ) `− |H + (M )| =β |H + (N )| : H(A). By Lemma 8 there are P and Q such that Γ `+ P =β Q : A with |P | ≡ |H + (M )| and |Q| ≡ |H + (N )|. Therefore Γ `+ P =β H + (M ) : A and Γ `+ Q =β H + (N ) : A by Lemma 7, so Γ `+ H + (M ) =β H + (N ) : A by Trans and Γ `+ M =βη N : A by Trans and Lemma 10. Corollary 1 (Completeness). If Γ `− J then there are ∆ and J 0 such that ∆ `+ J 0 , |∆| ≡ Γ and |J 0 | ≡ J. It is now possible to lift the metatheory of the `β system to the `βη system. The following reduction relation |βη| ignores the labels on the fully decorated terms. As we mentioned in the introduction, this relation is strongly normalizing and Church–Rosser, and so this could be the basis for an algorithm for testing conversion. Definition 7. Define the relations β and η as: B AppD x:C (λx:A (M ), N ) β E B λD x:C (Appx:A (M ), x )

η

[N/x]M M

Define reduction |βη| as the compatible closure over term and kind constructors that ignores labels of βη; for example, the compatible closure of application is completely defined by: B • If M  P then AppB x:A (M, N )  Appx:A (P, N ). B • If N  P then AppB x:A (M, N )  Appx:A (M, P ). + Lemma 11. If Γ `+ βη M : A and M |βη| N then H(M )β H(N ).

Define H + (M ) by induction on M : H + (Type) H + (El(P )) H + (Πx : A.B) H + (xA ) + B H (λx:A (M ))

+ Lemma 10. If Γ `+ M =βη H + (M ) : βη M : A then Γ `

Proof. By induction on M βη N , where the compatible closure rules follow by induction hypothesis. B ∗ For β, we need to show that H(AppD x:C (λx:A (M ), N )) β + D B H([N/x]M ), where Γ `βη Appx:C (λx:A (M ), N ) : E. By inB + version Γ `+ Πx : A.B =βη βη λx:A (M ) : Πx : A.B and Γ ` − Πx : C.D, so H(Γ) `β H(Πx : A.B) =βη H(Πx : C.D). By Proposition 1 Case 7 and Church–Rosser H(A) =β H(C) and H(B) =β H(D), so: B B B H(AppD x:C (λx:A (M ), N )) ≡ H(Appx:A (λx:A (M ), N ))

and the reduction sequence follows as for rule β in Soundness. The reasoning for η-reduction is similar. The properties listed in Proposition 1 can now be shown directly or transferred from the target language to the source language.

Proposition 3. 1. If Γ `+ βη M : A then FV(M ) ∪ FV(A) ⊆ FV(Γ). + 0 2. If Γ, Γ0 `+ βη J, Γ `βη A kind and x 6∈ FV(Γ) ∪ FV(Γ ) 0 + then Γ, x : A, Γ `βη J.

• Γ; Type ⇒+ kind.

+ 0 + 3. If Γ, x : A, Γ0 `+ βη J and Γ `βη N : A then Γ, [N/x]Γ `βη [N/x]J.

• Γ; Πx : A.B ⇒+ kind if Γ; A ⇒+ kind and Γ, x : A; B ⇒+ kind.

+ 4. If Γ `+ βη M : A then Γ `βη A kind. + + 5. If Γ `+ βη M : A and Γ `βη M : B then Γ `βη A = B kind. + 6. If Γ `+ βη Πx : A.B =βη Πx : C.D kind then Γ `βη + A =βη C kind and Γ, x : A `βη B =βη D kind. + 7. If Γ `+ βη M : A and M |βη| N then Γ `βη N : A.

8. If Γ `+ βη M : A then M is strongly normalizing under βη .

6.

Definition 9. We define the type checking algorithm on fully decorated terms Γ; A ⇒+ kind and Γ; P ⇒+ A inductively as follows:

TYPE CHECKING

Given the full metatheory of `+ βη developed above, the decidability of type checking is similar to the standard treatment [19]. The novelty in our presentation in this section is that we derive the fully decorated terms, using the standard presentation of terms with no labels in variables or application and a single label for the domain in abstractions. Definition 8. We define the decorating type checking algorithm Γ; A ⇒ B; kind and Γ; M ⇒ P ; A inductively as follows: • Γ; Type ⇒ Type; kind. • Γ; El(M ) ⇒ El(P ); kind if Γ; M ⇒ P ; Type. • Γ; Πx : A.B ⇒ Πx : C.D; kind if Γ; A ⇒ C; kind and Γ, x : C; B ⇒ D; kind. • Γ; x ⇒ xC ; C if x : C ∈ Γ. • Γ; λx : A.M ⇒ λD x:C (P ); Πx : C.D if Γ; A ⇒ C; kind and Γ, x : C; M ⇒ P ; D. • Γ; M (N ) ⇒ AppD x:C (P, Q); [Q/x]D if Γ; M ⇒ P ; Πx : C.D, Γ; N ⇒ Q; C 0 and C =|βη| C 0 . Lemma 12

(Correctness of the Algorithm).

• If Γ; A ⇒ C; kind then Γ `+ βη C kind. • If Γ; M ⇒ P ; C then Γ `+ βη P : C. Proof. By induction on derivations of Γ; A ⇒ C; kind and Γ; M ⇒ P ; C, using Lemma 3 Case 4 and Completeness for application. We now introduce a type checking algorithm directly on fully decorated terms to show completeness of the algorithm. Similar to our proof of completeness for the target language in the previous section, this allows us to decompose completeness of the algorithm into simpler results about the erasure and the algorithm itself.

• Γ; El(M ) ⇒+ kind if Γ; M ⇒+ Type.

• Γ; xC ⇒+ C if x : C ∈ Γ. + • Γ; λD Πx : C.D0 if Γ; C ⇒+ kind, Γ, x : x:C (M ) ⇒ C; D ⇒+ kind, Γ, x : C; M ⇒+ D0 and D =|βη| D0 . + • Γ; AppD [N/x]D0 if Γ; C ⇒+ kind, Γ, x : x:C (M, N ) ⇒ C; D ⇒+ kind, Γ; M ⇒+ Πx : C 0 .D0 , Γ; N ⇒+ C 00 , C =|βη| C 0 =|βη| C 00 and D =|βη| D0 .

Lemma 13. + 1. If Γ `+ βη A kind then Γ; A ⇒ kind. + 2. If Γ `+ βη P : A then there is a C such that Γ; P ⇒ C + and Γ `βη A = C kind.

Proof. By induction on derivations. Finally, we define a second stripping operation strip(M ) that strips off the labels on variables and applications and the codomain off of abstractions. Definition 10. Stripping from the fully decorated terms to the standard presentation of lambda terms is defined as follows: strip(xA )

=

x

strip(λB x:A (M )) strip(AppB x:A (M, N ))

=

λx : strip(A).strip(M )

=

strip(M )(strip(N ))

Observe that if strip(M ) ≡ strip(N ) then |M | ≡ |N |, and so Lemma 7 lifts to the map strip(−). Lemma 14. 1. If Γ; A ⇒+ kind and strip(Γ) ≡ strip(Γ0 ) then there is an A0 such that Γ; strip(A) ⇒ A0 ; kind and strip(A) ≡ strip(A0 ). 2. If Γ; P ⇒+ C and strip(Γ) ≡ strip(Γ0 ) then there are P 0 and C 0 such that Γ0 ; strip(P ) ⇒ P 0 ; C 0 , strip(C) ≡ strip(C 0 ) and strip(P ) ≡ strip(P 0 ). Proof. By induction on derivations. We consider P ≡ AppD x:C (M, N ). By induction hypothesis Γ0 ; strip(M ) ⇒ M 0 ; Πx : C 000 .D00 with strip(Πx : C 000 .D00 ) ≡ strip(Πx : C 0 .D0 ), and strip(M ) ≡ strip(M 0 ) and Γ0 ; strip(N ) ⇒ N 0 ; C 0000 with strip(C 00 ) ≡ strip(C 0000 ) and strip(N ) ≡ strip(N 0 ). Furthermore, C 0000 =|βη| C 000 , since by assumption C 0 =|βη| C 00 and by Correctness of the Algorithm, Lemma 7 and Proposition 1 Case 7 C 00 =|βη| C 0000 and C 000 =|βη| C 0 . Therefore: strip([N/x]D0 )

≡

strip([N 0 /x]D00 )

strip(AppD x:C (M, N ))

≡

0 0 strip(AppD x:C 000 (M , N ))

Γ0 ; strip(AppD x:C (M, N ))

≡

strip(M )(strip(N ))

00

00

0 0 0 00 ⇒ AppD x:C 000 (M , N ); [N /x]D

Corollary 2

(Completeness of the Algorithm).

0 1. If Γ `+ βη C kind then there is a C such that Γ; strip(C) ⇒ C 0 ; kind. 0

`+ βη

0

2. If Γ P : C then there are P and C such that Γ; strip(P ) ⇒ P 0 ; C 0 and Γ `+ C =βη C 0 kind. Theorem 3 (Decidability of `+ βη ). The judgements Γ `+ J are decidable. βη

7.

SINGLETONS AND DEPENDENT PAIRS

We now extend the above proofs to cover singletons and dependent pairs as well. As we mentioned before, the important difference with the earlier sections is that reduction for the system with these kinds is not Church–Rosser. We begin by presenting the fully decorated syntax for singletons and dependent pairs, and then outline the metatheory for these new kinds.

7.1

Singletons

We introduce new kind and term formers as used in the following rules of inference: (S)

Γ `+ M : A Γ `+ SA (M ) kind

(q-Eq)

(pair-Uniq)

Γ `+ M : A Γ `+ N : [M/x]B B B Γ qx:A (pairx:A (M, N )) = N : [M/x]B

Γ

`+

Γ `+ M : Σx : A.B = M : Σx : A.B

B B `+ pairB x:A (px:A (M ), qx:A (M ))

plus the obvious compatible closure rules for formers Σ, pair, p and q. Again, for the unlabeled system the term formers pair(M, N ), p(M ) and q(N ) have no labels.

7.3

Metatheory

We begin by assuming that the metatheory of the new kinds is well-behaved for the systems without the weakly extensional equalities. These kinds of inductive definitions have been studied extensively [12, 24]. The reduction relations are defined analogously to those for the Logical Framework with Π-kinds. The metatheory of singletons and dependent pairs with the weakly extensional equalities closely follows the above development, and the statement of the results in Sections 3, 4 and 5 does not change. We give here the extension of the definitions to the new kinds and show some examples of the extended proofs for them. Definition 11. P(∗A (M )) = P(outA (M )) =

(∗)

Γ `+ M : A Γ `+ ∗A (M ) : SA (M )

(out)

(out-∗)

P(pairB x:A (M, N )) =

Σx : A.B

P(pB x:A (M )) =

A

P(qB x:A (M )) =

[pB x:A (M )/x]B

Γ `+ N : SA (M ) Γ `+ outA (N ) : A

Γ `+ M : A + Γ ` outA (∗A (M )) = M : A

SA (M ) A

The definitions of x : A ∈ B and x : A ∈ M extend trivially to the new term formers. Definition 12.

Γ `+ N : SA (M ) (∗-Uniq) Γ `+ ∗A (M ) = N : SA (M ) plus the obvious compatible closure rules for kind and term formers S, ∗ and out. For the unlabeled system, the term formers ∗(M ) and out(M ) have no labels.

7.2

Dependent Pairs Γ `+ A kind Γ, x : A `+ B kind (Σ) + Γ ` Σx : A.B kind Γ `+ M : A Γ `+ N : [M/x]B (pair) B + Γ ` pairx:A (M, N ) : Σx : A.B (p)

(q)

(p-Eq)

Γ `+ M : Σx : A.B Γ `+ pB x:A (M ) : A

Γ `+ M : Σx : A.B B Γ `+ q B x:A (M ) : [px:A (M )/x]B

Γ `+ M : A Γ `+ N : [M/x]B B B Γ `+ px:A (pairx:A (M, N )) = M : A

ηSA (M ) (N ) = ηΣx:A.B (M ) =

∗(M ) pair(ηA (p(M )), η[p(M )/x]B (q(M )))

Definition 13. H(∗A (M )) = H(outA (M )) = H(pairB x:A (M, N )) H(pB x:A (M ))

∗(H(M )) ηH(A) (out(H(M )))

=

ηH(Σx:A.B) (pair(H(M ), H(N )))

=

ηH(A) (p(H(M )))

H(qB x:A (M )) =

η[H(pB

x:A

(M ))/x]H(B) (q(H(M )))

We now show the case of ∗-Uniq for Theorem 1. By Lemma 1 Γ `+ N : P(N ) and either P(N ) ≡ SA (M ) or Γ `+ P(N ) =βη SA (M ) kind as a subderivation; in the latter case we also have P(N ) ≡ SA0 (M 0 ) and subderivations of Γ `+ M =βη M 0 : A and Γ `+ A =βη A0 kind, and so by induction hypothesis H(Γ) `− H(M ) =β H(M 0 ) : H(A) and H(Γ) `− H(A) =β H(A0 ) kind. In either case, we have ∗(H(M )) ≡ ηH(P(N )) (H(N )) ≡ ηH(SA (M )) (H(N )) ∗ H(N ) by Lemma 5, so H(N ) ≡ ∗(H(M )), and so H(Γ) `− H(N ) ≡ ∗(H(M )) =β ∗(H(M )) : SH(A) (H(M )) ≡ H(SA (M )). Finally, although the equalities corresponding to the weakly extensional equality rules cannot be interpreted as reductions because they are not Church–Rosser, the translation to

the unlabeled terms yields an algorithm that is both strongly normalizing and Church–Rosser, and so that algorithm can be used to test conversion of the source-language terms.

8.

[3]

CONCLUSIONS AND FUTURE WORK

We have demonstrated that the terms of the source Logical Framework with βη-equality can be represented in the target language with only β-equality, with the consequence that type checking for the source language is decidable. We further extended our results to show that weakly extensional equality for singletons and dependent pairs is decidable. To provide a complete basis for modules systems, we need to extend our results to include the implicit form of singletons and subtyping. We believe that the additional complexity of subtyping in Stone and Harper’s presentation can be dealt with by applying appropriate η-expansions for the supertype, but we have not studied the technical details: with the interrelated judgements, it is not clear whether the η-expansion can be applied at the judgemental level or if the explicit term language needs to be extended with references to subtyping. We are also interested in studying whether the general approach of modeling weakly extensional equalities can be extended to include colimit types such as the empty type or sum types. Finally, we have demonstrated [14] that the results established here for the Logical Framework with βη reduction are sufficient to justify the decidability of Coquand’s original algorithm for deciding βη-equality [5] and Harper and Pfenning’s algorithm [15], but we would like to extend this approach to types beyond dependent function spaces. This article concentrates on type theories sufficient as a theoretical basis for modules systems, and so we are able to avoid a sophisticated model construction for the basic Logical Framework. However, extending our technique to systems with either impredicativity or higher-order typevalued operators would force us to use some kind of model construction. To see this, consider that for the expansions to be sound the type-directed η-expansion function needs to be closed under substitution within its type argument, but substituting a type for a type variable in the type argument, for example Πx : A.B for X, leads to a different expansion.

[4]

[5]

[6]

[7]

[8]

[9]

[10] [11]

[12]

Acknowledgments I would like to thank Mariangiola Dezani for her kind invitation to visit the Universit` a di Torino, Robert Harper for suggesting that I study the metatheory of singletons, Gilles Barthe for pointing me to [6], Thierry Coquand and Randy Pollack for interesting discussions on their model construction, Eduardo Bonelli for recommending [8], and Zhaohui Luo for asking whether reduction was preserved by an earlier definition of the H(−) map. I would also like to thank my wife Adriana Compagnoni both for helpful technical discussions and for her encouragement as I was writing this article.

[13]

9.

[17]

REFERENCES

[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L´evy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991. [2] G. Barthe. Existence and uniqueness of normal forms in pure type systems with beta-eta conversion. In Proceedings of Computer Science Logic, CSL’98,

[14] [15]

[16]

[18]

volume 1584 of Lecture Notes in Computer Science, pages 241–259. Springer–Verlag, 1998. A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. A later version is published as [4]. A. Compagnoni and H. Goguen. Typed operational semantics for higher-order subtyping. Information and Computation, 184(2):242–297, Aug. 2003. T. Coquand. An algorithm for testing conversion in type theory. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991. T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. Extended version of [7], 2003. T. Coquand, R. Pollack, and M. Takeyama. A logical framework with dependently typed records. In Proceedings of Typed Lambda Calculus and Applications, TLCA’03, volume 2701 of Lecture Notes in Computer Science. Springer-Verlag, 2003. See extended version [6]. R. D. Cosmo and D. Kesner. A confluent reduction system for the extensional typed lambda-calculus with pairs, sum, recursion and terminal object. In Proceedings of the 20st International Colloquium on Automata, Languages and Programming (ICALP’93), volume 700 of Lecture Notes in Computer Science, pages 645–656. Springer–Verlag, July 1993. G. Dowek, G. Huet, and B. Werner. On the definition of the eta-long normal form in type systems of the cube. In Informal Proceedings of the Workshop on Types for Proofs and Programs, 1993. H. Geuvers. Logics and Type Systems. PhD thesis, Katholieke Universiteit Nijmegen, Sept. 1993. N. Ghani. Eta-expansions in dependent type theory the calculus of constructions. In Typed Lambda Calculus and Applications, volume 1210 of Lecture Notes in Computer Science, pages 164–180. Springer–Verlag, 1997. H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, Aug. 1994. H. Goguen. A Kripke-style model for the admissibility of structural rules. In Proceedings of TYPES, volume 2277 of Lecture Notes in Computer Science, pages 112–124. Springer–Verlag, 2000. H. Goguen. Justifying algorithms for beta-eta conversion. 2004. Submitted to FOSSACS 2005. R. Harper and F. Pfenning. On equivalence and canonical forms in the LF type theory. ACM Trans. on Computational Logic, 2003. (To appear). F. Joachimski. Syntactic analysis of eta-expansions in pure type systems. Information and Computation, 182(1):53–71, 2003. J. W. Klop. Combinatory reduction systems. Mathematical Centre Tracts 127, Centre for Mathematics and Computer Science, Amsterdam, 1980. PhD thesis J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge studies in

advanced mathematics. Cambridge University Press, 1989. [19] Z. Luo. Computation and Reasoning. Oxford University Press, 1994. [20] D. MacQueen. Using dependent types to express modular structure. In Proceedings of the Thirteenth ACM Symposium on the Principles of Programming Languages, 1986. [21] A. Salvesen. The Church-Rosser property for pure type systems with βη-reduction, Nov. 1991.

Unpublished manuscript. [22] C. A. Stone and R. Harper. Equivalence and singletons. ACM Transactions on Programming Languages and Systems, 2004. Submitted. [23] T. Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkh¨ auser, 1991. [24] B. Werner. Une Th´eorie des Constructions Inductives. PhD thesis, Universit´e Paris 7, 1994.