\( \newcommand\D{\mathrm{d}} \newcommand\E{\mathrm{e}} \newcommand\I{\mathrm{i}} \newcommand\bigOh{\mathcal{O}} \newcommand{\cat}[1]{\mathbf{#1}} \newcommand\curl{\vec{\nabla}\times} \newcommand{\CC}{\mathbb{C}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\RR}{\mathbb{R}} \newcommand{\ZZ}{\mathbb{Z}} \)
UP | HOME

Automath

Table of Contents

1. Introduction

A proof assistant invented by Nick de Bruijn back in the '60s, it seems to be the first one using dependently-typed lambda calculus. It's also the first logical framework.

A proof script for Automath is called a "Book", its statements are called "Lines".

2. Expressions

There are four or five types of expressions:

  1. Symbols (namespaced identifiers within paragraphs/modules, or "just identifiers")
  2. Lambda abstractions, written [x:T]e where e is an expression (sometimes [x,T]e is used in older literature) — note here that x is an identifier, not a symbol
  3. Applications, <arg>fn instead of fn arg
  4. Abbreviations, d(c_1, ..., c_k)
  5. "Kinds", specifically TYPE (and sometimes PROP)

What's the difference between an abbreviation and an application? Well, we typically do things in math like "Let G be a group, then we call H a subgroup of G if…". If we want to say N is a subgroup of M in Automath, we write N : Subgroup(M).

As far as the kernel cares, it could treat the two as the same, with the caveat that if d is an abbreviation with n>k parameters, then d(c_1, ..., c_k) fixes the last k parameters (x_(n-k)=c_1, …, x_n=c_k).

2.1. Order of Evaluation

Note that if we encounter an expression like <t>f(e_1, ..., e_n), then we first evaluate f(e_1, ..., e_n) and then apply the result as the "rator" to an application with "rand" t.

2.2. Terms, Types, Kinds

The jargon used by de Bruijn and the Automath community is that:

  • A 1-expression is either TYPE or PROP
  • A 2-expression is one of the form T:TYPE or T:PROP (we call them "types" nowadays)
  • A 3-expression is of the form t:T where T is a 2-expression (we call them "terms" nowadays)

2.3. Comments

The only current implementation for Automath is Freek Wiedijk's wonderful implementation. Comments in his implementation come in two forms:

  • Single line comment, start at # or % and continues until the end of the line
  • Multi-line comments, anything in between { and } (possibly nested)

3. Lines

There are three types of lines:

  1. Block Openers push the identifier onto the context, <context> <turnstile> <identifier> := <EB> : <expr>
  2. Primitive Notions defines new primitive notions, <context> <turnstile> <identifier> := <PN> : <expr>
  3. Definitions (or abbreviations) <context> <turnstile> <identifier> := <expr> : <expr>

We see these are all basically the same, but we have some freedom here. (Well, there's a lot more freedom, e.g., we can place the typing annotation after the identifier, <context> <turnstile> <identifier> : <expr> :=..., for example.) In Automath, we can suppress the <context> <turnstile> prefix sometimes (I'm still figuring out when we can).

  • <turnstile> can be either * or @
  • <PN> can be 'pn', 'prim', PN
  • <EB> can be ---, EB, 'eb'
  • We can use ; instead of : for the typing declaration at the end of the line

Note to self: the modern syntax for lines, as used in Coq (and friends), is something more like <context> <turnstile> <identifier> : <expr> := ...

3.1. Contexts

We have a directed "tree of knowledge", where the EB lines form branches, and the other two lines are leafs (leaves?). Automath uses "indicator strings" for the context, i.e., the symbol which is the end of the context. The root node for this tree-of-knowledge is the empty context.

The context is set using the <symbol> <turnstile> prefix. We can set the context to be empty by just writing <turnstile>.

Consider the following (adapted from Freek Wiedijk's formalization of HOL Light's logic): 

  * type : TYPE := PRIM    # sets the context to be initial empty context
  * bool : type := PRIM
  * A : type := ---        # sets the context to be A
    term : TYPE := PRIM
A * B : type := ---

    fun : type := PRIM
    [t:term(fun(A,B))][u:term(A)] comb : term(B) := PRIM

What is the context for the fourth line, term : TYPE := PRIM? We see the third line pushes A onto the top of the empty context. Without a turnstile, it reuses the previous context (which is basically A).

Similarly, the fifth line A * B : type := --- pushes B on top of the context ending at A, creating a new context A:type, B:type.

3.2. Lambda Abstraction as Block Openers

The kernel interprets a line of the form 

a * [x:T] b := ... : T'

as two lines: 

a * x := --- : T
x * b := ... : T'

See Wiedijk's "A new implementation of Automath", section 3.4 for discussion on this.

4. Quasi-Expressions

De Bruijn revised the original Automath to include the following situation: suppose we want to encode a predicate. How to do it? Well, we have a proposition be a 2-expression ("type") of the form p : PROP. A predicate would parametrize this by a "term": 

   * T : TYPE := ---
 T * [x:T]predicate : [x:T]PROP := PN

But is [x:T]PROP a valid expression? De Bruijn calls such a thing a Quasi-Expression. This makes encoding first-order logic (and higher-order logic) really nifty.

Quantifiers can be written down easily as: 

T * [p:[z:T]PROP] forall : PROP := p
  * [a:PROP][b:PROP] imp:PROP := [x:a]b
  * false : PROP := PRIM
a * not : PROP := imp(false)
p * exists : PROP := not(forall([z,T]not(<z>p)))

We use de Morgan's laws to express existential quantification in terms of negating the universal quantifier.

4.1. Type Inclusion

There's also Type Inclusion, where we can take any 2-expression of the form T : [x,T']TYPE and assert it is also acceptable in situations when we just need a T:TYPE. However, this makes it impossible for a 2-expression to have a unique type: we just saw how T : [x,T']TYPE and T:TYPE, but [x,T']TYPE != TYPE.

5. References

  • F. Wiedijk,
    "A new implementation of Automath".
    Journal of Automated Reasoning 29 (2002) 365-387, Eprint.
  • F. Wiedijk,
    "Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics".
    Journal of Applied Logic 4 (2006) 622-645, Eprint and Code
  • Freek Wiedijk, A Nice and Accurate Checker for the Mathematical Language Automath. Manual for his implementation
  • R.Nederpelt, J.Geuvers, and R.de Vrijer,
    Selected Papers on Automath.
    Elsevier Science, 1994.
    • A valuable (and expensive) reference, collating many papers on Automath.
  • Automath Archive has scanned a number of tech. reports written by de Bruijn's team.
  • Herman Geuvers, Rob Nederpelt,
    "Characteristics of de Bruijn's early proof checker Automath".
    arXiv:2203.01173, 24 pages.
    • Discusses the merits and idiosyncracies of Automath, then reformulates its "essence" in modern type theory, relating it to \(\lambda\mathrm{D}\).
  • N.G. de Bruijn,
    "The mathematical language AUTOMATH, its usage and some of its extensions".
    Eprint, dated December 1968; Eprint 2
  • N.G. de Bruijn,
    "AUTOMATH, a language for mathematics".
    Eprint, T.H. Report 66-WSK-05, dated November 1968

Last Updated 2023-03-09 Thu 09:28.