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 language that closely resembles assembly code, but has idiosyncratic notions. I’ll try to unravel the basics of Automath in this post, and walk-through 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:

Contexts are a directed tree whose root node is the initial empty context. Identifiers are unique, so instead of giving the entire context (which would repeat a lot of declarations), we can just give the “last entry” in the context. We should then think of this <symbol> which appears in the context part as the “Indicator” of the context.

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

  1. Definitions or Abbreviations, which define a new function or constant <fn_identifier> : <type> := <body>.
  2. Variable introduction (or “EB lines”), indicated by the assignment <var_identifier> : <type> := --- or <var_identifier> : <type> := EB or <var_identifier> : <type> := 'eb'.
  3. 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.

Example: Encoding 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

Observe the second line introduces a variable a:prop, and this is treated as a new branch to the empty context (since the context of the second line is * — i.e., the empty context).

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.

  *                false : prop := PRIM
a *         [b:prop] imp : prop := PRIM
  * [p:[z:term]prop] for : prop := PRIM

Some points worth observing here:

  1. 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”.
  2. 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.”

  3. We have two “branches” in the context “tree”, namely (i) a:prop, b:prop and (ii) 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.

    (For example: the context part 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)

Observe the unique definition may be read as: “Given a predicate p, for any term z, if <z>p, then for any other term z' also satisfying <z'>p necessarily implies z = z'”. This amounts to saying there exists no more than one term z satisfying the supplied predicate p.

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, Prop Kind. 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.) The slogan is: Propositions as Types and Proofs as Terms.

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.

  1. Variable introduction lines a * x : sigma := --- are assumptions “let sigma hold” (or more accurately “let x be a proof of sigma).
  2. Primitive notion lines a * p : sigma := PRIM are axioms or axiom schemas (by the dependence on the variables contained in the context a).
  3. 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

…and that’s the entire active community.

Other References