aut

Freek Wiedijk University of Nijmegen

‘35 years of Automath’ workshop Heriot-Watt University Edinburgh

20020410, 16:00 an exercise by Knuth

reimplementation of Automath Christmas holiday (for fun) about five years ago

reduction strategy from paper by Zandleven

– no new ideas there

– βδη-reduction

– program can trace reductions

– program can limit number of reductions per type-check

– program can keep statistics on number of reductions

implemented in C – portable, fast

both AUT-68 and AUT-QE differences between AUT-68 and AUT-QE can be chosen independently

not AUT-SYNT not ‘telescopes’ why you don’t need it

Automath is a dead language

– if you want mathematics: use Mizar

– if you want mathematics and automation of boring tasks: use HOL (or one of the ‘HOL clones’: Isabelle, PVS)

– if you want Automath: use Agda

Automath is still interesting in the spectrum of formal systems

– many interesting ideas

repairing Jutting’s Grundlagen

a stack of floppy floppies

Jutting’s formalization of Landau’s ‘Grundlagen der Analysis’ corrupted electronic copy

– a few bytes missing every kilobyte or so

– no regularity in damage using printed version: repair it – checker needed a Rosetta stone edition of the Grundlagen

plan: to have an edition of the Grundlagen

– left pages: German

– right pages: Automath

already scanned/typed the German version already labeled corresponding points in both files still needed: TEX hacking to merge the two texts in a nice layout the de Bruijn factor comparing sizes of informal math and formalization

German TEX  ↔  Automath
190K  3.9×  740K
compressed German TEX ↔ compressed Automath
42K 3.7× 160K

for most formalizations: de Bruijn factor turns out to be between 3 and 5 fact to remember:

de Bruijn factor ≅ 4

λ-typed versus Π-typed λ-calculus

Automath is incompatible with Coq PTS-style type theory:

x ⊢ a : A : ∗ then ⊢ λx.a : Πx.A : ∗

In Automath λ and Π are the same thing:

\begin{aligned}λx.a & → & [x]a \\ Πx.A & → & [x]A \end{aligned}

In AUT-QE one has ‘type inclusion’:

[x]A : [x]∗ and [x]A : ∗

not easy to ‘convert’ AUT-QE λ-terms to Coq λ-terms type theories are too different λ-typed λ-calculus is the type theory from outer space

in the later versions of de Bruijn’s systems:

– no type inclusion: not needed for Automath as a logical framework – binders never evaporate: [x]A : [x]∗

advantages:

– more regular than PTS-style

– simpler than PTS-style → PTS-like presentation by de Groote

disadvantages:

– predicative, but no straight-forward set theoretic model

– for λP as a logical framework there’s correspondence theory for λ-typed type theory as a logical framework there’s not

I would like a ‘cross’ of both systems: λ_{0} ≡ λ, λ_{1} ≡ Π, λ_{2}, λ_{3}, …

named variables, de Bruijn indices and term graphs the two common approaches: named variables and de Bruijn indices two main implementation styles for λ-terms:

– named variables: traditional logic, ‘first Automath’, HOL Light, Agda, …

– de Bruijn indices:

‘second Automath’, Mizar, Coq, … named variables often used with delayed substitutions term graphs where variables point back to λs

third implementation style: term graphs variable points back at a λ

if you have a hammer, everything looks like a nail

– not natural in functional programming languages ML, Haskell: they don’t do it

– natural in imperative programming languages C, Java → Martijn Oostdijk’s Java implementation of Coq terms

no need for renumbering on substitutions

variables will sometimes point at λs that don’t ‘see’ the variable!

Automath syntax

cutting lines into halves

Automath ‘lines’ have traditionally four ‘parts’ f(x, y) ≡ c is written in Automath like

                       * x := --- : A
                     x * y := --- : A
                     y * f := c   : A

‘y *’ sets the context → becomes a first class citizen

     y * f := c : A  becomes two lines  {y * \atop f := c : A}

syntactic variants three ways to write ‘empty blocks’ = introduction of parameters

                 x := EB  : A   f := c : A
                 x := --- : A   f := c : A
                       [x : A]  f := c : A

other notational differences:

                    *  ↔  @
                    :=  ↔  =
                    :  ↔  _E  ← ‘ ^HE’
                    PN  ↔  'prim'
                  [x,A]  ↔  [x:A]
                f := c : A ↔ f : A := c

extracting parts of an Automath book

extracting the minimal formalization that proves the theorem one of the features of the original Automath ‘remove all lines that are not needed for a theorem’ example:

full Jutting formalization 10691 lines
extract of ‘satz301f’  2825 lines

satz301f:

r + si = t + ui ⇒ s = u

the primitive notions of the Grundlagen

Automath axioms are called ‘primitive notions’ ‘what are the axioms of this formalization?’

– minimal formalization that contains exactly the primitive notions

Grundlagen

– 32 primitive notions

              con, et, is, refis, isp, ind, oneax
                fisi, ot, in, inp, otax1, otax2
                pairtype, pair, first, second
                pairis1, firstis1, secondis1
            set, esti, setof, estii, estie, isseti
                  nat, 1, suc, ax3, ax4, ax5

the de Bruijn principle and ‘Automath-single line’ terms an analogy

machine code ↔  λ-term
‘binary’  ‘proof object’
assembler  ↔ Automath, Coq

‘line based’

Pascal, C, Java ↔ Mizar, Isabelle/Isar

‘block structured’ generating huge λ-terms

de Bruijn’s AUT-SL or AUT-ΔΛ → Nederpelt and de Groote a whole ‘book’ as one big λ-term a directed graph with 5 kinds of nodes:

out-degree:

local definition  3
λ-abstraction  2
application  2
variable  1
‘type’  0

de Bruijn indices: starting from 0, writing 0 with 0 digits

aut -Q -g 320 grundlagen.aut: 1.8M of proof term

performance of proof assistants

procedural versus declarative proof checkers

proof styles: who does the proof?

– procedural: the computer, directed by the human interactive, ‘tactics’

– declarative: the human, checked by the computer batch

most current systems are procedural

declarative systems: Automath, Agda, Mizar performance figures: Automath, Metamath, Mizar, Coq

speed in lines checked per second:

aut 30× as fast as Mizar 30× as fast as Coq

aut checks the Grundlagen in 0.6 seconds:

however: aut has never been stress-tested (maybe forgets to check something or checks it wrong) (I don’t hope so!)

Norman Megill’s Metamath: similar program (also written in C), similar speed

– a few seconds to check the whole Metamath library

Automath and the fourteen provers of the world

where do the current provers differ from Automath?

properties Automath doesn’t have:

– calculations can be proved automatically, ‘Poincaré principle’ (HOL, PVS, Coq, Otter, Isabelle, ACL2, PhoX, IMPS, Theorema, Lego, Nuprl)

– extensible/programmable by the user (HOL, PVS, Coq, Isabelle, Nuprl)

– powerful automation (HOL, PVS, Otter, Isabelle, ACL2, Theorema)

– readable proof input files (Mizar, Isabelle, ACL2, Theorema)

– large mathematical standard library (HOL, Mizar, PVS, Coq, Isabelle, IMPS, Nuprl) what can the current provers learn from Automath?

– λ-typed λ-calculus is a beautiful logical framework – graph representation of λ-terms works well

– very big ‘de Bruijn principle’ proof terms are possible – very fast checkers are possible

maybe with the help of ‘proof caching’ will the Automath/QED dream ever come true?

I expect: yes! I expect: not soon! but even when not yet usable for mathematical practice:

formalizing mathematics is the best computer game there is

the beauty of programming… but without fear of bugs! the beauty of mathematics… and the computer takes care of all details!