convertibility proof terms

Herman Geuvers & Freek Wiedijk University of Nijmegen

LFM’04, IJCAR Cork, Ireland 2004 07 05, 12:00

the problem

a ‘proof’ of the Riemann hypothesis

Theorem. The non-trivial zeroes of Riemann’s ζ(s) function all lie on the complex line ℜs = \frac{1}{2}. Proof. There exists a derivation of this statement with a length less than 10^{10^{100}} symbols (finding it is left as an exercise to the reader). Therefore the statement is true. □

suppose that a proof of the Riemann hypothesis will be found then this is a correct proof too! but: is it an acceptable proof?

formalizing this proof as a Coq lambda-term is doable (using reflection) but: ‘left as an exercise to the reader’ in a formal proof object? linear time proof checking?

‘following a proof with your finger’

proof checking in type theory … is decidable … can be intractable

deciding whether two terms are convertible ‘convertible’ = equal up to beta-reductions and definitional expansions

naive way: fully normalize both terms and compare not practical

in practice: clever search for ‘convertibility proof’ slow checking of errors

error in formalization: checking ‘freezes’

Automath solution: limit on the number of reductions limit exceeded → probably incorrect

Coq solution: limit automatic definitional expansions definitions can be ‘transparent’ and ‘opaque’ systems without convertibility checking

type theory → conversion rule
LF  → conversion rule
HOL  → no conversion rule
Isabelle/Pure → no conversion rule

in HOL each beta reduction step takes an inference step beta rule is one of the proof rules

proof objects checkable in linear time

\begin{matrix}comparing two terms \\ substituting a term in a term \end{matrix} \} unit time

the system

a logical framework with explicit conversions

judgments

\begin{matrix}Γ ⊢ a : A \\ Γ ⊢ H : A = B \end{matrix}

terms

T ::= x | □ | ∗ | Πx:T .T | λx:T .T | T T | T^{H}
H ::= β(T) | ι(T) |
T̄ | H^{†} | H · H |
{H, [x:T]H} | ⟨H, [x:T]H⟩ | HH

derivation rules

• six ‘pure type system’ rules (all the usual rules, minus the conversion rule)

• nine equality proof rules (one for every equality proof term constructor, plus weakening for equality proofs)

• our conversion rule

\frac{Γ ⊢ a : A Γ ⊢ H : A = A′}{Γ ⊢ a^{H} : A′}

basic equality proofs

beta reduction rule

β((λx:A.b)a) : (λx:A.b)a = b[x := a]

John-Major rule

ι(a^{H}) : a = a^{H}

we do not have equality for equality proofs this rule allows us to interchange ‘equal’ equality proofs combining equality proofs

reflexitivity, symmetry, transitivity

\begin{aligned}H & : & a = b \\ H′ & : & b = c \end{aligned} ⇒ \begin{aligned}ā & : & a = a \\ H^{†} & : & b = a \\ H · H′ & : & a = c \end{aligned}

equalities in contexts

\begin{aligned}H & : & A = A′ \\ H′ & : & B = B′ \\ H′′ & : & B = B′[x′ := x^{H}] \end{aligned} ⇒ \begin{aligned}HH′ & : & AB = A′B′ \\ \{H, [x:A]H′\} H′′\} & : & Πx:A.B = Πx′:A′.B′ \\ ⟨H, [x:A]H′⟩ H′′⟩ & : & λx:A.B = λx′:A′.B′ \end{aligned}

type uniqueness

⊢ a : A & ⊢ a : A′ ⇒ A ≡ A′

not just equal up to βδ-equality identical terms

example

\begin{aligned}F : Πx:A.B, a : A & ⊢ & F a : B[x := a] \\ F : Πx:A.B, a : A & ⊬ & F a : (λx:A.B)a \\ F : Πx:A.B, a : A & ⊢ & (F a)^{β((λx:A.B)a)^{†}} : (λx:A.B)a \end{aligned}

\begin{aligned}β((λx:A.B)a) & : & (λx:A.B)a = B[x := a] \\ β((λx:A.B)a)^{†} & : & B[x := a] = (λx:A.B)a \end{aligned}

Martin-Löf type theory ↔ our system

MLTT  Γ ⊢ a = b : A

Γ ⊢ a = b : B

our system  Γ ⊢ H : a = b

types of a and b need not be identical John-Major equality

in our system the judgment really is something like

Γ ⊢ H : (a : A) = (b : B)

subject reduction

a → →_{β} b & ⊢ a : A ⇒ ⊢ b : A

our system does not have reduction ‘subject reduction’ for our system:

⊢ a = b & ⊢ a : A & ⊢ b : B ⇒ ⊢ A = B

‘if two terms are convertible then their types are also convertible’ ⊢ A = B means that some H exists with ⊢ H : A = B two versions of our system

LF = λP λH

convertibility path does not need to be type-correct explicit convertibility proof terms

λH λF

β((λx:A.b)a) : (λx:A.b)a = b[x := a]

λF: beta rule is only allowed when ⊢ a : A λH: beta rule is allowed even when the type of a is ‘wrong’

John-Major rule of λF: ι(a) : a = a^{H}
John-Major rule of λH: ι(a) : |a| = a

|a| ‘erase all conversions from the term a’ is not generally a well-typed λH-term!

the results

correspondence of our systems to LF • λF future work

• λH

Γ ⊢_{λH} a : A ⇒ |Γ| ⊢_{λP} |a| : |A|
Γ′ ⊢_{λP} a′ : A′ ⇒ ∃Γ a A. Γ′ ≡ |Γ| ∧ a′ ≡ |a| ∧ A′ ≡ |A| ∧
Γ ⊢_{λH} a : A
\begin{matrix}Γ ⊢_{λH} A : s ∧ \\ |Γ| ⊢_{λP} a′ : |A| \end{matrix} ⇒ ∃a. a′ ≡ |a| ∧ Γ ⊢_{λH} a : A

ephemeral proofs

our systems: proof terms become much bigger

Coq: ‘proof objects’ are stored as terms in memory HOL: ‘proof objects’ are not stored in memory ephemeral proof objects computed & checked & garbage collected away on the fly λF/λH implementation with ephemeral proof terms?