Machine Logic

Martin-Löf type theory in Isabelle: formalisation

23 Nov 2022

Last July, I described how Isabelle emerged from a jumble of influences: AUTOMATH, LCF and Martin-Löf. I stated that Isabelle had originated as a proof assistant for Martin-Löf type theory. Eventually I realised that the type theory community wasn’t interested in this work, just as it wasn’t much interested in Nuprl, which was by far the most developed type theory implementation out there. Both implementations had been left behind by the sudden change to intensional equality. As I mentioned in the earlier post, the type theory influence remains strong in the other formalisms supported by Isabelle, notably higher-order logic and ZF set theory. Few however may be aware that Isabelle’s instance for constructive type theory, Isabelle/CTT, still exists and still runs.

Syntactic prerequisites

The syntactic framework for type theory is the system of arities, which determines how many arguments an operator must be given before it is saturated. This system is nothing but the typed λ-calculus, so we begin by introducing the types (or rather arities) of individuals, types and judgments.

typedecl i
typedecl t
typedecl o

Now we introduce the four forms of judgment: to be a well-formed type, equality of types, membership in a type, equality for members of the type:

consts
  Type      :: "t ⇒ prop"          ("(_ type)" [10] 5)
  Eqtype    :: "[t,t]⇒prop"        ("(_ =/ _)" [10,10] 5)
  Elem      :: "[i, t]⇒prop"       ("(_ /: _)" [10,10] 5)
  Eqelem    :: "[i,i,t]⇒prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)

Each of these includes Isabelle mixfix declarations to support standard notation such as $x=y:A$. (A fifth judgment form, a hack used to implement rewriting, isn’t shown.)

The basic propositional types

The false proposition is represented, via the propositions-as-types principle, by the empty type F. It has an eliminator, called contr. True is represented by T, which has one element: tt.

  F         :: "t"
  T         :: "t" 
  contr     :: "i⇒i"
  tt        :: "i"

Skipping forward a bit, let’s look at some of the inference rules for type F. The first simply says that it is a type. The second rule concerns contr, the eliminator for F; it says that from any p belonging to F and any well-formed type, it can return something of that type. This rule expresses the emptiness of F through the principle of ex falso quodlibet.

  F:  "F type"
  FE: "⟦p: F; C type⟧ ⟹ contr(p) : C"

The corresponding rules for the equality judgments are what you might expect and are omitted.

The type of natural numbers

We declare the type N of the natural numbers along with its constructors 0 and successor, and its eliminator, rec:

consts
  N         :: "t"
  Zero      :: "i"                  ("0")
  succ      :: "i⇒i"
  rec       :: "[i, i, [i,i]⇒i] ⇒ i"

We again skip ahead to see the corresponding rules: N is a type containing the element 0 and closed under successors. These last two facts take the form of introduction rules.

  NF:  "N type"
  NI0: "0 : N"
  NI_succ: "a : N ⟹ succ(a) : N"

The elimination rule for N takes the following form:

  NE: "⟦p: N; a: C(0); ⋀u v. ⟦u: N; v: C(u)⟧ ⟹ b(u,v): C(succ(u))⟧
       ⟹ rec(p, a, λu v. b(u,v)) : C(p)"

In more conventional notation it should be recognisable as mathematical induction, as it appears in the propositions-as-types paradigm.

Equality rules describe reductions or computations. Here, they tell us that rec provides primitive recursion. Given 0, it returns the base value, namely a:

  NC0:
   "⟦a: C(0); ⋀u v. ⟦u: N; v: C(u)⟧ ⟹ b(u,v): C(succ(u))⟧
   ⟹ rec(0, a, λu v. b(u,v)) = a : C(0)"

Given a successor value, rec makes a recursive call:

NC_succ:
   "⟦p: N;  a: C(0); ⋀u v. ⟦u: N; v: C(u)⟧ ⟹ b(u,v): C(succ(u))⟧ ⟹
   rec(succ(p), a, λu v. b(u,v)) = b(p, rec(p, a, λu v. b(u,v))) : C(succ(p))"

The disjoint union of two types

The disjoint union of two types is well known to many through functional programming or as the categorical notion of a pushout. An instance of this type is formed from two other types:

  PlusF: "⟦A type; B type⟧ ⟹ A+B type"

The introduction rules for this type create values by injecting into the left part or right part, respectively. The type for the opposite part must be well-formed:

  PlusI_inl: "⟦a : A; B type⟧ ⟹ inl(a) : A+B"
  PlusI_inr: "⟦A type; b : B⟧ ⟹ inr(b) : A+B"  

The elimination rule expects an instance of the union type and performs case analysis on whether the left or the right part is present:

PlusE:
    "⟦p: A+B;
      ⋀x. x:A ⟹ c(x): C(inl(x));
      ⋀y. y:B ⟹ d(y): C(inr(y)) ⟧ ⟹ when(p, λx. c(x), λy. d(y)) : C(p)"

Finally, the equality rules describe how this when operator is evaluated:

  PlusC_inl:
    "⟦a: A;
      ⋀x. x:A ⟹ c(x): C(inl(x));
      ⋀y. y:B ⟹ d(y): C(inr(y)) ⟧
    ⟹ when(inl(a), λx. c(x), λy. d(y)) = c(a) : C(inl(a))"

The rule for Inr is analogous. By the propositions-as-types principle, the disjoint union corresponds to disjunction and the elimination rule performs a logical case analysis.

The disjoint union of a family of types

To form a ∑-type you need to supply both a type $A$ and a family of types $B(x)$ indexed by elements of $A$:

  SumF:  "⟦A type; ⋀x. x:A ⟹ B(x) type⟧ ⟹ ∑x:A. B(x) type"

The ∑-type is sometimes called a dependent product because its elements are ordered pairs $\langle a,b \rangle$ where the type of $b$ may depend upon the value of $a$. (But just to be confusing, it is more often called the “dependent sum” type. This is incredibly annoying. And it’s wrong.) The introduction rule constructs such ordered pairs.

  SumI:  "⟦a : A; b : B(a)⟧ ⟹ <a,b> : ∑x:A. B(x)" 

The elimination rule reasons about an element of the Σ-type, which must be an ordered pair, in terms of the separate components x and y.

  SumE: "⟦p: ∑x:A. B(x); ⋀x y. ⟦x:A; y:B(x)⟧ ⟹ c(x,y): C(<x,y>)⟧
         ⟹ split(p, λx y. c(x,y)) : C(p)"

The equality rule describes the computation of this split operator, which takes a given pair and delivers the separate components to the function c:

  SumC: "⟦a: A;  b: B(a); ⋀x y. ⟦x:A; y:B(x)⟧ ⟹ c(x,y): C(<x,y>)⟧
    ⟹ split(<a,b>, λx y. c(x,y)) = c(a,b) : C(<a,b>)" 

According to propositions-as-types, a ∑-type corresponds to existential quantification. If the family $B(x)$ is just one single type $B$, the ∑-type degenerates to the Cartesian product $A\times B$, which corresponds to logical conjunction. It’s remarkable how one type can do so much!

The product of a family of types

A ∏-type is formed from an indexed family, similarly to a ∑-type. However, its elements are functions.

  ProdF: "⟦A type; ⋀x. x:A ⟹ B(x) type⟧ ⟹ ∏x:A. B(x) type"

The introduction rule forms an element of the ∏-type, given a dependent function: the type of the result may depend on the value of the argument. The sort of people who (incorrectly) refer to a ∑-type as a dependent sum may refer to a ∏-type as a dependent product (also incorrectly), although you can’t count on consistency here. If memory serves, this terminology is due to Robert Constable, who led the Nuprl project and wrote a lot of expository material about type theory. If you find yourself getting confused, just refer to “Pi and Sigma types”.

  ProdI: "⟦A type; ⋀x. x:A ⟹ b(x):B(x)⟧ ⟹ ❙λx. b(x) : ∏x:A. B(x)" 

The elimination rule takes a supplied function, an element of the ∏-type, and applies it to the given argument a. The result of this application has type B(a).

  ProdE:  "⟦p : ∏x:A. B(x); a : A⟧ ⟹ p`a : B(a)" 

The equality rule, given a well-typed function application, applies the function to its argument. This corresponds to β-reduction in the λ-calculus.

  ProdC: "⟦a : A; ⋀x. x:A ⟹ b(x) : B(x)⟧ ⟹ (❙λx. b(x)) ` a = b(a) : B(a)" 

According to propositions as types, a ∏-type corresponds to universal quantification. In its degenerate form (no dependence in $B$), it is the function type $A\to B$ and the inference rules are precisely those for implication. In particular, the elimination rule is modus ponens.

Equality types

The equality (or identity) types mediate between equality judgments $a=b:A$ and ordinary membership judgments. To form an equality type you need only a type $A$ and two expressions $a$ and $b$ belonging to type $A$. It expresses the proposition that $a$ and $b$ are equal when considered as elements of $A$. It is a principle of type theory that identity is regarded as being bound up with a type as opposed to being a property of $a$ and $b$ alone.

  EqF: "⟦A type; a : A; b : A⟧ ⟹ Eq(A,a,b) type" 

Whenever we possess an equality judgment, for example through a computation rule, the corresponding equality type can be introduced.

  EqI: "a = b : A ⟹ eq : Eq(A,a,b)" 

The type theory of 1982 is extensional. In particular, a proof of any identity however deep was collapsed down to a unique token, eq.

  EqE: "p : Eq(A,a,b) ⟹ a = b : A" 

And this eq is the only possible element of an equality type.

  EqC: "p : Eq(A,a,b) ⟹ p = eq : Eq(A,a,b)" 

To the objection that the equality type rules unreasonably destroy information, we have following response:

You seem to believe that every constructive mathematician means the same thing by “proof” that you do. In fact the word “proof’ as used in Martin-Löf’s systems means, the information that a computer would need to verify a statement.¹

This quote is said to be a paraphrase of a letter from Peter Aczel to Michael Beeson. And the claim is that there is no need for the complicated proof of an identity to be preserved in the elements of identity types, merely the fact of the identity itself, which is trivial to check by calculation in any particular instance.

The ability to erase the derivations of identities is powerful. It was the foundation of my early paper on well-founded recursion. I outlined an approach for constructing well-founded relations in order to prove the termination of almost any recursive function likely to arise in a computational context. The complicated proofs of the recursion equations would be erased by the elimination rule for the equality type. Similarly, the rewriting tactics that I devised for Isabelle/CTT relied on our ability to apply a chain of identities without having to store any details.

Boom!

Unfortunately, sometime towards the end of the 1980s I learned that the equality types had been reformulated to destroy this erasing property: and extensionality in general. Ever since (in most type theories apparently), a fundamental distinction must be made between $n+0=n$ and $0+n=n$ on natural numbers: one of them will hold by definition but the other only by induction. In the latter case, the equality will forever be second class, and $T(n+0)$ and $T(0+n)$ will be different types.

I am pretty sure that the rules for the intensional identity type could be entered in the Isabelle as straightforwardly as the other rules shown above. But I never saw the point of trying.

Next week, we’ll see the formalisation in action.