This post is part of a series on how to reason about code. It describes $\lambda C$, a precursor to the formal language understood by Coq, an interactive proof assistant I'm learning. Prior posts:

• first, long-ago post here
• a concrete example of symbolic execution
• why I'm interested in type theory
• the λ Calculus
• the Simply Typed Lambda Calculus
• $\lambda 2$
• $\lambda \underset{―}{\omega }$
• $\lambda P$

This exposition follows that in "Type Theory & Formal Proof" by Nederpelt & Geuvers (abbreviated TTFP throughout), with help from "Lambda Calculi with Types" by Henk Barendregt. Also recommended is the post A Guide to Typed Lambda Calculus.

In this series, we've introduced the λ Calculus as a formal model of general computation & we've added a type system ($\lambda \to$) to regularize the terms therein. $\lambda \to$ provided a strong normalization guarantee but was not very expressive. In truth, it had a number of other desirable properties, as well, but I never got into those. We've spent the past few posts exploring extensions to $\lambda \to$ that preserved those nice features while giving more expressiveness:

• $\lambda 2$
• $\lambda \underset{―}{\omega }$
• λ P

This post will bring those extensions together into a unified family of typed lambda calculii.

In some sense, $\lambda 2$, $\lambda \underset{―}{\omega }$ and $\lambda P$ are "independent" of one another. If $\lambda \to$ provides a system whose terms depend upon other terms…

• $\lambda 2$ provides terms depending on types, in that $\mathrm{\Lambda }\alpha :\ast .\lambda x:\alpha .x$ can only be used for computation after being applied to a type
• $\lambda \underset{―}{\omega }$ provides types depending on types, in that we can here build functions on types, such as $\lambda \alpha :\ast .\alpha \to \alpha$
• $\lambda P$ provides types depending on terms in the form of dependent types

Therefore, they can be combined at will: we can imagine a type system that provides terms depending on types and types depending on types, for instance. Barendregt, in "Lambda Calculi with Types" showed that all eight combinations could be expressed within a single unified system of derivation rules and laid them out on the λ-Cube (also known as the Barendregt Cube)¹:

Here, the system $\lambda \omega$ is a combination of $\lambda 2$ and $\lambda \underset{―}{\omega }$, $\lambda P2$ is a combination of $\lambda 2$ & $\lambda P$, $\lambda P\underset{―}{\omega }$ is a combination of $\lambda \underset{―}{\omega }$ & $\lambda P$, and, at the far corner, $\lambda C$ is a combination of all three.

Here is the unified set of derivation rules for the $\lambda$ Cube:

$$\begin{array}{rlr}& \mathbf{\text{(sort) }}& \mathrm{\varnothing }⊢\ast :◻\\ \\ & \mathbf{\text{(var) }}& \frac{\mathrm{\Gamma }⊢A:s}{\mathrm{\Gamma },x:A⊢x:A}\text{ if }x\notin \mathrm{\Gamma }\\ \\ & \mathbf{\text{(weak) }}& \frac{\mathrm{\Gamma }⊢A:B\mathrm{\Gamma }⊢C:s}{\mathrm{\Gamma },x:C⊢A:B}\text{ if }x\notin \mathrm{\Gamma }\\ \\ & \mathbf{\text{(form) }}& \frac{\mathrm{\Gamma }⊢A:s_1\mathrm{\Gamma },x:A⊢B:s_2}{\mathrm{\Gamma }⊢\mathrm{\Pi }.x:A.B:s_2}\\ \\ & \mathbf{\text{(appl) }}& \frac{\mathrm{\Gamma }⊢M:\mathrm{\Pi }x:A.B\mathrm{\Gamma }⊢N:A}{\mathrm{\Gamma }⊢MN:B[x:=N]}\\ \\ & \mathbf{\text{(abst) }}& \frac{\mathrm{\Gamma },x:A⊢M:B\mathrm{\Gamma }⊢\mathrm{\Pi }x:A.B:s}{\mathrm{\Gamma }⊢\lambda x:A.M:\mathrm{\Pi }x:A.B}\\ \\ \text{(1)}& & \mathbf{\text{(conv) }}& \frac{\mathrm{\Gamma }⊢A:B\mathrm{\Gamma }⊢B^{\prime }:s}{\mathrm{\Gamma }⊢A:B^{\prime }}\text{ if }B{\equiv }_{\beta }{B}^{\prime }\end{array}$$

Note in particular the (form) rule– this is the heart of the matter. We're now letting the sorts of both the variable being abstracted over and the abstraction body vary independently. By limiting the range of each term in the formation rule in different ways, we obtain the eight different type systems in the λ Cube. The following table displays the eight type systems along with the permissible values for $s_1,s_2$ in the formation rule:

Table 1: Type systems of the lambda cube

system
$\lambda \to$	(∗,∗)
$\lambda 2$	(∗,∗)	$(◻,\ast )$
$\lambda \underset{―}{\omega }$	(∗,∗)		$(◻,◻)$
$\lambda P$	(∗,∗)			$(\ast ,◻)$
$\lambda \omega$	(∗,∗)	$(◻,\ast )$	$(◻,◻)$
$\lambda P2$	(∗,∗)	$(◻,\ast )$		$(\ast ,◻)$
$\lambda P\underset{―}{\omega }$	(∗,∗)		$(◻,◻)$	$(\ast ,◻)$
$\lambda P\omega =\lambda C$	(∗,∗)	$(◻,\ast )$	$(◻,◻)$	$(\ast ,◻)$

Showing that the eight rules listed here reduce to those for each of the four type systems we've covered for appropriate choices of $s_1$ & $s_2$ is left as an exercise for the reader (see Remark 6.2.3 in TTFP for a sketch of the demonstration).

It should be noted that this is in no way a complete accounting of the type systems that have been built on top of the λ Calculus. In particular, the λ Cube itself has been generalized to Pure Type Systems (PTS) which allow an arbitrary number of sorts.

$\lambda C$, also known as the Calculus of Constructions, sits at the far end of the λ Cube. It was developed in the eighties by Thierry Coquand (one of the originators of the Coq proof assistant).

The easiest way to conceptualize $\lambda C$ itself is probably as an extension of $\lambda P$ by adding types depending on types. In terms of the formation rule, $s_1$ & $s_2$ are free to vary over $\{\ast ,◻\}$ independently.

Terms continue to be strongly normalizing. Well-typedness & type checking continue to be decidable, though term finding is undecidable (as it is everywhere outside $\lambda \to$ & $\lambda \underset{―}{\omega }$).

Unsurprisingly, $\lambda C$ is considerably more expressive than the systems we've seen so far. We can now encode predicate logic with not only implication & universal quantification, but negation, conjunction, disjunction and existential quantification as well.

I started this series of posts looking to understand Coq in terms of first principles. Since Coq is at heart a system for writing down terms in a certain formal language, I went back to the beginning: Church's λ Calculus. I worked from there in an exercise in the Feynman technique, and we're almost to Coq's formal language. Coq extends $\lambda C$ slightly to include inductive types in a system called the Calculus of Inductive Constructions.

It was only when we got to the last post that we were finally in a position to see exactly how "proof as term finding" actually worked, and I found myself wondering: why use type theory for this? I'm still not entirely clear, but it's undeniable that to date, the latter has been predominant in the development of proof assistants such as Coq.

Both approaches seem to date back to the early seventies; Mizar (which is based on set theory rather than type theory) dates back to 1973. Per TTFP: "The first system to actually use type theory to formalise mathematics was the Automath system, developed by N.G. de Bruijn and his research team in the early 1970s… There are various Automath type theories and several of them have been implemented as proof checkers."

The abovelinked MathOverflow question "What makes dependent type theory more suitable than set theory for proof assistants?" suggests that the real driver lies in the needs of the higher-level language that proof assistants use to define the mathematical objects about which the user is reasoning. This is generally known as the "vernacular", as opposed to the the smaller, simpler language used in the proof assistant kernel for proof checking. Because type theory can describe objects and sets with greater generality than set theory with predicate logic, the a proof assistant's vernacular almost has to be based on either type theory, or an extension to set theory with predicates that "looks a lot like type theory." At which point, "why bother with the set-theoretic kernel?"

Regardless, I think this post will wrap-up the series for a bit. A really complete treatment would show how we encode things like negation, conjunction & so forth in $\lambda C$, perhaps along with some more worked exercises in proof as term finding, but I think I got what I needed in the last post around $\lambda P$. My theoretical itch scratched, my plan now is to turn to the practical aspects of using Coq in anger.

05/28/24 18:30