Extensional Normalization in the Logical Framework with Proof Irrelevant Equality

Andreas Abel Department of Computer Science Ludwig-Maximilians-University Munich

Abstract

We extend the Logical Framework by proof irrelevant equality types and present an algorithm that computes unique long normal forms. The algorithm is inspired by normalization-by-evaluation. Equality proofs which are not reflexivity are erased to a single object ∗. The algorithm decides judgmental equality, its completeness is established by a PER model.

1. Introduction

In intensional Martin-Löf type theory (ITT), but also in the Calculus of Inductive Constructions which underlies the Coq proof assistant, we distinguish between definitional equality of terms t and t′ of type T, given by the judgement Γ ⊢ t = t′ : T, and propositional equality which is established by providing an inhabitant of the identity set Id_{T} t t′. While definitional equality is decidable and invoked during type checking, propositional equality is not. Inhabitants of Id_{T} t t′ can be assumed and constructed by induction. However, there is at most one canonical inhabitant, the polymorphic constant refl; if t is definitionally equal to t′, then Γ ⊢ refl : Id_{T} t t′ is canonical, otherwise, there are only non-canonical inhabitants.

In this respect, identity sets are similar to the unit set which has exactly one canonical inhabitant. For the unit set one easily proves that any two inhabitants are propositionally equal. The question whether this can be shown for the identity set as well has been answered negatively by Hofmann and Streicher [11]. The principle UIP (uniqueness of identity proofs) which states that any two proofs of propositional equality are propositionally equal themselves is refuted by interpreting each set T of ITT as a groupoid, and each identity set Id_{T} t t′ as a set of isomorphisms between the objects t and t′ in the groupoid T. This model leaves room for more than one isomorphism per each pair of objects. Awodey and Warren [8] and Gambino and Garner [10] continue this program by looking at isomorphisms of isomorphisms and towers of identity sets leading to weak ω-groupoids and homotopy theory.

While UIP is not provable and adding it as a constant might destroy canonicity,^{1} we can add the principle of proof irrelevance for identity sets, as Altenkirch suggested [5].

\frac{Γ ⊢ p, q : Id_{T} t t′}{Γ ⊢ p = q : Id_{T} t t′}

Any two proofs of a propositional equality are definitionally equal. In the presence of this rule, UIP has a trivial proof. An instance of proof irrelevance (for q = refl) is Martin-Löf’s η-expansion for the identity type [12]:

\frac{Γ ⊢ p : Id_{T} t t}{Γ ⊢ p = refl : Id_{T} t t}

Streicher’s axiom K [14] is the propositional variant of this principle, again, it has a trivial proof.

In this article, we are concerned with a decision procedure for definitional equality in the presence of proof irrelevant identity sets. We aim at computing unique η-long β-normal forms of well-typed terms which can then be compared syntactically. There are a few challenging issues:

1. Unlike in settings with proof-irrelevant propositions that are never eliminated [4, 7], we need to distinguish a refl-proof from a merely hypothetical proof of a possibly false identity in order to resolve identity elimination.

\frac{Γ ⊢ S : Set  Γ ⊢ s, s′ : S  Γ ⊢ p : Id_{S} s s′ Γ ⊢ C : (x, x′:S) → Id_{S} x x′ → Set Γ ⊢ h : (x:S) → C x x refl}{Γ ⊢ idElim_{S,s,s′} p C h : C s s′ p}
idElim_{S,s,s} refl C h = h s

2. An η-expansion at identity type can trigger a new βreduction.^{2}

idElim_{A,a,a} p C h ⟶_{η^{−}} idElim_{A,a,a} refl C h ⟶_{β} h a Hence, we cannot simply compute β-normal forms which we η-expand in a second phase.

1Canonicity means that each closed term reduces to a canonical form, e.g., each closed term of natural number type reduces to a numeral

Our solution is as follows: We introduce a symbol ∗ for irrelevant proofs which may be different from refl.

\frac{Γ ⊢ p : Id_{T} t t′}{Γ ⊢ ∗ : Id_{T} t t′}

To obtain unique normal forms, we replace each proof p : Id_{T} t t′ with refl if t and t′ have the same normal form, and with ∗ otherwise. This step may not be done too early, in particular, bottom-up normalization (like hereditary substitutions [15]) does not work. For example, consider the following computation in context X:Set, x:X.

nf((λy:X.λp:Id_{X} x y. p) x)
= nf(λy:X.λp:Id_{X} x y. p) nf(x)
= (λy:X.λp:Id_{X} x y. ∗) x
= λp:Id_{X} x x. ∗

We have checked for identity of x and y too early. A topdown normalization function might work, but it is not compositional, thus, a proof of normalization could be hard.

In this article, we consider a strategy that is inspired by normalization-by-evaluation. It is type-directed; a term of function type is normalized by applying it to a fresh, ηexpanded variable. At base type, it is sufficient to compute the β-normal form. However, here we have the same issue that η-expansion may not be executed eagerly, otherwise we will produce ∗s where we could have refls. For example, a variable f of type (x:X) → (y:X) → Id_{X} x y will eagerly expand to λxλy. ∗, missing that f x x = refl. We therefore treat η-expansion of variables lazily, we introduce markers Up^{T} t which remember that t needs to be η-expanded.

For the moment, we can show completeness of our normalization procedure only for the logical framework [13] with identity sets (see the rules in Sec. 2). In particular, we did not succeed in adding function sets. However, adding a natural number set and other base types imposes no problem.

Overview. In Sec. 2 we recapitulate syntax and inference rules of the logical framework with proof irrelevant identity sets. In Sec. 3 we define unique normal forms and present a partial normalization function whose soundness is immediate. For completeness, we construct a PER model in Sec. 4. For two semantic objects, we show that if they are related in the PER of their type, then they have the same normal form.

The opposite direction could only be shown for objects of base type. Termination and completeness of the normalization function follows from the usual fundamental theorem.

2. Syntax

We consider Martin-Löf’s logical framework with Id as the only set former. While it is unproblematic to add a set of natural numbers, we do not know how to extend the present word to function sets or Σ-sets yet.

Raw expressions and typing contexts are given by the following grammar, where we use uppercase letter to indicate types and lowercase letters to indicate terms.

Exp ∋ p, q, r, s, t ::= x | λxt | r s | (x:S) → T
| Set |Type
| refl | idElim_{S,s,s′} p T t | Id_{T} t t′
Cxt ∋ Γ  ::= ⋄ | Γ, x:T

Note that we use refl polymorphically, as opposed to adding a monomorphic constant refl : (T :Set) → (t:T) → Id_{T} t t to the logical framework. Typing and equality is specified via the following five judgements, which are introduced by the rules in Figure 1. Note that we have omitted all congruence rules for equality.

Γ ⊢  Γ is a well-formed context
Γ ⊢ T  T is a well-formed type in Γ
Γ ⊢ t : T  t has type T in Γ
Γ ⊢ T = T′  T and T′ are equal types in Γ
Γ ⊢ t = t′ : T t and t′ are equal terms of type T in Γ

We write Γ ⊢ J to mean one of these judgements. These judgements enjoy the usual properties such as weakening, context conversion, substitution, and inversion of typing. We extend Exp to Exp^{∗} by adding the constructors ∗ and Up^{T} t. Normalization will erase all hypothetical identity proofs to ∗, i.e., all proofs that do not normalize to refl but to a term with a variable in head position. In order to define well-typed normal forms, we introduce another set of judgements ⊢^{∗} which are clones of the ⊢ judgements, with the additional rule

\frac{Γ ⊢^{∗} p : Id_{T} t t′}{Γ ⊢^{∗} ∗ : Id_{T} t t′} .

Our normalization procedure will use marked terms Up^{T} t which express that term t is to be eta-expanded at type T. These markers have only administrative purpose, so we add the rules

\frac{Γ ⊢^{∗} t : T}{Γ ⊢^{∗} Up^{T} t : T} \frac{Γ ⊢^{∗} t : T}{Γ ⊢^{∗} Up^{T} t = t : T} .

Theorem 1 (Conservativity) If Γ ⊢^{∗} J and Γ, J do not mention ∗ and Up, then Γ ⊢ J.

2Note that this is unlike the case for function types where unrestricted η expansion can create a β-redex whose reduction leads back to the original term but makes no progress.

t^{A→B} x ⟶_{η^{−}} (λy. t y) x ⟶_{β} t x

Well-formed contexts.

\overline{⋄ ⊢} \frac{Γ ⊢ Γ ⊢ T :Type}{Γ, x:T ⊢}

Dependently-typed λ-calculus.

\frac{Γ ⊢  (x:T) ∈ Γ}{Γ ⊢ x : T}  \frac{Γ ⊢ t : T  Γ ⊢ T = T′ :Type}{Γ ⊢ t : T′}
\frac{Γ ⊢ S :Type  Γ, x:S ⊢ T :Type}{Γ ⊢ (x:S) → T :Type}  \frac{Γ, x:S ⊢ t : T}{Γ ⊢ λxt : (x:S) → T}  \frac{Γ ⊢ r : (x:S) → T  Γ ⊢ s : S}{Γ ⊢ r s : T [s/x]}

Equality axioms.

\frac{Γ, x:S ⊢ t : T Γ ⊢ s : S}{Γ ⊢ (λxt) s = t[s/x] : T [s/x]} \frac{Γ ⊢ t : (x:S) → T}{Γ ⊢ t = λx. t x : (x:S) → T} x ∉ FV(t)

Sets.

\frac{Γ ⊢}{Γ ⊢ Set :Type}  \frac{Γ ⊢ T : Set}{Γ ⊢ T :Type}

Identity set.

\frac{Γ ⊢ T : Set  Γ ⊢ t : T  Γ ⊢ t′ : T}{Γ ⊢ Id_{T} t t′ : Set}  \frac{Γ ⊢ T : Set  Γ ⊢ t : T}{Γ ⊢ refl : Id_{T} t t}
\frac{Γ ⊢ S : Set  Γ ⊢ s, s′ : S  Γ ⊢ p : Id_{S} s s′  Γ ⊢ C : (x, x′:S) → Id_{S} x x′ → Set  Γ ⊢ h : (x:S) → C x x refl}{Γ ⊢ idElim_{S,s,s′} p C h : C s s′ p}

Equality axioms.

\frac{Γ ⊢ S : Set Γ ⊢ s : S Γ ⊢ C : (x, x′:S) → Id_{S} x x′ → Set Γ ⊢ h : (x:S) → C x x refl}{Γ ⊢ idElim_{S,s,s} refl C h = h s : C s s refl}

\frac{Γ ⊢ p, q : Id_{T} t t′}{Γ ⊢ p = q : Id_{T} t t′}

Figure 1. Inference rules Proof. As in [4]: Replace in the derivation of Γ ⊢^{∗} J each occurrence of ∗, which has been introduced by forgetting proof p, by just this p. Also, replace every Up^{T} t by t. Remove or replace the affected inference steps. □

3. Normalization

In this section, we exhibit a type-directed algorithm norm^{Γ ⊢T} t which, given a well-typed term Γ ⊢ t : T, computes the unique long normal form of t where all identity proofs have been replaced by either refl or ∗. The purpose of the algorithm is to decide judgmental equality, in particular we ask for the following properties. Let Γ ⊢ t, t′ : T.

1. Soundness: If norm^{Γ ⊢T} t = norm^{Γ ⊢T} t′ then Γ ⊢ t = t′ : T.

2. Completeness: If Γ ⊢ t = t′ : T then norm^{Γ ⊢T} t = norm^{Γ ⊢T} t′.

3. Termination: norm^{Γ ⊢T} t is defined.

We will define normalization on terms, hence, the algorithm will be sound by construction. Our soundness theorem is no more than subject reduction. Completeness and termination will follow from the construction of a PER model in Section 4.

3.1. Normal forms

It is illustrative to first present a grammar of normal forms, to see where the algorithm is supposed to take us. We distinguish long normal forms v, identified by a judgement Γ ⊢ v ⇑ T, from neutral normal forms u, identified by Γ ⊢ u ⇓ T. Neutral normal forms are terms whose head is a variable or ∗ and whose spine consists of long normal forms. Only certain expressions are candidates for long normal forms. In any case, they need to be β-normal; in particular, they must be generated by the following grammar.

u, U ::= x | u v | idElim_{V,v,v′} ∗ C h
v, V ::= u | λxv | refl | ∗
| (x:V) → V′ | Id_{V} v v′ | Set

Neutral normal forms Γ ⊢^{∗} u ⇓ T.

\frac{Γ ⊢^{∗}}{Γ ⊢^{∗} x ⇓ Γ(x)}

\frac{Γ ⊢^{∗} u ⇓ (x:S) → T Γ ⊢^{∗} v ⇑ S}{Γ ⊢^{∗} u v ⇓ T [v/x]}

\frac{Γ ⊢^{∗} V ⇑ Set  Γ ⊢^{∗} v, v′ ⇑ V  v ≢ v′ Γ ⊢^{∗} C ⇑ (x, x′:V) → Id_{V} x x′ → Set Γ ⊢^{∗} h ⇑ (x:V) → C x x refl}{Γ ⊢^{∗} idElim_{V,v,v′} ∗ C h ⇓ C v v′ ∗}

\frac{Γ ⊢^{∗} u ⇓ T Γ ⊢^{∗} T = T′ :Type}{Γ ⊢^{∗} u ⇓ T′}

Usually, one would consider idElim_{V,v,v′} u C h neutral if u was. In our case, we only have two possible proofs u of identity: refl and ∗. The first would constitute a β-redex, thus, only the second is possible, and it forces v ≢ v′.

(Long) normal forms (lnf) Γ ⊢^{∗} v ⇑ T.

\frac{Γ ⊢^{∗} U ⇓ Set  Γ ⊢^{∗} u ⇓ U}{Γ ⊢^{∗} u ⇑ U}  \frac{Γ ⊢^{∗} t : T}{Γ ⊢^{∗} refl ⇑ Id_{T} t t}

\frac{Γ ⊢^{∗} v, v′ ⇑ T  v ≢ v′  Γ ⊢^{∗} p : Id_{T} v v′}{Γ ⊢^{∗} ∗ ⇑ Id_{T} v v′}

\frac{Γ, x:S ⊢^{∗} v ⇑ T}{Γ ⊢^{∗} λxv ⇑ (x:S) → T}

\frac{Γ ⊢^{∗} v ⇑ T Γ ⊢^{∗} T = T′ :Type}{Γ ⊢^{∗} v ⇑ T′}

Neutral nfs of base type U are lnfs, yet in our case, we exclude the identity type Id_{T} t t′ as base type, thus, only neutral types Γ ⊢^{∗} U ⇓ Set remain. The two possible lnfs of identity type have their own introduction rules: ∗ is a lnf of identity type Id_{T} v v′ if v and v′ are different lnfs and there the identity type is inhabited by some proof p.

Normal types Γ ⊢^{∗} V ⇑ Set/Type.

\frac{Γ ⊢^{∗} U ⇓ Set}{Γ ⊢^{∗} U ⇑ Set}  \frac{Γ ⊢^{∗} V ⇑ Set  Γ ⊢^{∗} v, v′ ⇑ V}{Γ ⊢^{∗} Id_{V} v v′ ⇑ Set}

\frac{Γ ⊢^{∗} V ⇑ Set}{Γ ⊢^{∗} V ⇑Type}  \frac{Γ ⊢^{∗}}{Γ ⊢^{∗} Set ⇑Type}

\frac{Γ ⊢^{∗} V ⇑Type Γ, x:V ⊢^{∗} V′ ⇑Type}{Γ ⊢^{∗} (x:V) → V′ ⇑Type}

The three judgements entail well-typedness and are preserved under weakening with well-formed contexts. Note that these judgements do not immediately give us an method to check whether a term is normal, since they rely on the type equality judgement.

Remark 2 Note that while we can derive Γ ⊢ x ⇓ Id_{T} t t′ for a suitable Γ, we do not get Γ ⊢ x ⇑ Id_{T} t t′, since Id_{T} t t′ is not a neutral type.

3.2. Normalization Algorithm

We denote parallel substitution by tσ, where σ is a map from variables to expressions such that σ(x) ≠ x for only finitely many x. Update of σ at x by t is written (σ, x = t).

A weak head normal form (whnf) w is an expression without β-redex in weak head position. In our case, this means concretely:

w ::= u | Up^{(x:S)→T} u | λxt | (x:S) → T
| refl | ∗ | Id_{T} t t′ | Set

The algorithm is given by the entry point function norm^{Γ ⊢T} t and six mutual recursive partial functions:

nf^{W} w  compute lnf of whnf w, directed by type W
NF W  compute lnf of type W
↑^{W} u  η-expand neutral nf u at type W
⦇t⦈  compute whnf of term t
w@s  compute whnf of application w s
idE …  compute whnf of idElim

The top-level normalization function replaces free variables x : S by their reflection ↑^{S} x and calls nf on the whnfs.

norm^{Γ ⊢T} t = nf^{⦇T σ⦈}⦇tσ⦈ where σ(x) = ↑^{⦇Γ(x)⦈} x.

Type-directed normalization η-expands its argument, a whnf, at function type, using active application to a reflected fresh variable ↑ x. Active application triggers further normalization. At identity type, whnfs are already nfs, and at neutral types U we only encounter neutral nfs u.

nf^{(x:S)→T} w = λx. nf^{⦇T [s/x]⦈}w@s
where x ∉ FV(w) and s = ↑^{⦇S⦈} x
nf^{Set}W  = NF W
nf^{Type}W  = NF W
nf^{Id_{S} s s′}w = w
nf^{U}u  = u

Type normalization. This is just nf for types.

NF Set  = Set
NF ((x:S) → T) = (x:NF ⦇S⦈) → NF ⦇T [(↑^{⦇S⦈} x)/x]⦈
NF (Id_{T} t t′)  = Id_{(NF W)} (nf^{W} ⦇t⦈) (nf^{W} ⦇t′⦈)
where W = ⦇T ⦈
NF U  = U

Eta-expansion (reflection) acts on a neutral nf u of type W. In case of an identity type Id_{T} t t′, if t and t′ have the same normal form, we can safely expand u to refl, and if not, then to ∗. It is crucial that the point of evaluating ↑^{Id_{T} t t′} u we have the complete information about t and t′. This is ensured by two means:

1. Free variables in any term involved in normalization are reflected, i. e., they can only appear inside marked terms Up^{(x:S)→T} u or neutral nfs u of neutral type.

2. Reflection at function types is delayed: ↑^{(x:S)→T} u produces a marked term Up^{(x:S)→T} u which waits for an argument. Only after application, reflection continues (see below).

↑^{(x:S)→T} u = Up^{(x:S)→T} u
↑^{Id_{T} t t′} u = \{ \begin{matrix}refl & if nf^{⦇T ⦈}⦇t⦈ ≡ nf^{⦇T ⦈}⦇t′⦈ \\ ∗ & otherwise \end{matrix}
↑^{Set} U  = U
↑^{U} u  = u

Weak head normalization is standard: It eliminates all top level β-redexes.

⦇r s⦈  = ⦇r⦈@s
⦇idElim_{S,s,s′} p C h⦈ = idE_{S,s,s′} ⦇p⦈ C h
⦇w⦈  = w

Active application eliminates functions, which are either λabstractions or delayed reflections Up^{(x:S)→T} u at function type.

\begin{aligned}(λxt)@s & = & ⦇t[s/x]⦈ \\ (Up^{(x:S)→T} u)@s & = & ↑^{⦇T [s/x]⦈} (u (nf^{⦇S⦈}⦇s⦈)) \end{aligned}

Identity proof elimination of refl is a β-redex which is resolved by idE. Elimination of ∗ leads to a neutral normal form, which is subjected to η-expansion. This way, idElim can never stack up in neutrals.

idE_{S,s,s′} refl C h = ⦇h s⦈
idE_{S,s,s′} ∗ C h = ↑^{⦇C s s′ ∗⦈} (idElim_{V_{S},v_{s},v_{s′}} ∗ V_{C} v_{h})

where W_{S} = ⦇S⦈

V_{S} = NF W_{S}
v_{s} = nf^{W_{S}}⦇s⦈
v_{s′} = nf^{W_{S}}⦇s′⦈
V_{C} = nf^{(x,x′:S)→Id_{S} x x′→Set}⦇C⦈
v_{h} = nf^{(x:S)→C x x refl}⦇h⦈

3.3. Soundness

Soundness of normalization follows simply by inspection of the equations. Formally, we prove:

Theorem 3 (Subject reduction) Let Γ ⊢^{∗} t : T.

1. If norm^{Γ ⊢T} t = v then Γ ⊢^{∗} t = v : T.

2. If nf^{T} t = v then Γ ⊢^{∗} t = v : T.

3. If NF T = V then Γ ⊢^{∗} T = V :Type.

4. If ↑^{T} t = w then Γ ⊢^{∗} t = w : T.

5. If ⦇t⦈ = w then Γ ⊢^{∗} t = w : T.

6. If Γ ⊢^{∗} t s : S and t@s = w then Γ ⊢^{∗} t s = w : S.

7. If Γ ⊢ idElim_{S,s,s′} p C h : T and idE_{S,s,s′} p C h = w then Γ ⊢ idElim_{S,s,s′} p C h = w : T.

Proof. Simultaneously, by induction on the evaluation trace of the functions. More precisely, we view the functions as mutually inductive relations, e.g., ⦇ ⦈ as the binary relation ⦇ ⦈ = , which are given by inference rules, for instance,

\frac{\begin{matrix}⦇T ⦈ = W  ⦇t⦈ = w  ⦇t′⦈ = w′ \\ nf^{W} w = v  nf^{W} w′ = v \end{matrix}}{↑^{Id_{T} t t′} u = refl}

Then, we show the theorem by mutual induction on these relations. In case of the rule above, we have Γ ⊢^{∗} u : Id_{T} t t′ which entails Γ ⊢^{∗} T : Set and Γ ⊢^{∗} t, t′ : T by inversion. By induction hypotheses we get Γ ⊢^{∗} T = W : Set, Γ ⊢^{∗} t = w : T, Γ ⊢^{∗} t′ = w′ : T, Γ ⊢^{∗} w = v : W and Γ ⊢^{∗} w′ = v : W. Putting these equalities together, we get Γ ⊢^{∗} t = t′ : T, hence, Γ ⊢^{∗} refl : Id_{T} t t′. By proof irrelevance, Γ ⊢^{∗} u = refl : Id_{T} t t′. □

Corollary 4 (Soundness) If Γ ⊢ t, t′ : T and norm^{Γ ⊢T} t = norm^{Γ ⊢T} t′ then Γ ⊢ t = t′ : T.

Proof. Certainly, Γ ⊢^{∗} t, t′ : T, hence, by subject reduction Γ ⊢^{∗} t = norm^{Γ ⊢T} t : T and Γ ⊢^{∗} t′ = norm^{Γ ⊢T} t′ : T. It follows Γ ⊢^{∗} t = t′ : T and, by conservativity, Γ ⊢ t = t′ : T. □

4. Model and Completeness

In this section we prove that normalization terminates and is complete for judgmental equality, i. e., if Γ ⊢ t = t′ : T then norm^{Γ ⊢T} t and norm^{Γ ⊢T} t′ are defined and αequivalent. To this end, we construct a partial equivalence relation (PER) [W] for each type W in whnf such that:

1. If Γ ⊢ t = t′ : T and σ(x) = ↑^{⦇Γ(x)⦈} x for all x ∈ dom(Γ) then (⦇tσ⦈, ⦇t′σ⦈ ∈ [⦇T σ⦈].

2. If (w, w′) ∈ [W] then nf^{W} w and nf^{W} w′ are defined and equal.

We do not prove here that nf^{W} w is actually a long normal form Γ ⊢ nf^{W} w ⇑ W; this result could be achieved by switching to a Kripke model where Γ is available. Also, the PER model is unsound: every type is inhabited in the model. This does not bother us either; soundness can also be obtained by switching to a Kripke model.

4.1. PER Model

Dealing with a predicative type theory, we can construct a model from below. For convenience, we use inductionrecursion [9]. Our construction is analogous to previous work [1, 2].

We write w = w′ ∈ W for (w, w′) ∈ [W] and extend this to all terms by letting t = t′ ∈ T be ⦇t⦈ = ⦇t′⦈ ∈ ⦇T ⦈, which more precisely means the conjunction of ⦇t⦈ = w, ⦇t′⦈ = w′, ⦇T ⦈ = W, and w = w′ ∈ W. Also t ∈ T is short for t = t ∈ T.

First, we construct a PER = ∈ Set by induction, and simultaneously for each W ∈ Set its extension, a PER [W], by recursion on W ∈ Set. Then, we proceed with = ∈ Type and [W] for W ∈ Type. We will not repeat the proofs that the obtained relations are indeed PERs and that related sets or types have the same extension [1]. In our case, the construction of Set is trivial: there are only two types of sets, namely neutral sets and identity sets.

Neutral sets.

\overline{U = U ∈ Set}

[U] = {(u, u)}

Identity sets.

\frac{T = T′ ∈ Set  t_{1} = t′_{1} ∈ T  t_{2} = t′_{2} ∈ T}{Id_{T} t_{1} t_{2} = Id_{T′} t′_{1} t′_{2} ∈ Set}
[Id_{T} t_{1} t_{2}] = {(refl, refl) | nf^{⦇T ⦈}⦇t_{1}⦈ ≡ nf^{⦇T ⦈}⦇t_{2}⦈}
∪ {(∗, ∗) | nf^{⦇T ⦈}⦇t_{1}⦈ ≢ nf^{⦇T ⦈}⦇t_{2}⦈}

If the normal form of t_{1} or t_{2} is undefined, then [Id_{T} t_{1} t_{2}] is empty, according to the definition. However, this will never happen, since t_{1}, t_{2} ∈ T by definition. Thus, [Id_{T} t_{1}t_{2}] will be the singleton {(refl, refl)} if t_{1} and t_{2} have the same normal form, and {(∗, ∗)} otherwise. Since α-equivalence is decidable, our construction does not leave intuitionistic logic.

Universe of sets.

\frac{W = W′ ∈ Set}{W = W′ ∈Type}

Set = Set ∈Type

No new PERs [W] need to be constructed here, since [Set] = {(W, W′) | W = W′ ∈ Set} already by our notational convention.

Function types. The standard construction.

\frac{S = S′ ∈Type ∀s = s′ ∈ S. T [s/x] = T [s′/x]′ ∈Type}{(x:S) → T = (x:S′) → T′ ∈Type}

[(x:S) → T] = \{(w, w′) | \begin{matrix}∀s = s′ ∈ S. \\ w@s = w′@s′ ∈ T [s/x]\} \end{matrix}

4.2. Escape Lemma

We would like to establish that nf decides model equality, i. e., if w, w′ ∈ W then w = w′ ∈ W if and only if nf^{W} w ≡ nf^{W} w′. We show it for sets W, but for function types we can only prove the direction “only if”.

In the following, when we formulate a property for the PERType, we mean it also for Set, and a proof by induction on W = W′ ∈Type shall mean that we first do a induction on W = W′ ∈ Set.

Lemma 5 (Out of and into of the model) Let W = W′ ∈ Type. Then,

1. NF W ≡ NF W′.

2. If w = w′ ∈ W then nf^{W} w ≡ nf^{W′}w′.

3. ↑^{W} u = ↑^{W′} u ∈ W.

Proof. By induction on W = W′ ∈Type.

Case \overline{U = U ∈ Set}

1. Clear, since NF U = U.

2. Assume u = u ∈ U. We have nf^{U}u = u.

3. By definition, ↑^{U} u = ↑^{U} u ∈ U.

Case

\frac{T = T′ ∈ Set  t_{1} = t′_{1} ∈ T  t_{2} = t′_{2} ∈ T}{Id_{T} t_{1} t_{2} = Id_{T′} t′_{1} t′_{2} ∈ Set}

1. Clear, using the induction hypotheses.

2. Case

\frac{nf^{⦇T ⦈}⦇t_{1}⦈ ≡ nf^{⦇T ⦈}⦇t_{2}⦈}{refl = refl ∈ Id_{T} t_{1} t_{2}}

Trivial, since nf^{Id_{T} t_{1} t_{2}}refl = refl. Case

\frac{nf^{⦇T ⦈}⦇t_{1}⦈ ≢ nf^{⦇T ⦈}⦇t_{2}⦈}{∗ = ∗ ∈ Id_{T} t_{1} t_{2}}

Trivial, since nf^{Id_{T} t_{1} t_{2}}∗ = ∗.

3. Let v_{1} := nf^{⦇T ⦈}⦇t_{1}⦈ and v_{2} := nf^{⦇T ⦈}⦇t_{2}⦈ which are both defined by induction hypothesis. If v_{1} ≡ v_{2} then ↑^{Id_{T} t_{1} t_{2}} u = refl. Since by induction hypothesis also nf^{⦇T′⦈}⦇t′_{1}⦈ = v_{1} ≡ v_{2} = nf^{⦇T′⦈}⦇t′_{2}⦈, we have ↑^{Id_{T′} t′_{1} t′_{2}} u = refl, thus ↑^{Id_{T} t_{1} t_{2}} u = ↑^{Id_{T′} t′_{1} t′_{2}} u ∈ Id_{T} t_{1} t_{2}. If v_{1} ≢ v_{2}, then ↑^{Id_{T} t_{1} t_{2}} u = ∗ = ↑^{Id_{T′} t′_{1} t′_{2}} u, thus, also ↑^{Id_{T} t_{1} t_{2}} u = ↑^{Id_{T′} t′_{1} t′_{2}} u ∈ Id_{T} t_{1} t_{2}.

Case

\frac{S = S′ ∈Type ∀s = s′ ∈ S. T [s/x] = T [s′/x]′ ∈Type}{(x:S) → T = (x:S′) → T′ ∈Type}

1. Observe that NF ((x:S) → T) = (x:NF⦇S⦈) → NF ⦇T [(↑^{⦇S⦈} x)/x]⦈. By induction hypothesis, we have ↑^{⦇S⦈} x = ↑^{⦇S′⦈} x ∈ ⦇S⦈. Thus, by induction hypothesis NF ⦇T [(↑^{⦇S⦈} x)/x]⦈ ≡ NF ⦇T′[(↑^{⦇S′⦈} x)/x]⦈, and also NF ⦇S⦈ ≡ NF ⦇S′⦈. Together, NF ((x:S) → T) ≡ NF ((x:S′) → T′).

2. Assume w = w′ ∈ (x: S) → T. Observe that nf^{(x:S)→T} w = λx. nf^{⦇T [(↑^{⦇S⦈} x)/x]⦈}(w@ ↑^{⦇S⦈} x). Similar as in the last case, we have w@ ↑^{⦇S⦈} x = w′@ ↑^{⦇S′⦈} x ∈ ⦇T [(↑^{⦇S⦈} x)/x]⦈, from which nf^{(x:S)→T} w ≡ nf^{(x:S′)→T′}w′ follows.

3. To show ↑^{(x:S)→T} u = ↑^{(x:S′)→T′} u ∈ (x : S) → T, assume arbitrary s = s′ ∈ S and show (↑^{(x:S)→T} u)@s = (↑^{(x:S′)→T′} u)@s′ ∈ ⦇T [s/x]⦈. Observe that (↑^{(x:S)→T} u)@s = ↑^{⦇T [s/x]⦈} (u (nf^{⦇S⦈}⦇s⦈)). Let v := nf^{⦇S⦈}⦇s⦈. By induction hypothesis, v ≡ nf^{⦇S′⦈}s′ and ↑^{⦇T [s/x]⦈} (u v) = ↑^{⦇T′[s′/x]⦈} (u v) ∈ ⦇T [s/x]⦈.

□

Lemma 6 (Eta-expansion in the model) Let W ∈ Set and w ∈ W.

1. NF W = W ∈ Set.

2. nf^{W} w = w ∈ W.

3. ↑^{W} w = w ∈ W.

Proof. By induction on W ∈ Set.

Case

\overline{U ∈ Set}

1. We have NF U = U, hence, NF U = U ∈ Set.

2. Since nf^{U}u = u, we have nf^{U}u = u ∈ U.

3. With ↑^{U} u = u we immediately obtain ↑^{U} u = u ∈ U.

Case

\frac{⦇T ⦈ ∈ Set  ⦇t_{1}⦈ ∈ ⦇T ⦈  ⦇t_{2}⦈ ∈ ⦇T ⦈}{Id_{T} t_{1} t_{2} ∈ Set}

Let W = ⦇T ⦈, w_{1} = ⦇t_{1}⦈ and w_{2} = ⦇t_{2}⦈.

1. NF (Id_{T} t_{1} t_{2}) = Id_{NF W} (nf^{W} w_{1}) (nf^{W} w_{2}) entails NF (Id_{T} t_{1} t_{2}) = Id_{T} t_{1} t_{2} ∈ Set by the induction hypotheses.

2. nf^{Id_{T} t_{1} t_{2}}w = w by definition.

3. We distinguish two cases:

\frac{nf^{W} w_{1} ≡ nf^{W} w_{2}}{refl ∈ Id_{T} t_{1} t_{2}}

Since ↑^{Id_{T} t_{1} t_{2}} w = refl for any w, clearly ↑^{Id_{T} t_{1} t_{2}} refl = refl ∈ Id_{T} t_{1} t_{2}.

\frac{nf^{W} w_{1} ≢ nf^{W} w_{2}}{∗ ∈ Id_{T} t_{1} t_{2}}

Since ↑^{Id_{T} t_{1} t_{2}} w = ∗ for any w, clearly ↑^{Id_{T} t_{1} t_{2}} ∗ = ∗ ∈ Id_{T} t_{1} t_{2}.

□

Corollary 7 If W ∈ Set, w, w′ ∈ W, and nf^{W} w = nf^{W} w′, then w = w′ ∈ W.

It is unclear how to extend Lemma 6 to function types. Hence, we could not prove it for types W ∈ Type, and we can not extend Set by function sets.

4.3. Fundamental Theorem

In this section, we show that judgmental equality is modeled by the PERs, and as a consequence, is decided by normalization.

Let σ = σ′ ∈ Γ iff σ(x) = σ′(x) ∈ Γ(x) for all x ∈ dom(Γ). We define Γ ⊩ J, meaning that Γ ⊢ J is valid in the PER model by induction on Γ:

⋄ ⊩  :⟺ true
Γ, x:T ⊩  :⟺ Γ ⊩ T :Type
Γ ⊩ t : T  :⟺ Γ ⊩ t = t : T
Γ ⊩ t = t′ : T :⟺ Γ ⊩ T and

∀σ = σ′ ∈ Γ. ⦇tσ⦈ = ⦇t′σ′⦈ ∈ ⦇T σ⦈

Γ ⊩ T  :⟺ either T =Type and Γ ⊩

or Γ ⊩ T :Type

The proof of the fundamental theorem requires Lemma 6 for the soundness of the typing of idElim.

Theorem 8 (Fundamental theorem) If Γ ⊢ J then Γ ⊩ J.

Proof. By induction on Γ ⊢ J.

Case

\frac{Γ ⊢ t : T}{Γ ⊢ refl : Id_{T} t t}

Assume σ = σ′ ∈ Γ. Let w := ⦇tσ⦈ and W := ⦇T σ⦈. By induction hypothesis, w ∈ W. Hence v := nf^{W} w is defined. Clearly, refl ∈ Id_{W} w w.

Case

\frac{Γ ⊢ S : Set Γ ⊢ s, s′ : S Γ ⊢ p : Id_{S} s s′ Γ ⊢ C : (x, x′:S) → Id_{S} x x′ → Set Γ ⊢ h : (x:S) → C x x refl}{Γ ⊢ idElim_{S,s,s′} p C h : C s s′ p}

Let W = ⦇Sσ⦈, w = ⦇sσ⦈, and w′ = ⦇s′σ⦈. By induction hypothesis, ⦇pσ⦈ = ⦇pσ′⦈ ∈ ⦇(Id_{S} s s′)σ⦈.

In case nf^{W} w ≡ nf^{W} w′ we have ⦇pσ⦈ = ⦇pσ′⦈ = refl and ⦇(idElim_{S,s,s′} p C h)σ⦈ = ⦇(h s)σ⦈. By Cor. 7 w = w′ ∈ W, hence, sσ = s′σ ∈ Sσ. Also by induction hypothesis, Cσ = Cσ ∈ (x, x′ : Sσ) → Id_{Sσ} x x′ → Set, which implies (C s s′ p)σ = (C s s refl)σ ∈ Set. By induction hypothesis hσ = hσ′ ∈ (x: Sσ) → Cσ x x refl, which implies (h s)σ = (h s)σ′ ∈ (C s s refl)σ, and finally (idElim_{S,s,s′} p C h)σ = (idElim_{S,s,s′} p C h)σ′ ∈ (C s s′ p)σ.

In case nf^{W} w ≢ nf^{W} w′ we have ⦇pσ⦈ = ⦇pσ′⦈ = ∗. The proof is finished using the definition of idE_{Sσ,sσ,s′σ} ∗ Cσ hσ and Lemma 5.

Case

\frac{Γ ⊢ S : Set Γ ⊢ s : S Γ ⊢ C : (x, x′:S) → Id_{S} x x′ → Set Γ ⊢ h : (x:S) → C x x refl}{Γ ⊢ idElim_{S,s,s} refl C h = h s : C s s refl}

By induction hypothesis, hσ = hσ′ ∈ (x : Sσ) → Cσ x x refl and sσ = sσ′ ∈ Sσ. Since ⦇(idElim_{S,s,s} refl C h)σ⦈ = ⦇hσ⦈@(sσ) and ⦇(h s)σ′⦈ = ⦇hσ′⦈@(sσ′), the goal ⦇(idElim_{S,s,s} refl C h)σ⦈ = ⦇(h s)σ′⦈ ∈ ⦇(C s s refl)σ⦈ follows immediately.

Case

\frac{Γ ⊢ p, q : Id_{T} t t′}{Γ ⊢ p = q : Id_{T} t t′}

This is trivial by definition of the semantics of the identity type. Here is a proof: Assume σ = σ′ ∈ Γ and show p′ = q′ ∈ W where p′ := ⦇pσ⦈, q′ := ⦇qσ′⦈, and W := ⦇(Id_{T} t t′)σ⦈. By induction hypothesis and Lemma 5, v := nf^{⦇T ⦈}⦇t⦈ and v′ := nf^{⦇T ⦈}⦇t′⦈ are both defined. If they are identical, it must be the case that p = q = refl, otherwise, p = q = ∗. In both cases p′ = q′ ∈ W.

Case

\frac{Γ, x:S ⊢ t : T Γ ⊢ s : S}{Γ ⊢ (λxt) s = t[s/x] : T [s/x]}

Assume σ = σ′ ∈ Γ. W. l. o. g., choose x such it does not interfere with σ or σ′. Observe that ⦇((λxt) s)σ)⦈ = ⦇(λx. t(σ, x = x)) sσ⦈ = ⦇λx. t(σ, x = x)⦈@sσ = ⦇t(σ, x = x)[sσ/x]⦈ = ⦇t(σ, x = sσ)⦈. Further, ⦇(t[s/x])σ′⦈ = ⦇t(σ′, x = sσ′)⦈. By induction hypothesis, ⦇sσ⦈ = ⦇sσ′⦈ ∈ ⦇S⦈, thus, sσ = sσ′ ∈ S. Hence, (σ, x = sσ) = (σ′, x = sσ′) ∈ Γ, x : S. By induction hypothesis again, Δ ⊢ ⦇t(σ, x = sσ)⦈ = ⦇t(σ′, x = sσ′)⦈ ∈ ⦇T (σ, x = sσ)⦈. Using the calculations above, this implies the goal ⦇((λxt) s)σ⦈ = ⦇(t[s/x])σ′⦈ ∈ ⦇(T [s/x])σ⦈.

□

Corollary 9 (Completeness of Normalization) Let Γ ⊢ t = t′ : T and σ(x) = ↑^{⦇Γ(x)⦈} x. Then nf^{⦇T σ⦈}⦇tσ⦈ ≡ nf^{⦇T σ⦈}⦇t′σ⦈.

Proof. By Lemma 5, σ = σ ∈ Γ. Then fundamental theorem yields ⦇tσ⦈ = ⦇t′σ⦈ ∈ ⦇T σ⦈. The goal follows by Lemma 5. □

5. Conclusion

We have shown how to decide judgmental equality in a logical framework with proof irrelevant identity types. Identities are restricted to base types. It is not clear yet how to extend our approach to identities between function types, future research will show.

5.1. More Related Work

In his habilitation thesis, Streicher [14] considers the η-rule idElim_{S,s,s′} p C (λx. e x x refl) = e for e : (x, y : S) → (q:Id_{S} x y) →C x y q and proves that it entails equality reflection, i. e., Extensional Type Theory. Clearly, this rule destroys decidability of definitional equality and type checking. Streicher also proves that in the presence of UIP, idElim can be replaced by the simpler substitution operator subst : (S : Set) → (s, s′:S) → Id_{S} s s′ → (P:S → Set) → P s → P s′. Thus, we could have chosen subst instead of idElim without losing expressivity.

Werner [16] considers the Calculus of Inductive Constructions (CIC) with proof-irrelevant propositions. During equality checking t =_{ϵ} t′, all proofs are replaced by ϵ (our ∗), in particular, canonical and hypothetical proofs of propositional equality are no longer distinguished. Consequently, for identity elimination Werner switches to the reduction rule subst_{S,s,s′} p P x ⟶ x in case s =_{ϵ} s′. This is generalized to all inductive propositions (which can have at most one constructor in the CIC). We hope to extend our approach to the CIC as well; this would integrate η-equality into the CIC with proof-irrelevance.

Very interesting related work is Observational Type Theory by Altenkirch, McBride, and Swierstra [6]. They implement a heterogeneous propositional equality which features functional extensionality by definition. Proof irrelevance is obtained by type-directed quotation (very similar to contextual reification [3]) which happens after evaluation and “boxes” all proofs such that they can be disregarded in the syntactical equality test. How their approach relates to mine exactly I do not know yet.

Acknowledgments. The idea to look at η-expansion for the identity type came up in discussions with James Chapman and Tarmo Uustalu during a visit to IOC Tallinn in March 2009. I am grateful for their invitation.

References

[1] A. Abel, K. Aehlig, and P. Dybjer. Normalization by evaluation for Martin-Löf type theory with one universe. In M. Fiore, editor, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIII), New Orleans, LA, USA, 11-14 April 2007, volume 173 of Electronic Notes in Theoretical Computer Science, pages 17–39. Elsevier, 2007.

[2] A. Abel, T. Coquand, and P. Dybjer. Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements. In 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings, pages 3–12. IEEE Computer Society Press, 2007.

[3] A. Abel, T. Coquand, and P. Dybjer. Verifying a semantic βη-conversion test for Martin-Löf type theory. In P. Audebaud and C. Paulin-Mohring, editors, Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, volume 5133 of Lecture Notes in Computer Science, pages 29–56. Springer-Verlag, 2008.

[4] A. Abel, T. Coquand, and M. Pagano. A modular typechecking algorithm for type theory with singleton types and proof irrelevance. In P.-L. Curien, editor, Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009, Proceedings, volume 5608 of Lecture Notes in Computer Science, pages 5–19. Springer-Verlag, 2009.

[5] T. Altenkirch. Extensional equality in intensional type theory. In 14th Annual IEEE Symposium on Logic in Computer Science, 2-5 July, 1999, Trento, Italy, Proceedings, pages 412–420, 1999.

[6] T. Altenkirch, C. McBride, and W. Swierstra. Observational equality, now! In A. Stump and H. Xi, editors, Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007, pages 57–68. ACM Press, 2007.

[7] S. Awodey and A. Bauer. Propositions as [types]. J. Log. Comput., 14(4):447–471, 2004.

[8] S. Awodey and M. A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45–55, 2009.

[9] P. Dybjer. A general formulation of simultaneous inductiverecursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000.

[10] N. Gambino and R. Garner. The identity type weak factorisation system. Theoretical Computer Science, 409(1):94– 109, 2008.

[11] M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In Twenty-five Years of Constructive Type Theory, Festschrift, Venice 1995, volume 36 of Oxford Logic Guides, pages 83–111. Oxford University Press, 1998.

[12] P. Martin-Löf. Constructive mathematics and computer programming. In Proc. of a discussion meeting of the Royal Society of London on Mathematical logic and programming languages, pages 167–184, Upper Saddle River, NJ, USA, 1985. Prentice-Hall, Inc.

[13] B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin Löf’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990.

[14] T. Streicher. Investigations into Intensional Type Theory, 1993. Habilitation thesis, Ludwig-Maximilians-University Munich.

[15] K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework I: Judgements and properties. Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.

[16] B. Werner. On the strength of proof-irrelevant type theories. Logical Methods in Computer Science, 4, 2008.