A Syntactic Approach to Eta Equality in Type Theory

Healfdene Goguen
AT&T Labs
180 Park Ave.
Florham Park NJ 07932 USA
hhg@att.com

ABSTRACT of type theories with the additional equality rules. This con-
This paper outlines an elementary approach for showing trasts with other approaches to η-reduction by not requir-
the decidability of type checking for type theories with βη- ing extensive redevelopment for a βη-system given existing
equality, relevant to foundations for modules systems and results for the β-system. Philosophically, our approach ex-
type theory-based proof systems. The key to the approach is plains uniqueness rules without a clear computational justi-
a syntactic translation mapping terms in the βη presentation fication in terms of the well-understood computational rules.
into their full η-expansions in the β presentation. Decidabil- We begin by studying Martin-Löf’s Logical Framework
ity of type checking is lifted from the target β presentation with Π-kinds and βη equality. In this case βη reduction is
to the βη presentation. The approach extends to other in- strongly normalizing and Church–Rosser, and so we could
ductive kinds with a single constructor, and is demonstrated use this relation directly to implement an algorithm for test-
for singletons and dependent pairs. ing conversion.
We follow by studying the extension of the Logical Frame-
work with singletons and dependent pairs at the level of
Categories and Subject Descriptors kinds, similar to that of Stone and Harper [22], although
F.4.1 [Theory of Computation]: Lambda calculus and our singletons include explicit term constructors and elimi-
related systems nation constants. This language has the key difficulties that
the equalities are type-directed and that the η-equalities di-
rected as reductions do not have the Church–Rosser prop-
General Terms erty, and so conversion must be implemented by a cus-
Theory, Languages tomized 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
Keywords source language with the additional η-style equalities over
Logical frameworks, type checking, decidability, beta-eta fully decorated terms, as introduced by Streicher [23] but
equality with full labels for variables and abstraction. Each term
constructor contains explicit labels allowing the reconstruc-
tion of the premises in the rule of inference; for example,
1. INTRODUCTION the application constructor AppB x:A (M, N ) allows us to infer
In this article we introduce an elementary approach to the that M must have kind Πx : A.B and N must have kind A,
metatheory of type theories with βη-style equalities. These even from a judgement Γ ` AppB x:A (M, N ) : C. Because of
weakly extensional equational theories have applications to this explicit information in the term structure, we are able to
programming languages, especially for understanding mod- define a total translation from terms in the source language
ules systems like that of Standard ML [20], to categorical into the target language, without reference to derivations of
combinators [18] and systems of explicit substitution [1], and well-kindedness.
to the foundations of type theory-based proof assistants [19]. We reuse the basic definition of type-directed η-expansion,
Our intention in this article is to justify the weakly exten- like that used in defining η-long normal forms [6, 9]. The
sional η rules by translating them into a system with only the new approach taken here is to apply that expansion to ev-
traditional β-style computation rules. Practically, our ap- ery subterm of the source term. The labels in the fully dec-
proach provides a short and direct proof of the decidability orated 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
Permission to make digital or hard copies of all or part of this work for on derivations of the source language.
personal or classroom use is granted without fee provided that copies are The target language of the interpretation is formed from
not made or distributed for profit or commercial advantage and that copies β-equality over unlabeled terms, i.e. the terms of the un-
bear this notice and the full citation on the first page. To copy otherwise, to typed λ-calculus. This is necessary because β-reduction un-
republish, to post on servers or to redistribute to lists, requires prior specific
permission and/or a fee.
der the translation does not preserve the kind labels of η-
POPL’05, January 12–14, 2005, Long Beach, California, USA. reduction: writing ηA (M ) for the η-expansion of M at kind
Copyright 2005 ACM 1-58113-830-X/05/0001 ...$5.00.
A, we only have that ηΠx:C.D (AppD B A
x:C (λx:A (M ), x )) reduces extend the proofs to singletons and dependent pairs, and in
D B
to λx:C (M ), not to λx:A (M ) as would be required by a fully Section 8 we summarize and outline future work.
decorated term language.

1.1 Related Work 2. SYNTAX

Deciding βη-equality is a long-standing problem in type The term language of the Logical Framework is given by
theory. While various approaches have been studied exten- the following grammar:
sively, including interpreting the η-style equality rules as ei-
A, B, C, D ∈ Kind ::= Type | El(M ) | Πx : A.B
ther reduction rules [10, 12, 21] or expansion rules [11], each
M, N, P, Q ∈ Term ::= xA | λB B
x:A (M ) | Appx:A (M, N )
of these approaches suffers from deficiencies. The systems
Γ, ∆, Φ ∈ Ctxt ::= () | Γ, x : A
arising from interpreting η-equality rules as reductions can
fail to be confluent [17, 18], invalidating the primary advan- We identify terms and kinds that are equivalent up to
tage of the reduction approach. Interpreting the η-equality the renaming of bound variables, and we write M ≡ N if
rules as expansions appears natural for simple type systems, M and N are equal in this way. We write FV(M ) for the
but it becomes increasingly unnatural for more complex type free variables in a term M , those variables not bound by
theories: for example, Ghani’s treatment of η-expansions abstractions. We write [N/x]M for the usual capture-free
for the Calculus of Constructions [11] requires kinds of ex- substitution of N for occurrences of the variable x in M .
panded abstractions to be in normal form. Barthe [2] and Each of these operations is lifted to kinds and contexts in
Joachimski [16] study strong normalization for η expansions the natural way.
given the strong normalization of βη reduction for the type As we have mentioned earlier, in this article we consider
theory with βη equality, and so their results will also fol- two versions of Martin-Löf’s Logical Framework, with judge-
low for type theories with β equality where our approach ments Γ `+ M =β N : A and Γ `+ M =βη N : A. We write
applies. Γ `+ M = N : A for the remainder of this section, with the
Salvesen [21] gives a syntactic proof of Church–Rosser for understanding that the rules of inference presented here de-
βη-reduction, but this proof makes the much stronger as- fine =βη , and that =β is defined by the same rules without
sumption that βη-reduction is strongly normalizing, instead the rule of inference η.
of just β-reduction. In practice this assumption is difficult to The Logical Framework has several judgements:
establish without Church–Rosser for most systems. Geuvers
[10] also relates systems with βη-reduction to those with β- • `+ Γ valid, meaning Γ is a valid context,
reduction, but his proof is much more complex and relies on
properties of untyped conversion. • Γ `+ A kind, meaning A is a valid kind in context Γ,
Di Cosmo and Kesner [8] also use η-expansions in a trans-
lation to a target language, where a simply-typed source
• Γ `+ M : A, meaning M is a valid term of kind A in
language with η expansions is shown confluent and strongly
context Γ,
normalizing; since the article treats simple types it is not
clear whether it would extend to dependent types, since
• Γ `+ A = B kind, meaning A and B are equal in
the system with βη equality has different valid judgements
context Γ, and
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 • Γ `+ M = N : A, meaning M and N are equal and of
by untyped β-equality, and they show the correctness and kind A in context Γ.
decidability of type checking for a Logical Framework with
singletons and dependent pairs. The derivations are given by the following rules of infer-
Coquand [5] and Harper and Pfenning [15] treat the decid- ence.
ability of type checking by defining logical relations directly
over specific choices of algorithms for type checking. This (Emp) `+ () valid
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 jus- Γ `+ A kind x 6∈ FV(Γ)
(Ext)
tifying algorithms for type checking more sophisticated than `+ Γ, x : A valid
simple reduction to common normal form, including Co-
quand’s and Harper and Pfenning’s for the Logical Frame- `+ Γ valid
(Type)
work, on the basis of βη normalization. Γ `+ Type kind

1.2 Overview Γ `+ M : Type

(El)
In Section 2 we introduce the judgements for the Logical Γ `+ El(M ) kind
Framework over two separate term languages, fully deco-
rated and unlabeled terms. In Section 3 we introduce the Γ `+ A kind Γ, x : A `+ B kind
basic metatheory, primarily for the target language. In Sec- (Π)
Γ `+ Πx : A.B kind
tions 4 and 5 we show the soundness and completeness of β-
equality on unlabeled λ-terms for the fully decorated terms
Figure 1: Contexts and Kinds
under βη-equality, and in Section 6 we show that type check-
ing for the full source language is decidable. In Section 7 we
 `+ Γ valid x:A∈Γ
(Type) (Var)
Γ `+ Type = Type kind Γ `+ xA = xA : A

Γ `+ M = N : Type Γ `+ A = C kind Γ, x : A `+ B = D kind

(El) +
Γ `+ El(M ) = El(N ) kind Γ, x : A ` M = N : B
(λ)
Γ `+ λB D
x:A (M ) = λx:C (N ) : Πx : A.B
Γ `+ A = C kind Γ, x : A `+ B = D kind
(Π) Γ `+ A = C kind Γ, x : A `+ B = D kind
Γ ` Πx : A.B = Πx : C.D kind
+
+
Γ ` M = P : Πx : A.B Γ `+ N = Q : A
(App)
Figure 2: Kind Equality Γ `+ AppB D
x:A (M, N ) = Appx:C (P, Q) : [P/x]B

Γ, x : A `+ M : B Γ `+ N : A
`+ Γ valid x : A ∈ Γ +
Γ ` [N/x]M : [N/x]B
(Var)
Γ `+ xA : A (β)
Γ `+ AppB B
x:A (λx:A (M ), N ) = [N/x]M : [N/x]B

Γ `+ A kind Γ, x : A `+ B kind
Γ, x : A `+ M : B Γ `+ M : Πx : A.B
(λ) (η) B
Γ `+ λB Γ `+ λB A
x:A (Appx:A (M, x ))
= M : Πx : A.B
x:A (M ) : Πx : A.B

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

(Eq)
+
Γ ` M : Πx : A.B Γ `+ N : A Γ` M =N :B
+
(App)
Γ `+ AppB
x:A (M, N ) : [N/x]B Γ `+ M : A
(Refl)
Γ `+ M = M : A
Γ `+ M : A Γ `+ A = B kind
(Eq)
Γ `+ M : B Γ `+ M = N : A
(Sym)
Γ `+ N = M : A
Figure 3: Terms
Γ `+ M = N : A Γ `+ N = P : A
(Trans)
Γ` M =P :A
+
2.1 Unlabeled Terms
Finally, our development also requires a type system for Figure 4: Term Equality
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 The following notation x : A ∈ M means that A ≡ B for
translate the source language to unlabeled λ-terms because all free occurrences of xB in M .
the labels in η-reduction are not preserved by the transla-
tion.
Definition 2. Define x : A ∈ M inductively as follows:
The judgement forms for the unlabeled target language
are the same as those for the fully decorated target language. • x : A ∈ xA .
We distinguish by annotating the turnstile `− β . The rules
of inference are also identical: the distinction between the • x : A ∈ y B if x 6= y.
labeled and unlabeled systems lies in the information that
can be extracted from terms, not derivations. • x : A ∈ λC
x:B (M ).

3. BASIC METATHEORY • x : A ∈ λC
y:B (M ) if x 6= y, x : A ∈ B, x : A ∈ C and
x : A ∈ M.
3.1 Properties of the Source Language
• x : A ∈ AppC
x:B (M, N ).

Definition 1. Define the principal kind P(M ) by case anal-

• x : A ∈ AppCy:B (M, N ) if x 6= y, x : A ∈ B, x : A ∈ C,
ysis on M :
x : A ∈ M , and x : A ∈ N .
P(xA ) = A
The extension to kinds x : A ∈ B is straightforward.
P(λB
x:A (M )) = Πx : A.B
P(AppB
x:A (M, N )) = [N/x]B Lemma 2.

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

Proof. By induction on derivations. Proof. By induction on derivations.

3.2 Properties of the Target Language Definition 3. Define ηA (M ), for M an unlabeled λ-term,
We assume that the standard properties hold for the tar- by induction on A:
get language, the Logical Framework with fully decorated ηType (M ) = M
terms and β-equality. We also take β to be the usual com-
patible closure of β-reduction with no restrictions on the ηEl(P ) (M ) = M
labels, that is: ηΠx:A.B (M ) = λx.η[ηA (x)/x]B (M (ηA (x)))

AppD B
x:C (λx:A (M ), N ) β [N/x]M 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.

Proof. Each follows by induction on the length of A.

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

6. If Γ `+ + Proof. Case 1 follows by induction on A, and Case 2

β Πx : A.B =β Πx : C.D kind then Γ `β A =β
+ follows by induction on derivations of A β B and inversion
C kind and Γ, x : A `β B =β D kind. of the definition of ηA (M ).
Case 3 follows by induction on A. We consider Πx : A.B,
7. If Γ `+ M =β N : A then M =β N . where we assume x 6∈ FV(M ):
Proof. This is largely standard, following Streicher [23]. ηΠx:A.B (ηΠx:A.B (M ))
One subtlety of our presentation is that the rule β has
a premise that Γ `+ ≡ λx.η[ηA (x)/x]B (ηΠx:A.B (M )(ηA (x)))
β [N/x]M : [N/x]B. The equivalence
with the usual presentation can be demonstrated by first ≡ λx.η[ηA (x)/x]B ((λx.η[ηA (x)/x]B (M (ηA (x))))(ηA (x)))
proving Cases 2 and 3 for our presentation, and then show- β λx.η[ηA (x)/x]B (η[ηA (x)/x]B (M (ηA (ηA (x)))))
ing the equivalence of the two presentations by induction
∗β λx.η[ηA (x)/x]B (M (ηA (x)))
on derivations of each system. Alternatively, the properties
listed here can be shown directly for our presentation using ≡ ηΠx:A.B (M )
a Kripke-style model construction [3, 13].

3.3 The Unlabeled Target Language Definition 4. Define H(A) and H(M ) by structural in-
The judgements in the unlabeled system have the prop- duction:
erties of Proposition 1, as well as the following standard
H(Type) = Type
properties.
H(El(P )) = El(H(P ))
Proposition 2. H(Πx : A.B) = Πx : H(A).H(B)
H(xA ) = ηH(A) (x)
β M : A and M β N then Γ `β N : A.
1. If Γ `− −

H(λB
x:A (M )) = ηΠx:H(A).H(B) (λx.H(M ))
2. If Γ `−
β M : A then M is strongly normalizing under
β . 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.
3. Typechecking for `−
β is decidable.
Lemma 5. ηH(P(M )) (H(M )) ∗β H(M ). Furthermore, if
4. SOUNDNESS P(M ) ≡ Πx : A.B then ηH(Πx:A.B) (H(M )) +
β H(M ).

We now show that the η-expansions of terms typable in Proof. By induction on M , using Lemma 4 Case 3 di-
the βη-system are typable in the β-system. rectly for each term constructor.
We begin by defining two maps on terms, ηA (−) and
H(−). Intuitively, ηA (M ) represents the η-expansion of M The following lemma is similar to typical substitution lem-
at kind A, and H(M ) replaces all subterms of M with their mas. We need to include the side condition that x not occur
η-expansions at their principal kinds. This translation in- free in its kind because the definition of H(−) is for arbitrary
serting η-expansions through all subterms clearly models η terms and kinds, not only well-formed ones, and so imposes
equality, since the subterm M in an η-redex λB D E
x:A (Appx:C (M, x )) no conditions on subterms of its argument. The side con-
will be translated to a λ-abstraction, and so the translation dition will always hold for terms and kinds in well-formed
of the η-redex is β-equal to the translation of its reduct. judgements.
 Lemma 6. by Lemma 3, and
1. If x : C ∈ A, H(C) =β H(P(P )) and x 6∈ FV(H(C)) H(Γ) `− [H(N )/x]H(B) =β H([N/x]B) kind
then [H(P )/x]H(A) ∗β H([P/x]A).
by Lemma 6, Proposition 1 Case 4 (for `− ) and Sub-
2. If x : C ∈ M , H(C) =β H(P(P )) and x 6∈ FV(H(C)) ject Reduction (Proposition 2 Case 1), so H(Γ) `−β
then [H(P )/x]H(M ) ∗β H([P/x]M ). H(AppB x:A (M, N )) : H([N/x]B) by Eq.
Proof. By induction on A and M . We consider several
• β. By induction hypothesis H(Γ) `− H(λB x:A (M )) :
cases.
H(Πx : A.B) and H(Γ) `− H(N ) : H(A), so H(Γ) `−
• xA . Then: H(AppB B
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 rea-
[H(P )/x]ηH(A) (x) soning similar to App for the kind equality. Further-
≡ η[H(P )/x]H(A) (H(P )) more, by inversion Γ, x : A `+ M : B, so x : A ∈ M
≡ ηH(A) (H(P )) by Lemma 2. By Lemma 1, there either exists a sub-
derivation of Γ `+ P(N ) =βη A, in which case by in-
≡ ηH(P(P )) (H(P ))
duction hypothesis H(Γ) `− H(P(N )) =β H(A) kind,
∗β H(P ) or P(N ) ≡ A, in which case H(Γ) `− H(P(N )) =β
H(A) kind by Proposition 1 Case 4 and Refl; fur-
by Lemma 5, since x 6∈ FV(H(C)) and x : C ∈ xA
thermore, in either case x 6∈ FV(H(A)) by Proposi-
implies C ≡ A by inversion.
tion 1 Case 1. Similarly, H(Γ) `− H(P([N/x]M )) =β
• y B . Then [H(P )/x]ηH(B) (y) ≡ η[H(P )/x]H(B) (y) ≡ H([N/x]B) and x 6∈ FV(H([N/x]B)).
ηH([P/x]B) (y), by Lemma 4 Case 2 since [H(P )/x]H(B)∗β Therefore, by Lemma 4 Cases 2 and 3 and Lemma 6:
H([P/x]B) by induction hypothesis.
H(AppB B
x:A (λx:A (M ), N ))
• λB
y:A (M ). Then, by definition, Lemma 4 Cases 1 and ≡ η[H(N )/x]H(B) (ηH(Πx:A.B) (λx.H(M ))(H(N )))
2 and induction hypothesis: ≡ η[H(N )/x]H(B) (λx.η[ηH(A) (x)/x]H(B) (
[H(P )/x]H(λB
y:A (M ))
(λx.H(M ))(ηH(A) (x)))(H(N )))
β η[H(N )/x]H(B) (η[ηH(A) (H(N ))/x]H(B) (
≡ [H(P )/x]ηΠy:H(A).H(B) (λy.H(M ))
(λx.H(M ))(ηH(A) (H(N )))))
≡ ηΠy:[H(P )/x]H(A).[H(P )/x]H(B) ([H(P )/x]λy.H(M )) ≡ η[H(N )/x]H(B) (η[ηH(P(N )) (H(N ))/x]H(B) (
≡ ηΠy:H([P/x]A).H([P/x]B) ([H(P )/x]λy.H(M )) (λx.H(M ))(ηH(P(N )) (H(N )))))
≡ ηΠy:H([P/x]A).H([P/x]B) (λy.[H(P )/x]H(M )) ∗β η[H(N )/x]H(B) (η[H(N )/x]H(B) (
∗β ηΠy:H([P/x]A).H([P/x]B) (λy.H([P/x]M )) (λx.H(M ))(H(N ))))
β η[H(N )/x]H(B) (η[H(N )/x]H(B) ([H(N )/x]H(M )))
[P/x]B
≡ H(λy:[P/x]A ([P/x]M )) ∗β η[H(N )/x]H(B) (H([N/x]M ))
≡ ηH([N/x]B) (H([N/x]M ))
≡ H([P/x](λB
y:A (M )))
≡ ηH(P([N/x]M )) (H([N/x]M ))
∗β H([N/x]M )

Theorem 1 (Soundness). • η. By Lemma 1 either Γ `+ P(M ) =βη Πx : A.B as a

−
subderivation, in which case by induction hypothesis
• If Γ `+
βη A kind then H(Γ) `β H(A) kind. H(Γ) `− H(M ) : H(Πx : A.B), or P(M ) ≡ Πx : A.B;
in either case H(Γ) `− H(P(M )) =β H(Πx : A.B).
• If Γ `+ A =βη B kind then H(Γ) `− H(A) =β
Therefore:
H(B) kind.
−
H(λB B A
x:A (Appx:A (M, x )))
• If Γ `+
βη M : A then H(Γ) `β H(M ) : H(A). ≡ ηH(Πx:A.B) (λx.η[ηH(A) (x)/x]H(B) (
• If Γ `+ M =βη N : A then H(Γ) `− H(M ) =β H(M )(ηH(A) (x))))
H(N ) : H(A). ≡ ηH(Πx:A.B) (ηH(Πx:A.B) (H(M ))
+
β ηH(Πx:A.B) (H(M ))
Proof. By induction on derivations. We consider several ≡ ηH(P(M )) (H(M ))
cases. ∗β 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 : 5. COMPLETENESS
A.B) ≡ Πx : H(A).H(B) and H(Γ) `− β H(N ) : H(A), This section shows that the judgements in the target lan-
so H(Γ) `−β H(M )(H(N )) : [H(N )/x]H(B) by App. guage can be lifted to judgements in the source language:
Then: that is, judgements under the η-expansion translation H(−)
H(Γ) `− H(AppB in the system with unlabeled terms and β equality can be
β x:A (M, N ))
lifted to the system with decorated terms and βη equality.
≡ η[H(N )/x]H(B) (H(M )(H(N ))) First, we show that lifting equality over unlabeled terms
: [H(N )/x]H(B) to the fully decorated terms is possible: this is because the
derivations of well-formedness of unlabeled terms contain all Lemma 10. If Γ `+
βη M : A then Γ `
+
M =βη H + (M ) :
of the kind information necessary to assign kinds in the deco- A.
rated terms. Our presentation relating fully decorated terms
Proof. By induction on M , using Lemma 1 and the sim-
and unlabeled terms is strongly influenced by Streicher [23].
ple lemma that Γ `+ M =βη ηA (M ) : A.
Then we define an η-expansion translation with fully deco-
rated terms as the target, and show that all terms are βη- Theorem 2 (Completeness of Equality).
equal to themselves under the translation. The composition
of these two operations is equivalent to the original transla- 1. If Γ `+
βηM, N : A and H(Γ) `− H(M ) =β H(N ) :
tion from fully decorated terms to unlabeled terms, and so H(A) then Γ `+ M =βη N : A.
Completeness follows from the properties of each component
−
of the translation. 2. If Γ `+
βη A, B kind and H(Γ) ` H(A) =β H(B) kind
We begin by defining the stripping function from fully +
then Γ ` A =βη B kind.
decorated terms to unlabeled terms.
Proof. We show Case 1, where Case 2 is similar.
Definition 5. Define the stripping function |M | by induc- We know by Lemma 9 that H(Γ) `− |H + (M )| =β |H + (N )| :
tion on M : H(A). By Lemma 8 there are P and Q such that Γ `+ P =β
Q : A with |P | ≡ |H + (M )| and |Q| ≡ |H + (N )|. Therefore
|Type| = Type Γ `+ P =β H + (M ) : A and Γ `+ Q =β H + (N ) : A by
|El(P )| = El(|P |) Lemma 7, so Γ `+ H + (M ) =β H + (N ) : A by Trans and
|Πx : A.B| = Πx : |A|.|B| Γ `+ M =βη N : A by Trans and Lemma 10.
A
|x | = x Corollary 1 (Completeness). If Γ `− J then there
|λB
x:A (M )| = λx.|M | are ∆ and J 0 such that ∆ `+ J 0 , |∆| ≡ Γ and |J 0 | ≡ J.
B
|Appx:A (M, N )| = |M |(|N |) It is now possible to lift the metatheory of the `β sys-
tem to the `βη system. The following reduction relation
Lemma 7. If Γ `+
M : A, Γ
β `+
β N : A and |M | ≡ |N | |βη| ignores the labels on the fully decorated terms. As
then Γ `+ M =β N : A. we mentioned in the introduction, this relation is strongly
Proof. As in [23]. normalizing and Church–Rosser, and so this could be the
basis for an algorithm for testing conversion.
Lemma 8.
Definition 7. Define the relations β and η as:
1. If Γ `− +
β M : A then there is a P such that Γ `β P : A
AppD B
x:C (λx:A (M ), N ) β [N/x]M
and |P | ≡ M .
λD B E
x:C (Appx:A (M ), x ) η M
2. If Γ `− M =β N : A then there are P and Q such that
Γ `+ P =β Q : A, |P | ≡ M and |Q| ≡ N . Define reduction |βη| as the compatible closure over term
and kind constructors that ignores labels of βη; for example,
Proof. As in [23]. the compatible closure of application is completely defined
by:
The following map H + (M ) differs from H(M ) only by
mapping to fully decorated terms instead of unlabeled terms. x:A (M, N )  Appx:A (P, N ).
• If M  P then AppB B

+
Definition 6. Define ηA (M ) by induction on A: • If N  P then AppB
x:A (M, N )  Appx:A (M, P ).
B

+
βη M : A and M |βη| N then H(M )β
ηType (M ) = M Lemma 11. If Γ `+ +

+ H(N ).
ηEl(P ) (M ) = M
ηΠx:A.B (M ) = λB B A
x:A (Appx:A (M, x ))
Proof. By induction on M βη N , where the compatible
closure rules follow by induction hypothesis.
Define H + (M ) by induction on M :
x:C (λx:A (M ), N )) β
∗
For β, we need to show that H(AppD B
+ D B
H + (Type) = Type H([N/x]M ), where Γ `βη Appx:C (λx:A (M ), N ) : E. By in-
H + (El(P )) = El(H + (P )) version Γ `+ B
βη λx:A (M ) : Πx : A.B and Γ `
+
Πx : A.B =βη
H + (Πx : A.B) = Πx : H + (A).H + (B) −
Πx : C.D, so H(Γ) `β H(Πx : A.B) =βη H(Πx : C.D). By
+
H + (xA ) = ηH A
+ (A) (x ) Proposition 1 Case 7 and Church–Rosser H(A) =β H(C)
+ B and H(B) =β H(D), so:
H (λx:A (M )) =
+ H + (B)
+
ηΠx:H + (A).H + (B) (λx:H + (A) (H (M ))) H(AppD B B B
x:C (λx:A (M ), N )) ≡ H(Appx:A (λx:A (M ), N ))
+ B
H (Appx:A (M, N )) =
+ H + (B) + +
and the reduction sequence follows as for rule β in Sound-
η[H + (N )/x]H + (B) (Appx:H + (A) (H (M ), H (N ))) ness.
The reasoning for η-reduction is similar.
The H + (−) map extends to contexts in the obvious way.
The properties listed in Proposition 1 can now be shown
Lemma 9. |H + (M )| ≡ H(M ).
directly or transferred from the target language to the source
Proof. Induction on M . language.
 Proposition 3. Definition 9. We define the type checking algorithm on
fully decorated terms Γ; A ⇒+ kind and Γ; P ⇒+ A induc-
1. If Γ `+
βη M : A then FV(M ) ∪ FV(A) ⊆ FV(Γ). tively as follows:
2. If Γ, Γ0 `+ + 0 • Γ; Type ⇒+ kind.
βη J, Γ `βη A kind and x 6∈ FV(Γ) ∪ FV(Γ )
0 +
then Γ, x : A, Γ `βη J. • Γ; El(M ) ⇒+ kind if Γ; M ⇒+ Type.

3. If Γ, x : A, Γ0 `+ + 0 +
βη J and Γ `βη N : A then Γ, [N/x]Γ `βη
• Γ; Πx : A.B ⇒+ kind if Γ; A ⇒+ kind and Γ, x :
[N/x]J. A; B ⇒+ kind.
• Γ; xC ⇒+ C if x : C ∈ Γ.
4. If Γ `+ +
βη M : A then Γ `βη A kind.
• Γ; λD
x:C (M ) ⇒
+
Πx : C.D0 if Γ; C ⇒+ kind, Γ, x :
5. If Γ `+ + +
βη M : A and Γ `βη M : B then Γ `βη A = C; D ⇒+ kind, Γ, x : C; M ⇒+ D0 and D =|βη| D0 .
B kind.
• Γ; AppD
x:C (M, N ) ⇒
+
[N/x]D0 if Γ; C ⇒+ kind, Γ, x :
6. If Γ `+ +
βη Πx : A.B =βη Πx : C.D kind then Γ `βη C; D ⇒+ kind, Γ; M ⇒+ Πx : C 0 .D0 , Γ; N ⇒+ C 00 ,
+
A =βη C kind and Γ, x : A `βη B =βη D kind. C =|βη| C 0 =|βη| C 00 and D =|βη| D0 .
Lemma 13.
βη M : A and M |βη| N then Γ `βη N : A.
7. If Γ `+ +

1. If Γ `+ +
βη A kind then Γ; A ⇒ kind.
8. If Γ `+
βη M : A then M is strongly normalizing under
βη . 2. If Γ `+ +
βη P : A then there is a C such that Γ; P ⇒ C
+
and Γ `βη A = C kind.
6. TYPE CHECKING Proof. By induction on derivations.
Given the full metatheory of `+βη developed above, the de- Finally, we define a second stripping operation strip(M )
cidability of type checking is similar to the standard treat-
that strips off the labels on variables and applications and
ment [19]. The novelty in our presentation in this section is
the codomain off of abstractions.
that we derive the fully decorated terms, using the standard
presentation of terms with no labels in variables or applica- Definition 10. Stripping from the fully decorated terms
tion and a single label for the domain in abstractions. to the standard presentation of lambda terms is defined as
follows:
Definition 8. We define the decorating type checking al-
gorithm Γ; A ⇒ B; kind and Γ; M ⇒ P ; A inductively as strip(xA ) = x
follows: strip(λB
x:A (M )) = λx : strip(A).strip(M )
• Γ; Type ⇒ Type; kind. strip(AppBx:A (M, N )) = strip(M )(strip(N ))

• Γ; El(M ) ⇒ El(P ); kind if Γ; M ⇒ P ; Type. Observe that if strip(M ) ≡ strip(N ) then |M | ≡ |N |, and
so Lemma 7 lifts to the map strip(−).
• Γ; Πx : A.B ⇒ Πx : C.D; kind if Γ; A ⇒ C; kind and
Lemma 14.
Γ, x : C; B ⇒ D; kind.
1. If Γ; A ⇒+ kind and strip(Γ) ≡ strip(Γ0 ) then there is
• Γ; x ⇒ xC ; C if x : C ∈ Γ. an A0 such that Γ; strip(A) ⇒ A0 ; kind and strip(A) ≡
strip(A0 ).
• Γ; λx : A.M ⇒ λD x:C (P ); Πx : C.D if Γ; A ⇒ C; kind
and Γ, x : C; M ⇒ P ; D. 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) ≡
• Γ; M (N ) ⇒ AppD
x:C (P, Q); [Q/x]D if Γ; M ⇒ P ; Πx : strip(C 0 ) and strip(P ) ≡ strip(P 0 ).
C.D, Γ; N ⇒ Q; C 0 and C =|βη| C 0 .
Proof. By induction on derivations.
Lemma 12 (Correctness of the Algorithm). 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 ) ≡
• If Γ; A ⇒ C; kind then Γ `+
βη C kind. 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 ).
• If Γ; M ⇒ P ; C then Γ `+
βη P : C. Furthermore, C 0000 =|βη| C 000 , since by assumption C 0 =|βη|
C 00 and by Correctness of the Algorithm, Lemma 7 and
Proof. By induction on derivations of Γ; A ⇒ C; kind
Proposition 1 Case 7 C 00 =|βη| C 0000 and C 000 =|βη| C 0 .
and Γ; M ⇒ P ; C, using Lemma 3 Case 4 and Completeness
Therefore:
for application.
strip([N/x]D0 ) ≡ strip([N 0 /x]D00 )
We now introduce a type checking algorithm directly on 00
0 0
fully decorated terms to show completeness of the algorithm. strip(AppD
x:C (M, N )) ≡ strip(AppD
x:C 000 (M , N ))

Similar to our proof of completeness for the target language Γ0 ; strip(AppD

x:C (M, N )) ≡ strip(M )(strip(N ))
in the previous section, this allows us to decompose com- 00
0 0 0 00
⇒ AppD
x:C 000 (M , N ); [N /x]D
pleteness of the algorithm into simpler results about the
erasure and the algorithm itself.
 Corollary 2 (Completeness of the Algorithm). Γ `+ M : A Γ `+ N : [M/x]B
(q-Eq) B B
Γ`+ qx:A (pairx:A (M, N )) = N : [M/x]B
0
1. If Γ `+ βη C kind then there is a C such that Γ; strip(C) ⇒ Γ `+ M : Σx : A.B
C 0 ; kind. (pair-Uniq)
Γ `+ pairB B B
x:A (px:A (M ), qx:A (M ))
= M : Σx : A.B
0 0
2. If Γ `+
βη P : C then there are P and C such that plus the obvious compatible closure rules for formers Σ, pair,
Γ; strip(P ) ⇒ P 0 ; C 0 and Γ `+ C =βη C 0 kind. p and q.
Again, for the unlabeled system the term formers pair(M, N ),
Theorem 3 (Decidability of `+
βη ). The judgements
p(M ) and q(N ) have no labels.
Γ `+ J are decidable.
βη 7.3 Metatheory
We begin by assuming that the metatheory of the new
7. SINGLETONS AND DEPENDENT PAIRS kinds is well-behaved for the systems without the weakly
We now extend the above proofs to cover singletons and extensional equalities. These kinds of inductive definitions
dependent pairs as well. As we mentioned before, the im- have been studied extensively [12, 24].
portant difference with the earlier sections is that reduction The reduction relations are defined analogously to those
for the system with these kinds is not Church–Rosser. We for the Logical Framework with Π-kinds.
begin by presenting the fully decorated syntax for singletons The metatheory of singletons and dependent pairs with
and dependent pairs, and then outline the metatheory for the weakly extensional equalities closely follows the above
these new kinds. development, and the statement of the results in Sections 3,
4 and 5 does not change. We give here the extension of the
7.1 Singletons definitions to the new kinds and show some examples of the
We introduce new kind and term formers as used in the extended proofs for them.
following rules of inference:
Definition 11.
Γ `+ M : A
(S) P(∗A (M )) = SA (M )
Γ `+ SA (M ) kind
P(outA (M )) = A
Γ `+ M : A P(pairB
x:A (M, N )) = Σx : A.B
(∗)
Γ `+ ∗A (M ) : SA (M ) P(pB
x:A (M )) = A

Γ `+ N : SA (M ) P(qB
x:A (M )) = [pB
x:A (M )/x]B
(out)
Γ `+ outA (N ) : A
The definitions of x : A ∈ B and x : A ∈ M extend
Γ `+ M : A trivially to the new term formers.
(out-∗)
Γ ` outA (∗A (M )) = M : A
+
Definition 12.
Γ `+ N : SA (M ) ηSA (M ) (N ) = ∗(M )
(∗-Uniq)
Γ `+ ∗A (M ) = N : SA (M ) ηΣx:A.B (M ) = pair(ηA (p(M )), η[p(M )/x]B (q(M )))
plus the obvious compatible closure rules for kind and term
Definition 13.
formers S, ∗ and out.
For the unlabeled system, the term formers ∗(M ) and H(∗A (M )) = ∗(H(M ))
out(M ) have no labels. H(outA (M )) = ηH(A) (out(H(M )))
7.2 Dependent Pairs H(pairB
x:A (M, N )) = ηH(Σx:A.B) (pair(H(M ), H(N )))
H(pB x:A (M )) = ηH(A) (p(H(M )))
Γ `+ A kind Γ, x : A `+ B kind H(qB
(Σ) x:A (M )) = η[H(pB (M ))/x]H(B) (q(H(M )))
x:A
Γ ` Σx : A.B kind
+

We now show the case of ∗-Uniq for Theorem 1. By

Γ `+ M : A Γ `+ N : [M/x]B Lemma 1 Γ `+ N : P(N ) and either P(N ) ≡ SA (M ) or
(pair) B
Γ ` pairx:A (M, N ) : Σx : A.B
+ Γ `+ P(N ) =βη SA (M ) kind as a subderivation; in the lat-
ter case we also have P(N ) ≡ SA0 (M 0 ) and subderivations
Γ `+ M : Σx : A.B of Γ `+ M =βη M 0 : A and Γ `+ A =βη A0 kind, and so
(p) by induction hypothesis H(Γ) `− H(M ) =β H(M 0 ) : H(A)
Γ `+ pB
x:A (M ) : 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 )) ∗
Γ `+ M : Σx : A.B H(N ) by Lemma 5, so H(N ) ≡ ∗(H(M )), and so H(Γ) `−
(q)
Γ `+ q B B
x:A (M ) : [px:A (M )/x]B H(N ) ≡ ∗(H(M )) =β ∗(H(M )) : SH(A) (H(M )) ≡ H(SA (M )).
Finally, although the equalities corresponding to the weakly
Γ `+ M : A Γ `+ N : [M/x]B extensional equality rules cannot be interpreted as reduc-
(p-Eq) B B
Γ `+ px:A (pairx:A (M, N )) = M : A tions because they are not Church–Rosser, the translation to
the unlabeled terms yields an algorithm that is both strongly volume 1584 of Lecture Notes in Computer Science,
normalizing and Church–Rosser, and so that algorithm can pages 241–259. Springer–Verlag, 1998.
be used to test conversion of the source-language terms. [3] A. Compagnoni and H. Goguen. Typed operational
semantics for higher order subtyping. Technical
8. CONCLUSIONS AND FUTURE WORK Report ECS-LFCS-97-361, University of Edinburgh,
We have demonstrated that the terms of the source Log- July 1997. A later version is published as [4].
ical Framework with βη-equality can be represented in the [4] A. Compagnoni and H. Goguen. Typed operational
target language with only β-equality, with the consequence semantics for higher-order subtyping. Information and
that type checking for the source language is decidable. We Computation, 184(2):242–297, Aug. 2003.
further extended our results to show that weakly extensional [5] T. Coquand. An algorithm for testing conversion in
equality for singletons and dependent pairs is decidable. type theory. In G. Huet and G. Plotkin, editors,
To provide a complete basis for modules systems, we need Logical Frameworks. Cambridge University Press,
to extend our results to include the implicit form of single- 1991.
tons and subtyping. We believe that the additional com- [6] T. Coquand, R. Pollack, and M. Takeyama. A logical
plexity of subtyping in Stone and Harper’s presentation can framework with dependently typed records. Extended
be dealt with by applying appropriate η-expansions for the version of [7], 2003.
supertype, but we have not studied the technical details: [7] T. Coquand, R. Pollack, and M. Takeyama. A logical
with the interrelated judgements, it is not clear whether the framework with dependently typed records. In
η-expansion can be applied at the judgemental level or if the Proceedings of Typed Lambda Calculus and
explicit term language needs to be extended with references Applications, TLCA’03, volume 2701 of Lecture Notes
to subtyping. in Computer Science. Springer-Verlag, 2003. See
We are also interested in studying whether the general extended version [6].
approach of modeling weakly extensional equalities can be [8] R. D. Cosmo and D. Kesner. A confluent reduction
extended to include colimit types such as the empty type or system for the extensional typed lambda-calculus with
sum types. Finally, we have demonstrated [14] that the re- pairs, sum, recursion and terminal object. In
sults established here for the Logical Framework with βη re- Proceedings of the 20st International Colloquium on
duction are sufficient to justify the decidability of Coquand’s Automata, Languages and Programming (ICALP’93),
original algorithm for deciding βη-equality [5] and Harper volume 700 of Lecture Notes in Computer Science,
and Pfenning’s algorithm [15], but we would like to extend pages 645–656. Springer–Verlag, July 1993.
this approach to types beyond dependent function spaces. [9] G. Dowek, G. Huet, and B. Werner. On the definition
This article concentrates on type theories sufficient as a of the eta-long normal form in type systems of the
theoretical basis for modules systems, and so we are able cube. In Informal Proceedings of the Workshop on
to avoid a sophisticated model construction for the basic Types for Proofs and Programs, 1993.
Logical Framework. However, extending our technique to [10] H. Geuvers. Logics and Type Systems. PhD thesis,
systems with either impredicativity or higher-order type- Katholieke Universiteit Nijmegen, Sept. 1993.
valued operators would force us to use some kind of model [11] N. Ghani. Eta-expansions in dependent type theory -
construction. To see this, consider that for the expansions the calculus of constructions. In Typed Lambda
to be sound the type-directed η-expansion function needs to Calculus and Applications, volume 1210 of Lecture
be closed under substitution within its type argument, but Notes in Computer Science, pages 164–180.
substituting a type for a type variable in the type argument, Springer–Verlag, 1997.
for example Πx : A.B for X, leads to a different expansion.
[12] H. Goguen. A Typed Operational Semantics for Type
Theory. PhD thesis, University of Edinburgh, Aug.
Acknowledgments 1994.
I would like to thank Mariangiola Dezani for her kind invi- [13] H. Goguen. A Kripke-style model for the admissibility
tation to visit the Università di Torino, Robert Harper for of structural rules. In Proceedings of TYPES, volume
suggesting that I study the metatheory of singletons, Gilles 2277 of Lecture Notes in Computer Science, pages
Barthe for pointing me to [6], Thierry Coquand and Randy 112–124. Springer–Verlag, 2000.
Pollack for interesting discussions on their model construc- [14] H. Goguen. Justifying algorithms for beta-eta
tion, Eduardo Bonelli for recommending [8], and Zhaohui conversion. 2004. Submitted to FOSSACS 2005.
Luo for asking whether reduction was preserved by an ear- [15] R. Harper and F. Pfenning. On equivalence and
lier definition of the H(−) map. I would also like to thank canonical forms in the LF type theory. ACM Trans.
my wife Adriana Compagnoni both for helpful technical dis- on Computational Logic, 2003. (To appear).
cussions and for her encouragement as I was writing this [16] F. Joachimski. Syntactic analysis of eta-expansions in
article. pure type systems. Information and Computation,
182(1):53–71, 2003.
9. REFERENCES [17] J. W. Klop. Combinatory reduction systems.
[1] M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Mathematical Centre Tracts 127, Centre for
Explicit substitutions. Journal of Functional Mathematics and Computer Science, Amsterdam,
Programming, 1(4):375–416, 1991. 1980. PhD thesis
[2] G. Barthe. Existence and uniqueness of normal forms [18] J. Lambek and P. J. Scott. Introduction to Higher
in pure type systems with beta-eta conversion. In Order Categorical Logic. Cambridge studies in
Proceedings of Computer Science Logic, CSL’98,
 advanced mathematics. Cambridge University Press, Unpublished manuscript.
1989. [22] C. A. Stone and R. Harper. Equivalence and
[19] Z. Luo. Computation and Reasoning. Oxford singletons. ACM Transactions on Programming
University Press, 1994. Languages and Systems, 2004. Submitted.
[20] D. MacQueen. Using dependent types to express [23] T. Streicher. Semantics of Type Theory: Correctness,
modular structure. In Proceedings of the Thirteenth Completeness and Independence Results. Birkhäuser,
ACM Symposium on the Principles of Programming 1991.
Languages, 1986. [24] B. Werner. Une Théorie des Constructions Inductives.
[21] A. Salvesen. The Church-Rosser property for pure PhD thesis, Université Paris 7, 1994.
type systems with βη-reduction, Nov. 1991.