Slide 1

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

Andreas Abel

joint work with Thierry Coquand

ProgLog Seminar Chalmers, Göteborg, Sweden May 11, 2005

Work supported by: TYPES & APPSEM-II (EU), CoVer (SSF)

Slide 2

Background: βη-equality

• Checking dependent types requires equality test

• One approach: reduce to normal form and compare syntactically

• Works fine for β-equality

• Problem with η-reduction: surjective pairing destroys confluence (Klop 1980)

• Even subject reduction fails:

z : Pair A (λx. F x) ⊢ (z L, z R) : Pair A (λ . F (z L))

[I write Pair A (λxB) for Σx:A. B] Slide 3

Thierry’s Equality Algorithm

• Incremental check for βη-equality in dependently-typed λ-calculus (Coquand 1991)

• Alternates weak head normalization and comparison of head symbols

• We extend this algorithm to Σ-types with surjective pairing

• Challenge: termination and completeness

• Two major technical difficulties to overcome

Slide 4

Martin-Löf’s Logical Framework (MLF)

• Expressions = Curry-style λ-terms

c  ::= Fun | El | Set  constants
r, s, t  ::= c | x | λxt | r s  expressions
A, B, C ::= Set | El t | Fun A (λxB) types

• Examples

Fun A (λxB)  dependent function space Πx:A. B
Fun Set (λa. Fun (El a) (λ . El a)) type of identity: ∀a:∗. a → a

Slide 5

Martin-Löf’s logical framework

• Judgements for typing and equality, e.g.,

Γ ⊢ t : A  t has type A
Γ ⊢ t = t′ : A t and t′ are equal terms of type A

• Example: application rule

\frac{Γ ⊢ r : Fun A (λxB) Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}

• β- and η-rules

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

\frac{Γ ⊢ t = t′ : Fun A (λxB)}{Γ ⊢ (λx. t x) = t′ : Fun A (λxB)} x ∉ FV(t)

Slide 6

Lambda Model

• Entities

v, f, V, F ∈ D  elements of the model
ρ  ∈ Var → D environments

• Operations

f · v ∈ D application in the model
tρ ∈ D denotation of expression t in environment ρ

Slide 7

Lambda Model Axiomatization

Computation (β)

(λxt)ρ · v = t(ρ, x=v)

Congruences

cρ = c
xρ = ρ(x)
(r s)ρ = rρ · (sρ)

Injectivity

El · v = El · v′  implies v = v′
Fun · V · F = Fun · V′ · F′ implies V = V′ and F = F′

Slide 8

PER Model

• Assume a basic partial equivalence relation (PER) S on D

• Interpretation of types in D as sub-PERs of S

[Set]  = S
[El · v]  = S
[Fun · V · F] = {(f, f′) | (f · v, f′ · v′) ∈ [F · v] for all (v, v′) ∈ [V]}

• Soundness of typing and equality rules If Γ ⊢ t : A then (t ρ, t ρ) ∈ [Aρ] for all ρ ∈ [Γ]. If Γ ⊢ t = t′ : A then (t ρ, t′ρ) ∈ [Aρ] for all ρ ∈ [Γ].

• Implication: (t ρ, t′ρ) ∈ S Slide 9

Substitution and Extensionality

• Difficulty 1: Soundness proof of application rule

\frac{Γ ⊢ r : Fun A (λxB) Γ ⊢ s : A}{Γ ⊢ r s : B[s/x]}

• requires substitution property (B[s/x])ρ = B(ρ, x=sρ).

• Hence, model needs additional axiom

(ξ) (λxt)ρ = (λxt′)ρ′

if t(ρ, x=v) = t′(ρ′, x=v) for all v ∈ D

• Also gives irrelevance t(ρ, x=v) = tρ if x ∉ FV(t), needed for η.

Slide 10

Weak head evaluation

• Weak head values

n ::= c t⃗ | x t⃗ neutral expressions
w ::= n | λxt weak head values

• Weak head evaluation (call-by-name)

(r s)↓ := r↓@s
t↓ := t  t not application
n@s := n s
(λxt)@s := (t[s/x])↓

Slide 11

Untyped Algorithmic βη-Equality

• βη-conversion test for normalizable weak head values w ∼^{−} w′ • Two neutral expressions

\overline{c ∼^{−} c} \overline{x ∼^{−} x} \frac{n ∼^{−} n′ s↓ ∼^{−} s′↓}{n s ∼^{−} n′ s′}

• At least one λ

\frac{t↓ ∼^{−} t′↓}{λxt ∼^{−} λxt′} \frac{t↓ ∼^{−} n x}{λxt ∼^{−} n} \frac{n x ∼^{−} t′↓}{n ∼^{−} λxt′}

• Relation ∼^{−} is a PER

Slide 12

Transitivity of Algorithmic Equality

• Lemma:

1. If D_{1} :: w ∼ n x⃗ and D_{2} :: n ∼ n′ then w ∼ n′ x⃗ (plus symmetrical proposition).

2. If D_{1} :: w_{1} ∼ w_{2} and D_{2} :: w_{2} ∼ w_{3} then w_{1} ∼ w_{3}.

• Proof by simultaneous induction on D_{1} and D_{2}.

• 1. is needed for the following case of 2.

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

Slide 13

Completeness of Algorithmic Equality

• Recall: ⊢ t = t′ : A implies (t, t′) ∈ S

• Take model instance

D  = β-equivalence classes
f · v = \overline{f v}
tρ = \overline{t[ρ]}
S  = lifted algorithmic equality ∼

• algorithmic equality on β-equivalence classes

\overline{t} ∼ \overline{t′} :⟺ t =_{β} v and t′ =_{β} v′ for some v, v′ with v ∼ v′

Slide 14

Standardization

• Using standardization, \overline{t} ∼ \overline{t′} implies t↓ ∼ t′↓.

• Summary (ρ_{0} is identity valuation):

Γ ⊢ t = t′ : A

Soundness of judgement

(tρ_{0}, t′ρ_{0}) ∈ [Aρ_{0}]

[Aρ_{0}] ⊆ S

\overline{t} ∼ \overline{t′}

Standardization

t↓ ∼ t′↓ Slide 15

Extension to Σ-types

• Expressions

c ::= ⋯ | Pair constants
r, s, t  ::= ⋯ | (r, s) | t L | t R expressions
A, B, C ::= ⋯ | Pair A (λxB)  types

• Example: Pair A (λxB) dependent type of pairs (Σx:A. B)

• Surjective pairing rule

\frac{Γ ⊢ r = r′ : Pair A (λxB)}{Γ ⊢ (r L, r R) = r′ : Pair A (λxB)}

Slide 16

η-Reduction Destroys Subject Reduction

• Pair intro: types of s and t do not determine type of (s, t)

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

• E.g., if B[s/x] = Eq A s s, then B ∈ {Eq A x x, Eq A x s, … } • Change typing through η-expansion

{z : Pair A (λxB) \atop z L : A} {z : Pair A (λxB) \atop z R : B[z L/x]}
(z L, z R) : Pair A (λ . B[z L/x])

• Subtyping does not solve this problem Slide 17

Extended Algorithmic Equality

• Neutral expressions

\frac{n ∼ n′}{n L ∼ n′ L}  \frac{n ∼ n′}{n R ∼ n′ R}

• At least one pair

\frac{r↓ ∼ r′↓ s↓ ∼ s′↓}{(r, s) ∼ (r′, s′)}

\frac{r↓ ∼ n L  s↓ ∼ n R}{(r, s) ∼ n}  \frac{n L ∼ r′↓  n R ∼ s′↓}{n ∼ (r′, s′)}

Slide 18

Transitivity

• Problem 2: Alg. Eq. not transitive

• λx. z x ∼ z and z ∼ (z L, z R), but not λx. z x ∼ (z L, z R)

• Solution: “Transitivization” ∼^{+} through additional rules

\frac{t↓ ∼^{+} n x n L ∼^{+} r n R ∼^{+} s}{λxt ∼^{+} (r, s)}

+ symmetrical rule

• If t, t′ are of the same type, t ∼^{+} t′ does not use extra rules • Equality ∼ is transitive for expressions of the same type Slide 19

Proof of Transitivity

• Measure # on derivations

aq^{+}-fun-pair \frac{\begin{matrix}D_{1} \\ t↓ ∼^{+} n x \end{matrix}  \begin{matrix}D_{21} \\ n L ∼^{+} r \end{matrix}  \begin{matrix}D_{22} \\ n R ∼^{+} s \end{matrix}}{λxt ∼^{+} (r, s)}
#aq^{+}-fun-pair(D_{1}, D_{21}, D_{22}) = 1 + #D_{1} + max(#D_{21}, #D_{22})
#r(D_{1}, …, D_{n})  = 1 + max{#D_{i} | 1 ≤ i ≤ n}

• Prove simultaneously by induction on #D_{1} + #D_{2}:

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

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

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

Slide 20

Summary of Completeness Proof

Γ ⊢ t = t′ : A

Soundness of judgement

(tρ_{0}, t′ρ_{0}) ∈ [Aρ_{0}]

[Aρ_{0}] ⊆ S

\overline{t} ∼^{+} \overline{t′}

Standardization

t↓ ∼^{+} t′↓

Transitivity (with Γ ⊢ t, t′ : A)

t↓ ∼ t′↓ Slide 21

Proof Economics

Injectivity  required
Inversion of typing  required
Standardization  required
Subject reduction  not required
Confluence (Church-Rosser) not required
Normalization  not required
Certificate  good economics!

Slide 22

Related Work

• Vaux (2004): PER model for MLF with intersection

• Aspinall/Hofmann (TAPL II), Goguen (2005): completeness of algorithmic equality using standard meta theory

• Coquand, Pollack, and Takeyama (2003): extension of MLF by records with manifest fields

• Harper and Pfenning (2005): algorithmic equality for ELF directed by simple types (obtained by erasure)

• Schürmann and Sarnat (2004): extension to Σ-types

• Adams (2001): Luo’s LF with Σ-kinds and type-directed equality Slide 23

Future Work

• Logical framework with proof-irrelevant propositions

• Type-directed equality without erasure

Thanks to Frank Pfenning, Carsten Schürmann, and Lionel Vaux