Please note that Llama Labs is under construction!
This website is an attempt to organize and share what I've learned over the years about type theory and artificial intelligence (AI). It is also the home of some related software which can be downloaded and run on any Unix-compatible computer.
Here's what you'll find at Llama Labs:
| Expository essays (below) | An introduction to the ideas behind the project. |
| Llama Light | A general-purpose programming language. |
| Deductive Llama | Adds theorem proving to Llama Light. |
| Inductive Llama | Adds programming-by-example to Llama Light. |
Thanks for visiting! You can leave comments over at the wiki.
Type theory, a branch of logic, is the study of type systems. Most programmers are at least somewhat familiar with type systems, whether they realize it or not, as almost every programming language comes with some notion of a type. For example, in Java, there is a type system that includes integers and strings.
The most important type systems have set-theoretic interpretations. Therefore, I'll take a concrete approach (which isn't the usual one) and define a type system as a way of assigning names to some sets, and also to some elements of those sets. The set-names are called types; the element-names are called terms. Note that people aren't usually so careful to distinguish the sets from their names, and use the word "type" to refer to the sets themselves.
An important early type system is sometimes called simple type theory. In this system, as formulated by Alonzo Church (1940), a type is either the fixed set ι, or it is the set of all functions from one type to another. Church didn't specify the interpretation of ι, but it could, for example, be the set of integers. Furthermore, although Church's formulation only provided ι, simple type theory can include more than one fixed set.
The terms of simple type theory are almost as simple as the types. Among them are certain terms for defining functions, traditionally written with a syntax involving the letter λ. For example, the term "λx : ι. x" denotes the identity function on the type ι. Because of this syntax, simple type theory is also called the typed λ-calculus.
Hindley-Milner type theory extends simple type theory by adding variables that represent unspecified types. Thus, a Hindley-Milner type must in general be understood not as a set, but as a map from set-tuples to sets. In practice, Hindley-Milner is also taken to include "inductive types" such as Cartesian products, tagged unions, and lists.
There exist still fancier type systems, such as ones that include so-called dependent types, which I won't try to define here. These systems make essential use of a fascinating analogy between computer programs and mathematical proofs, known as the Curry-Howard correspondence.
Hindley-Milner has been called a "sweet spot" among type systems. It is the basis of many programming languages, including ML, Haskell, and Objective Caml. It is also the basis of the Llama systems.
Type theory is useful not only for programming but also for proving theorems. It is even possible to view type theory, rather than set theory, as the foundation of mathematics. However, I'll continue to treat type theory as a layer atop set theory.
To use Hindley-Milner type theory as a system of logic, one first observes that there is a boolean type whose terms may be viewed as mathematical propositions. Then one needs a notion of proof, i.e. a description of a recursively enumerable set of propositions which are taken to be provable. Such systems are known, rather imprecisely, as higher-order logic (HOL). An especially simple formulation of HOL is the underlying logic of the theorem prover HOL Light (as described, though incompletely, on Wikipedia).
It is natural to wish that all proofs could be expressed in higher-order logic. Unfortunately, in view of Kurt Gödel's famous incompleteness results, it is probable that no formal definition of proof can ever capture the informal notion perfectly. What can be said is that some logical systems are stronger than others. More can be proved in the stronger systems, but the weaker systems are more obviously sound.
The traditional foundation of mathematics is Zermelo-Fraenkel set theory with the axiom of choice (ZFC). Compared with this system, higher-order logic is a weak system whose soundness is relatively obvious, but in which less can be proved.
If the axiom of replacement is removed from ZFC, the resulting system is known as Zermelo set theory with choice. HOL is weaker even than this system. Relatedly, when HOL is interpreted in set theory, the sets involved need not be "large" in the foundational sense. They can all be smaller than N ∪ Pow(N) ∪ Pow(Pow(N)) ∪ ..., the countably iterated powerset of the natural numbers. As a cardinal, this set is denoted Vω+ω and is a stage of the so-called cumulative hierarchy.
It isn't clear whether HOL should be considered weak in an absolute sense. A great deal of ordinary mathematics does not require the axiom of replacement and can be proved within HOL. The best-known exception is probably the Borel determinacy theorem (which, if the replacement axiom were dropped, would no longer be a theorem). It has been suggested that such results are outside "ordinary mathematics"; however, this idea hasn't been generally accepted and it isn't clear that a meaningful boundary exists. The logician Harvey Friedman has found many ordinary-looking statements — including ones that involve only arithmetic — which may or may not be theorems, depending upon one's exact beliefs about sets.
The state of mathematical foundations thus arguably leaves something to be desired. Meanwhile, type theory appears to be extremely useful for developing actual formal proofs. The mathematician Freek Wiedijk maintains a list of 100 well-known theorems and keeps track of how many have been proved within various systems. HOL Light, having proved seventy-five, leads the rankings by a significant margin. Several of the other high-ranking systems are also based on HOL. And almost all of the systems use some flavor of type theory.
To be written.
...