avoiding state with infinite contexts

Freek Wiedijk Radboud University Nijmegen The Netherlands

10th Asian Logic Conference special session: model theory and proof theory Kobe, Japan

2008 09 05, 15: 40

trusting a proof checker

proof checking of mathematics fully verified for correctness by a computer:

• Gödel’s first incompleteness theorem nqthm (1986), Coq (2003), HOL Light (2005)

• Jordan curve theorem HOL Light (2005), Mizar (2005)

• prime number theorem Isabelle (2004), HOL Light (2008)

• four color theorem Coq (2004) the de Bruijn criterion

all software has bugs … why trust a proof checker?

N.G. de Bruijn, 1968:

[ …] This is one of the reasons for keeping AUTOMATH as primitive as possible. [ …]

two approaches:

• small independent checker(s)

e.g.: Ivy system for Otter/Prover9

• small proof checking kernel inside the system LCF architecture

Robin Milner, 1972 systems and kernels source sizes in 10^{3} lines of code

kernel system  thms
HOL Light  ocaml  0.7  30  69
Isabelle  sml  5  160  40
Twelf  sml  6  70  —
ProofPower  sml  7  90  42
Coq  ocaml  14  180  39
Mizar  pascal  80  45
ACL2  lisp  170  12
PVS  lisp  280  15

proving the kernel correct

• Coq in Coq Bruno Barras, 1997–1999

executable Coq model of the Coq logic

two different systems (the real system versus the extracted code) extracted code not yet used for serious proof development

• HOL in HOL

John Harrison, 2006

HOL model of the actual HOL Light kernel source

not yet the full code (no type polymorphism, no definitions) no systematic relation between HOL model and executable code kernels and state to make proving a kernel feasible:

• code should be as ‘mathematical’ as possible

• for current technology:

kernel should be programmed in a purely functional language Lisp, ML, Haskell, Coq

current practice:

• kernels always have a state:

definitions from the formalization that already have been processed • corresponds to a context in the formal treatment of the logic

Γ ⊢ M : A

undo for HOL

abstract datatypes of the HOL Light kernel

type hol_type = private
| Tyvar of string
| Tyapp of string * hol_type list
type term = private
| Var of string * hol_type
| Const of string * hol_type
| Comb of term * term
| Abs of term * term
type thm = private
| Sequent of term list * term

                                                # `pi`;;
                                                val it : term = `pi`
                                                #

                                       [figure: Const; "pi"; Tyapp; "real"; []]

the problem with undoing definitions

hypothetical HOL Light session:

# let X0 = new_definition `X = 0`;;
val ( X0 ) : thm = |- X = 0
# undo_definition "X";;
val it : unit = ()
# let X1 = new_definition `X = 1`;;
val ( X1 ) : thm = |- X = 1
# TRANS (SYM X0) X1;;
val it : thm = |- 0 = 1
#

undoing definitions can change the meaning of existing thms inconsistent!

⇒ HOL Light does not support ‘undo’ putting the definitions in the names

• current HOL Light names of constants: string pair of a string and a type

• stateless HOL Light names of constants: pair of the traditional name and the definition

comparing equal definitions by pointer comparison is cheap

     [figure: Const; "X"; `:num`; `X = 0`        `; Const; "0"; definition of `O`]

nested kernels

current HOL Light  stateless HOL Light

[figure: system; kernel; state; system; kernel; state]

about 10 % slower

type theory without explicit contexts

first order logic and contexts

first order logic  type theory
\frac{\frac{A ⊢ P (x)}{A ⊢ ∀x P (x)}^{∀I}}{⊢ A → ∀x P (x)}_{→I}  \frac{\frac{H : A , x : D ⊢ M_{1} : P (x)}{H : A ⊢ M_{2} : Πx : D. P (x)}^{λ}}{⊢ M_{3} : A → Πx : D. P (x)}_{λ}
‘sea’ of free variables  ‘free’ variables in the context

\frac{\frac{A ⊢_{\{x\}} P (x)}{A ⊢_{\{\}} ∀x P (x)}^{∀I}}{⊢_{\{\}} A → ∀x P (x)}_{→I}

⊢_{{}} (∀x P (x)) → (∃x P (x)) ? merging all contexts into an infinite context category of contexts for a given type theory

• objects:

Γ

Γ is a finite or countably infinite context

• morphisms:

Γ ⟶^{f} Γ′

f is an injection mapping the variables from Γ to variables from Γ′ this category has pushouts: every two contexts can be combined into a bigger context direct limit of all contexts:

Γ_{∞}

the system Γ_{∞}

Γ_{∞}: system equivalent to the PTS rules but without explicit contexts (we reuse the name of the infinite context for the system)

PTS = Pure Type System

we write

M : A

to morally mean

Γ_{∞} ⊢ M : A

Γ_{∞} preterms:

A ::= s | x_{i}^{A} | x_{i} | AA | λx_{i}:A.A | Πx_{i}:A.A

two kind of variables: free variables x_{i}^{A} and bound variables x_{i} superscript A of x_{i}^{A} may be any preterm two of the six Γ_{∞} rules

PTS rules  equivalent Γ_{∞} rules
\frac{Γ ⊢ A : s}{Γ, x_{i} : A ⊢ x_{i} : A}  \frac{A : s}{x_{i}^{A} : A}
\frac{Γ ⊢ A : s_{1} Γ, x_{i} : A ⊢ B : s_{2}}{Γ ⊢ Πx_{i}:A.B : s_{3}}  \frac{A : s_{1} B : s_{2}}{Πx_{i}:A.B[x_{j}^{A} := x_{i}] : s_{3}}

binding a variable in Γ_{∞}: replace a free variable by a bound variable correspondence theorems

derivable PTS judgment ⟷ derivable Γ_{∞} judgment

from left to right: alpha convert the judgement to separate free from bound variables then: remove the context

from right to left: topological sort of the free variables in the Γ_{∞} judgement then: put them in that order in the context

implementing Γ_{∞} for LF

the datatypes of the kernel

type preterm =
| Star
| Ref of int
| Var of string * preterm
| Const of string * preterm * preterm list  axioms used
| App of preterm * preterm
| Bind of int * preterm * preterm  0 = λ, 1 = Π
type term = private
| Box
| In of preterm * term
type red = private
| Red of preterm * preterm

difference of this approach with other kernels most purely functional kernels:

                 App : preterm * preterm -> preterm
           typecheck : state -> (preterm -> term)
        extend_state : string * preterm -> state -> state

mutually inconsistent terms (from mutually inconsistent states) possible internally inconsistent state not possible

our approach: function application in LCF style

                 app : term * term -> term

mutually inconsistent terms not possible comparing kernel sizes

current HOL Light  all lines content
kernel  fusion.ml  669  394

stateless HOL Light

kernel  core.ml  404  330
state  state.ml  95  71

Γ_{∞} for LF

kernel  214  166
convertibility  64  49
typechecker  29  25

outlook

future work but does this scale? experiment:

Γ_{∞} for LF

HOL Light

kernel

kernel

LF context for HOL

how much slower than current HOL Light? 100 times? ∞ times?