Computer Aided Formal Reasoning 1996/7 Lecture notes 2 Judith Underwood

Proofs and typed lambda-calculus

Last time we saw three proof rules:

Axiom :  \overline{G, A ⊢ A}

->introduction  \frac{G, A ⊢ B}{G ⊢ A->B}

                       ->elimination  \frac{G1 ⊢ A->B   G2 ⊢ A}{G1 ∪ G2 ⊢ B}

Today we will look at these rules and the proofs built out of them more carefully. We will develop another notation for proofs and show how to describe a process of proof simplification.

This time we will be a little more careful about how we treat the collection of assumptions G. We consider it to be a multiset, that is, a set which may have multiple copies of particular elements. A multiset is like a list, except that the order of the elements does not matter. In the ->elimination rule, we discharge (eliminate) one occurrence of A in the multiset of assumptions in the conclusion of the rule. There may be other occurrences of A still in the multiset of assumptions after this happens.

A proof is a tree of sequents connected by the rules above. (Recall that a sequent is something of the form G ⊢ A.) The leaves of the tree are instances of the axiom rule; inner nodes of the tree are created by applying the introduction and elimination rules to sequents which are themselves the conclusion of a proof. A somewhat more formal way of saying this is by giving an inductive definition of what a proof is and what it proves:

1. If A is in the multiset G, then G ⊢ A is a proof of G ⊢ A.

2. If ⋮ ; G, A ⊢ B is a proof of G,A ⊢ B, then ⋮ ; G, A ⊢ B ; G ⊢ A->B is a proof of G ⊢ A->B.

3. If ⋮ ; G1 ⊢ A->B is a proof of G1 ⊢ A->B and ⋮ ; G2 ⊢ A is a proof of G2 ⊢ A, then ⋮ ; G1 ⊢ A->B  ⋮ ; G2 ⊢ A G1 ∪ G2 ⊢ B

is a proof of G1 ∪ G2 ⊢ B. When taking the union of the two multisets, we may remove duplicates if we wish.

So, a proof of a sequent G ⊢ A is a tree built according to these rules such that the root of the tree is the sequent G ⊢ A.

When developing proofs, it is easiest to start with the root of the proof tree and build towards the leaves. Here is a proof of (P->Q->R)->(P->Q)->(P->R) (an exercise from last time):

P->(Q->R),P->Q,P ⊢ P->(Q->R)   P->(Q->R),P->Q,P ⊢ P
              P->(Q->R),P->Q,P ⊢ Q->R

                                                       P->(Q->R),P->Q,P ⊢ P->Q   P->(Q->R),P->Q,P ⊢ P

P->(Q->R),P->Q,P ⊢ Q P->(Q->R),P->Q,P ⊢ R P->(Q->R),P->Q ⊢ P->R P->(Q->R) ⊢ (P->Q)->(P->R)

⊢ (P->(Q->R))->(P->Q)->(P->R)

How did I come up with this proof? Well, I began with the conclusion:

                          ⊢ (P->(Q->R))->(P->Q)->(P->R)

It isn’t an axiom, so the only way to prove this is by either the ->introduction or ->elimination rules. Using ->elimination would require that I come up with some formula A such that I could prove A->((P->(Q->R))->(P->Q)->(P->R)) and also prove A; this seems difficult since I have no clue what A might be. Instead, let’s see what happens if I try to prove this with the ->introduction rule. I can apply the ->introduction rule if I have a proof of

                            P->(Q->R) ⊢ (P->Q)->(P->R)

so now I try to prove this. Using a similar argument, I use ->introduction backwards twice more until my goal is a proof of

                              P->(Q->R),P->Q,P ⊢ R.

Now I can’t use ->introduction anymore – I’ll have to prove this with ->elimination. But now I have some idea what could imply R – if I had both P and Q, I could prove R by using the assumption P->(Q->R) and the ->elimination rule twice. With a little thought I can see that I can prove both P and Q from the assumptions I have, though the proof of Q requires another use of ->elimination.

Later on in these notes I will show you how to do this example in Lego. First, though, we shall see a different notation for proofs. One motivation for this new notation is simply that writing out these trees is a pain in the neck. Another is that if we have a multiset of assumptions, it’s not clear which element of that set we’re referring to in the axiom rule, for example in P,P ⊢ P. Finally, this new notation will be better for describing the relationship between proofs, and the process of simplifying proofs by eliminating unneeded pairs of ->introduction/->elimination rules.

Before we introduce the notation, we will look a bit more closely at the idea of proof simplification. Last time, we saw that we could have multiple proofs for a single formula. Here are two proofs of the formula B->B.

                                     \begin{matrix}B ⊢ B \\ ⊢ B->B \end{matrix}

                              A->A,B ⊢ B
                              A->A ⊢ B->B
                            ⊢ (A->A)->(B->B)

                                               \begin{matrix}A ⊢ A \\ ⊢ A->A \end{matrix}

                                      ⊢ B->B

In this second proof, the ->introduction rule which creates the formula (A->A)->(B->B) is unnecessary, as it is eliminated immediately because we have a closed proof of A->A. Notice that we can’t simplify this by just cutting off the last steps, as this would leave us with the proof

                                   A->A,B ⊢ B
                                  A->A ⊢ B->B

which does not prove ⊢ B->B. We want to represent the fact that we can get rid of the assumption A->A because we have a proof of it given by the other branch. This proof should reduce to

                                     \begin{matrix}B ⊢ B \\ ⊢ B->B \end{matrix}

In this proof, we haven’t actually used the assumption A->A to prove B, so we know we can throw it away. In general, though, we may have the situation:

                               ⋮ . ; G1,A ⊢ B ; G1 ⊢ A->B  G2 ⊢ A
                                  G1 ∪ G2 ⊢ B

We want to eliminate the introduction/elimination rule pair by replacing the assumption A on the left branch with its proof from the right branch, wherever it occurs. If the proof of A has some assumptions G2, we will have to add these to the assumptions to the assumptions in the proof of B from A, which will leave us with the proof

                                  ⋮ . ; G1 ∪ G2 ⊢ B

The idea is that wherever we had

                                    G, A ⊢ A

in the proof on the left branch, we can replace it with

                                   G, G2 ⊢ A,

that is, the proof of A from assumptions G2.

Now, although we may have many different proofs for a single formula, we may wish to consider that two proofs are related if we can transform one into the other, or transform both into some common form, by these reductions. In order to do this, we will have to define these reductions more formally. This is possible but tedious, mostly because the notation we have for proofs is difficult to manipulate. There is a great deal of redundant information in a proof tree, and the tree structure itself is somewhat unwieldy.

So, let us look at a more concise notation for proofs. The main ideas of this notation are:

1. Instead of repeating the list of assumptions at each step, introduce each assumption once. If we wish to assume a single formula A more than once, we must introduce it explicitly each time, with a label so that we can keep track of which one we use.

2. Instead of an explicit tree structure for a proof, build terms which have the tree structure implicit in their parse trees.

We show how to do this by showing how each proof construction rule builds a proof term which represents the proof of the conclusion from the assumptions.

First, consider the axiom rule. We will label all the assumptions with letters x, y, z .... Then, when we use an axiom rule, we will specify which assumption justifies the conclusion if we have more than one copy of an assumption. So, we may have axioms like x:P,y:P ⊢ x:P. The proof term for the conclusion P is just x.

Next, we consider the ->introduction rule. Suppose we have a proof of

                                A1, ...An, A ⊢ B

and we wish to produce a proof of

                                A1, ...An ⊢ A->B

First, we label all the assumptions, and we assume we have some term b describing the proof of B from these assumptions. In other words, the sequent now looks like:

                           x1:A1, ...xn:An, y:A ⊢ b:B

We need a notation which describes the fact that we have used the ->introduction rule. We will also want to eliminate the assumption y:A. But we may have used y in the proof b of B, so we cannot forget it altogether – we must augment the proof of b to show that the assumption A we had has now been discharged and made part of the formula proved. We will do this by creating a new proof term for the formula A->B which looks like [y:A]b. So, our proof rule, combined with the term-building rule, is

                        \frac{x1:A1, ...xn:An , y:A ⊢ b:B}{x1:A1, ...xn:An ⊢ [y:A]b :  A->B}

We do something similar for ->elimination:

               \frac{x1:A1, ...xn:An ⊢ s:  A->B   x1:A1, ...xn:An ⊢ t:A}{x1:A1, ...xn:An ⊢ st:B}

This says that we glue together the proof s (of A->B) and the proof t (of A) to make a proof of B simply by joining the two proof terms into st. We may put parentheses around s (and possibly t) for clarity, so the proof term may look like (s)t.

We can look at these rules in two ways. First, we can view them as describing how to build proof terms which represent proofs in implicational logic. However, we can also view them as describing typing judgements for terms – considering the assumed formulas as types and the labels for them as variables of that type, these rules describe how to build correctly typed terms from the variables given. So, our proof terms can be viewed as well-typed terms in some language. Below, we will look at this language more carefully and see that it can be viewed as a programming language.

Let us go back to our example, and augment it with proof terms:

                      f:A->A,y:B ⊢ y:B

                   f:A->A ⊢ [y:B]y :  B->B
              ⊢ [f:A->A][y:B]y :  (A->A)->(B->B)

                                                      x:A ⊢ x:A

                                                   ⊢ [x:A]x :  A->A
                        ⊢ ([f:A->A][y:B]y)([x:A]x) :  B->B

The whole proof can be reconstructed from just the proof term in last line:

                        ⊢ ([f:A->A][y:B]y)([x:A]x) :  B->B

The reduction we wanted to perform may now be clearer – we wish to substitute the actual proof [x:A]x of A->A for the assumption f : A->A everywhere it occurs in the proof of B->B. Since it doesn’t occur anywhere, the substitution leaves us with

                                 ⊢ [y:B]y :  B->B

which corresponds to the proof

                                   y:B ⊢ y:B
                                 ⊢ [y:B]y :  B->B

So, we want to be able to reduce a proof of the form ([f:A->A][y:B]y)([x:A]x) to [y:B]y. Let’s rewrite our notation a little bit – instead of [z:P]t, I’ll write λz^{P} .t. This makes our complicated proof term (λf^{A→A}.λy^{B}.y)(λx^{A}.x) and the simple one λy^{B}.y. Now those familiar with λ-calculus can see that the rewriting rule

(λf^{A→A}.λy^{B}.y)(λx^{A}.x) ⟶ λy^{B}.y

is just an example of applying β reduction in typed λ-calculus. In general, we will see that a proof of a formula A describes a λ term with type A, and we may consider that proofs compute in the same way that λ terms do.

Typed lambda-calculus

This section may be review for some of you. I will not go into the λ-calculus in great depth – the goal is to explain how λ-calculus works as a computation system. I’ll retain the Lego notation ([x:A]x instead of λx^{A}.x), but you should be aware that the other notation is the standard. (Lego doesn’t use it because λ isn’t on our keyboards.)

Just as we have been studying reasoning without reference to what we are reasoning about, λ-calculus at first looks like programming without using data. (It turns out that you can represent data in λ-calculus, so it’s not quite as bad as it seems.) When data has been abstracted away, what is left is the creation and application of functions. A function is created by specifying what its arguments are, and then by giving an expression which describes what happens to those arguments when the function is applied. Application involves substituting actual arguments for the variables which stand for them in the function definition. The λ calculus is a formal notation for this kind of abstract programming.

The mechanism for function definition is called λ abstraction. Given an expression made up of variables, λ abstraction turns one of the variables into a parameter representing an argument to the function. For example, if the expression consists of the single variable x, then the λ-abstraction [x:A]x (read “lambda x (of type A) dot x”) is the function which returns its argument – the identity function. We can abstract a variable which doesn’t actually appear; for example, [x:A]y represents a function which ignores its argument and returns y.

A function is applied by substituting an argument for the variable name in the body of the λ abstraction. So, applying the function [x:A]x to an argument z results in z – the body of the abstraction (x) with z substituted for x. An argument may be another function, or other more complex expression.

The basic computational building block of λ-calculus is the evaluation of function application, and each step of substituting an argument for a variable is called β-reduction. Performing this substitution is a bit trickier than you might think at first. For example, suppose we want to substitute x for y in the term [x:A]y. Naively, this would leave us with [x:A]x. But this describes a function which returns its argument, rather than a function which returns a constant (which was earlier called y and which we now want to call x). The variable x changes its role from constant to parameter when it is substituted inside a term [x:A].... This unintended change is called capture, and the rules of substitution are carefully defined to avoid it.

We need some definitions to clarify the roles of the variables in a term.

The free variables of a term t, denoted FV(t), are defined as follows:

FV(x)  = x
FV([x:A] m) = FV(m) -{x}
FV(m n)  = FV(m) ∪ FV(n)

If a variable in a term is not free, it is called bound. Bound variables are created by λabstractions, i.e. terms like [x:A]m. For example, in the term [x:A]yx, x is bound but y is free. (Hence the term capture – a variable is captured if it was free but becomes bound.) You can think of a bound variable as representing a placeholder for a function’s argument; while we define the body of a function, the argument can be thought of as a constant, but in order to make a function which can be applied, we make the argument into a parameter. Thus, evaluating a function application should substitute the argument for the bound variable in the function definition wherever it occurs. However, we must avoid accidentally capturing any free variables in the argument.

Here are the rules for substitution. The notation is m[n/x], which means m with n substituted for x.

    x[n/x]          =  n
    y[n/x]          =  y  if y≠x
    (m m') [n/x]    =  (m[n/x] ) (m'[n/x] )
    ([x:A] m)[n/x]  =  [x:A] m
    ([y:A] m)[n/x]  =  [y:A] (m[n/x] )  if y≠x and y is not in FV(n)
    ([y:A] m)[n/x]  =  ([z:A] m[z/y])[n/x] if y is in FV(n)

and z is not in FV(m) or FV(n)

The last rule is the one which avoids capture of free occurrences of y in n by renaming the bound variable y to z in [y:A]m. Renaming of bound variables is called α-conversion; terms which are the same except for choice of variable names are called α-equivalent. Generally we’ll think of α-equivalent terms as being identical.

Finally, we can now define β-reduction, or evaluation of function application, by the following rewrite rule:

                              ([x:A]m)a ⟶ m[a/x]

Notice that I haven’t made any reference to the formulas (or types) attached to the variables in these reduction rules. Types do not affect reduction directly; however, having a well-typed term (one in which the types of the bound variables and the arguments substituted for them are always the same) means that you can guarantee certain nice properties of reduction. Proof terms are always well-typed, and indeed every well-typed term is a proof term.

Some facts about β-reduction of well-typed terms:

• Reduction of a term does not change its type. In proof language, reducing a proof does not change the formula which has been proved. This property is called subject reduction.

• You may have several choice of reductions to make within a term. No matter which reductions you choose, eventually you will run out – you cannot reduce forever. In other words, every reduction sequence terminates. This property is called strong normalization. (Weak normalization says that there is some reduction sequence which terminates.) A term which cannot be reduced is said to be in normal form.

• No matter which sequence of reductions you choose for a term, you will always end up with the same normal form. This property is called uniqueness of normal form, and is a consequence of more general properties called confluence, or the Church-Rosser property. (Some people use these last two words to mean slightly different things, some use them as synonyms.)

As the course develops, we’ll see how λ-calculus can be used as a programming language, especially when we extend the type system a bit. Next time, though, we’ll concentrate on the λ calculus as a proof term language, and see how to add and and or to the logic.

Example: Church numerals

I mentioned above that data could be embedded in λ calculus. As it happens, untyped λ calculus is a Turing complete computation system – anything you can compute with Turing machines can be computed in untyped λ calculus. Typed λ calculus is more restrictive, but even in the simple version we have here, we can do some arithmetic on natural numbers.

First, we need definitions for the numbers as λ-terms. We use Church numerals, which are defined as follows:

                           0  =  [f:A->A][x:A]x
                           1  =  [f:A->A][x:A]fx
                           2  =  [f:A->A][x:A]f(fx)
                           3  =  [f:A->A][x:A]f(f(fx))

and so on. Notice that each numeral is a function which takes two arguments – a function f and an argument to that function x. The numeral for n describes the fact that f is applied to x n times. The type of each numeral is (A->A)->A->A. Let us call this type N.

The successor function is:

succ = [n:N][f:A->A][x:A]f (n f x)

Addition and multiplication are defined by:

plus = [n1:N][n2:N][f:A->A][x:A] n1 f (n2 f x)
times = [n1:N][n2:N][f:A->A][x:A] (n1 (n2 f)) x

Exercises: These exercises will give you some practice in working with reduction in typed λ calculus.

1. Check that plus and times are really functions which take two arguments of type N and produce something of type N. (Remember, N = (A->A)->A->A.)

2. Calculate 2 times 2 using Church numerals.

3. Calculate 2 plus 1 using Church numerals.

4. Calculate 1 plus 2 using Church numerals.

Getting started in Lego

Writing out complete formal proofs on paper is fairly tedious, particularly since it involves copying formulas over and over again. The examples and exercises I’ve given you are just about the biggest ones you ever want to do by hand. However, given a tool to help you keep track of what you need to prove and what your assumptions are, it is easier to do larger proofs.

Lego is just such a tool. In today’s notes I’ll try to give you enough information to enable you to get started; over the course of the term, you should become fairly accomplished Lego users.

It is recommended that you use Lego in conjunction with Emacs. By using Emacs to edit a file ending in “.l”, you will automatically start Emacs’s Lego mode. To find out how to start Lego, see “Getting Started with LEGO” on the course’s web page. This document contains a pointer to a file containing the example proof given below, and instructions on how to interact with Lego.

Once you have Lego up and running, you can build your own proofs. The main proof-building commands are Refine and intros. In this case, an example is worth a thousand words, so let’s see how to prove (P->Q ->R) ->(P->Q)->(P->R) (an exercise from last time, and also an example given earlier).

First, we must declare P, Q, and R as propositional variables:

Lego> [P,Q,R:Prop];
[P,Q,R:Prop];
decl  P Q R : Prop

Lego> is Lego’s prompt. Note that the declaration ends with a semicolon, as do all commands. Now we state the formula we want to prove:

Lego> Goal (P->Q->R)->(P->Q)->(P->R);
Goal
  ?0 : (P->Q->R)->(P->Q)->P->R

Lego has labelled the goal ?0. In order to prove an implication, we use the ->introduction rule. The Lego syntax for this is “intros”. We can either provide a name for the assumption introduced, or Lego will make up a name itself (usually H or some variation of it). Here we provide the name

x:
Lego> intros x;
intros (1) x
  x : P->Q->R
  ?1 : (P->Q)->P->R

Now we have the assumption P->Q->R, which has the label x. We no longer have the goal ?0 – it has been replaced by the goal ?1 : (P->Q)->P->R. In sequent form, we have replaced

                         ⊢ ?0 :  (P->Q->R)->(P->Q)->P->R

with

                        x :  P->Q->R ⊢ ?1 :  (P->Q)->P->R,

which is just the ->introduction rule upside down. Having ?1 instead of a proof term describes the fact that this proof is incomplete.

Again, the only rule we can apply is ->-introduction:

Lego> intros y;
intros (1) y
  y : P->Q
  ?2 : P->R
Lego> intros z;
intros (1) z
  z : P
  ?3 : R

Although they are not displayed each time, we still have the assumptions x : P->Q->R and y : P->Q. (Assumptions are present until discharged, and Lego tells us when an assumption is discharged.) We can check this with the command Prf which shows us the current state:

Lego> Prf;
  x : P->Q->R
  y : P->Q
  z : P
  ?3 : R

Now we need to produce a proof of R. The only way we have to do this is to use ->-elimination with x : P->Q->R and a proof of P, leaving Q->R, and then again with a proof of R. We can give Lego the function part of the ->-elimination rule using the command Refine, and it will give us the arguments as subgoals:

Lego> Refine x;
Refine by  x
  ?4 : P
  ?5 : Q

Now we have two subgoals, ?4 : P and ?5 : Q. By default, we work with the lowest-numbered (first-listed) current subgoal, in this case ?4 : P. We still have the assumption z : P, which we use to prove the current goal, again with the command Refine:

Lego> Refine z;
Refine by  z
  ?5 : Q

We do the same thing again to get a proof of Q:

Lego> Refine y;
Refine by  y
  ?6 : P
Lego> Refine z;
Refine by  z
Discharge..  z
Discharge..  y
Discharge..  x
*** QED ***

And we’re done. Lego checks that we’ve finished everything and builds the proof term. Notice that the assumptions are discharged; this happens when the ->-introduction rule is applied forwards, building the λ-abstraction in the process.

We can save the theorem by giving it a name:

Lego> Save example;
Save example;
"example"  saved as global

Now if we wish to use this theorem, say, in another proof, we can refer to it by its name. Typically, this would be part of a refinement step. We can review both the statement and proof of the theorem by just typing its name:

Lego> example;
example;
value of example = [x:P->Q->R][y:P->Q][z:P]x z (y z)
type  of example = (P->Q->R)->(P->Q)->P->R

Note that the value of example is the proof term which describes the whole proof, and its type is the formula we proved.

This proof was somewhat long since I wanted to explain every step. Here is a shorter version:

Lego> Goal example:(P->Q->R)->(P->Q)->P->R;
Goal
  ?0 : (P->Q->R)->(P->Q)->P->R
Lego> intros x y z;
intros x y z;
intros (3) x y z
  x : P->Q->R
  y : P->Q
  z : P
  ?1 : R
Lego> Refine x z (y z);
Refine x z (y z);
Refine by  x z (y z)
Discharge..  z y x
*** QED ***
Lego> Save;
"example"  saved as global

This time, I gave the proof a name at the start instead of when I saved it. If you give your proofs descriptive names, this makes it easier to make the connection between the intended meaning of the theorem and its formal statement.

In this proof, I did all the intros in one step, and I supplied the whole proof of R from the assumptions in one use of Refine. Refine may seem mysterious right now, but if you experiment a bit you will be able to do the examples and exercises. We will learn more about what Refine really does later on in the course.

Exercises: Do all the exercise proofs from lecture notes 1 in Lego.

Exercise: Prove (A->A)->(B->B) and A->A separately in Lego, and save the proofs by giving them names. Then prove B->B by combining the two proofs, using their names.

The Lego command Normal applies reductions to its argument until a normal form is reached. The command Hnf applies reductions at the top level only (not within a term) until the top level constructor is not an application.

Exercise: Try reducing the proof of B->B from the previous exercise.