## One λ-calculus, many times…

Previously, I mentioned that one of the most common posts on Agda blogs is implementing the simply-typed λ-calculus. Gergő Érdi even goes as far as to call it the FizzBuzz of dependently-typed programming, and rightfully so: If you do a quick search, you’ll find dozens of examples.

In *Dependently-Typed Programming with Agda*, Ulf Norell implements a type checker the simply-typed λ-calculus; Francesco Mazzoli more or less follows Ulf, but extends his λ-calculus with a primitive operator for addition; and, Gergő Érdi extends Ulf’s approach with a checker for scope and binding.

I figured it would be more fun if, instead of rewriting the type checker example, I would do something a little bit different. So for my λ-calculus post, I’ll have a look at kinds of different ways of implementing the simply-typed λ-calculus. Today, natural deduction and the sequent calculus.

### Natural Deduction and the λ-Calculus

We’ll start our discussion with the syntax of types. Usually, types are defined inductively over some set of atomic types. We don’t really care what these atomic types will be, so we might as well abstract over them:

module Syntax (Atom : Set) where

But, if it makes you feel better, we can pretend that they’ll be some like this:

data↓515"> Atom : Set where

Int : Atom

String : Atom

Next, we defined our types. Since we’re talking about minimal propositional logic, a type is either atomic (marked by El) or an implication:

infixr 6 _⇒_ data Type : Set where El : Atom → Type _⇒_ : Type → Type → Type

Now we’ll define sequents. Even though this is just a tiny piece of syntax, we should put some thought behind it…

Traditionally, the antecedent of some sequent would be a *set* of formulas. However, we’re looking at this from the perspective of λ-calculus, and there may well be a difference between two terms of the same type. This is usually solved by changing the antecedent to a set of *type assignments*, which means x:A and y:A are now distinct. From the logical perspective, this is the same as using a *bag* or *multiset* antecedent. If we were doing mathematics, we’d be done, but implementation-wise a bag is actually a rather complex beast. For this reason, we’ll use a *list*:^{1}

infix 4 _⊢_ data Sequent : Set where _⊢_ : List Type → Type → Sequent

So what does a *proof* of a sequent look like? The logical system that is most familiar to a computer scientist is probably *natural deduction*. The natural deduction system for minimal propositional logic has *three* rules:

\frac{A \in \Gamma}{\Gamma \vdash A}{\small ax} \quad \frac{A , \Gamma \vdash B}{\Gamma \vdash A \Rightarrow B}{\small{\Rightarrow}\!i} \quad \frac{\Gamma \vdash A \Rightarrow B \quad \Gamma \vdash A}{\Gamma \vdash B}{\small{\Rightarrow}\!e}

Recall that λ-terms are constructed in one of three ways: a λ-term is either a *variable*, an *abstraction* or an *application*:

M, N ::= x \mid (\lambda x . M) \mid (M\;N)

These correspond exactly to the rules of natural deduction. In fact, in type systems they are usually presented together:

\frac{(x : A) \in \Gamma}{\Gamma \vdash x : A} \quad \frac{x : A , \Gamma \vdash M : B}{\Gamma \vdash (\lambda x. M) : A \Rightarrow B} \quad \frac{\Gamma \vdash M : A \Rightarrow B \quad \Gamma \vdash N : A}{\Gamma \vdash (M\;N) : B}

However, I like the clean look of the logical notation, so in the interest of keeping things simple I will use that.

In what follows, we’ll use the following metavariables for types, contexts, and sequents. That means that if you see one of these names, and you can’t find a binding site, it’s implicitly bound at the top-level:

variable A B C : Type variable Γ Γ′ : List Type variable S : Sequent

We encode the natural deduction system as a datatype, with each rule corresponding to a *constructor*, and each proof a *value*:

infix 3 ND_ data ND_ : Sequent → Set where ax : A ∈ Γ → ND Γ ⊢ A ⇒i : ND A ∷ Γ ⊢ B → ND Γ ⊢ A ⇒ B ⇒e : ND Γ ⊢ A ⇒ B → ND Γ ⊢ A → ND Γ ⊢ B

Note: for the sake of brevity, I’m using an Agda notation in which implicit arguments are hidden. That means that any unbound variable—such as the As, Bs and \Gammas above—is implicitly universally quantified.

I prefer to think of things of the type ND as proofs made up of rules, but if you prefer to think of them as programs made up of the constructors of lambda terms, just use the following syntax:

pattern var x = ax x pattern lam x = ⇒i x pattern _∙_ f x = ⇒e f x

Earlier, we made the conscious choice to use *lists* to represent the antecedent. However, this introduced a minor problem: while two programs of the same type may not do the same thing, they *should* be equivalent, as far as the type system is concerned, and so it *should* be possible to rewrite a program which needs *two* values of type A to a program which needs only *one*.

Similarily, by using lists, we have introduced a fixed order in our antecedent which isn’t exactly desirable. While they may be different programs, we *should* be able to rewrite the program f : A \to B \to C to receive its arguments in the different order, i.e. to a program f\prime : B \to A \to C.

Collectively, such properties are known as *structural* properties, and for this particular logic we can summarise them neatly as follows:

If \Gamma \subseteq \Gamma\prime and \Gamma \vdash A, then \Gamma\prime \vdash A.

We can give a proof of this theorem by induction on the structure of natural deduction proofs. Note that we represent the subset relation as a *function*, that is to say \Gamma \subseteq \Gamma\prime is the *function* A\in\Gamma\to A\in\Gamma\prime:

struct : Γ ⊆ Γ′ → ND Γ ⊢ A → ND Γ′ ⊢ A struct Γ⊆Γ′ (ax x) = ax (lookup Γ⊆Γ′ x) struct Γ⊆Γ′ (⇒i f) = ⇒i (struct (++⁺ ⊆-refl Γ⊆Γ′) f) struct Γ⊆Γ′ (⇒e f g) = ⇒e (struct Γ⊆Γ′ f) (struct Γ⊆Γ′ g)

Note that values of type A\in\Gamma are constructed using here and there, which makes them more or less just numbers, i.e. “first value”, “second value”, etc…

I mentioned two uses of this structural rule: contracting two different variables of the *same* type into one, and exchanging the order of the types in the antecedent. There is one more canonical use: *weakning*.

Weakening is so obvious to programmers that they don’t really think of it, but what it says is that if you can run a program in *some* environment, then you should *certainly* be able to run that program in that enviroment with some irrelevant stuff added to it. Formally, we write it as:

w′ : ND Γ ⊢ B → ND A ∷ Γ ⊢ B w′ f = struct (++⁺ˡ _ ⊆-refl) f

Passing there to struct simply moves every value by one: the first value becomes the second, the second becomes the third, etc… In the new antecedent, the first value will be our “irrelevant stuff”.

### Sequent Calculus and Natural Deduction

We’ve got enough to start talking about the sequent calculus now. The sequent calculus is a different way of writing down logical systems, and it has some pros and cons when compared to natural deduction. It’s usual presentation is as follows:

\frac{A \in \Gamma}{\Gamma \vdash A}{\small ax} \quad \frac{\Gamma \vdash A \quad A , \Gamma \vdash B}{\Gamma \vdash B}{\small cut} \quad \frac{\Gamma \vdash A \quad B , \Gamma \vdash C}{A \Rightarrow B , \Gamma \vdash C}{\small{\Rightarrow}\!l} \quad \frac{A , \Gamma \vdash B}{\Gamma \vdash A \Rightarrow B}{\small{\Rightarrow}\!r}

We can encode these rules in Agda as follows:

infix 3 SC_ data SC_ : Sequent → Set where ax : A ∈ Γ → SC Γ ⊢ A cut : SC Γ ⊢ A → SC A ∷ Γ ⊢ B → SC Γ ⊢ B ⇒l : SC Γ ⊢ A → SC B ∷ Γ ⊢ C → SC A ⇒ B ∷ Γ ⊢ C ⇒r : SC A ∷ Γ ⊢ B → SC Γ ⊢ A ⇒ B

We will define a few patterns that we’d otherwise have to write out, over and over again. Namely, names for the first, second, and third variable in a context:

pattern ax₀ = ax (here refl) pattern ax₁ = ax (there (here refl)) pattern ax₂ = ax (there (there (here refl))) --- etc.

It’s a little bit of a puzzle, but given w′ it becomes quite easy to show that the two logics are in fact equivalent—that they derive the *same sequents*:

module ND⇔SC where ⟹ : ND S → SC S ⟹ (ax x) = ax x ⟹ (⇒i f) = ⇒r (⟹ f) ⟹ (⇒e f g) = cut (⟹ f) (⇒l (⟹ g) ax₀) ⟸ : SC S → ND S ⟸ (ax p) = ax p ⟸ (cut f g) = ⇒e (⇒i (⟸ g)) (⟸ f) ⟸ (⇒l f g) = w′ (⇒i (⟸ g)) ∙ (ax₀ ∙ w′ (⟸ f)) ⟸ (⇒r f) = ⇒i (⟸ f)

The rules for sequent calculus obviously no longer correspond *directly* to the λ-calculus. However, we’ve just shown that there is in fact *some* correspondence between them. In the λ-calculus, computation is represented by β-reduction, which is the iterative removal of redexes

(\lambda x.M)\; N\mapsto M[x := N]

Likewise, sequent calculus comes equipped with its own notion of computation: cut-elimination. And the beautiful thing about cut elimination is that it has a *very* concrete normal form. Instead of faffing about, claiming the structure is free of β-redexes, cut elimination—as its name implies—allows you to all occurances of the “cut” rule. It would be interesting to show exactly what kind of relation cut elimination has to β-reduction…

*Alas*! It may be too much effort for a single post to implement both of these logics *and* a procedure for cut elimination. However, there *is* a much simpler thing we can do. Agda itself has a pretty servicable implementation of β-reduction for Agda terms, and we can quite easily piggyback on that mechanism. In fact, most of the articles I linked to at the beginning do exactly this.

### Interpretations in Agda

As a first step, we write down what an interpretation is—and since we want to use the intepretation brackets in as many places as possible, we create a type class for it, and give ⟦_⟧ the least restrictive type possible:

record Interpret {a} {b} (A : Set a) (B : Set b) : Set (a ⊔ b) where field ⟦_⟧ : A → B open Interpret {{...}}

Now, in order to interpret natural deduction proofs in Agda, we’ll need an interpretation for the atomic types. Below we say as much:

module Semantics (Atom : Set) {{InterpretAtom : Interpret Atom Set}} where

Unsurprisingly, we interpret the implication as Agda’s function type:

instance InterpretType : Interpret Type Set InterpretType = record { ⟦_⟧ = ⟦_⟧′ } where ⟦_⟧′ : Type → Set ⟦ El A ⟧′ = ⟦ A ⟧ ⟦ A ⇒ B ⟧′ = ⟦ A ⟧′ → ⟦ B ⟧′

In order to interpret sequents, we’ll need an interpretation for the antecedent. For this we’ll create a type for *environments*, Env, which is indexed by a list of types, and which stores values of the *interpretations* of those types:

infixr 5 _∷_ data Env : List Type → Set where [] : Env [] _∷_ : ⟦ A ⟧ → Env Γ → Env (A ∷ Γ)

Using this, we can interpret sequents as functions from environments to values:

instance InterpretSequent : Interpret Sequent Set InterpretSequent = record { ⟦_⟧ = ⟦_⟧′ } where ⟦_⟧′ : Sequent → Set ⟦ Γ ⊢ A ⟧′ = Env Γ → ⟦ A ⟧

Let’s get to interpreting terms! First off, variables. We can interpret variables simply by looking them up in the environment:

lookup : A ∈ Γ → Env Γ → ⟦ A ⟧ lookup (here refl) (x ∷ _) = x lookup (there A∈Γ) (_ ∷ e) = lookup A∈Γ e

(If you’re wondering what we’re rewriting by: the here constructor carries a small proof that the element at the top of the list is *really* the element you were looking for.)

The translation for natural deduction proofs is, of course, completely routine—we translate variables withs lookups, introductions by abstractions and eliminations by applications:

instance InterpretND : Interpret (ND S) ⟦ S ⟧ InterpretND = record { ⟦_⟧ = ⟦_⟧′ } where ⟦_⟧′ : ND S → ⟦ S ⟧ ⟦ ax p ⟧′ e = lookup p e ⟦ ⇒i f ⟧′ e = λ x → ⟦ f ⟧′ (x ∷ e) ⟦ ⇒e f g ⟧′ e = (⟦ f ⟧′ e) (⟦ g ⟧′ e)

Hooray! And even better, as a corollary, we immediately obtain a translation from sequent calculus into Agda:

instance InterpretSC : Interpret (SC S) ⟦ S ⟧ InterpretSC = record { ⟦_⟧ = ⟦_⟧ ∘ ND⇔SC.⟸ }

Which means that we’ve now implemented the following functions:

\begin{array}{ccc} ND & \rightarrow & Agda \\ \\ \updownarrow \\ \\ SC \\ \end{array}

If you are looking for more reading on this topic, I can recommend the highly readible *Lambda terms for natural deduction, sequent calculus and cut elimination* by Henk Barendregt and Silvia Ghilezan.

Next time, I’ll talk about Gentzen’s LJ, which has explicit structural rules, and variations which use other, non-list structures as the antecedent.

This is a good time to note that I’m not showing any of the import statements. If you wish to see them, they’re there in the HTML source. However, it may be much easier to click the symbol that confuses you—that should take you directly to its definition in the standard library.↩︎