IOS Press

Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs

Andreas Abel^{∗} ^{C}

Institut für Informatik, Ludwigs-Maximilians-Universität München

      abel@informatik.uni-muenchen.de

Thierry Coquand^{∗}

Department of Computer Science, Chalmers University of Technology

      coquand@cs.chalmers.se

Abstract. Martin-Löf’s Logical Framework is extended by strong Σ-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped βη-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with η-equality on β-normal forms, which is shown equivalent to the algorithmic equality.

1. Introduction

Central to dependent type theories is the rule of conversion: The type of an expression can be converted to an equal type, where in intensional type theories the notion of equality between types is decidable. In the past, research has focused on β-equality, and since β-reduction is confluent, two types are equal iff they have a common β-reduct. This both suggest an implementation for equality—β-normalize and compare for syntactical identity—and provides a specification sufficient to reason about the meta-theoretic properties of the type theory: From confluence one gets injectivity of the dependent function space constructor Π, an important mile stone to prove subject reduction and, hence, soundness of the type theory. Because β is well behaved, one can consider β-reduction on untyped terms, which simplifies the reasoning significantly.

∗Research supported by the coordination action TYPES (510996) and thematic network Applied Semantics II (IST-2001-38957)

of the European Union and the project Cover of the Swedish Foundation of Strategic Research (SSF).

CCorresponding author

If one adds η-laws to the notion of equality, this strategy does not work any more. Surjective pairing, the strong η-law for Σ-types, destroys confluence of reduction for untyped terms [19]. In the presence of a unit type, η-reduction is not even locally confluent on well-typed terms [20]. Furthermore, for the type theory considered in this article, MLF_{Σ}, an extension of Martin-Löf’s logical framework with βη-equality by dependent surjective pairs (strong Σ types), subject reduction fails.

On the specification side, the short comings of η are salvaged by judgmental equality. Equality of two expressions is stated with reference to their type and a valid typing context. Soundness of type theories with judgmental equality follows directly from a PER model which interprets types as extensional partial equivalence relations. More problematic could be injectivity of Π; in our case, however, it is trivial since we follow Martin-L”of’s later approach and separate terms and types conceptually: Terms can appear in types only inside the El constructor.

Another issue is decidability of judgmental equality: the rules do not suggest an algorithm immediately. We take the incremental βη-convertibility test which has been given by the second author for dependently typed λ-terms [8], and extend it to pairs. The algorithm computes the weak head normal forms of the conversion candidates, and then analyzes the shape of the normal forms. In case the head symbols do not match, conversion fails early. Otherwise, the subterms are recursively weak head normalized and compared. There are two flavors of this algorithm.

Type-directed conversion. In this style, the type of the two candidates dictates the next step in the algorithm. If the candidates are of function type, both are applied to a fresh variable, if they are of pair type, their left and right projections are recursively compared, and if they are of base type, they are compared structurally, i. e., their head symbols and subterms are compared. Type-directed conversion has been investigated by Harper and Pfenning [17]. The advantage of this approach is that it can handle cases where the type provides extra information which is not present already in the shape of terms. An example is the unit type: any two terms of unit type, e. g., two variables, can be considered equal. Harper and Pfenning report difficulties in showing transitivity of the conversion algorithm, in case of dependent types. To circumvent this problem, they erase the dependencies and obtain simple types to direct the equality algorithm. In the theory they consider, the Edinburgh Logical Framework [16], erasure is sound, but in theories with types defined by cases (large eliminations), erasure is unsound and it is not clear how to make their method work. In this article, we investigate an alternative approach.

Shape-directed (untyped) conversion. As the name suggests, the shape of the candidates directs the next step. If one of the objects is a λ-abstraction, both objects are applied to a fresh variable, if one object is a pair, the algorithm continues with the left and right projections of the candidates, and otherwise, they are compared structurally. Since the algorithm does not depend on types, it is in principle applicable to many type theories with functions and pairs. In this article, we prove it complete for MLF_{Σ}, but since we are not using erasure, we expect the proof to extend to theories with large eliminations.

Main technical contributions of this article.

1. We extend the untyped type-checking algorithm of the second author [8] to a type system with Σ-types and surjective pairing. Recall that reduction in the untyped λ-calculus with surjective pairing is not Church-Rosser [6] (see Appendix A). Therefore, one cannot specify this type system with conversion defined on raw terms.^{1} However, since surjective pairing does not destroy local confluence, it is confluent on strongly normalizing terms. Thus, once the type theory is proven sound which implies that all terms are normalizing, one can use reduction to check for equality. One byproduct of the completeness proof of our equality algorithm is that we can decide equality also by the following strategy: first β-normalize, then check η-equality of the β-normal forms (which in our case can be done by η-reduction).

2. We take a modular approach for showing the completeness of the conversion algorithm. This result is obtained using a special instance of a general PER model construction. Furthermore this special instance can be described a priori without references to the typing rules.

Contents. Figure 1 summarizes the technical developments of this article. We start with a syntactical description of MLF_{Σ}, in the style of equality-as-judgement (Section 2). Then, we give an untyped algorithm to check βη-equality of two expressions, which alternates weak head reduction and comparison phases, plus a bidirectional type checking algorithm for normal terms (Section 3). The goal of this article is to show that the algorithmic presentation of MLF_{Σ} is equivalent to the declarative one. Soundness is proven rather directly in Section 4, requiring inversion for the typing judgement in order to establish subject reduction for weak head evaluation. Completeness, which implies decidability of MLF_{Σ}, requires construction of a model. Before giving a specific model, we describe a class of PER (partial equivalence relation) models of MLF_{Σ} based on a generic model of the λ-calculus with pairs (Section 5). In Section 6 we turn to the specific model of expressions modulo β-equality and show that η-equality of β-normal forms is a partial equivalence, hence, gives rise to a PER model. In Section 7 we give a proof that ηequivalence is decided by the algorithmic equality which implies that the algorithmic equality serves as basis for a PER model as well. This entails completeness of the algorithm. We could have done a more direct proof, without the intermediate model involving η-equality, and this (rather technical) path is taken in Section 8. Decidability of judgmental equality on well-typed terms in MLF_{Σ} ensues, which entails that type checking of normal forms is decidable as well (Section 9).

This article is an extended and revised version of a conference contribution with the same title [3].

2. Declarative Presentation of MLF_{Σ}

This section presents the typing and equality rules for an extension of Martin-Löf’s logical framework [21] by dependent pairs. We show some standard properties like weakening and substitution, as well as injectivity of function and pair types and inversion of typing, which will be crucial for the further development.

Expressions (terms and types). We do not distinguish between terms and types syntactically. Dependent function types, usually written Πx:A. B, are written Fun A (λxB); similarly, dependent pair types Σx:A. B are represented by Pair A (λxB). We write projections L and R postfix. The syntactic entities

1In the absence of confluence, one cannot show injectivity of type constructors, on which usually the proof of subject reduction rests. Adams [5] has shown the equivalence of pure type systems with judgmental and untyped equality, but only for β.

[figure: Γ ⊢ t = t′ : C; Sect. 2; Sect. 5; tρ = t′ρ ∈ [Cρ]; Sect. 6; Sect. 8; t ⟶_{β}^{∗} v =_{η} v′ _{β}^{∗}⟵ t′; Sect. 7; t ⟶_{β}^{∗} v ∼^{+} v′ _{β}^{∗}⟵ t′; Sect. 8; t↓ ∼^{+} t′↓; Sect. 7; Γ ⊢ t, t′ : C; t↓ ∼ t′↓; Sect. 4; Γ ⊢ t = t′ : C]

Legend:

Γ  typing context
C  type
t  term
v  β-normal form
⟶_{β}^{∗} β-reduction
=_{η}  η-equality
⊢ : typing judgement

⊢ = : equality judgement
↓  weak head evaluation
∼  algorithmic equality
∼^{+}  extended algorithmic equality
ρ  denotation in environment ρ
[ ]  type interpretation
= ∈  partial equivalence relation

Figure 1. Outline of Results.

A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing 5

Wellformed contexts Γ ⊢ ok.

cxt-empty \overline{⋄ ⊢ ok}  cxt-ext \frac{Γ ⊢ A :Type}{Γ, x:A ⊢ ok}

Type formation Γ ⊢ A :Type.

set-f \frac{Γ ⊢ ok}{Γ ⊢ Set :Type}  set-e \frac{Γ ⊢ t : Set}{Γ ⊢ El t :Type}
fun-f \frac{Γ, x:A ⊢ B :Type}{Γ ⊢ Fun A (λxB) :Type}  pair-f \frac{Γ, x:A ⊢ B :Type}{Γ ⊢ Pair A (λxB) :Type}

Typing Γ ⊢ t : A.

hyp \frac{Γ ⊢ ok  (x:A) ∈ Γ}{Γ ⊢ x : A}  conv \frac{Γ ⊢ t : A  Γ ⊢ A = B :Type}{Γ ⊢ t : B}
fun-i \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : Fun A (λxB)}  fun-e \frac{Γ ⊢ r : Fun A (λxB)  Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}
pair-i \frac{Γ, x:A ⊢ B :Type  Γ ⊢ s : A  Γ ⊢ t : B[s/x]}{Γ ⊢ (s, t) : Pair A (λxB)}
pair-e-l \frac{Γ ⊢ r : Pair A (λxB)}{Γ ⊢ r L : A}  pair-e-r \frac{Γ ⊢ r : Pair A (λxB)}{Γ ⊢ r R : B[r L/x]}

Figure 2. MLF_{Σ} rules for contexts, types and typing.

of MLF_{Σ} are given by the following grammar.

Var ∋ x, y, z  variables
Const ∋ c  ::= Fun | Pair | El | Set  constants
Proj ∋ p  ::= L | R  left and right projection
Exp ∋ r, s, t  ::= c | x | λxt | r s | (t, t′) | r p  expressions
Ty  ∋ A, B, C ::= Set | El t | Fun A (λxB) | Pair A (λxB) types
Cxt ∋ Γ  ::= ⋄ | Γ, x:A  typing contexts

The only binder is abstraction λxt, which binds variable x in expression t. Let FV(t) denote the set of free variables of expression t. We identify terms and types up to α-conversion and write t ≡ t′ to express syntactic equality between t and t′ (modulo α), as opposed to β-, η-, or judgemental equality which will be defined later. We adopt the convention that in contexts Γ, all variables must be distinct; hence, the context extension Γ, x : A presupposes x ∉ dom(Γ), where dom(Γ) denotes the domain of Γ viewed as a finite map from variables to types. This view also explains the notation Γ(x). Capture-avoiding subsitution of expression s for variable x in expression t is written as t[s/x].

Types Ty ⊆ Exp are distinguished expressions; they are closed under substitution. The inhabitants of Set are type codes; El maps type codes to types. For instance, Fun Set (λa. Fun (El a) (λ . El a)) denotes the type of the polymorphic identity λaλxx.

Judgements are inductively defined relations. If D is a derivation of judgement J, we write D :: J. The height of derivation D is denoted by #D. The type theory MLF_{Σ} is presented via five judgements:

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

A variable x is free in a judgement Γ ⊢ J, written x ∈ FV(J), if it is free in one of the expressions in J. Typing rules are given in Figure 2, together with the rules for well-formed contexts and types. The rules for the equality judgements are given in Figures 3 and 4.

Remark 2.1. (Subject reduction fails) In the typing context z : Pair A (λxB), the η-redex (z L, z R) can be given the non-dependent type Pair A (λ . B[z L/x]), but its reduct z not. A closer analysis of this problem leads us to rule pair-i : the types of s and t do not determine the type of (s, t). If the term s appears in B[s/x], then there are at least two different expressions B_{1} and B_{2} such that B_{1}[s/x] ≡ B_{2}[s/x] ≡ B[s/x], which lead to different types of (s, t).

For the remainder of this section we present properties of MLF_{Σ} which have easy syntactical proofs. In this, we follow roughly the path outlined by Harper and Pfenning [17]. However, there is a methodological difference: In all judgements Γ ⊢ J, we presuppose Γ ⊢ ok, which is not true for Harper and Pfenning’s presentation of the logical framework.

eq-set-f \frac{Γ ⊢ ok}{Γ ⊢ Set = Set :Type}  eq-set-e \frac{Γ ⊢ t = t′ : Set}{Γ ⊢ El t = El t′ :Type}

eq-fun-f \frac{Γ ⊢ A = A′ :Type  Γ, x:A ⊢ B = B′ :Type}{Γ ⊢ Fun A (λxB) = Fun A′ (λxB′) :Type}

eq-pair-f \frac{Γ ⊢ A = A′ :Type  Γ, x:A ⊢ B = B′ :Type}{Γ ⊢ Pair A (λxB) = Pair A′ (λxB′) :Type}

Figure 3. MLF_{Σ} type equality rules.

Type equality (see Figure 3) is reflexive, symmetric, and transitive, which can only be shown after establishing context conversion (Lemma 2.9) and syntactic validity (Theorem 2.1). But injectivity and non-confusion for type-constructors is completely trivial in our formulation of type equality, which lacks computation on the type level and rules for symmetry and transitivity.

Lemma 2.1. (Injectivity) 1. If D :: Γ ⊢ Set = C :Type then C ≡ Set.

2. If D :: Γ ⊢ El t = C :Type then C ≡ El t′ and Γ ⊢ t = t′ : Set.

3. Let c ∈ {Fun, Pair}. If D :: Γ ⊢ c A (λxB) = C : Type then C ≡ c A′ (λxB′) with Γ ⊢ A = A′ :Type and Γ, x:A ⊢ B = B′ :Type.

Proof: By cases on D. ⊓ ⊔

For Harper and Pfenning’s version of the Edinburgh LF which lacks type-level λ-abstraction [17], injectivity is also not hard to prove. In the Edinburgh LF with type-level λ it involves a normalization argument and is proven using logical relations [26].

In the following, we prove a sequence of technical lemmata that bring us to the important theorem of syntactic validity which states that all syntactic entities in a derived judgement are well-formed.

Lemma 2.2. (Scoping) 1. If D :: Γ ⊢ J then FV(J) ⊆ dom(Γ).

2. If D :: Γ′, x:A, Γ′′ ⊢ J then FV(A) ⊆ dom(Γ′).

Proof: Simultaneously by induction on D. ⊓ ⊔

8 A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing

Equivalence, hypotheses, conversion.

eq-sym \frac{Γ ⊢ t = t′ : A}{Γ ⊢ t′ = t : A}  eq-trans \frac{Γ ⊢ r = s : A  Γ ⊢ s = t : A}{Γ ⊢ r = t : A}
eq-hyp \frac{Γ ⊢ ok  (x:A) ∈ Γ}{Γ ⊢ x = x : A}  eq-conv \frac{Γ ⊢ t = t′ : A  Γ ⊢ A = B :Type}{Γ ⊢ t = t′ : B}

Dependent functions.

eq-fun-i \frac{Γ, x:A ⊢ t = t′ : B}{Γ ⊢ λxt = λxt′ : Fun A (λxB)}
eq-fun-e \frac{Γ ⊢ r = r′ : Fun A (λxB)  Γ ⊢ s = s′ : A}{Γ ⊢ r s = r′ s′ : B[s/x]}
eq-fun-β \frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λxt) s = t[s/x] : B[s/x]}

eq-fun-η \frac{Γ ⊢ t : Fun A (λxB)}{Γ ⊢ (λx. t x) = t : Fun A (λxB)} x ∉ FV(t)

Dependent pairs.

eq-pair-i \frac{Γ ⊢ s = s′ : A  Γ ⊢ t = t′ : B[s/x]}{Γ ⊢ (s, t) = (s′, t′) : Pair A (λxB)}
eq-pair-e-l \frac{Γ ⊢ r = r′ : Pair A (λxB)}{Γ ⊢ r L = r′ L : A}  eq-pair-e-r \frac{Γ ⊢ r = r′ : Pair A (λxB)}{Γ ⊢ r R = r′ R : B[r L/x]}
eq-pair-β-l \frac{Γ ⊢ s : A Γ ⊢ t : B}{Γ ⊢ (s, t) L = s : A} eq-pair-β-r \frac{Γ ⊢ s : A Γ ⊢ t : B}{Γ ⊢ (s, t) R = t : B}
eq-pair-η \frac{Γ ⊢ r : Pair A (λxB)}{Γ ⊢ (r L, r R) = r : Pair A (λxB)}

Figure 4. MLF_{Σ} term equality rules.

Lemma 2.3. (Weakening) If D_{1} :: Γ, Γ′ ⊢ J and both D_{2} :: Γ ⊢ A :Type and x ∉ dom(Γ, Γ′), then E :: Γ, x:A, Γ′ ⊢ J.

Remark 2.2. The result derivation E is at most as long as the input derivations together: #E ≤ #D_{1} + #D_{2}. Note that the special case Γ′ = ⋄ cannot be proven by itself; e.g., the case fun-f fails since the order of the hypotheses matters in the context.

Proof: By induction on D_{1}. First, consider J = ok. Γ′ can be empty or not:

1. Case D_{1} :: Γ, Γ′ ⊢ ok and Γ′ = ⋄. From D_{2} we get E :: Γ, x:A ⊢ ok by rule cxt-ext .

2. Case D_{1} :: Γ, Γ′ ⊢ ok and Γ′ ≠ ⋄. The only matching rule is:

cxt-ext \frac{Γ, Γ′′ ⊢ B :Type}{Γ, Γ′′, y:B ⊢ ok}

By induction hypothesis, Γ, x:A, Γ′′ ⊢ B :Type. We conclude by rule cxt-ext .

Now we look at the other judgements. There are two principal cases for the last rule in D_{1}: First, the rule discharges a hypothesis, and second, the context is left unchanged by the rule.

1. A hypothesis is discharged in the last rule of D_{1}, for instance:

fun-f \frac{Γ, Γ′, y:B ⊢ C :Type}{Γ, Γ′ ⊢ Fun B (λyC) :Type}

Extending Γ′ by the assumption y: B for the induction hypothesis, we obtain Γ, x: A, Γ′, y: B ⊢ C :Type. The goal follows by fun-f .

2. The last rule application in D_{1} leaves the context unchanged. Most rules fall into this pattern, for instance:

hyp \frac{Γ, Γ′ ⊢ ok  (y:B) ∈ (Γ, Γ′)}{Γ, Γ′ ⊢ y : B}

By induction hypothesis, Γ, x:A, Γ′ ⊢ ok, hence, Γ, x:A, Γ′ ⊢ y : B by hyp .

Mixed forms, like eq-fun-f , can be treated analogously. ⊓ ⊔

The following lemma materializes the fact that in all judgements, the context is well-formed, which implies that all types in the contexts must be well-formed.

Lemma 2.4. (Context well-formedness) 1. If D :: Γ, Γ′ ⊢ J then E :: Γ ⊢ ok and the derivation E is at most as long as D.

2. If D :: Γ, x:A, Γ′ ⊢ J, then E :: Γ ⊢ A :Type and E is shorter than D.

Proof: The first proposition holds since in the leaves of type formation, typing, and equality derivations (rules set-f , hyp , eq-hyp , and eq-set-f ) we require well-formed contexts. Formally, it is proven by induction on D. All cases are easy, for instance:

fun-f \frac{Γ, Γ′, y:B ⊢ C :Type}{Γ, Γ′ ⊢ Fun B (λyC) :Type}

By induction hypothesis, Γ ⊢ ok.

For the second proposition, use the first proposition to derive E :: Γ, x: A ⊢ ok. The last rule in E must be cxt-ext with premise E′ :: Γ ⊢ A :Type. We have #E′ < #E ≤ #D. ⊓ ⊔

Corollary 2.1. (Iterative weakening) If Γ ⊢ J and Γ, Γ′ ⊢ J′ then Γ, Γ′ ⊢ J.

Proof: By induction on the length of Γ′. If Γ′ is empty, there is nothing to show, otherwise Γ′ = (x:A, Γ′′). By the lemma, Γ ⊢ A :Type, hence by weakening, Γ, x:A ⊢ J. By induction hypothesis, Γ, x:A, Γ′′ ⊢ J.

⊓ ⊔

Another consequence of context well-formedness is that we can decompose well-formed types:

Lemma 2.5. (Inversion for types) 1. If D :: Γ ⊢ El t :Type then D′ :: Γ ⊢ t : Set.

2. Let c ∈ {Fun, Pair}. If D :: Γ ⊢ c A (λxB) : Type then D_{1} :: Γ ⊢ A : Type and D_{2} :: Γ, x: A ⊢

B :Type. In all cases, the derivations D′, D_{1}, and D_{2} are shorter than D.

Proof: By cases on D, using Lemma 2.4 for part 2. For instance:

fun-f \frac{Γ, x:A ⊢ B :Type}{Γ ⊢ Fun A (λxB) :Type}

From the premise, D_{2}, we get D_{1} :: Γ ⊢ A :Type by context well-formedness. ⊓ ⊔

Similarly, context well-formedness is required to establish reflexivity.

Lemma 2.6. (Reflexivity) 1. If D :: Γ ⊢ t : A then Γ ⊢ t = t : A.

2. If D :: Γ ⊢ A :Type then Γ ⊢ A = A :Type.

Proof: Each by induction on D. Reflexivity for terms is proven mechanically, by replacing typing rules R in D with their counterpart eq-R from the set of equality rules. Reflexivity for types requires some attention in case of fun-f and pair-f , for instance:

fun-f \frac{Γ, x:A ⊢ B :Type}{Γ ⊢ Fun A (λxB) :Type}

First, the induction hypothesis gives us Γ, x: A ⊢ B = B : Type. Secondly, by the Lemma 2.4, we obtain a derivation Γ ⊢ A : Type which is shorter than D, so we can apply the induction hypothesis again to obtain Γ ⊢ A = A :Type. The goal follows by eq-fun-f . ⊓ ⊔

The substitution lemma allows us to replace a variable by a term of the correct type in a derivation. It relies on weakening and context well-formedness.

Lemma 2.7. (Substitution) Let Γ ⊢ s : A. If D :: Γ, x:A, Γ′ ⊢ J then Γ, Γ′[s/x] ⊢ J[s/x].

Proof: By induction on D.

• Case:

cxt-ext \frac{Γ ⊢ A :Type}{Γ, x:A ⊢ ok}

Then Γ ⊢ ok by context well-formedness.

• Case:

cxt-ext \frac{Γ, x:A, Γ′ ⊢ B :Type}{Γ, x:A, Γ′, y:B ⊢ ok}

By induction hypothesis, Γ, Γ′[s/x] ⊢ B[s/x] :Type, hence Γ, Γ′[s/x], y:B[s/x] ⊢ ok.

• Cases hyp and eq-hyp , e. g.:

hyp \frac{Γ, x:A, Γ′ ⊢ ok}{Γ, x:A, Γ′ ⊢ x : A}

First observe that by scoping (Lemma 2.2) we have FV(A) ⊆ dom(Γ), so x ∉ FV(A) and A[s/x] ≡ A. By induction hypothesis, Γ, Γ′[s/x] ⊢ ok. We apply iterative weakening on Γ ⊢ s : A to conclude Γ, Γ′[s/x] ⊢ s : A.

All other cases go through by induction hypothesis, using the properties of the substitution operation. ⊓ ⊔

In the following lemmata, which are all required to prove syntactic validity, there are some hypotheses (\underline{underlined}) which will turn out to be redundant after we have proven syntactic validity. But until then, they are required for “boot-strapping”.

Lemma 2.8. (Functionality for typing and type formation) Let Γ ⊢ s = s′ : A and \underline{Γ ⊢ s : A}.

1. If D :: Γ, x:A, Γ′ ⊢ t : C then Γ, Γ′[s/x] ⊢ t[s/x] = t[s′/x] : C[s/x].

2. If D :: Γ, x:A, Γ′ ⊢ C :Type then Γ, Γ′[s/x] ⊢ C[s/x] = C[s′/x] :Type.

Proof: Each by induction on D. We spell out some cases for the first proposition, for the second, there are no surprises.

• In the case of an hypothesis rule, we have Γ, x : A, Γ′ ⊢ ok, hence, by the substitution lemma, Γ, Γ′[s/x] ⊢ ok. We consider the following subcases:

– The used hypothesis is x: A. Since all types in Γ′[s/x] are wellformed, we can iteratively weaken (Cor. 2.1) the assumption of this lemma to obtain the desired Γ, Γ′[s/x] ⊢ s = s′ : A. Note that A ≡ A[s/x] since x cannot be free in A (Lemma 2.2).

– The used hypothesis is (y:B) ∈ Γ. Then x cannot be free in B and Γ, Γ′[s/x] ⊢ y = y : B is an instance of rule eq-hyp .

– The used hypothesis is (y : B) ∈ Γ′. Then (y : B[s/x]) ∈ Γ′[s/x] and we can again use eq-hyp .

• Case:

conv \frac{Γ, x:A, Γ′ ⊢ t : B  Γ, x:A, Γ′ ⊢ B = C :Type}{Γ, x:A, Γ′ ⊢ t : C}

Γ, Γ′[s/x] ⊢ t[s/x] = t[s′/x] : B[s/x]  induction hypothesis
Γ ⊢ s : A  assumption
Γ, Γ′[s/x] ⊢ B[s/x] = C[s/x] :Type  substitution lemma
Γ, Γ′[s/x] ⊢ t[s/x] = t[s′/x] : C[s/x]  rule eq-conv

• Case:

fun-i \frac{Γ, x:A, Γ′, y:B ⊢ t : C}{Γ, x:A, Γ′ ⊢ λyt : Fun B λyC}

Γ, Γ′[s/x], y:B[s/x] ⊢ t[s/x] = t[s′/x] : C[s/x]  induction hypothesis
Γ, Γ′[s/x] ⊢ λy. t[s/x] = λy. t[s′/x] : Fun (B[s/x]) λy. C[s/x]  rule eq-fun-i
Γ, Γ′[s/x] ⊢ (λyt)[s/x] = (λyt)[s′/x] : (Fun B λyC)[s/x]  properties of substitution

• Case:

pair-e-r \frac{Γ, x:A, Γ′ ⊢ r : Pair B λyC}{Γ, x:A, Γ′ ⊢ r R : C[r L/y]}

Γ, Γ′[s/x] ⊢ r[s/x] = r[s′/x] : Pair (B[s/x]) λy. C[s/x]  induction hypothesis
Γ, Γ′[s/x] ⊢ (r R)[s/x] = (r R)[s′/x] : (C[s/x])[(r[s/x] L)/y]  rule eq-pair-e-r
Γ, Γ′[s/x] ⊢ (r R)[s/x] = (r R)[s′/x] : (C[r L/y])[s/x]  properties of substitution

⊓ ⊔

Lemma 2.9. (Context conversion) Let Γ ⊢ B = A :Type and \underline{Γ ⊢ B :Type}. If D :: Γ, x:A, Γ′ ⊢ J then Γ, x:B, Γ′ ⊢ J.

Proof: By induction on D.

• Case Γ′ = ⋄ and J = ok:

cxt-ext \frac{Γ ⊢ A :Type}{Γ, x:A ⊢ ok}

From the assumption Γ ⊢ B :Type we get Γ, x:B ⊢ ok.

• Case:

hyp \frac{Γ, x:A, Γ′ ⊢ ok}{Γ, x:A, Γ′ ⊢ x : A}

By induction hypothesis Γ, x: B, Γ′ ⊢ ok, hence, Γ, x: B, Γ′ ⊢ x : B. The goal follows by rule conv .

The other cases can be handled mechanically using the induction hypothesis. ⊓ ⊔

Next, we will establish that type equality is an equivalence relation. Symmetry is needed to use a context conversion the other way round in the syntactic validity lemma.

Lemma 2.10. (Symmetry) Let \underline{Γ ⊢ C′ :Type}. If D :: Γ ⊢ C = C′ :Type then Γ ⊢ C′ = C :Type.

Proof: By induction on D.

• Case:

eq-set-e \frac{Γ ⊢ t = t′ : Set}{Γ ⊢ El t = El t′ :Type}

By eq-sym , Γ ⊢ t′ = t : Set. The goal follows by eq-set-e .

• Case:

eq-fun-f \frac{Γ ⊢ A = A′ :Type  Γ, x:A ⊢ B = B′ :Type}{Γ ⊢ Fun A (λxB) = Fun A′ (λxB′) :Type}

First, Γ ⊢ A : Type by context well-formedness. By inversion on \underline{Γ ⊢ Fun A′ (λxB′) :Type} we have Γ ⊢ A′ : Type, hence by induction hypothesis, Γ ⊢ A′ = A : Type. Again, by inversion, Γ, x: A′ ⊢ B′ : Type, and we apply context conversion to obtain Γ, x: A ⊢ B′ : Type. We obtain the second induction hypothesis, Γ, x:A ⊢ B′ = B :Type, from which we infer Γ, x:A′ ⊢ B′ = B :Type by context conversion. We conclude Γ ⊢ Fun A′ (λxB′) = Fun A (λxB) :Type.

⊓ ⊔

Lemma 2.11. (Transitivity) If D :: Γ ⊢ C_{1} = C_{2} :Type and Γ ⊢ C_{2} = C_{3} :Type then Γ ⊢ C_{1} = C_{3} :Type.

Proof: By induction on D. The case eq-set-e can be handled by eq-trans , interesting is the following one:

\frac{Γ ⊢ A_{1} = A_{2} :Type Γ, x:A_{1} ⊢ B_{1} = B_{2} :Type}{Γ ⊢ Fun A_{1} (λxB_{1}) = Fun A_{2} (λxB_{2}) :Type}

\frac{Γ ⊢ A_{2} = A_{3} :Type Γ, x:A_{2} ⊢ B_{2} = B_{3} :Type}{Γ ⊢ Fun A_{2} (λxB_{2}) = Fun A_{3} (λxB_{3}) :Type}

By context well-formedness, Γ ⊢ A_{1} : Type, hence, we can apply context conversion to obtain Γ, x: A_{1} ⊢ B_{2} = B_{3} : Type. By induction hypothesis it follows that Γ, x: A_{1} ⊢ B_{1} = B_{3} : Type. The rest is easy. ⊓ ⊔

Theorem 2.1. (Syntactic validity) 1. Typing: If D :: Γ ⊢ t : A then Γ ⊢ A :Type.

2. Equality: If D :: Γ ⊢ t = t′ : A then Γ ⊢ A :Type and both Γ ⊢ t : A and Γ ⊢ t′ : A.

3. Type equality: If D :: Γ ⊢ A = A′ :Type then Γ ⊢ A :Type and Γ ⊢ A′ :Type.

Proof: Simultaneously by induction on D. A few interesting cases are:

• Case:

conv \frac{Γ ⊢ t : A  Γ ⊢ A = B :Type}{Γ ⊢ t : B}

By induction hypothesis (3.), Γ ⊢ B :Type.

• Case:

pair-i \frac{Γ, x:A ⊢ B :Type  Γ ⊢ s : A  Γ ⊢ t : B[s/x]}{Γ ⊢ (s, t) : Pair A (λxB)}

By induction hypotheses, Γ ⊢ A : Type, and Γ ⊢ B[s/x] : Type. By assumption Γ, x: A ⊢ B : Type, from which we conclude Γ ⊢ Pair A (λxB) :Type by rule pair-f .

• Case:

pair-e-r \frac{Γ ⊢ r : Pair A (λxB)}{Γ ⊢ r R : B[r L/x]}

By inversion on the induction hypothesis, Γ, x: A ⊢ B : Type. Also, by rule pair-e-l , Γ ⊢ r L : A. Hence, Γ ⊢ B[r L/x] :Type by substitution.

• Case:

eq-fun-f \frac{Γ ⊢ A = A′ :Type  Γ, x:A ⊢ B = B′ :Type}{Γ ⊢ Fun A (λxB) = Fun A′ (λxB′) :Type}

By induction hypothesis, Γ ⊢ A, A′ : Type and Γ, x : A ⊢ B, B′ : Type. We infer Γ ⊢ Fun A (λxB) : Type directly, by fun-f , whereas Γ ⊢ Fun A′ (λxB′) : Type follows only after we converted the type of x in the context to A′ (Lemma 2.9). This conversion is possible since we obtain Γ ⊢ A′ = A :Type by symmetry (Lemma 2.10).

• Case:

eq-fun-e \frac{Γ ⊢ r = r′ : Fun A (λxB)  Γ ⊢ s = s′ : A}{Γ ⊢ r s = r′ s′ : B[s/x]}

Γ ⊢ s, s′ : A  induction hypothesis
Γ ⊢ Fun A (λxB) :Type  induction hypothesis
Γ, x:A ⊢ B :Type  inversion
Γ ⊢ B[s/x] :Type  substitution lemma
Γ ⊢ r, r′ : Fun A (λxB)  induction hypothesis
Γ ⊢ r s : B[s/x]  rule fun-e
Γ ⊢ r′ s′ : B[s′/x]  rule fun-e
Γ ⊢ s′ = s : A  rule eq-sym
Γ ⊢ B[s′/x] = B[s/x] :Type  functionality for typing
Γ ⊢ r′ s′ : B[s/x]  rule conv

• Case:

eq-fun-β \frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λxt) s = t[s/x] : B[s/x]}

By induction hypothesis, Γ, x : A ⊢ B : Type, and we get the first goal Γ ⊢ B[s/x] : Type by the substitution lemma. Directly, we obtain Γ ⊢ λxt : Fun A (λxB) and the second goal Γ ⊢ (λxt) s : B[s/x]. Again by substitution, the last goal Γ ⊢ t[s/x] : B[s/x] follows.

• Case:

eq-fun-η \frac{Γ ⊢ t : Fun A (λxB)}{Γ ⊢ (λx. t x) = t : Fun A (λxB)} x ∉ FV(t)

W. l. o. g., x is not bound by context Γ. By induction hypothesis, Γ ⊢ Fun A (λxB) : Type. By inversion for types, Γ ⊢ A : Type, hence we can apply weakening to obtain Γ, x : A ⊢ t : Fun A (λxB). This entails Γ, x:A ⊢ t x : B by fun-e and Γ ⊢ λx. t x : Fun A (λxB) by fun-i .

⊓ ⊔

After having established syntactical validity, we can drop all \underline{underlined} hypotheses from the lemmata.

Figure 5 recapitulates the dependencies between the lemmata that lead up to syntactic validity. The following lemma is more or less a consequence of substitution and functionality for typing, but

it will allow for a more concise reasoning in Section 4.

Lemma 2.12. (Functionality for equality) 1. If Γ, x:A, Γ′ ⊢ t = t′ : C and Γ ⊢ s = s′ : A then Γ, Γ′[s/x] ⊢ t[s/x] = t′[s′/x] : C[s/x].

2. If Γ, x:A, Γ′ ⊢ C = C′ :Type and Γ ⊢ s = s′ : A then Γ, Γ′[s/x] ⊢ C[s/x] = C′[s′/x] :Type.

Figure 5. Lemma dependencies.

Proof: Direct (cf. Harper and Pfenning [17]). We show the proof of the first proposition:

Γ ⊢ s : A  syntactic validity
Γ, Γ′[s/x] ⊢ t[s/x] = t′[s/x] : C[s/x]  substitution lemma
Γ, x:A, Γ′ ⊢ t′ : C  syntactic validity
Γ, Γ′[s/x] ⊢ t′[s/x] = t′[s′/x] : C[s/x]  functionality for typing
Γ, Γ′[s/x] ⊢ t[s/x] = t′[s′/x] : C[s/x]  rule eq-trans
⊓ ⊔

The next lemma will be central for the soundness proof of algorithmic equality in Section 4. Other names for the theorem are generation lemma or stripping lemma, and it is central for proving subject reduction (which we will not do in this article).

Lemma 2.13. (Inversion of Typing) 1. If D :: Γ ⊢ x : C then Γ ⊢ Γ(x) = C :Type.

2. If D :: Γ ⊢ λxt : C then C ≡ Fun A (λxB) and Γ, x:A ⊢ t : B.

3. If D :: Γ ⊢ r s : C then Γ ⊢ r : Fun A (λxB) with Γ ⊢ s : A and Γ ⊢ B[s/x] = C :Type.

4. If D :: Γ ⊢ (r, s) : C then C ≡ Pair A (λxB) with Γ ⊢ r : A and Γ ⊢ s : B[r/x].

5. If D :: Γ ⊢ rL : A then Γ ⊢ r : Pair A (λxB).

6. If D :: Γ ⊢ rR : C then Γ ⊢ r : Pair A (λxB) and Γ ⊢ B[rL/x] = C :Type.

Proof: By induction on D. For each shape of term t in Γ ⊢ t : C, there are two matching rules. One is the introduction resp. elimination rule fitting t, which entails the inversion property trivially. The other one is rule conv :

• Case:

conv \frac{Γ ⊢ λxt : C  Γ ⊢ C = C′ :Type}{Γ ⊢ λxt : C′}

By induction hypothesis C ≡ Fun A (λxB) and Γ, x : A ⊢ t : B. By injectivity, C′ ≡ Fun A′ (λxB′) with Γ ⊢ A = A′ : Type and Γ, x : A ⊢ B = B′ : Type. By conversion and context conversion we conclude Γ, x:A′ ⊢ t : B′.

• Case:

conv \frac{Γ ⊢ r s : C  Γ ⊢ C = C′ :Type}{Γ ⊢ r s : C′}

By induction hypothesis Γ ⊢ r : Fun A (λxB) for some A, B with Γ ⊢ s : A and Γ ⊢ B[s/x] = C :Type. We infer Γ ⊢ B[s/x] = C′ :Type by transitivity.

• Case:

conv \frac{Γ ⊢ r L : A  Γ ⊢ A = A′ :Type}{Γ ⊢ r L : A′}

By induction hypothesis, Γ ⊢ r : Pair A (λxB). Syntactic validity (Theorem 2.1), inversion, and reflexivity entail Γ, x: A ⊢ B = B : Type, hence, Γ ⊢ Pair A (λxB) = Pair A′ (λxB) : Type by rule eq-pair-f . The desired Γ ⊢ r : Pair A′ (λxB) follows by conv .

⊓ ⊔

Remark 2.3. (Weaker inversion property for left projection) The statement “if Γ ⊢ rL : C then Γ ⊢ r : Pair A (λxB) and Γ ⊢ A = C :Type” can be proven without reference to syntactic validity.

3. Algorithmic Presentation

In this section, we present algorithms for deciding equality and for type-checking. The goal of this article is to show these algorithms sound and complete.

Syntactic classes. The algorithms work on weak head normal forms WVal. For convenience, we introduce separate categories for normal forms which can denote a function and for those which can denote a

18 A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing

pair. In the intersection of these categories live the neutral expressions.

WElim ∋ e ::= s | p  eliminations
WNe ∋ n ::= c | x | n e neutral expressions
WFun ∋ w_{f} ::= n | λxt weak head function values
WPair ∋ w_{p} ::= n | (t, t′) weak head pair values
WVal ∋ w ::= w_{f} | w_{p} weak head values

Note that types A ∈ Ty ⊆ WNe are always neutral weak head values. Weak head evaluation. We define simultaneously two judgements:

↘  ⊆ Exp × WVal
@ ↘ ⊆ WVal × WElim × WVal

Weak head evaluation t ↘ w.

eval-c \overline{c ↘ c}  eval-var \overline{x ↘ x}
eval-fun-i \overline{λxt ↘ λxt}  eval-fun-e \frac{r ↘ w_{f}  w_{f}@s ↘ w}{r s ↘ w}
eval-pair-i \overline{(t, t′) ↘ (t, t′)}  eval-pair-e \frac{r ↘ w_{p}  w_{p}@p ↘ w}{r p ↘ w}

Active elimination w@e ↘ w′.

elim-ne \overline{n@e ↘ n e}  elim-fun \frac{t[s/x] ↘ w}{(λxt)@s ↘ w}
elim-pair-l \frac{t ↘ w}{(t, t′)@L ↘ w}  elim-pair-r \frac{t′ ↘ w}{(t, t′)@R ↘ w}

Weak head evaluation t ↘ w is equivalent to multi-step weak head reduction to weak head normal form. Conversion. Two terms t, t′ are algorithmically equal if t ↘ w, t′ ↘ w′, and w ∼ w′ for some w, w′. We combine these three propositions to t↓ ∼ t′↓. Similarly, t@e ∼ t′@e′ shall denote t@e ↘ w, t′@e′ ↘ w′, and w ∼ w′. The algorithmic equality on weak head normal forms w ∼ w′ is given inductively by the following rules:

aq-c \overline{c ∼ c}  aq-var \overline{x ∼ x}

aq-ne-fun \frac{n ∼ n′  s↓ ∼ s′↓}{n s ∼ n′ s′}  aq-ne-pair \frac{n ∼ n′}{n p ∼ n′ p}

aq-ext-fun \frac{w_{f}@x ∼ w′_{f}@x}{w_{f} ∼ w′_{f}} x ∉ FV(w_{f}, w′_{f})

aq-ext-pair \frac{w_{p}@L ∼ w′_{p}@L  w_{p}@R ∼ w′_{p}@R}{w_{p} ∼ w′_{p}}

For two neutral values, the rules (aq-ne -x) are preferred over aq-ext-fun and aq-ext-pair . Thus, conversion is deterministic. It is easy to see that it is symmetric as well.

In our presentation, untyped conversion resembles type-directed conversion. In the terminology of Harper and Pfenning [17] and Sarnat [25], the first four rules aq-c , aq-var , aq-ne-fun and aq-ne-pair compute structural equality, whereas the remaining extensionality rules aq-ext-fun and aq-ext-pair compute type-directed equality. The difference is that in our formulation, the shape of a value—function or pair— triggers application of the extensionality rules.

Remark 3.1. In contrast to the corresponding equality for λ-terms without pairs [8], which we obtain by removing aq-ne-pair and aq-ext-pair , this relation is not transitive. For instance, λx. n x ∼ n and n ∼ (nL, nR), but not λx. n x ∼ (nL, nR).

Type checking. In the following, we give a bidirectional type checking algorithm [9, 22, 17] for βnormal terms. The judgement Γ ⊢ t ⇓ A infers type A from neutral terms t and the simultaneously defined judgement Γ ⊢ t ⇑ C checks whether the β-normal term t has type C. A third judgement Γ ⊢ A ⇓ Type identifies wellformed types A ∈ Ty and depends on the type-checking judgement. Although the algorithm works only for well-formed contexts, well-formed types, and β-normal terms, we do not presuppose these properties in the definition of the judgements. However, these conditions will appear in the soundness (4.1) and completeness (9.2) theorems. Type inference Γ ⊢ t ⇓ A. (Input: Γ well-formed, t neutral and β-normal. Output: A with Γ ⊢ t : A.)

inf-var \overline{Γ ⊢ x ⇓ Γ(x)}  inf-fun-e \frac{Γ ⊢ r ⇓ Fun A (λxB)  Γ ⊢ s ⇑ A}{Γ ⊢ r s ⇓ B[s/x]}

inf-pair-e-l \frac{Γ ⊢ r ⇓ Pair A (λxB)}{Γ ⊢ rL ⇓ A}  inf-pair-e-r \frac{Γ ⊢ r ⇓ Pair A (λxB)}{Γ ⊢ rR ⇓ B[rL/x]}

Type checking Γ ⊢ t ⇑ A. (Input: Γ, C with Γ ⊢ C :Type, t β-normal. Output: none.)

chk-inf \frac{Γ ⊢ r ⇓ A  A ∼ B}{Γ ⊢ r ⇑ B}  chk-fun-i \frac{Γ, x:A ⊢ t ⇑ B}{Γ ⊢ λxt ⇑ Fun A (λxB)}

chk-pair-i \frac{Γ ⊢ t ⇑ A  Γ ⊢ t′ ⇑ B[t/x]}{Γ ⊢ (t, t′) ⇑ Pair A (λxB)}

Type well-formedness Γ ⊢ A ⇓Type. (Input: Γ well-formed, A type. Output: none.)

chk-set-f Γ ⊢ Set ⇓Type chk-set-e

\frac{Γ ⊢ t ⇑ Set}{Γ ⊢ El t ⇓Type}

chk-dep-f \frac{Γ ⊢ A ⇓Type Γ, x:A ⊢ B ⇓Type}{Γ ⊢ c A (λxB) ⇓Type} c ∈ \{Fun, Pair\}

When starting type-checking Γ ⊢ t ⇑ C of term t, we suppose that C has been checked for wellformedness before. Also, we suppose one starts the type-checker with an empty context in the beginning and adds only checked types to the context. Under these assumptions, one can see that all rules maintain a checked context—the only rules that extend the context by a type A are chk-fun-i and chk-dep-f , and in both cases A has been checked before. Another observation is that only checked terms are substituted into types (rules inf-fun-e , inf-pair-e-r , and chk-pair-i ). This implies that inference Γ ⊢ t ⇓ A always returns a well-formed type: in case inf-var , since it comes from the checked context, and in the other cases, since it results from a substitution of a checked term into a well-formed type. Finally, we can conclude that equality test A ∼ B is only invoked on well-formed types A, B. All these observations will be proven formally in the next section and in Section 9.

The algorithms in this section have been prototypically implemented in Haskell using explicit substitutions [1].

4. Soundness

The soundness proofs for conversion and type-checking in this section are entirely syntactical and rely crucially on injectivity of El, Fun and Pair (Lemma 2.1) and inversion of typing (Lemma 2.13). First, we show soundness of weak head evaluation, which subsumes subject reduction.

Lemma 4.1. (Soundness of weak head evaluation) 1. If D :: t ↘ w and Γ ⊢ t : C then Γ ⊢ t = w : C.

2. If D :: w@e ↘ w′ and Γ ⊢ w e : C then Γ ⊢ w e = w′ : C.

Note that we do not need a corresponding lemma for weak head evaluation of types, since they are neutral and therefore always weak head normal.

Proof: Simultaneously by induction on D, making essential use of inversion laws.

• Case:

eval-fun-e \frac{r ↘ w_{f}  w_{f}@s ↘ w}{r s ↘ w}

Γ ⊢ r s : C  hypothesis
Γ ⊢ r : Fun A (λxB)  &
Γ ⊢ s : A  &
Γ ⊢ B[s/x] = C :Type  inversion
Γ ⊢ r = w_{f} : Fun A (λxB)  first ind. hyp.
Γ ⊢ r s = w_{f} s : B[s/x]  eq-fun-e
Γ ⊢ r s = w_{f} s : C  conv
Γ ⊢ w_{f} s : C  syntactic validity
Γ ⊢ w_{f} s = w : C  second ind. hyp.
Γ ⊢ r s = w : C  eq-trans

• Case:

elim-fun \frac{t[s/x] ↘ w}{(λxt)@s ↘ w}

Γ ⊢ (λxt) s : C  hypothesis
Γ ⊢ λxt : Fun A (λxB)  &
Γ ⊢ s : A  &
Γ ⊢ B[s/x] = C :Type  inversion
Γ, x:A ⊢ t : B  inversion
Γ ⊢ (λxt) s = t[s/x] : B[s/x]  eq-fun-β
Γ ⊢ (λxt) s = t[s/x] : C  eq-conv
Γ ⊢ t[s/x] : C  syntactic validity
Γ ⊢ t[s/x] = w : C  ind. hyp.
Γ ⊢ (λxt) s = w : C  eq-trans
⊓ ⊔

Two algorithmically convertible well-typed expressions must also be equal in the declarative sense. In case of neutral terms, we also obtain that their types are equal. This is due to the fact that we can read off the type of the common head variable and break it down through the sequence of eliminations.

Lemma 4.2. (Soundness of conversion) 1. Neutral terms: If D :: n ∼ n′ and Γ ⊢ n : C and Γ ⊢ n′ : C′ then Γ ⊢ n = n′ : C and Γ ⊢ C = C′ :Type.

2. Weak head values: If D :: w ∼ w′ and Γ ⊢ w, w′ : C then Γ ⊢ w = w′ : C.

3. All terms: If t↓ ∼ t′↓ and Γ ⊢ t, t′ : C then Γ ⊢ t = t′ : C.

Proof: The third proposition is a consequence of the second, using soundness of evaluation (Lemma 4.1) and transitivity. We prove the first two propositions simultaneously by induction on D.

• Case:

aq-ne-fun \frac{n ∼ n′  s↓ ∼ s′↓}{n s ∼ n′ s′}

Γ ⊢ n s : C  hypothesis
Γ ⊢ n : Fun A (λxB)  &
Γ ⊢ s : A  &
Γ ⊢ B[s/x] = C :Type  inversion
Γ ⊢ n′ s′ : C′  hypothesis
Γ ⊢ n′ : Fun A′ (λxB′)  &
Γ ⊢ s′ : A′  &
Γ ⊢ B′[s′/x] = C′ :Type  inversion
Γ ⊢ n = n′ : Fun A (λxB)  &
Γ ⊢ Fun A (λxB) = Fun A′ (λxB′) :Type  first ind. hyp.
Γ ⊢ A = A′ :Type  injectivity
Γ ⊢ s′ : A  symmetry, rule conv
Γ ⊢ s = s′ : A  second ind. hyp. (3.)
Γ, x:A ⊢ B = B′ :Type  injectivity
Γ ⊢ B[s/x] = B′[s′/x] :Type  functionality
Γ ⊢ C = C′ :Type  transitivity, symmetry
Γ ⊢ n s = n′ s′ : C  rules eq-fun-e ,conv

• Case (instance of aq-ext-fun with w_{f} ≡ λxt and w′_{f} = n):

aq-ext-fun \frac{(λxt)@x ↘ w  w ∼ n x  n@x ↘ n x}{λxt ∼ n} x ∉ FV(n)

Γ ⊢ λxt : C  hypothesis
C ≡ Fun A (λxB)  &
Γ, x:A ⊢ t : B  inversion
t ↘ w  assumption
Γ, x:A ⊢ t = w : B  eval. sound (Lemma 4.1)
Γ ⊢ n : Fun A (λxB)  hypothesis, def. C
Γ ⊢ λx. n x = n : Fun A (λxB)  eq-fun-η , x ∉ FV(n)
Γ, x:A ⊢ n : Fun A (λxB)  weakening
Γ, x:A ⊢ n x : B  fun-e , hyp
Γ, x:A ⊢ w = n x : B  ind. hyp.
Γ, x:A ⊢ t = n x : B  transitivity (eq-trans )
Γ ⊢ λxt = λx. n x : Fun A (λxB)  eq-fun-i
Γ ⊢ λxt = n : C  eq-trans , conv
⊓ ⊔

Lemma 4.3. (Soundness of type conversion) Let C ∼ C′. If D :: Γ ⊢ C :Type and Γ ⊢ C′ :Type, then Γ ⊢ C = C′ :Type.

Proof: By induction on D. For instance, if C ≡ Fun A (λxB), we obtain by inversion for types the two derivations Γ ⊢ A : Type and Γ, x : A ⊢ B : Type which are shorter than D. By inversion on the derivation of Fun A (λxB) ∼ C′ using the fact that C′ is a type, we can determine C′ ≡ Fun A′ (λxB′) and both A ∼ A′ and λxB ∼ λxB′. The last proposition can only be derived from B ∼ B′. Inverting the well-formedness derivation of C′ and using context conversion gives us Γ ⊢ A′ :Type and Γ, x:A ⊢ B′ :Type. Now we can assemble the induction hypotheses Γ ⊢ A = A′ :Type and Γ, x:A ⊢ B = B′ : Type to conclude Γ ⊢ C = C′ :Type. ⊓ ⊔

It follows that also type checking is correct, if started in a correct context and with a well-formed type.

Theorem 4.1. (Soundness of bidirectional type checking) 1. If D :: Γ ⊢ t ⇓ A and Γ ⊢ ok then Γ ⊢ t : A.

2. If D :: Γ ⊢ t ⇑ C and Γ ⊢ C :Type, then Γ ⊢ t : C.

3. If D :: Γ ⊢ C ⇓Type and Γ ⊢ ok then Γ ⊢ C :Type.

Proof: All three propositions by induction on D, the first two simultaneously, then the third. ⊓ ⊔

5. Models

To show completeness of algorithmic equality, we leave the syntactic discipline. Although a syntactical proof should be possible along the lines of Goguen [13, 14], we prefer a model construction since it is more apt to extensions of the type theory.

The contribution of this section is that any PER model over a λ-model with full β-equality is a model of MLF_{Σ}. Only in the next section will we decide on a particular model which enables the completeness proof.

5.1. λ Models

We assume a set D with the four operations

· ∈ D × D → D  application,
L ∈ D → D  left projection,
R ∈ D → D  right projection, and
∈ Exp × Env → D denotation.

Herein, we use the following entities:

c  ∈ Const := {Set, El, Fun, Pair} constants
u, v, f, V, F ∈ D  ⊇ Const  domain of the model
ρ  ∈ Env := Var → D  environments

Let p range over the projection functions L and R. To simplify the notation, we write also f v for f · v. Update of environment ρ by the binding x = v is written ρ, x = v. The operations f · v, v p and tρ must satisfy the following laws:

den-const  cρ = c  if c ∈ Const
den-var  xρ = ρ(x)
den-fun-e  (r s)ρ = rρ (sρ)
den-pair-e  (r p)ρ = rρ p
den-β  tρ = t′ρ  if t =_{β} t′
den-irr  tρ = tρ′  if ρ(x) = ρ′(x) for all x ∈ FV(t)

These laws axiomatize a syntactical λ-algebra [6, 5.3.2.(ii)] extended by projections. In an earlier version of this work [3] we required D to be a syntactical λ-model, with weak extensionality. However, this is an unnecessary requirement and excludes closed term models.

The following laws for β are admissible:

den-fun-β  (λxt)ρ v = t(ρ, x=v)
den-pair-β-l  (r, s)ρ L = rρ
den-pair-β-r  (r, s)ρ R = sρ

Proof: We show soundness of den-fun-β .

(λxt)ρ v
= (λxt)ρ x(ρ, x=v)  den-var
= (λxt)(ρ, x=v) x(ρ, x=v)  den-irr
= ((λxt) x)(ρ, x=v)  den-fun-e
= t(ρ, x=v)  den-β .
⊓ ⊔

The substitution property is a consequence of β-equality:

Lemma 5.1. (Soundness of substitution) (t[s/x])ρ = t(ρ, x=sρ).

Proof: (t[s/x])ρ = ((λxt) s)ρ = (λxt)ρ sρ = t(ρ, x=sρ). ⊓ ⊔

Injectivity laws. We require the type constructors in the model to be injective. This is necessary since we want to interpret distinguished elements of D, the types, as semantical types later. In the following, let c, c′ ∈ {Fun, Pair}.

den-set-not-el  Set ≠ El v
den-set-not-dep  Set ≠ c V F
den-el-not-dep  El v ≠ c V F
den-el-inj  El v = El v′  implies v = v′
den-dep-inj  c V F = c′ V′ F′ implies c = c′ and V = V′ and F = F′

5.2. PER Models

In the definition of PER models, we follow a paper of the second author with Pollack and Takeyama [10] and Vaux [27]. The only difference is, since we have codes for types in D, we can define the semantical property of being a type directly on elements of D, whereas the first cited work defines a new syntactic class of type expressions on top of D, there being the untyped λ-calculus, and the second cited work introduces an intensional type equality on closures tρ.

Relations on D. Let Rel denote the set of relations over D. If A ∈ Rel, we say v ∈ A if v is in the carrier of A, i. e., (v, w) ∈ A or (w, v) ∈ A for some w ∈ D.

Partial equivalence relations (PERs) and families. A PER is a symmetric and transitive relation. Let Per ⊆ Rel denote the set of PERs over D. If A ∈ Per, we write v = v′ ∈ A if (v, v′) ∈ A. For A a PER, v ∈ A means v = v ∈ A. Each set A ⊆ D can be understood as the discrete PER where v = v′ ∈ A holds iff v = v′ and v ∈ A. Let Fam(A) be the set of functions F ∈ A → Per such that F(v) = F(v′) if (v, v′) ∈ A.

Constructions on PERs. Let A ∈ Rel and F ∈ A → Rel . We define Fun(A, F), Pair(A, F) ∈ Rel:

(f, f′) ∈ Fun(A, F) iff (f v, f′ v′) ∈ F(v) for all (v, v′) ∈ A
(v, v′) ∈ Pair(A, F) iff (v L, v′ L) ∈ A and (v R, v′ R) ∈ F(v L)

Lemma 5.2. (Fun and Pair operate on PERs) If A ∈ Per and F ∈ Fam(A) then Fun(A, F), Pair(A, F) ∈ Per.

In the following, assume some Set ∈ Per and some Eℓ ∈ Fam(Set).

Semantical types. We define inductively a new relation Type ∈ Per and a function [ ] ∈ Fam(Type):

Set = Set ∈ Type and [Set] is Set.

El v = El v′ ∈ Type if v = v′ ∈ Set. Then [El v] is Eℓ(v).

Fun V F = Fun V′ F′ ∈ Type if V = V′ ∈ Type and v = v′ ∈ [V] implies F v = F′ v′ ∈ Type. We define then [Fun V F] to be Fun([V], v ↦ [F v]).

Pair V F = Pair V′ F′ ∈ Type if V = V′ ∈ Type and v = v′ ∈ [V] implies F v = F′ v′ ∈ Type. We define then [Pair V F] to be Pair([V], v ↦ [F v]).

This definition is possible by the injectivity laws. Notice that in the last two clauses, we have

Fun([V], v ↦ [F v]) = Fun([V′], v ↦ [F′ v]), and

Pair([V], v ↦ [F v]) = Pair([V′], v ↦ [F′ v]).

Remark 5.1. Type and [ ] are an instance of an inductive-recursive definition [12]. Appendix B presents an alternative formulation, via a relation which is not a priori a PER, and a partial function.

5.3. Validity

If Γ is a context, we define a corresponding PER on Env, written [Γ]. We define ρ = ρ′ ∈ [Γ] to mean that, for all x:A in Γ, we have Aρ = Aρ′ ∈ Type and ρ(x) = ρ′(x) ∈ [Aρ].

Semantical contexts Γ ∈ Cxt are defined inductively by the following rules:

sem-cxt-empty \overline{⋄ ∈ Cxt}

sem-cxt-ext \frac{Γ ∈ Cxt  Aρ = Aρ′ ∈ Type for all ρ = ρ′ ∈ [Γ]}{(Γ, x:A) ∈ Cxt}

Theorem 5.1. (Soundness of the rules of MLF_{Σ}) 1. If D :: Γ ⊢ ok then Γ ∈ Cxt.

2. If D :: Γ ⊢ A :Type then Γ ∈ Cxt, and if ρ = ρ′ ∈ [Γ] then Aρ = Aρ′ ∈ Type.

3. If D :: Γ ⊢ t : A then Γ ∈ Cxt, and if ρ = ρ′ ∈ [Γ] then Aρ = Aρ′ ∈ Type and tρ = tρ′ ∈ [Aρ].

4. If D :: Γ ⊢ A = A′ :Type then Γ ∈ Cxt, and if ρ = ρ′ ∈ [Γ] then Aρ = A′ρ′ ∈ Type.

A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing 27

5. If D :: Γ ⊢ t = t′ : A then Γ ∈ Cxt, and if ρ = ρ′ ∈ [Γ] then Aρ = Aρ′ ∈ Type and

tρ = t′ρ′ ∈ [Aρ]. Proof: Simultaneously by induction on D, using lemma 5.1.

• Case:

fun-i \frac{Γ, x:A ⊢ t : B}{Γ ⊢ λxt : Fun A (λxB)}
(Γ, x:A) ∈ Cxt  ind. hyp. (*)
Γ ∈ Cxt  inversion
ρ = ρ′ ∈ [Γ]  assumption
Aρ = Aρ′ ∈ Type  from (*)
v = v′ ∈ [Aρ]  assumption (v, v′ arbitrary)
(ρ, x=v) = (ρ′, x=v′) ∈ [Γ, x:A]  def. [Γ, x:A]
B(ρ, x=v) = B(ρ′, x=v′) ∈ Type  ind. hyp.
(λxB)ρ v = (λxB)ρ′ v′ ∈ Type  den-fun-β
(Fun A λxB)ρ = (Fun A λxB)ρ′ ∈ Type  def. Type, den-fun-e , den-const
t(ρ, x=v) = t(ρ′, x=v′) ∈ [B(ρ, x=v)]  ind. hyp.
(λxt)ρ v = (λxt)ρ′ v′ ∈ [(λxB)ρ v]  den-fun-β
(λxt)ρ = (λxt)ρ′ ∈ [(Fun A λxB)ρ]  def. Fun, den-fun-e , den-const

• Case:

fun-e \frac{Γ ⊢ r : Fun A (λxB)  Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}
Γ ∈ Cxt  ind. hyp.
ρ = ρ′ ∈ [Γ]  assumption
Fun (Aρ) ((λx.B)ρ) = Fun (Aρ′) ((λx.B)ρ′) ∈ Type  ind. hyp.
sρ = sρ′ ∈ [Aρ]  ind. hyp.
B(ρ, x=sρ) = B(ρ′, x=sρ′) ∈ Type  def. Type
(B[s/x])ρ = (B[s/x])ρ′ ∈ Type  subst. (Lemma 5.1)
rρ = rρ′ ∈ Fun([Aρ], v ↦ [B(ρ, x=v)])  ind. hyp.
rρ (sρ) = rρ′ (sρ′) ∈ [B(ρ, x=sρ)]  def. Fun
(r s)ρ = (r s)ρ′ ∈ [(B[s/x])ρ]  den-fun-e , Lemma 5.1

28 A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing

• Case:

eq-fun-β \frac{Γ, x:A ⊢ t : B  Γ ⊢ s : A}{Γ ⊢ (λxt) s = t[s/x] : B[s/x]}
Γ ∈ Cxt  ind. hyp.
ρ = ρ′ ∈ [Γ]  assumption
Aρ = Aρ′ ∈ Type  ind. hyp.
sρ = sρ′ ∈ [Aρ]  ind. hyp.
(ρ, x=sρ) = (ρ′, x=sρ′) ∈ [Γ, x:A]  def. [Γ, x:A]
B(ρ, x=sρ) = B(ρ′, x=sρ′) ∈ Type  ind. hyp.
(B[s/x])ρ = (B[s/x])ρ′ ∈ Type  subst. (Lemma 5.1)
t(ρ, x=sρ) = t(ρ′, x=sρ′) ∈ [B(ρ, x=sρ)]  ind. hyp.
(λxt)ρ (sρ) = (t[s/x])ρ′ ∈ [(B[s/x])ρ]  den-fun-β , subst.

• Case:

eq-fun-η \frac{Γ ⊢ t : Fun A (λxB)}{Γ ⊢ (λx. t x) = t : Fun A (λxB)} x ∉ FV(t)

Γ ∈ Cxt  ind. hyp.
ρ = ρ′ ∈ [Γ]  assumption
(Fun A λxB)ρ = (Fun A λxB)ρ′ ∈ Type  ind. hyp.
Aρ = Aρ′ ∈ Type  inversion on Type
v = v′ ∈ [Aρ]  assumption (v, v′ arbitrary)
tρ = tρ′ ∈ [(Fun A λxB)ρ]  ind. hyp.
tρ v = tρ′ v′ ∈ [(λxB)ρ v]  def. Fun
t(ρ, x=v) v = tρ′ v′ ∈ [(λxB)ρ v]  irrelevance den-irr
(t x)(ρ, x=v) = tρ′ v′ ∈ [(λxB)ρ v]  den-fun-e , den-var
(λx. t x)ρ v = tρ′ v′ ∈ [(λxB)ρ v]  den-fun-β
(λx. t x)ρ = tρ′ ∈ [(Fun A λxB)ρ]  since v, v′ arb.

• Case:

eq-pair-η \frac{Γ ⊢ r : Pair A (λxB)}{Γ ⊢ (r L, r R) = r : Pair A (λxB)}

Γ ∈ Cxt  ind. hyp.
ρ = ρ′ ∈ [Γ]  assumption
(Pair A λxB)ρ = (Pair A λxB)ρ′ ∈ Type  ind. hyp.
rρ = rρ′ ∈ [(Pair A λxB)ρ]  ind. hyp.
(r L)ρ = rρ′ L ∈ [Aρ]  def. Pair, den-pair-e
(r L, r R)ρ L = rρ′ L ∈ [Aρ]  den-pair-β-l
(r R)ρ = rρ′ R ∈ [(λxB)ρ (r L)ρ]  def. Pair, den-pair-e
(r L, r R)ρ R = rρ′ R ∈ [(λxB)ρ ((r L, r R)ρ L)]  den-pair-β-r
(r L, r R)ρ = rρ′ ∈ [(Pair A λxB)ρ]  def. Pair
⊓ ⊔

5.4. Safe Types

We define an abstract notion of safety, similar to what Vaux calls “saturation” [27]. A PER is safe if it lies between a PER N on neutral expressions and a PER S on safe expressions [28]. In the following, we use set notation ⊆ and ∪ also for PERs.

Safety. N , S_{fun}, S_{pair} ∈ Per form a safety range if the following conditions are met:

safe-int  N ⊆ S = S_{fun} ∪ S_{pair}
safe-ne-fun  u v = u′ v′ ∈ N if u = u′ ∈ N and v = v′ ∈ S
safe-ne-pair  u p = u′ p ∈ N if u = u′ ∈ N
safe-ext-fun v = v′ ∈ S_{fun} if v u = v′ u′ ∈ S for all u = u′ ∈ N
safe-ext-pair  v = v′ ∈ S_{pair} if v L = v′ L ∈ S and v R = v′ R ∈ S

A relation A ∈ Per is called safe w. r. t. to a safety range (N , S_{fun}, S_{pair}) if N ⊆ A ⊆ S. Usually there is just one safety range in scope and then all uses of “safe” refer to this one.

Lemma 5.3. (Fun and Pair preserve safety) Let R = (N , S_{fun}, S_{pair}) be a safety range. If A ∈ Per is safe (w. r. t. R) and F ∈ Fam(A) is such that F(v) is safe (w. r. t. R) for all v ∈ A then Fun(A, F) and Pair(A, F) are safe (w. r. t. R).

Proof: By monotonicity of Fun and Pair, if one considers the following reformulation of the conditions:

safe-ne-fun  N ⊆ Fun(S, ↦ N)
safe-ne-pair  N ⊆ Pair(N , ↦ N)
safe-ext-fun  Fun(N , ↦ S) ⊆ S_{fun}
safe-ext-pair  Pair(S, ↦ S) ⊆ S_{pair}
⊓ ⊔

Lemma 5.4. (Type interpretations are safe) Let (N , S_{fun}, S_{pair}) be a safety range. Let Set be safe and Eℓ(v) be safe for all v ∈ Set. If V ∈ Type then [V] is safe.

Proof: By induction on the proof that V ∈ Type, using Lemma 5.3. ⊓ ⊔

6. Term Model

In this section, we instantiate the model of the previous section to the set of expressions modulo βequality. Application is interpreted as expression application and the projections of the model are mapped to projections for expressions.

We define β-reduction ⟶_{β} as the closure of the axioms (λxt) s ⟶_{β} t[s/x], (t, t′) L ⟶_{β} t, and (t, t′) R ⟶_{β} t′ under all term constructors. Its reflexive-transitive closure ⟶_{β}^{∗} is confluent, which enables us to define β-equality t =_{β} t′ as there exists some t_{0} such that t ⟶_{β}^{∗} t_{0} _{β}^{∗}⟵ t′.

Let \overline{r} ∈ D denote the equivalence class of r ∈ Exp with regard to =_{β}. Similarly, let \overline{ρ} ∈ Var → D denote the equivalence class of ρ ∈ Var → Exp, meaning that \overline{ρ}(x) = \{t | t =_{β} ρ(x)\}.

D := Exp/=_{β}
\overline{r} · \overline{s} := \overline{r s}
\overline{r} L := \overline{r L}
\overline{r} R := \overline{r R}
t\overline{ρ} := \overline{t[ρ]}

Herein, t[ρ] denotes the substitution of ρ(x) for x in t, carried out in parallel for all x ∈ FV(t).

Lemma 6.1. Exp/=_{β} is a λ model in the sense of the last section.

Proof: We have to show that all operations are well-defined. For application, consider pairs of equivalent members r =_{β} r′ and s =_{β} s′. Since r s =_{β} r′ s′, application is well-defined. The projections are similarly easy. For the denotation operation, let t a term with F V (t) = x⃗. We assume two equivalent valuations ρ and ρ′, meaning that ρ(x) =_{β} ρ′(x) for all variables x. Now^{2}

\begin{aligned}t[ρ] & =_{β} & ((λx⃗t) x⃗)[ρ] & =_{β} & (λx⃗t)[ρ] x⃗[ρ] & =_{β} & (λx⃗t) x⃗[ρ] \\ & =_{β} & (λx⃗t)[ρ′] x⃗[ρ] & =_{β} & (λx⃗t)[ρ′] x⃗[ρ′] & =_{β} & ((λx⃗t) x⃗)[ρ′] & =_{β} & t[ρ′]. \end{aligned}

If we weaken the assumption such that ρ and ρ′ coincide only on the free variables of t, the calculation is still sound and validates den-irr . The laws den-const , den-var , den-fun-e and den-pair-e follow directly by the definition of parallel substitution, with a little work also den-β . The injectivity requirements follow from confluence and the fact that El, Fun, and Pair are unanimated constants. ⊓ ⊔ η-reduction and -equality. Let one-step η-reduction be the least congruence generated by the axioms λx. r x ⟶_{η} r if x ∉ FV(r) and (r L, r R) ⟶_{η} r. It is locally confluent and preserves free variables. Its reflexive-transitive closure ⟶_{η}^{∗} is strongly normalizing (each step removes an abstraction or a pair) and confluent (Newman’s Lemma). Because of confluence, we can define η-equality t =_{η} t′ as t ⟶_{η}^{∗} t_{0} _{η}^{∗}⟵ t′. In this article, we are only interested in η for β-normal forms.

2 Benzmüller, Brown, and Kohlhase [7] prove a similar result by converting t into an SK-combinatorial term.

Value classes. The β-normal forms v ∈ Val can be described by the following grammar. As it will become clear at the end of this section, they completely represent the β-equivalence classes \overline{t} ∈ Exp/=_{β} of well-typed terms t.

VNe ∋ u ::= c | x | u v | u p neutral values
VFun ∋ v_{f} ::= u | λxv  function values
VPair ∋ v_{p} ::= u | (v, v′)  pair values
Val ∋ v ::= v_{f} | v_{p}  values

Note that η-reduction on β-normal forms does not create β-redexes, hence it is well-defined on Val. Neutral values reduce to neutral values, so it is even well-defined on VNe. Even on values, it does not preserve typing, see Remark 2.1.

Lemma 6.2. (Inversion properties of ⟶_{η}^{∗}) 1. If D :: x ⟶_{η}^{∗} t then t ≡ x. If D :: c ⟶_{η}^{∗} t then t ≡ c.

2. If D :: r s ⟶_{η}^{∗} t then t ≡ r′ s′ with r ⟶_{η}^{∗} r′ and s ⟶_{η}^{∗} s′.

3. If D :: r p ⟶_{η}^{∗} t then t ≡ r′ p with r ⟶_{η}^{∗} r′.

4. If D :: λxv ⟶_{η}^{∗} t then either

• t ≡ u neutral value, x ∉ FV(u), and v ⟶_{η}^{∗} u x, or • t ≡ λxv′ and v ⟶_{η}^{∗} v′.

5. If D :: (v_{1}, v_{2}) ⟶_{η}^{∗} t then either

• t ≡ u neutral and both v_{1} ⟶_{η}^{∗} u L and v_{2} ⟶_{η}^{∗} u R, or • t ≡ (v′_{1}, v′_{2}) and both v_{1} ⟶_{η}^{∗} v′_{1} and v_{2} ⟶_{η}^{∗} v′_{2}.

Proof: Each by induction on D. Proposition 4 relies on the fact that if λx. r x is β-normal, then r must be neutral. ⊓ ⊔

As a consequence of these inversion properties, we can decompose η-equations between values as follows. Some of these decompositions, e. g. 5., do not carry over to arbitrary terms: We have λx. (λxz) x =_{η} λxz, but not (λxz) x =_{η} z.

Corollary 6.1. (Inversion on =_{η}) 1. If x =_{η} u_{0} then u_{0} ≡ x. If c =_{η} u_{0} then u_{0} ≡ c.

2. If u v =_{η} u_{0} then u_{0} ≡ u′ v′ with u =_{η} u′ and v =_{η} v′.

3. If u p =_{η} u_{0} then u_{0} ≡ u′ p with u =_{η} u′.

4. If λxv =_{η} u then v =_{η} u x and x ∉ FV(u).

5. If λxv =_{η} λxv′ then v =_{η} v′.

6. If (v_{1}, v_{2}) =_{η} u then v_{1} =_{η} u L and v_{2} =_{η} u R.

7. If (v_{1}, v_{2}) =_{η} (v′_{1}, v′_{2}) then v_{1} =_{η} v′_{1} and v_{2} =_{η} v′_{2}.

8. If (v_{1}, v_{2}) =_{η} λxv then v_{1} ⟶_{η}^{∗} u L, v_{2} ⟶_{η}^{∗} u R, and u x _{η}^{∗}⟵ v for some u.

An η-equality on β-equivalence classes. Since η-equality is an equivalence on Val, the relation

t ≃ t′ :⟺ t =_{β} v and t′ =_{β} v′ for some v, v′ with v =_{η} v′

is a partial equivalence on Exp. Note that if t ≃ t′, then t and t′ are β-normalizable. If t, t′ are β-normal forms, then t ≃ t′ if t =_{η} t′. We lift ≃ to β-equivalence classes: \overline{t} ≃ \overline{t′} iff t ≃ t′. Two classes can only be related if both contain a β-normal form. Choosing these normal forms as representatives, we have

\overline{v} ≃ \overline{v′} ⟺ v =_{η} v′.

Safety range. We define the following sub-relations N , S_{fun}, S_{pair} ⊆ S := ≃.

(\overline{t}, \overline{t′}) ∈ N  :⟺ t =_{β} u =_{η} u′ =_{β} t′ for some u, u′ ∈ VNe
(\overline{t}, \overline{t′}) ∈ S_{fun} :⟺ t =_{β} v_{f} =_{η} v′_{f} =_{β} t′ for some v_{f}, v′_{f} ∈ VFun
(\overline{t}, \overline{t′}) ∈ S_{pair} :⟺ t =_{β} v_{p} =_{η} v′_{p} =_{β} t′ for some v_{p}, v′_{p} ∈ VPair

Lemma 6.3. N , S_{fun}, S_{pair} ∈ Per.

Lemma 6.4. (Extensionality for functions) If v x ≃ v′ x with x ∉ FV(v, v′), then v, v′ ∈ VFun and v =_{η} v′. Proof: Consider the cases:

• Case v, v′ neutral. Then v x =_{η} v′ x, and v =_{η} v′ follows by Cor. 6.1, item 2.

• Case v ≡ λxv_{0} and v′ ≡ u neutral. By assumption, x ∉ FV(u) and v x ≃ u x, and since (λxv_{0}) x ⟶_{β} v_{0}, we have v_{0} =_{η} u x. Hence, λxv_{0} =_{η} λx. u x =_{η} u.

• Case v ≡ λxv_{0} and v′ ≡ λxv′_{0}. From the assumption we get v_{0} =_{η} v′_{0} by β-reduction. Hence, λxv_{0} =_{η} λxv′_{0}.

• Case v ≡ (v_{1}, v_{2}). Then (v_{1}, v_{2}) x does not reduce to β-normal form, which is a contradiction to the assumption.

⊓ ⊔

Corollary 6.2. (safe-ext-fun ) If \overline{v u} = \overline{v′ u′} ∈ S for all \overline{u} = \overline{u′} ∈ N, then \overline{v} = \overline{v′} ∈ S_{fun}.

Proof: By the previous lemma with u ≡ u′ ≡ x ∉ FV(v, v′). ⊓ ⊔

Lemma 6.5. (safe-ext-pair ) If v L ≃ v′ L and v R ≃ v′ R then v, v′ ∈ VPair and v =_{η} v′.

Proof: By cases, similar to last lemma. ⊓ ⊔

Corollary 6.3. (Safety range) N , S_{fun}, S_{pair} form a safety range.

Proof: safe-int holds by definition of N , S_{fun}, S_{pair}. Requirements safe-ne-fun and safe-ne-pair are simple closure properties of η-equality. safe-ext-fun is satisfied by Cor. 6.2 and safe-ext-pair by Lemma 6.5. ⊓ ⊔

Now we can instantiate our generic PER model of MLF_{Σ}. We let Set := S and Eℓ(\overline{t}) := S. From this we get a decision procedure for judgmental equality.

Lemma 6.6. (Context satisfiable) Let ρ_{0}(x) := x for all x ∈ Var. If Γ ⊢ ok, then \overline{ρ_{0}} ∈ [Γ].

Theorem 6.1. (Equal terms are related) If Γ ⊢ t = t′ : C then \overline{t} ≃ \overline{t}′.

Proof: Note that t\overline{ρ_{0}} = \overline{t}. By soundness of MLF_{Σ} (Thm. 5.1), t\overline{ρ_{0}} = t′\overline{ρ_{0}} ∈ [C\overline{ρ_{0}}]. The claim follows since [C\overline{ρ_{0}}] ⊆ S by Lemma 5.4. ⊓ ⊔

Corollary 6.4. (Equal types are related) If D :: Γ ⊢ A = A′ :Type then \overline{A} ≃ \overline{A}′.

Proof: By induction on D, using the theorem in case A ≡ El t. ⊓ ⊔

We have shown that each well-typed term is β-normalizable and two judgmentally equal terms βηreduce to the same normal form. This gives us a decision procedure for equality of well-typed terms: By Theorem 5.1, instantiated to the term model of this section, well-typed terms Γ ⊢ t, t′ : C are βnormalizable, hence, the test t ≃ t′ terminates. If the test succeeds, then Γ ⊢ t = t′ : C holds; this is a consequence of Cor. 7.2, Lemma 7.1, and Lemma 4.2, and will be formally established in the next section. If the test fails, then by Theorem 6.1, Γ ⊢ t = t′ : C cannot be true.

It remains to show that our algorithmic equality is also a decision procedure. In the next section, we demonstrate that \overline{t} ≃ \overline{t}′ implies t↓ ∼ t′↓, which means that both t and t′ weak head normalize and these normal forms are algorithmically equal. Then we have proven completeness of the algorithmic equality.

7. Completeness

In this section, we show completeness of the algorithmic presentation of MLF_{Σ} by relating it to the term model of the last section.

7.1. A Transitive Extension of Algorithmic Equality

To relate the η-equality on β-normal forms ≃ to the algorithmic equality ∼, we first present a transitive extension ∼^{+} of the algorithmic equality which is conservative for terms of the same type. We then show that this extension ∼^{+} is equivalent to ≃. Since ≃ has been shown complete through the PER model, the algorithmic equality is also complete for terms of the same type.

Algorithmic equality, restated. We recapitulate the rules of algorithmic equality, this time without use of active elimination @.

Rules for neutral terms:

aq-c \overline{c ∼ c}  aq-var \overline{x ∼ x}

aq-ne-fun \frac{n ∼ n′  s↓ ∼ s′↓}{n s ∼ n′ s′}  aq-ne-pair \frac{n ∼ n′}{n p ∼ n′ p}

The following three rules are a synonym for aq-ext-fun .

aq-ext-fun-fun  \frac{t↓ ∼ t′↓}{λxt ∼ λxt′}

aq-ext-fun-ne \frac{t↓ ∼ n x}{λxt ∼ n} x ∉ FV(n) aq-ext-ne-fun \frac{n x ∼ t↓}{n ∼ λxt} x ∉ FV(n)

And these three rules are a synonym for aq-ext-pair .

aq-ext-pair-pair  \frac{r↓ ∼ r′↓  s↓ ∼ s′↓}{(r, s) ∼ (r′, s′)}

aq-ext-pair-ne \frac{r↓ ∼ n L  s↓ ∼ n R}{(r, s) ∼ n}  aq-ext-ne-pair \frac{n L ∼ r↓  n R ∼ s↓}{n ∼ (r, s)}

A transitive extension. Let w ∼^{+} w′ be given by the rules for algorithmic equality plus the following two:

aq^{+}-fun-pair \frac{t↓ ∼^{+} n x  n L ∼^{+} r↓  n R ∼^{+} s↓}{λxt ∼^{+} (r, s)} x ∉ FV(n)

aq^{+}-pair-fun \frac{r↓ ∼^{+} n L  s↓ ∼^{+} n R  n x ∼^{+} t↓}{(r, s) ∼^{+} λxt} x ∉ FV(n)

These rules destroy the algorithmic character, since the neutral term n has to be guessed if one reads the rules from bottom to top as in logic programming.

Lemma 7.1. (The extension ∼^{+} is conservative for same-typed terms) 1. If D :: n ∼^{+} n′ and Γ ⊢ n : C and Γ ⊢ n′ : C′ then n ∼ n′ and Γ ⊢ C = C′ :Type.

2. If D :: w ∼^{+} w′ and Γ ⊢ w, w′ : C then w ∼ w′.

3. If t↓ ∼^{+} t′↓ and Γ ⊢ t, t′ : C then t↓ ∼ t′↓.

Proof: The third proposition is a direct consequence of the second, using subject reduction for weak head evaluation which is implied by its soundness (Lemma 4.1) together with syntactic validity (Theorem 2.1). The first two propositions are proven simultaneously by induction on D. The requirement of being of the same type in (2.) prevents D from applying rules aq^{+}-fun-pair and aq^{+}-pair-fun . Hence D contains only the counterparts of the rules for the algorithmic equality. The most interesting case is the following one:

aq^{+}-ne-fun \frac{n ∼^{+} n′  s↓ ∼^{+} s′↓}{n s ∼^{+} n′ s′}

Γ ⊢ n s : C  hypothesis
Γ ⊢ n : Fun A (λxB)  &
Γ ⊢ s : A  &
Γ ⊢ B[s/x] = C :Type  inversion
Γ ⊢ n′ s′ : C′  hypothesis
Γ ⊢ n′ : Fun A′ (λxB′)  &
Γ ⊢ s′ : A′  &
Γ ⊢ B′[s′/x] = C′ :Type  inversion
n ∼ n′  &
Γ ⊢ Fun A (λxB) = Fun A′ (λxB′) :Type  first ind. hyp.
Γ ⊢ A = A′ :Type  injectivity
Γ ⊢ s′ : A  symmetry, rule conv
s↓ ∼ s′↓  second ind. hyp. (3.)
n s ∼ n′ s′  rule aq-ne-fun
Γ ⊢ s = s′ : A  soundness of algorithmic equality
Γ, x:A ⊢ B = B′ :Type  injectivity
Γ ⊢ B[s/x] = B′[s′/x] :Type  functionality
Γ ⊢ C = C′ :Type  transitivity, symmetry

⊓ ⊔

As a consequence, the algorithmic equality is transitive for terms of the same type, provided ∼^{+} is indeed transitive. This claim will be validated through equivalence with the transitive ≃.

7.2. Soundness of the Extended Algorithmic Equality

In this section, we show that the extended algorithmic equality ∼^{+} is sound w. r. t. the model equality ≃. Together with the dual result of the next section we establish equivalence of these two notions of equality. As a byproduct, we obtain transitivity of ∼^{+}, which we will later also obtain directly (see Section 8). However, for the completeness of the algorithmic equality, which is the main theme of this article, the soundness result of this section is not relevant.

Lemma 7.2. (Soundness of weak head evaluation w. r. t. β-equality) If t ↘ w then t =_{β} w.

Lemma 7.3. (Soundness of ∼^{+} w. r. t. ≃) If D :: w ∼^{+} w′ then w ≃ w′.

Proof: By induction on D, using the previous lemma. All cases are easy, for example:

• Case

aq^{+}-ne-fun \frac{n ∼^{+} n′  s↓ ∼^{+} s′↓}{n s ∼^{+} n′ s′}

By induction hypothesis, n =_{β} u =_{η} u′ =_{β} n′ and s =_{β} v =_{η} v′ =_{β} s′. Thus, n s =_{β} u v =_{η} u′ v′ =_{β} n′ s′.

• Case

aq^{+}-ext-fun-ne \frac{t↓ ∼^{+} n x}{λxt ∼^{+} n} x ∉ FV(n)

By assumption t ↘ w and by induction hypothesis w ≃ n x. Together with the previous lemma, t =_{β} w =_{β} v =_{η} u x =_{β} n x, hence, λxt =_{β} λxv =_{η} λx. u x =_{η} u =_{β} n.

• Case

aq^{+}-fun-pair \frac{t↓ ∼^{+} n x  n L ∼^{+} r↓  n R ∼^{+} s↓}{λxt ∼^{+} (r, s)} x ∉ FV(n)

By the previous lemma and induction hypothesis, t =_{β} v =_{η} u x =_{β} n x, hence, λxv =_{η} λx. u x =_{η} u. Further, n L =_{β} u L =_{η} v_{1} =_{β} r and n R =_{β} u R =_{η} v_{2} =_{β} s, thus, u =_{η} (u L, u R) =_{η} (v_{1}, v_{2}). Together, λxt =_{β} λxv =_{η} (v_{1}, v_{2}) =_{β} (r, s).

⊓ ⊔

Corollary 7.1. If t↓ ∼^{+} t↓ then t is β-normalizable.

7.3. Completeness of the Extended Algorithmic Equality

In the following, we demonstrate that two terms t ≃ t′ that are related in the term-PER model are also related by the extended algorithmic equality.

Lemma 7.4. (Completeness of ∼^{+} on β-normal forms) If v =_{η} v′ then v ∼^{+} v′.

For the proof we need an induction measure | · | on terms which is compatible with the subterm ordering and gives extra weight to introductions, such that |λxr| + |t| > |r| + |t x| and |(r, s)| + |t| > |r| + |t L|. These conditions are also met by Goguen’s [14] measure for proving termination of Coquand’s [8] algorithmic equality restricted to pure λ-terms. But we need the extra conditions |λxt| > 2|t| and both |(r, s)| > 2|r| and |(r, s)| > 2|s|.

\begin{aligned}|x| & := & |c| := 1 \\ |r s| & := & |r| + |s| \\ |r p| & := & |r| + 1 \\ |λxt| & := & 2|t| + 1 \\ |(r, s)| & := & 2|r| + 2|s| \end{aligned}

Observe that the conditions are met since |t| ≥ 1 for all terms t. This measure is compatible with η-reduction, i. e., if v ⟶_{η} v′ then |v| > |v′|.

Proof: Lemma 7.4 is proved by induction on |v| + |v′|. We first treat the cases for neutral terms u =_{η} u′.

• Case u ≡ c. Then u′ ≡ c by Cor. 6.1 and c ∼^{+} c.

• Case u ≡ x. Similar.

• Case u ≡ u_{1} v_{1}. Then by Cor. 6.1 u′ ≡ u_{2} v_{2} with u_{1} =_{η} u_{2} and v_{1} =_{η} v_{2}. By induction hypothesis u_{1} ∼^{+} u_{2} and v_{1} ∼^{+} v_{2}, hence u ∼^{+} u′ by aq^{+}-ne-fun .

• Case u ≡ u_{1} p. Similar.

Now we look at the general form v =_{η} v′, where we omit symmetrical cases.

• Case λxv =_{η} u. By Cor. 6.1, v =_{η} u x. Since |v| + |u x| = |v| + |u| + 1 < (2|v| + 1) + |u| = |λxv| + |u|, we can apply the induction hypothesis and obtain v ∼^{+} u x. Thus λxv ∼^{+} u by aq^{+}-ext-fun-ne .

• Case λxv =_{η} λxv′. By Cor. 6.1, v =_{η} v′, on which we apply the induction hypothesis and aq^{+}-ext-fun-fun .

• Case λxv =_{η} (v_{1}, v_{2}). By Cor. 6.1 there exists a neutral u such that v ⟶_{η}^{∗} u x and both u L _{η}^{∗}⟵ v_{1} and u R _{η}^{∗}⟵ v_{2}. Since reduction is compatible with the measure, we have |v| + |u x| ≤ 2|v| < 2|v| + 1 = |λxv| and can apply the induction hypothesis to obtain v ∼^{+} u x. Further, we have |u L| + |v_{1}| ≤ 2|v_{1}| < 2|v_{1}| + 2|v_{2}| = |(v_{1}, v_{2})|, thus, by induction hypothesis, u L ∼^{+} v_{1}, and similarly, u R ∼^{+} v_{2}. By aq^{+}-fun-pair we get λxv ∼^{+} (v_{1}, v_{2}).

38 A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing

• Case (v_{1}, v_{2}) =_{η} u. By Cor. 6.1, v_{1} =_{η} u L and v_{2} =_{η} u R. Since |v_{1}| + |u L| = |v_{1}| + |u| + 1 < 2(|v_{1}| + |v_{2}|) + |u| = |(v_{1}, v_{2})| + |u|, by induction hypothesis, v_{1} ∼^{+} u L, and with a similar calculation, v_{2} ∼^{+} u R. Thus, (v_{1}, v_{2}) ∼^{+} u by aq^{+}-ext-pair-ne .

• Case (v_{1}, v_{2}) =_{η} (v′_{1}, v′_{2}). By inversion, induction hypothesis, and rule aq^{+}-ext-pair-pair . ⊓ ⊔

Remark 7.1. (Alternative proof) First, show reflexivity v ∼^{+} v for all β-normal forms v by induction on v. Then prove that ∼^{+} is closed under η-expansion. More precisely, show that

1. u ⟶_{η} u′ and D :: u′ e⃗ ∼^{+} v imply u e⃗ ∼^{+} v for a vector of eliminations e⃗, and

2. v_{1} ⟶_{η} v_{2} and D :: v_{2} ∼^{+} v_{3} imply v_{1} ∼^{+} v_{3}

simultaneously by induction on D. For reasons of symmetry, ∼^{+} is also closed by η-expansion on the right hand side. Finally, assuming v_{1} ⟶_{η}^{∗} v_{2} _{η}^{∗}⟵ v_{3} we can show v_{1} ∼^{+} v_{3} from v_{2} ∼^{+} v_{2} by induction on the number of reduction steps.

Lemma 7.5. (Standardization) 1. If t =_{β} x then t ↘ x. If t =_{β} c then t ↘ c.

2. If t =_{β} n s then t ↘ n′ s′ with n =_{β} n′ and s =_{β} s′.

3. If t =_{β} n p then t ↘ n′ p with n =_{β} n′.

4. If t =_{β} λxr then t ↘ λxr′ with r =_{β} r′.

5. If t =_{β} (r, s) then t ↘ (r′, s′) with r =_{β} r′ and s =_{β} s′. Proof: Fact about the λ-calculus [6]. ⊓ ⊔

Lemma 7.6. (From normal to normalizing terms) 1. If n =_{β} u and n′ =_{β} u′ and D :: u ∼^{+} u′, then n ∼^{+} n′.

2. If t =_{β} v and t′ =_{β} v′ and D :: v ∼^{+} v′, then t↓ ∼^{+} t′↓.

Proof: Simultaneously by induction on D, using standardization.

• Case n =_{β} u v and n′ =_{β} u′ v′ and

aq^{+}-ne-fun \frac{u ∼^{+} u′  v ∼^{+} v′}{u v ∼^{+} u′ v′}

A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing 39

n ≡ n_{0} s with n_{0} =_{β} u and s =_{β} v  neutral n ⟶_{β}^{∗} u v application
n′ ≡ n′_{0} s′ with n′_{0} =_{β} u′ and s′ =_{β} v′  neutral n′ ⟶_{β}^{∗} u′ v′ application
n_{0} ∼^{+} n′_{0}  first ind. hyp.
s↓ ∼^{+} s′↓  second ind. hyp.
n_{0} s ∼^{+} n′_{0} s′  aq^{+}-ne-fun

• Case t =_{β} λxv and t′ =_{β} u and

aq^{+}-ext-fun-ne \frac{v ∼^{+} u x}{λxv ∼^{+} u} x ∉ FV(u)
t ↘ λxr with r =_{β} v  standardization
t′ ↘ n with n =_{β} u  standardization
x ∉ FV(n)  renaming
n x =_{β} u x  =_{β} is a congruence
r↓ ∼^{+} n x  induction hypothesis
λxr ∼^{+} n  aq^{+}-ext-fun-ne

• Case t =_{β} λxv and t′ =_{β} (v_{1}, v_{2}) and

aq^{+}-fun-pair \frac{v ∼^{+} u x  u L ∼^{+} v_{1}  u R ∼^{+} v_{2}}{λxv ∼^{+} (v_{1}, v_{2})} x ∉ FV(u)
t ↘ λxr with r =_{β} v  standardization
t′ ↘ (r_{1}, r_{2}) with r_{1} =_{β} v_{1} and r_{2} =_{β} v_{2}  standardization
r↓ ∼^{+} u x and u L ∼^{+} r_{1}↓ and u R ∼^{+} r_{2}↓  induction hypotheses
λxr ∼^{+} (r_{1}, r_{2})  aq^{+}-fun-pair
⊓ ⊔

Corollary 7.2. (Completeness of ∼^{+}) If t ≃ t′ then t↓ ∼^{+} t′↓. Proof: By assumption t =_{β} v =_{η} v′ =_{β} t′. First v ∼^{+} v′ by Lemma 7.4, then also t↓ ∼^{+} t′↓ by Lemma 7.6. ⊓ ⊔ Corollary 7.3. If t is β-normalizable, then t↓ ∼^{+} t↓.

Together with Cor. 7.1 we see that the diagonal of extended algorithmic equality—which coincides with the diagonal of pure algorithmic equality—characterizes the weakly normalizing terms t. Here, we consider a term weakly normalizing if is has a junk-free normal form v, which excludes β-normal forms like (λxx) L or (x, y) z. We define w ∈ WN :⟺ w ∼^{+} w and t ∈ WN :⟺ t ↘ w ∈ WN. Let us specialize the rules of algorithmic equality to WN:

\overline{c ∈ WN}  \overline{x ∈ WN}  \frac{n ∈ WN  s ∈ WN}{n s ∈ WN}  \frac{n ∈ WN}{n p ∈ WN}

\frac{r ∈ WN}{λxr ∈ WN}  \frac{r ∈ WN  s ∈ WN}{(r, s) ∈ WN}  \frac{t ↘ w  w ∈ WN}{t ∈ WN}

This predicate corresponds to Joachimski and Matthes’ [18] inductive characterization of weakly normalizing λ-terms. (Only that they use weak head reduction instead of weak head evaluation.)^{3}

7.4. Completeness of Algorithmic Equality

Now we can assemble the pieces of the jigsaw puzzle.

Theorem 7.1. (Completeness of algorithmic equality) 1. If Γ ⊢ t = t′ : C then t↓ ∼ t′↓.

2. If D :: Γ ⊢ A = A′ :Type then A ∼ A′.

Proof: Completeness for terms (1): By Theorem 6.1 we have \overline{t} ≃ \overline{t}′, which entails t↓ ∼^{+} t′↓ by Cor. 7.2. Since Γ ⊢ t, t′ : C, we infer t↓ ∼ t′↓ by Lemma 7.1. The completeness for types (2) is then shown by induction on D, using completeness for terms in case eq-set-e . ⊓ ⊔

8. A Shortcut: Disposing of η-Reduction

In sections 7.2 and 7.3 we have shown that the extended algorithmic equality ∼^{+} is equivalent to ηequality on β-normal forms. Hence, we could define more directly \overline{v} ≃ \overline{v′} iff v ∼^{+} v′. The requirement safe-ext-fun is simply fulfilled by the admissible rule

aq^{+}-ext-fun \frac{w_{f}@x ∼^{+} w′_{f}@x}{w_{f} ∼^{+} w′_{f}} x ∉ FV(w_{f}, w′_{f}),

and safe-ext-pair by a similar admissible rule aq^{+}-ext-pair . It remains to show—without reference to =_{η}—that ∼^{+} is transitive. We dedicate the remainder of this section to that task.

Let #D ≥ 1 denote the following measure on derivations D :: w ∼^{+} w′:

#aq^{+}-fun-pair (D_{1}, D_{21}, D_{22}) = 1 + #D_{1} + max(#D_{21}, #D_{22})
#aq^{+}-pair-fun (D_{11}, D_{12}, D_{2}) = 1 + max(#D_{11}, #D_{12}) + #D_{2}
#r(D_{1}, …, D_{n})  = 1 + max{#D_{i} | 1 ≤ i ≤ n}

3The inductive characterization originates from van Raamsdonk et. al. [24].

Here, r stands for any other rule application, or more precisely, a rule which has a counterpart in the original algorithmic equality judgement w ∼ w′. Hence, #D is just the height of derivation D if D corresponds to a derivation of w ∼ w′. Since rule aq^{+}-fun-pair stands for a pair of derivations D_{1} :: λxt ∼ n and D_{2} :: n ∼ (r, s), its weight is derived for the sum of the weight of these derivations; and similarly for aq^{+}-pair-fun .

Lemma 8.1. (∼^{+} is transitive) Let e⃗ be a possibly empty list of eliminations.

1. If D_{1} :: n ∼^{+} w and D_{2} :: w ∼^{+} n′ then E :: n ∼^{+} n′.

2. If D_{1} :: w ∼^{+} n e⃗ and D_{2} :: n ∼^{+} n′ then E :: w ∼^{+} n′ e⃗.

3. If D_{1} :: n ∼^{+} n′ and D_{2} :: n′ e⃗ ∼^{+} w then E :: n e⃗ ∼^{+} w.

4. If D_{1} :: w_{1} ∼^{+} w_{2} and D_{2} :: w_{2} ∼^{+} w_{3} then E :: w_{1} ∼^{+} w_{3}.

In all cases, #E < #D_{1} + #D_{2}.

Proof: Simultaneously by induction on #D_{1} + #D_{2}. In the remainder of this proof, leave # implicit. First, we prove (1):

• Case D_{1}, D_{2} :: x ∼^{+} x. Then E :: x ∼^{+} x with 1 = E < D_{1} + D_{2} = 2.

• Case

D_{1} = \frac{\begin{matrix}D_{11} \\ n_{1} ∼^{+} n_{2} \end{matrix}  \begin{matrix}D_{12} \\ s_{1}↓ ∼^{+} s_{2}↓ \end{matrix}}{n_{1} s_{1} ∼^{+} n_{2} s_{2}}  D_{2} = \frac{\begin{matrix}D_{21} \\ n_{2} ∼^{+} n_{3} \end{matrix}  \begin{matrix}D_{22} \\ s_{2}↓ ∼^{+} s_{3}↓ \end{matrix}}{n_{2} s_{2} ∼^{+} n_{3} s_{3}}

E_{1} :: n_{1} ∼^{+} n_{3}  E_{1} < D_{11} + D_{21} < D_{1} + D_{2} − 1  first ind. hyp.
E_{2} :: s_{1}↓ ∼^{+} s_{3}↓  E_{2} < D_{12} + D_{22} < D_{1} + D_{2} − 1  second ind. hyp.
E :: n_{1} s_{1}↓ ∼^{+} n_{3} s_{3}↓  E = max(E_{1}, E_{2}) + 1 < D_{1} + D_{2}  aq^{+}-ne-fun

• Case n_{1} p ∼^{+} n_{2} p and n_{2} p ∼^{+} n_{3} p: Similarly.

• Case

D_{1} = \frac{\begin{matrix}D′_{1} \\ n x ∼^{+} t↓ \end{matrix}}{n ∼^{+} λxt} x ∉ FV(n) D_{2} = \frac{\begin{matrix}D′_{2} \\ t↓ ∼^{+} n′ x \end{matrix}}{λxt ∼^{+} n′} x ∉ FV(n′)

E′ :: n x ∼^{+} n′ x  E′ < D′_{1} + D′_{2}  ind. hyp.
E :: n ∼^{+} n′  E < E′ < D_{1} + D_{2}  inversion

• Case

D_{1} = \frac{\begin{matrix}D_{11} \\ n L ∼^{+} r↓ \end{matrix}  \begin{matrix}D_{12} \\ n R ∼^{+} s↓ \end{matrix}}{n ∼^{+} (r, s)}  D_{2} = \frac{\begin{matrix}D_{21} \\ r↓ ∼^{+} n′ L \end{matrix}  \begin{matrix}D_{22} \\ s↓ ∼^{+} n′ R \end{matrix}}{(r, s) ∼^{+} n′}
E_{1} :: n L ∼^{+} n′ L  E_{1} < D_{11} + D_{21}  ind. hyp.
E :: n ∼^{+} n′  E < E_{1} < D_{1} + D_{2}  inversion

For (2), consider the cases:

• Case w is neutral and e⃗ is empty: By (1).

• Case w = n_{0} s_{0} and

D_{1} = \frac{\begin{matrix}D_{11} \\ n_{0} ∼^{+} n e⃗ \end{matrix}  \begin{matrix}D_{12} \\ s_{0}↓ ∼^{+} s↓ \end{matrix}}{n_{0} s_{0} ∼^{+} n e⃗ s}  \begin{matrix}D_{2} \\ n ∼^{+} n′ \end{matrix}
E′ :: n_{0} ∼^{+} n′ e⃗  E′ < D_{11} + D_{2}  ind. hyp. (D_{11} + D_{2} < D_{1} + D_{2})
E :: n_{0} s_{0} ∼^{+} n′ e⃗ s E = 1 + max(E′, D_{12}) < D_{1} + D_{2}  aq^{+}-ne-fun

• Case w = n_{0} p similar.

• Case w = λxt and

D_{1} = \frac{\begin{matrix}D′_{1} \\ t↓ ∼^{+} n e⃗ x \end{matrix}}{λxt ∼^{+} n e⃗} \begin{matrix}D_{2} \\ n ∼^{+} n′ \end{matrix}

E′ :: t↓ ∼^{+} n′ e⃗ x  E′ < D′_{1} + D_{2}  ind. hyp.
E :: λxt ∼^{+} n′ e⃗  E < D′_{1} + D_{2} + 1 = D_{1} + D_{2}  aq^{+}-ext-fun-ne

• Case

D_{1} = \frac{\begin{matrix}D_{11} \\ r↓ ∼^{+} n e⃗ L \end{matrix}  \begin{matrix}D_{12} \\ s↓ ∼^{+} n e⃗ R \end{matrix}}{(r, s) ∼^{+} n e⃗}  \begin{matrix}D_{2} \\ n ∼^{+} n′ \end{matrix}

A. Abel and T. Coquand / Algorithmic Equality with Surjective Pairing 43

E_{1} :: r↓ ∼^{+} n′ e⃗ L  E_{1} < D_{11} + D_{2}  ind. hyp.
E_{2} :: s↓ ∼^{+} n′ e⃗ R  E_{2} < D_{12} + D_{2}  ind. hyp.
E :: (r, s) ∼^{+} n′ e⃗  E = 1 + max(E_{1}, E_{2}) < D_{1} + D_{2}  aq^{+}-ext-pair-ne

Statement (3) is symmetrical to (2) and can be proven analogously. For (4), all of the following cases are easy:

• Case λxt ∼^{+} n and n ∼^{+} λxt′.

• Case λxt ∼^{+} λxt′ and λxt′ ∼^{+} n (plus symmetrical case).

• Case λxt_{1} ∼^{+} λxt_{2} and λxt_{2} ∼^{+} λxt_{3}.

• Case (r, s) ∼^{+} n and n ∼^{+} (r′, s′).

• Case (r, s) ∼^{+} (r′, s′) and (r′, s′) ∼^{+} n (plus symmetrical case).

• Case (r_{1}, s_{1}) ∼^{+} (r_{2}, s_{2}) and (r_{2}, s_{2}) ∼^{+} (r_{3}, s_{3}).

The following cases introduce a relation between a function and a pair.

• Case

D_{1} = \frac{\begin{matrix}D′_{1} \\ t↓ ∼^{+} n x \end{matrix}}{λxt ∼^{+} n} x ∉ FV(n)  D_{2} = \frac{\begin{matrix}D_{21} \\ n L ∼^{+} r↓ \end{matrix}  \begin{matrix}D_{22} \\ n R ∼^{+} s↓ \end{matrix}}{n ∼^{+} (r, s)}

E :: λxt ∼^{+} (r, s) by aq^{+}-fun-pair . E = 1 + D′_{1} + max(D_{21}, D_{22}) < D_{1} + D_{2}.

• Case (r, s) ∼^{+} n and n ∼^{+} λxt. Symmetrical. The remaining cases eliminate a relation between a function and a pair. We only spell out these cases where the second relation is of this kind, the other cases are done analogously.

• Case (x ∉ FV(n, n′))

D_{1} = \frac{\begin{matrix}D′_{1} \\ n x ∼^{+} t↓ \end{matrix}}{n ∼^{+} λxt}  D_{2} = \frac{\begin{matrix}D′_{2} \\ t↓ ∼^{+} n′ x \end{matrix}  \begin{matrix}D′_{3} \\ n′ L ∼^{+} r↓ \end{matrix}  \begin{matrix}D′_{4} \\ n′ R ∼^{+} s↓ \end{matrix}}{λxt ∼^{+} (r, s)}

E_{1} :: n x ∼^{+} n′ x  E_{1} < D′_{1} + D′_{2}  ind.hyp. onD′_{1}, D′_{2}
E_{2} :: n ∼^{+} n′  1 + E_{2} < D′_{1} + D′_{2}  inversion on E_{1}
E_{3} :: n L ∼^{+} n′ L  E_{3} < D′_{1} + D′_{2}  aq^{+}-ne-pair
E_{4} :: n R ∼^{+} n′ R  E_{4} < D′_{1} + D′_{2}  aq^{+}-ne-pair
E_{5} :: n L ∼^{+} r↓  E_{5} < E_{3} + D′_{3} < D_{1} + D_{2}  ind.hyp. onE_{3}, D′_{3}
E_{6} :: n R ∼^{+} s↓  E_{6} < E_{4} + D′_{4} < D_{1} + D_{2}  ind.hyp. onE_{4}, D′_{4}
E :: n ∼^{+} (r, s)  E = 1 + max(E_{5}, E_{6}) < D_{1} + D_{2}  aq^{+}-ext-ne-pair

• Case (x ∉ FV(n, n′))

D_{1} = \frac{\begin{matrix}D′_{1} \\ t↓ ∼^{+} t′↓ \end{matrix}}{λxt ∼^{+} λxt′}  D_{2} = \frac{\begin{matrix}D_{21} \\ t′↓ ∼^{+} n′ x \end{matrix}  \begin{matrix}D_{22} \\ n′ L ∼^{+} r↓ \end{matrix}  \begin{matrix}D_{23} \\ n′ R ∼^{+} s↓ \end{matrix}}{λxt′ ∼^{+} (r, s)}

E′ :: t↓ ∼^{+} n′ x  E′ < D′_{1} + D_{21}  ind.hyp. onD′_{1}, D_{21}
E :: λxt ∼^{+} (r, s)  E = 1 + E′ + max(D_{22}, D_{23}) < D_{1} + D_{2}  aq^{+}-fun-pair

• Case

D_{1} = \frac{\begin{matrix}D_{11} \\ r↓ ∼^{+} n L \end{matrix}  \begin{matrix}D_{12} \\ s↓ ∼^{+} n R \end{matrix}  \begin{matrix}D_{13} \\ n x ∼^{+} t↓ \end{matrix}}{(r, s) ∼^{+} λxt} x ∉ FV(n)

D_{2} = \frac{\begin{matrix}D_{21} \\ t↓ ∼^{+} n′ x \end{matrix}  \begin{matrix}D_{22} \\ n′ L ∼^{+} r′↓ \end{matrix}  \begin{matrix}D_{23} \\ n′ R ∼^{+} s′↓ \end{matrix}}{λxt ∼^{+} (r′, s′)} x ∉ FV(n′)

E_{1} :: n x ∼^{+} n′ x  E_{1} < D_{13} + D_{21}  ind. hyp.
E_{2} :: n L ∼^{+} n′ L  E_{2} < D_{13} + D_{21}  inversion
E_{3} :: n R ∼^{+} n′ R  E_{3} < D_{13} + D_{21}  inversion
E_{4} :: r↓ ∼^{+} n′ L  E_{4} < D_{11} + E_{2} < D_{11} + D_{13} + D_{21}  ind. hyp.
E_{5} :: s↓ ∼^{+} n′ R  E_{5} < D_{12} + E_{3} < D_{12} + D_{13} + D_{21}  ind. hyp.
E_{6} :: r↓ ∼^{+} r′↓  E_{6} < E_{4} + D_{22} < D_{11} + D_{13} + D_{21} + D_{22}  ind. hyp.
E_{7} :: s↓ ∼^{+} s′↓  E_{7} < E_{5} + D_{23} < D_{12} + D_{13} + D_{21} + D_{23}  ind. hyp.
E :: (r, s) ∼^{+} (r′, s′)  E = 1 + max(E_{6}, E_{7}) < D_{1} + D_{2}  aq^{+}-ext-pair-pair

We have three cases left, which can be proven similarly to the previous ones.

• Case n ∼^{+} (r, s) and (r, s) ∼^{+} λxt.

• Case (r, s) ∼^{+} (r′, s′) and (r′, s′) ∼^{+} λxt.

• Case λxt ∼^{+} (r, s) and (r, s) ∼^{+} λxt′.

⊓ ⊔

9. Decidability

By completeness of algorithmic equality, every well-typed term is weakly normalizing (Cor. 7.1). On weakly normalizing terms, the equality algorithm terminates, as we will see in this section.

9.1. Decidability of Equality

We have shown that two judgmentally equal terms t, t′ weak-head normalize to w, w′ and there exists a derivation of w ∼ w′, hence, the equality algorithm, which searches deterministically for such a derivation, terminates with success. What remains to show is that the query t↓ ∼ t′↓ terminates for all well-typed t, t′, either with success, if the derivation can be closed, or with failure, in case the search arrives at a point where there is no matching rule.

For a derivation D of algorithmic equality, we define the measure |D| which denotes the number of rule applications on the longest branch of D, counting the rules aq-ext-fun and aq-ext-pair twice.^{4}

Lemma 9.1. (Termination of equality) If D_{1} :: w_{1} ∼ w_{1} and D_{2} :: w_{2} ∼ w_{2} then the query w_{1} ∼ w_{2} terminates.

Proof: By induction on |D_{1}| + |D_{2}|. There are many cases to consider. First we consider neutral w_{1}, w_{2}, for instance:

4A similar measure is used by Goguen [14] to prove termination of algorithmic equality restricted to pure λ-terms [8].

• Case: w_{1} ≡ x and w_{2} ≡ n_{2} s_{2}. Since there is no rule with a conclusion of the shape x ∼ n_{2} s_{2}, the query fails.

• Case: w_{1} ≡ n_{1} s_{1} and w_{2} ≡ n_{2} s_{2}. Rule aq-ne-fun matches. By the first induction hypothesis, n_{1} ∼ n_{1} and n_{2} ∼ n_{2}, hence, the subquery n_{1} ∼ n_{2} terminates. Since by the second induction hypothesis, s_{1} ↘ w′_{1}, s_{2} ↘ w′_{2}, w′_{1} ∼ w′_{1}, and w′_{2} ∼ w′_{2}, the subquery w′_{1} ∼ w′_{2} terminates as well. Hence, the whole query terminates.

The other neutral cases work similarly. Let us consider some cases where at least one of the weak head normal forms is not neutral.

• Case w_{1} ≡ λxr and w_{2} ≡ (t, t′). There is no matching rule, the query fails.

• Case w_{1} ≡ n and w_{2} ≡ (t, t′). Rule aq-ext-pair matches. We apply the induction hypothesis to the derivations D̂_{1} :: n L ∼ n L and D′_{2} :: t↓ ∼ t↓, which is legal since |D_{1}| + |D_{2}| ≥ |D_{1}| + |D′_{2}| + 2 > (|D_{1}| + 1) + |D′_{2}| = |D̂_{1}| + |D′_{2}|. Hence, the first subquery n L ∼ t↓ terminates, and, by a similar argument, also the second subquery n R ∼ t′↓.

• Case w_{1} ≡ n and w_{2} ≡ λxr. Rule aq-ext-fun matches. Since x ∼ x is a derivation of height one, we can apply the induction hypothesis, with justification similar to the last case, on the only subquery n x ∼ r↓.

⊓ ⊔

Theorem 9.1. (Decidability of equality) If Γ ⊢ t, t′ : C then the query t↓ ∼ t′↓ succeeds or fails finitely and decides Γ ⊢ t = t′ : C.

Proof: By Theorem 7.1, t ↘ w, t′ ↘ w′, w ∼ w, and w′ ∼ w′. By the previous lemma, the query w ∼ w′ terminates. Since by soundness and completeness of the algorithmic equality, w ∼ w′ if and only if Γ ⊢ t = t′ : C, the query decides judgmental equality. ⊓ ⊔

Corollary 9.1. (Decidability of type equality) If D :: Γ ⊢ A : Type and Γ ⊢ A′ : Type then the query A ∼ A′ succeeds or fails finitely and decides Γ ⊢ A = A′ :Type.

Proof: By induction on D, using the theorem in case A = El t. ⊓ ⊔

9.2. Termination of Type Checking

The termination of the type checker is a consequence of termination of equality for well-typed objects.

Lemma 9.2. (Termination of type checking) Let Γ ⊢ ok.

1. The query Γ ⊢ t ⇓ ? terminates (? ≢Type).

2. If Γ ⊢ C :Type then the query Γ ⊢ t ⇑ C terminates.

Proof: Simultaneously by induction on t. The inference succeeds directly in case t ≡ x with rule inf-var , and fails immediately in case t ≡ c, t ≡ λxr, or t ≡ (t_{1}, t_{2}). We consider t ≡ r s. Then rule inf-fun-e matches.

inf-fun-e \frac{Γ ⊢ r ⇓ Fun A (λxB)  Γ ⊢ s ⇑ A}{Γ ⊢ r s ⇓ B[s/x]}
query Γ ⊢ r ⇓ ? terminates  induction hypothesis
Γ ⊢ r ⇓ C  &
C ≡ Fun A (λxB)  otherwise fail
Γ ⊢ r : Fun A (λxB)  inference sound (Thm. 4.1)
Γ ⊢ Fun A (λxB) :Type  syntactic validity
Γ ⊢ A :Type  inversion
query Γ ⊢ s ⇑ A terminates  induction hypothesis
Γ ⊢ s ⇑ A  otherwise fail
Γ ⊢ s : A  checking sound (Thm. 4.1)
Γ, x:A ⊢ B :Type  inversion
Γ ⊢ B[s/x] :Type  substitution (Lemma 2.7)

Γ ⊢ r s ⇓ B[s/x], query successful

The remaining case t ≡ r p is treated analogously. For the termination of checking, let us start with case t ≡ (t_{1}, t_{2}), where rule chk-pair-i matches.

chk-pair-i \frac{Γ ⊢ t_{1} ⇑ A  Γ ⊢ t_{2} ⇑ B[t_{1}/x]}{Γ ⊢ (t_{1}, t_{2}) ⇑ Pair A (λxB)}

Using the induction hypotheses, we basically need to show that Γ ⊢ B[t_{1}/x] : Type if Γ ⊢ t_{1} ⇑ A succeeds. The case t ≡ λxr matches rule chk-fun-i and is treated similarly. In the remaining cases, rule chk-inf fires.

chk-inf \frac{Γ ⊢ r ⇓ A  A ∼ C}{Γ ⊢ r ⇑ C}

By induction hypothesis, the inference algorithm terminates. If Γ ⊢ r ⇓ A then Γ ⊢ A :Type, hence the equality check terminates by Lemma 9.1, which implies termination of the type checker. ⊓ ⊔

Lemma 9.3. (Termination of type well-formedness) If Γ ⊢ ok then the query Γ ⊢ A ⇓Type terminates.

Proof: By induction on A, using the previous lemma in case A ≡ El t. ⊓ ⊔

9.3. Completeness of Type Checking

Once we have solved the hard problem of deciding equality, the decidability of typing is easy, provided we restrict to normal terms.

Normal and neutral terms. We introduce two predicates t ⇑ (t is normal) and t ⇓ (t is additionally neutral).

\overline{c ⇓}  \overline{x ⇓}  \frac{r ⇓  s ⇑}{r s ⇓}  \frac{r ⇓}{r p ⇓}  \frac{r ⇓}{r ⇑}  \frac{t ⇑}{λxt ⇑}  \frac{r ⇑  s ⇑}{(r, s) ⇑}

Theorem 9.2. (Completeness of type checking) 1. If D :: t ⇓ and Γ ⊢ t : C then Γ ⊢ t ⇓ A and A ∼ C.

2. If D :: t ⇑ and Γ ⊢ t : C then Γ ⊢ t ⇑ C.

Proof: Simultaneously by induction on D. ⊓ ⊔

Corollary 9.2. (Completeness of type well-formedness) If D :: Γ ⊢ A :Type and A ⇓ then Γ ⊢ A ⇓Type.

Proof: By induction on D. In case A ≡ El t, the premise A ⇓ forces t ⇑, hence we can apply the previous theorem. ⊓ ⊔

Our bidirectional algorithm can only check β-normal terms; however, it can be extended to arbitrary terms by requiring type annotations in redexes [11, 2], some of which can also be inferred by suitable heuristics [23].

10. Conclusion

We have presented a sound and complete conversion algorithm for MLF_{Σ}. The completeness proof builds on PERs over untyped expressions, hence, we need—in contrast to Harper and Pfenning’s completeness proof for type-directed conversion [17]—no Kripke model and no notion of erasure, what we consider an arguably simpler procedure. We see in principle no obstacle to generalize our results to type theories with type definition by cases (large eliminations), whereas it is not clear how to treat them with a technique based on erasure.

The disadvantage of untyped conversion, compared to type-directed conversion, is that it cannot handle cases where the type of a term provides more information on equality than its shape, e. g., unit types, singleton types and signatures with manifest fields [10].

A more general proof of completeness? Our proof uses a λ-model with full β-equality thanks to the rule den-β . We had also considered a weaker model (without den-β and den-irr , but with den-fun-β and den-pair-β ) which only equates weakly convertible objects. Combined with extensional PERs this would have been the model closest to our algorithm. But due to the use of substitution in the declarative formulation, we could not show MLF_{Σ}’s rules to be valid in such a model. Whether it still can be done, remains an open question.

Related work. The second author, Pollack, and Takeyama [10] present a model for βη-equality for an extension of the logical framework by singleton types and signatures with manifest fields. Equality is tested by η-expansion, followed by β-normalization and syntactic comparison. In contrast to this work, no syntactic specification of the framework and no incremental conversion algorithm are given.

Schürmann and Sarnat [25] have been working on an extension of the Edinburgh Logical Framework (ELF) by Σ-types (LF_{Σ}), following Harper and Pfenning [17]. In comparison to MLF_{Σ}, syntactic validity (Theorem 2.1) and injectivity are non-trivial in their formulation of ELF. Robin Adams [4] has extended Harper and Pfenning’s algorithm to Luo’s logical framework (i. e., MLF with typed λ-abstraction) with Σ-types and unit.

Goguen [13] gives a typed operational semantics for Martin-Löf’s logical framework. An extension to Σ-types has to our knowledge not yet been considered. Recently, Goguen [14] has proven termination and completeness for both the type-directed [17] and the shape-directed equality [8] from the standard meta-theoretical properties (strong normalization, confluence, subject reduction, etc.) of the logical framework. He also proposes a method to check βη-equality for Σ- and singleton types by a sequence of full η-expansion followed by β-reduction [15].

Acknowledgments. We are grateful to Lionel Vaux whose clear presentation of models for this implicit calculus [27] provided a guideline for our model construction. Thanks to Ulf Norell for proof-reading an earlier version of this article. The first author is indebted to Frank Pfenning who taught him typedirected equality and bidirectional type-checking at Carnegie Mellon University in 2000, and to Carsten Schürmann for communication on LF_{Σ}. Thanks to the anonymous referees for their helpful comments on the draft version, especially to the one who spotted many small mistakes by rigorously checking our proofs.

APPENDIX.

A. Surjective Pairing Destroys Confluence

Klop [19, pp. 195–208] shows that the untyped λ-calculus with the reduction (r L, r R) ⟶ r, called surjective pairing, is not confluent (Church-Rosser). It is, however, locally confluent (weakly Church-Rosser), hence, because of Newman’s Lemma, only a term with an infinite reduction sequence can fail to be confluent. Klop provides the following example.

Θ := (λxλy. y (x x y)) (λxλy. y (x x y))  Turing’s fixed-point combinator
e := z  free variable (or the term Ω)
c := Θ (λcλa. e (a L, (c a) R))
a := Θ c

Since c t ⟶^{+} e (t L, (c t) R) and a ⟶^{+} c a, we can construct the following reduction sequences:

c a ⟶^{+} e (a L, (c a) R) ⟶^{+} e ((c a) L, (c a) R) ⟶^{+} e (c a)
c a ⟶^{+} c (c a) ⟶^{+} c (e (c a))

The end reducts of both sequences cannot be joined again.

Not that only the last step in both sequences was a surjective pairing reduction, all others were βsteps. Thus, the example refutes even confluence of the relation ⟶_{β}^{∗}⟶_{η}^{∗}.

Remark A.1. (η-postponement fails) Surjective pairing destroys also η-postponement. In the reduction sequence ((λxt) L, (λxt) R) s ⟶_{η} (λxt) s ⟶_{β} t[s/x], the β-redex is created by η-reduction and cannot be reduced first.

B. Alternative to Inductive-Recursive Definition

In section 5.2 we have defined intensional type equality V = V′ ∈ Type and type interpretation [V] simultaneously by induction-recursion. In the following, we give conventional definitions of the two concepts.

Type interpretation. Type interpretation [ ] ∈ D ⇀ Rel is a partial function specified by the following equations.

int-set-f  [Set] = Set
int-set-e  [El v] = Eℓ(v)
int-fun-f  [Fun V F] = Fun([V], v ↦ [F v])
int-pair-f  [Pair V F] = Pair([V], v ↦ [F v])

Lemma B.1. Type interpretation [ ] ∈ D ⇀ Rel is a well-defined partial function.

Proof: Well-definedness, i. e., that V = V′ implies [V] = [V′], follows by injectivity and pairwise distinctness of type constructors. The latter guarantees that we can define the type interpretation by pattern matching although D is not necessarily a free structure. For instance, in the absence of the inequality Set ≠ Fun V F (den-set-not-dep ), the defining equations of type interpretation could imply the inconsistency Set = Fun([V], v ↦ [F v]). Injectivity proves that, e. g., [Fun V F] = [Fun V′ F′] if Fun V F = Fun V′ F′, since then V = V′ and F = F′ by law den-dep-inj . ⊓ ⊔

Intensional type equality Type ∈ Rel is given inductively by the following rules. Note that rule tyeq-dep has an infinitary premise.

tyeq-set-f Set = Set ∈ Type tyeq-set-e

\frac{v = v′ ∈ Set}{El v = El v′ ∈ Type}

tyeq-dep \frac{V = V′ ∈ Type F v = F′ v′ ∈ Type for all (v, v′) ∈ [V]}{c V F = c V′ F′ ∈ Type} c ∈ \{Fun, Pair\}

In the last rule, if [V] is not defined, the quantification is to be read as empty. The name intensional type equality [10] shall distinguish it from the more extensional type equality given by [V] = [V′].

The next lemma proves the following: For all semantical types V ∈ Type, the interpretation [V] is a well-defined PER, and intensionally equal types have the same interpretation. Together, [ ] ∈ Fam(Type).

Lemma B.2. (Soundness of intensional type equality) If D :: V = V′ ∈ Type then [V], [V′] ∈ Per and [V] = [V′].

Proof: By structural induction on D. We consider the following case:

\frac{V = V′ ∈ Type F v = F′ v′ ∈ Type for all v = v′ ∈ [V]}{Fun V F = Fun V′ F′ ∈ Type}

We have to show that Fun([V], v ↦ [F v]) and Fun([V′], v ↦ [F′ v]) are PERs and equal. By induction hypothesis, [V] and [V′] are PERs and equal. Assume v = v′ ∈ [V] arbitrary. We may use the induction hypothesis on the assumptions F v = F′ v, F v′ = F′ v ∈ Type to deduce [F v] = [F v′] ∈ Per, hence, the family F, defined by F(v) := [F v], is in Fam([V]), since v and v′ were arbitrary. Analogously, for the second family F′, where F′(v) := [F′ v], it holds that F′ ∈ Fam([V′]). By Lemma 5.2, Fun([V], F) and Fun([V′], F′) are PERs. Also by induction hypothesis, we obtain [F v] = [F′ v] for arbitrary v, so the two families F and F′ are equal. This entails our goal. ⊓ ⊔

Finally, we can prove that Type is itself a PER.

Lemma B.3. (Intensional type equality is a PER) 1. If D :: V_{1} = V_{2} ∈ Type and V_{2} = V_{3} ∈ Type then V_{1} = V_{3} ∈ Type.

2. If D :: V = V′ ∈ Type then V′ = V ∈ Type.

Proof: Each by structural induction on D. For transitivity (1.), we consider the case:

\frac{V_{1} = V_{2} ∈ Type F_{1} v_{1} = F_{2} v_{2} ∈ Type for all v_{1} = v_{2} ∈ [V_{1}]}{Fun V_{1} F_{1} = Fun V_{2} F_{2} ∈ Type}

\frac{V_{2} = V_{3} ∈ Type F_{2} v_{2} = F_{3} v_{3} ∈ Type for all v_{2} = v_{3} ∈ [V_{2}]}{Fun V_{2} F_{2} = Fun V_{3} F_{3} ∈ Type}

By soundness of intensional type equality (Lemma B.2), we have [V_{1}] = [V_{2}] ∈ Per, and by the first induction hypothesis, V_{1} = V_{3} ∈ Type. Assume arbitrary v = v′ ∈ [V_{1}]. Since [V_{1}] is a PER, v′ = v′ ∈ [V_{1}], hence, also v′ = v′ ∈ [V_{2}]. By assumption F_{1} v = F_{2} v′ ∈ Type and F_{2} v′ = F_{3} v′ ∈ Type, hence, we can apply the induction hypothesis to obtain F_{1} v = F_{3} v′ ∈ Type. Since v and v′ were arbitrary Fun V_{1} F_{1} = Fun V_{3} F_{3} ∈ Type by rule tyeq-dep . ⊓ ⊔

References

[1] Abel, A.: An Implementation of the Logical Framework with Σ-Types, Haskell code, available at http://www.tcs.ifi.lmu.de/˜ abel/MLFSigma.lhs, November 2004.

[2] Abel, A.: Termination Checking with Types, RAIRO – Theoretical Informatics and Applications, 38(4), 2004, 277–319, Special Issue: Fixed Points in Computer Science (FICS’03).

[3] Abel, A., Coquand, T.: Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs, Typed Lambda Calculi and Applications (TLCA 2005), Nara, Japan (P. Urzyczyn, Ed.), 3461, Springer-Verlag, April 2005.

[4] Adams, R.: Decidable Equality in a Logical Framework with Sigma Kinds, 2001, Unpublished technical report, available on http://www.cs.man.ac.uk/˜ radams/.

[5] Adams, R.: Pure Type Systems with Judgemental Equality, Journal of Functional Programming, 16(2), 2006, 219–246.

[6] Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics, North Holland, Amsterdam, 1984.

[7] Benzmüller, C., Brown, C. E., Kohlhase, M.: Higher-Order Semantics and Extensionality, The Journal of Symbolic Logic, 69(4), December 2004, 1027–1088.

[8] Coquand, T.: An Algorithm for Testing Conversion in Type Theory, in: Logical Frameworks (G. Huet, G. Plotkin, Eds.), Cambridge University Press, 1991, 255–279.

[9] Coquand, T.: An Algorithm for Type-Checking Dependent Types, Mathematics of Program Construction. Selected Papers from the Third International Conference on the Mathematics of Program Construction (July 17–21, 1995, Kloster Irsee, Germany), 26, Elsevier, May 1996.

[10] Coquand, T., Pollack, R., Takeyama, M.: A Logical Framework with Dependently Typed Records, Fundamenta Informaticae, 65(1-2), 2005, 113–134.

[11] Davies, R., Pfenning, F.: Intersection Types and Computational Effects, Proceedings of the fifth ACM SIG-PLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 2000.

[12] Dybjer, P.: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory, The Journal of Symbolic Logic, 65(2), 2000, 525–549.

[13] Goguen, H.: Soundness of the Logical Framework for Its Typed Operational Semantics, Typed Lambda Calculi and Applications, 4th International Conference, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings (J.-Y. Girard, Ed.), 1581, Springer-Verlag, 1999, ISBN 3-540-65763-0.

[14] Goguen, H.: Justifying Algorithms for βη Conversion, Foundations of Software Science and Computational Structures, 8th International Conference, FoSSaCS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings (V. Sassone, Ed.), 3441, Springer-Verlag, 2005, ISBN 3-540-25388-2.

[15] Goguen, H.: A Syntactic Approach to Eta Equality in Type Theory, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005 (J. Palsberg, M. Abadi, Eds.), ACM Press, January 2005, ISBN 1-58113-830-X.

[16] Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics, Journal of the Association of Computing Machinery, 40(1), January 1993, 143–184.

[17] Harper, R., Pfenning, F.: On Equivalence and Canonical Forms in the LF Type Theory, ACM Transactions on Computational Logic, 6(1), 2005, 61–101, ISSN 1529-3785.

[18] Joachimski, F., Matthes, R.: Short Proofs of Normalization, Archive of Mathematical Logic, 42(1), 2003, 59–87.

[19] Klop, J. W.: Combinatory Reduction Systems, Mathematical Center Tracts, 27, 1980.

[20] Lambek, J., Scott, P. J.: Introduction to Higher Order Categorical Logic, Cambridge University Press, New York, NY, USA, 1988, ISBN 0-521-35653-9.

[21] Nordström, B., Petersson, K., Smith, J.: Martin-Löf’s Type Theory, Handbook of Logic in Computer Science, 5, Oxford University Press, October 2000.

[22] Pierce, B. C., Turner, D. N.: Local Type Inference, 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’98, San Diego, California, 1998.

[23] Pottier, F.: A modern eye on ML type inference: old techniques and recent developments, September 2005, Lecture notes for the APPSEM Summer School.

[24] van Raamsdonk, F., Severi, P., Sørensen, M. H., Xi, H.: Perpetual Reductions in Lambda Calculus, Information and Computation, 149(2), March 1999, 173–225.

[25] Sarnat, J.: LF_{Σ}: The Metatheory of LF with Σ types, 2004, Unpublished technical report, kindly provided by Carsten Schürmann.

[26] Vanderwaart, J. C., Crary, K.: A Simplified Account of the Metatheory of Linear LF, Technical report, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2002.

[27] Vaux, L.: A type system with implicit types, June 2004, English version of his mémoire de maîtrise.

[28] Vouillon, J.: Subtyping Union Types, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (J. Marcinkowski, A. Tarlecki, Eds.), 3210, Springer-Verlag, 2004.