# Tutorial — Automath

by Alex Nelson, 27 December 2015

I’ve been studying the history of theorem provers (I intend to write a post summarizing the amazing history), and I’ve been stuck on Automath. It’s a peculiar langauge that closely resembles assembly code, but has idiosyncratic notions. I’ll try to unravel the basics of Automath in this post, and walkthrough some example code snippets.

# The Basics

**1. Lines.**
We should think of a program (or “text”) in Automath as a sequence of
statements (or “lines”). A statement consists of two parts: (a) the
context part, and (b) the body (“meat and potatoes”) of the line.

**1.1. Context.**
The “context” is a misleading term, since it suggests something
different in modern languages than in Automath. It is similar to
variable scope,
but combined with
named parameters.

Syntactically, each line starts with:

- a
`*`

(indicating we’re continuing to work in the given context/scope), - a
`<symbol> *`

(indicating we’re working with specific symbols as named parameters, while continuing to work in the given context), or - neither of these (indicating we’re starting a new scope/context).

**1.2. Body.**
There are three types of lines we can have:

- Definitions or Abbreviations, which define a new function or constant
`<fn_identifier> : <type> := <body>`

. - Variable introduction (or “EB lines”), indicated by the assignment
`<var_identifier> : <type> := ---`

or`<var_identifier> : <type> := EB`

or`<var_identifier> : <type> := 'eb'`

. - Declaring new types or constants as primitive notions (or “PN
lines”), indicated by
`<identifier> : <type> := PRIM`

or`<identifier> : <type> := PN`

.

**Caution:** We have chosen to stick with the convention `<term> : <type>`

and `<type> : <kind>`

, but Automath allows us to place the
type assignment *anywhere* after the variable, i.e., we could write
`<identifier> := <body> : <type>`

just as easily as
`<identifier> : <type> := <body>`

. Either convention is valid Automath
code, but since nowadays the convention is `<term> : <type>`

and
`<type> : <kind>`

, we stick with that. (End of Cautionary Remark)

**1.3. Syntax.**
The syntax for a line varies slightly, because the specification was
mildly free-form. (It was the ’60s, after all.) But the basic format
looks like:

```
# This is a comment
* nat : TYPE := PN # Define a new type called "nat"
* 1 : nat := PN # Define a new constant "1" in nat
* x : nat := --- # Define a new variable "x" in nat
```

I’ve highlighted in blue the new variable introduced, or the new entity being defined.

The `*`

at the beginning of each line tells us “This line continues to
use the previous line’s context”. This means that previous definitions,
variables, etc., are all “in scope”.

**1.4. Functions.**
Defining functions requires variables to be in the context. That is to
say, we treat the context as a “queue” of parameters, and we specify the
“endpoint” in the stack to refer to a slice (from the start to the
endpoint) as the parameters for the given function.

```
# To define a function, we need a variable explicitly in context.
# We have introduced "x" as a variable natural number, so we can
# use "x"--and all variables defined before it--as the function parameter.
x * successor : nat := PN # Define a new function called "successor"
* 2 : nat := successor(1) # Define a new term "2" defined as calling "successor" on "1"
* 3 : nat := successor(2) # Define a new term "3"
```

This is rather subtle, because it’s unlike any modern programming language. We can use a more modern approach, and use lambda abstractions to specify the parameters for the routine. We can introduce this alternate approach, consider the following snippet:

```
# The "successor" function is still in context, thanks to asterisk.
# Function composition is done by hand, e.g., the following.
x * plustwo : nat := successor(successor) # Define a new function called "plustwo"
* succfun : [x:nat]nat := [x:nat]successor(x) # Define a new function via lambda abstraction
* 3alt : nat := <2>succfun # Define a new term "3alt" via lambda calculus' "apply"
```

Notice that we have `λ x:type . body`

become `[x:type] body`

, and `apply f x`

become `<x>f`

. This is quirky Automath notation. Also observe, for
`succfun`

, its type is a function-type, hence its type is `[x:nat]nat`

.

**1.5. Remark (Context).**
The context for a line is the “function parameters” needed for that
line. Furthermore, if we introduce a variable into context, something like

```
* x : nat := --- # Define a new variable "x" in nat
x * successor : nat := PN # Define a new function called "successor"
```

This is equivalent to the following:

` * [x:nat] successor : nat := PN # Define a new function called "successor"`

That is to say, a variable introduction line `* x : nat := ---`

is the
same as writing `[x:nat]`

.

**1.6. Remark (Types).**
There is some subtlety here, because we can have “dependent types”. That
is to say, we have lambda expressions `[x:t]body`

which takes in a term,
and produces a type. Why would this be useful?

The textbook example is to eliminate bounds checking for lists. The not-so-textbook-example is to make sure that deductions are sensible. Lets investigate this latter example more fully.

But we should note, we’re not working in the “lambda cube”. We don’t
have a dependent product type, `Π x:type . body`

, because we have a
lambda-typed lambda calculus.

# First Order Logic

**2.**
First-order logic is probably the next interesting system to look at,
and exemplifies a lot of the syntax & semantics of Automath.

**2.0.1. Reference.**
I’m borrowing this section’s code from Freek Wiedijk’s
Automath restaurant. Specifically,
the ZFC code.

**2.1. Types.**
We have several basic parts for first-order logic: propositions, proofs
of propositions, and terms. We treat these as primitive notions.

```
* prop : TYPE := PRIM
* [a:prop] proof : TYPE := PRIM
* term : TYPE := PRIM
```

We have a variable `a:prop`

available to our disposal.

**2.2. First-Order Logic, Connectives and Quantifiers.**
We need to continue introducing relevant connectives and
quantifiers. The “bare minimum” amounts to a modest 5 definitions, but
we’ll also introduce “luxury goods” like the existential quantifier &
other connectives.

Some points worth observing here:

`imp`

is a function expecting two parameters,`a`

and`b`

. When supplied, and called, the term`imp(a,b)`

corresponds to the logical statement “*a*implies*b*”.- The
`for`

function is the universal quantifier. We call it as`for([z:term]<z>predicate)`

, which should translate intuitively as “for each*z*, the predicate on*z*holds.” - We have two “queues” of parameters, namely
`a:prop, b:prop`

and`p:[z:term]prop`

. When defining functions, we need to specify a variable before the`*`

asterisk, which will signal to Automath to find the queue with the variable, and select the sublist from the head of the queue to the symbol given. (So,`a *`

would tell Automath to look in the`a:prop, b:prop`

queue, take the symbols from the head of the list until it gets to`a`

, and inclusively use that as the parameters for the given function.)

**2.2.1. Luxury Connectives.**
We have the following “luxury connectives” and quantifiers. First, the
connectives, which are really just abbreviations…in the sense that we
can rewrite them in terms of `imp`

and `false`

.

```
a * not : prop := imp(a,false)
b * and : prop := not(imp(a,not(b)))
b * or : prop := imp(not(a),b)
b * iff : prop := and(imp(a,b),imp(b,a))
```

**2.2.2. Luxury Quantifiers.**
The two luxury quantifiers we can work with are the existential
quantifier, and its variant the uniquen existential quantifier. We can
implement these using an equality predicate on terms. We implement
existial quantification via negating universal quantification.

```
* [x:term][y:term] eq : prop := PRIM
# "p" refers to the parameters used in "forall"
p * ex : prop := not(for([z:term]not(<z>p)))
p * unique : prop :=
for([z:term]imp(<z>p,for([z':term]imp(<z'>p,eq(z,z')))))
p * ex_unique : prop := and(ex,unique)
```

**2.3. Proof System.**
We need to actually implement some proof system. The most popular
version, natural deduction, requires us to define *introduction* and
*elimination* rules of inference for each primitive connective and
quantifier in our logic. We really have just one primitive connective
(`imp`

), and one primitive quantifier (`for`

)…and for classical logic,
one additional rule for the law of the excluded middle.

```
# Rules of inference for implication, i.e., hypothetical derivations
b * [_:[_1,proof(a)]proof(b)] imp_intro : proof(imp(a,b)) := PRIM
b * [_:proof(imp(a,b))][_1:proof(a)] imp_elim : proof(b) := PRIM # AKA Modus Ponens
# Rules of inference for universal quantification
p * [_:[z,term]proof(<z>p)] for_intro : proof(for(p)) := PRIM
p * [_:proof(for(p))][z:term] for_elim : proof(<z>p) := PRIM
# Law of the excluded middle
a * [_:proof(not(not(a)))] classical : proof(a) := PRIM
```

If we were being 100% careful, we should also have rules of inference for equality introduction and elimination. This is actually a good exercise for the reader, who can cheat easily with the links supplied.

# Propositions as Types

**3.1. Curry-Howard Correspondence.**
We can invoke the Curry-Howard Correspondence (well, in truth, de
Bruijn did a lot of work on this independent of Howard, and at about the
same time). What to do? Well, we had only one kind `TYPE`

in our system
so far. We introduce a second kind `PROP`

.

If `foo : PROP`

, we can consider `foo`

as a proposition. If further, we
have `bar : foo`

, then we interpret `bar`

as establishing the truth of
`foo`

. (I.e., `bar`

is the “proof” of `foo`

.)

**3.2. Implication.**
Let `alpha : PROP`

and `beta : PROP`

. If we have some construction
establishing the truth of `alpha`

, and from it establish the truth of
`beta`

, then we have `alpha`

*implies* `beta`

. Hence implication may be
viewed as a *function* of the “proofs” of `alpha`

to the proofs of
`beta`

.

We can represent implication as a type-valued function ```
[x:alpha]beta :
PROP
```

. Compare this to our definition
which treated implication as `[a:prop][b:prop] imp : prop := PN`

.

Why bother with this newfangled version? We can implement *modus ponens*
as function application! That is, if we have `proof_of_alpha : alpha`

and `proof_of_alpha_implies_beta : [x:alpha]beta`

, then we can construct
`<proof_of_alpha>proof_of_alpha_implies_beta`

to get a proof of `beta`

.

**3.3. Universal Quantification.**
In like manner, if we have `alpha:TYPE`

, and `beta:PROP`

, then
we identify `[x:alpha]beta`

with the proposition “For all `x`

in
`alpha`

, the proposition `beta`

holds.” We get this fragment of
first-order logic *for free* in Automath.

**3.4. Negation.**
As we have seen in our system from section 2, we need to introduce
`false`

as a primitive notion to get negation. Otherwise statements like
“`alpha`

is not of type `beta`

” remain unspeakable.

But that’s not the end of the story for negation: we need some suitable
axioms. Classical mathematicians will impose the double negation
law. Intuitionistic mathematicians will impose the absurdity law (for
any proposition `alpha`

, from `false`

infer `alpha`

).

So, in this form, negation looks like: for `alpha:PROP`

we have
`not(alpha)`

defined as `[x:alpha] false`

. Or in Automath code:

```
* alpha : PROP := PRIM
alpha * not : PROP := [x:alpha]false
```

**3.5. Reinterpreting lines: assumptions, axioms, and theorems (oh my).**
We now have a logical interpretation of all three types of lines.

- Variable introduction lines
`a * x : sigma := ---`

are**assumptions**“let`sigma`

hold” (or more accurately “let`x`

be a proof of`sigma`

). - Primitive notion lines
`a * p : sigma := PRIM`

are**axioms**or axiom schemas (by the dependence on the variables contained in the context`a`

). - Definition lines
`a * def : sigma := body`

are**theorems**. Here the`body`

“proves” the proposition`sigma`

from the assumptions in the context`a`

.

# “Quasi-Expressions”

**4.**
So far we have been working with `AUT-68`

, the first version of
Automath. It has many strengths, but like most alpha-versions it has a
few shortcomings. We could only have lambda abstractions on terms and
types, but not kinds. That is to say, we could not have something like
`[x:foo]TYPE`

. We could shrug and say “Who cares?” But it vastly
simplifies the logical framework we just established if we allow such
things.

When such things are allowed, we have “quasi-expressions”. Thus we get
the second edition of Automath, `AUT-QE`

(where `QE`

stands for, yep,
“quasi-expression”).

**4.1. Definition of Quasi-Expressions.**
We consider kinds of the form `[x:alpha]...[x':alpha'] TYPE`

or
`[x:alpha]...[x':alpha'] PROP`

, where `alpha`

, …, `alpha'`

are
arbitrary types. Such kinds are called **“Quasi-Expressions”**.

We can consider, for example, an arbitrary type-valued function on
`alpha`

introduced by the following code snippet:

`a * f : [x:alpha]TYPE := ---`

**4.2. So What?**
We can have arbitrary `PROP`

-valued functions in AUT-QE. I.e., a
`PROP`

-valued function over `alpha`

is nothing but a *predicate* over
`alpha`

. That’s pretty nifty. Further, we could consider the following snippet:

`a * relation : [x:nat][y:nat]PROP := ---`

This defines an arbitrary binary predicate (or, as the identifier suggests, a
*binary relation*) on the natural numbers.

**4.3. No, really, so what?**
Another bonus, if we recall our discussion of LCF Tactics,
which transformed goals until we’ve proven the desired proposition, we
also had to add some postcondition checking the sequence of tactics
really proved the desired proposition. In other words, there is danger
of *invalid tactics* in LCF, which we desperately want to avoid.
(We don’t want to prove an invalid proposition!)

What can we do? Well, we can use a logical framework to avoid this problem.
Basically, the validity of the representation of the derivations
(“tactics”) becomes an *internal* property, while being *decidable* for free.
In other words, we get *judgments as types*. See Pfenning’s
paper for a review of
this.

**Example.** If we are still not convinced about this, we should
consider the following gist
describing the ZFC axioms,
which has 11 fewer primitive notions in AUT-QE than in AUT-68.
(End of Example)

# References

## On Automath

- R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer,
*Selected Papers on Automath*. North Holland, 1994. - Automath Archive many original papers are here!
- Philippe de Groote, Defining lambda-Typed lambda-Calculus by Axiomatizing the Typing Relation, pdf, 12 pages.
- Freek Wiedijk’s Automath Page and Automath restaurant.

…and that’s the entire active community.

## Other References

- Frank Pfenning,
“Logical Frameworks”.
Chapter 17 of
*Handbook of Automated Reasoning*. Eprint, 85 pages.