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.
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:
*(indicating we’re continuing to work in the given context/scope),
<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> := EBor
<var_identifier> : <type> := 'eb'.
- Declaring new types or constants as primitive notions (or “PN
lines”), indicated by
<identifier> : <type> := PRIMor
<identifier> : <type> := PN.
Caution: We have chosen to stick with the convention
<term> : <type>
<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.
* 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
<x>f. This is quirky Automath notation. Also observe, for
succfun, its type is a function-type, hence its type is
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
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:
impis a function expecting two parameters,
b. When supplied, and called, the term
imp(a,b)corresponds to the logical statement “a implies b”.
forfunction 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
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:propqueue, 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
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
foo : PROP, we can consider
foo as a proposition. If further, we
bar : foo, then we interpret
bar as establishing the truth of
bar is the “proof” of
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
beta. Hence implication may be
viewed as a function of the “proofs” of
alpha to the proofs of
We can represent implication as a type-valued function
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
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
3.3. Universal Quantification.
In like manner, if we have
[x:alpha]beta with the proposition “For all
alpha, the proposition
beta holds.” We get this fragment of
first-order logic for free in Automath.
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
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
sigmahold” (or more accurately “let
xbe a proof of
- Primitive notion lines
a * p : sigma := PRIMare axioms or axiom schemas (by the dependence on the variables contained in the context
- Definition lines
a * def : sigma := bodyare theorems. Here the
body“proves” the proposition
sigmafrom the assumptions in the context
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
When such things are allowed, we have “quasi-expressions”. Thus we get
the second edition of Automath,
QE stands for, yep,
4.1. Definition of Quasi-Expressions.
We consider kinds of the form
[x:alpha]...[x':alpha'] TYPE or
[x:alpha]...[x':alpha'] PROP, where
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)
- 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.
- Frank Pfenning, “Logical Frameworks”. Chapter 17 of Handbook of Automated Reasoning. Eprint, 85 pages.