Slide 1

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

Andreas Abel

joint work with Thierry Coquand

TLCA’05 Nara, Japan April 21, 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, A, B, C ::= c | x | λxt | r s expressions

• 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]}

Slide 6

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 7

Untyped Algorithmic Equality

• βη-conversion test for 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 transitive

• Completeness to be shown by model construction

Slide 8

Lambda Model

• Entities

u, 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 9

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 10

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 11

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

Slide 12

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 13

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 14

Extension to Σ-types

• Expressions

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

• 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 15

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 16

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 17

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 18

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 19

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 20

Future Work

• Logical framework with proof-irrelevant propositions

• Type-directed equality without erasure

• An open problem?!

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