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

Lego exercises due 30 October: I have put the first set of Lego exercises on the course web page at

http://www.dcs.ed.ac.uk/home/lego/html/CAFR/96-97/exercises.html.

Propositional Logic II

Let us look at the logic we defined last time from a slightly different perspective. Last time, we began with proofs and extracting proof terms which look like λ calculus. This time, we begin with a definition the simply typed λ calculus, and then augment it with operators to deal with pairing and disjoint union types. So, instead of thinking of rules as building a proof terms for a formula, we will think of them as justifying the type given to a λ-term. Nevertheless, the rules will remain the same. Remember the slogans – “Proofs as programs” and “Propositions as types”.

Simply typed lambda calculus

We assume we have a collection of type variables (e.g. P, Q, R). Types are constructed from variables according to the grammar

A = P  (P a variable)
| A->A

This is essentially an inductive definition which says that a type is either a variable, or two types connected by an arrow. We will use the letters A, B, ... to stand for arbitrary types.

We also assume we have a collection V of term variables (e.g. x, y, z). The collection of welltyped terms is defined (inductively) according to the following rules, where G is a set of assumptions about the assignments of types to terms (e.g. x:P, y:Q, ...), and M and N are well-typed terms:

                                   \overline{G, x:A ⊢ x:A}

                \frac{G, x:A ⊢ M:B}{G ⊢ [x:A]M :A->B}          \frac{G ⊢ M: A->B    G ⊢ N: A}{G ⊢ M N:B}

A closed term of type A is a term M such that we can use these rules to conclude

                                      ⊢ M:A

The reduction rule for terms is

                              ([x:P]M) N ⟶ M[N/x]

where M[N/x] is M with N substituted for x, as describe in lecture notes 2.

Here are a couple of sample derivations:

                                  x:P,y:Q ⊢ x:P
                                x:P ⊢ [y:Q]x:Q->P
                             ⊢ [x:P][y:Q]x:P->(Q->P)

This derivation shows that the term [x:P][y:Q]x has type P->(Q->P). This is a special term, so we will give it a name:

                                 K = [x:P][y:Q]x
                               K has type P->(Q->P).

In the next derivation, let G be an abbreviation for f:P->(Q->R),g:P->Q,x:P .

                 G ⊢ f:P->(Q->R)  G ⊢ x:P

                      G ⊢ f x :  Q->R

                                           G ⊢ g:P->Q   G ⊢ x:P
                                               G ⊢ (g x):  Q
                                 G ⊢ f x (g x):R

                  f:  P->(Q->R), g:P->Q ⊢ [x:P] f x (g x):  P->R
              f:P->(Q->R) ⊢ [g:P->Q ][x:P] f x (g x):(P->Q)->(P->R)

      ⊢ [f:P->(Q->R)][g:P->Q ][x:P] f x (g x):  (P->(Q->R))->(P->Q)->(P->R)

Call this term S:

                    S = [f:P->(Q->R)][g:P->Q ][x:P] f x (g x)

The derivation shows that

                      S has type (P->(Q->R))->(P->Q)->(P->R).

Logical interpretation of S and K

These two terms, S and K, are special because their types, taken as general schemas, form a basis for all of implicational logic (or at least implicational constructive logic). An axiom schema is a description of a pattern which axioms follow; for example, P->(Q->P) and (P->R)->(Q->(P->R)) are both instances of the axiom schema A->(B->A). (You can think of the variables in an axiom schema as being universally quantified and ranging over all propositions, if you know what this means. If not, there’s an informal introduction later in these notes.)

   Now if we take as axiom schemas A->(B->A) and (A->(B->C))->(A->B)->(A->C), then, by

combining instances of these axioms using modus ponens, we can prove the same implicational formulas that we could prove using the proof system presented last time. (Recall that modus ponens is the rule which says “From A->B and A, conclude B.) As a consequence, since application is the computational equivalent of modus ponens all closed typed λ terms can be expressed as a sequence of applications of instances of S and K, eg.

                                  [x:P]x = SKK

Proof systems which are based on having a list of axioms which are combined with modus ponens are called Hilbert systems. Hilbert, as one of the founders of formalism, thought this was the best way to describe formal systems.

Exercise: Use the reduction rule to check the assertion that [x:P]x:P->P is equivalent to SKK. You will have to choose appropriate instantiations for the type variables in the types of S and K.

Terms like S and K (which are called combinators) are used in some implementations of lazy functional programming languages. You can think of a program which only does S and K reductions as a virtual RISC (Reduced Instruction Set Computer) for lambda calculus.

It is generally easier for us to think of lambda terms as themselves rather than as combinations of S and K, so we will continue to write terms such as [x:P]x.

Additions to simply typed lambda calculus

Let us now extend the calculus by adding a new constant type absurd and two new type constructors and and or. Instead of rules, we add new function constants to the language and give reduction rules for terms involving those functions.

The functions, and their types, are:

pair : P -> Q -> and P Q
fst : and P Q -> P
snd : and P Q -> Q
inl : P -> or P Q
inr : Q -> or P Q
or_elim : (or P Q) -> (P->R) -> (Q->R) -> R
absurd_elim : absurd -> P

These types are really type schemas – we may substitute other types for P, Q and R as desired. We add the following new reduction rules:

fst (pair x y) --> x
snd (pair x y) --> y
or_elim (inl x) f g --> f x
or_elim (inr x) f g --> g x

There is no reduction rule for absurd elim.

Looking at this as a logic, we have added seven axiom schemas, corresponding to the type schemas for the new functions. We can think of the functions as labels for which axiom is being used; applying one of these functions to an argument represents the use of modus ponens to produce a result. (We could make this explicit by adding another constant, apply, to denote use of modus ponens, but application is so fundamental that this would just make a mess.)

We can bring this idea into the derivation system for terms described above by adding seven new axiom schemas:

    ⊢ pair :  A ->B ->and A B
    ⊢ fst:  and A B ->A
    ⊢ snd:  and A B ->B
    ⊢ inl:  A ->or A B
    ⊢ inr:  B ->or A B
    ⊢ or elim:(or A B)->(A->C)->(B->C) ->C
    ⊢ absurd elim:absurd ->A

Thus we may now have derivations like:

          ⊢ inl:P ->(or P Q)

                             ⊢ fst:(and P Q)->P   x:and P Q ⊢ x:and P Q

                                        x:and P Q ⊢ (fst x):P
                    x:and P Q ⊢ inl (fst x):or P Q
               ⊢ [x:and P Q]inl (fst x):and P Q ->or P Q

The types and terms of this language are exactly the same as the types and terms of the proof term language presented in previous lecture notes. Only the shape of the derivations is different. In this system functions like pair are considered as the computational representation of an axiom, whereas, in the system presented last time, pair described the rule which was applied.

From axiom schemas to axioms

We are slowly moving towards adding quantifiers to the logic, so that we can form statements like “for all x… ” and “there exists y. …” Informally, this shouldn’t be too hard to understand, but in a formal system quantification brings up all kinds of issues. So, we will defer most of the formal quantifier rules for a few lectures, and just treat them somewhat informally for now.

Above, I talked about using axiom schemes to represent a family of axioms following some pattern. For example, consider the axiom schemes:

                             pair:  A ->B ->and A B
                             fst:  and A B ->A
                             snd:  and A B ->B

We can look at these in two ways: as a (logical) list of axiom schemes together with names for them, or as programming language constructs which can be given types of a particular pattern.

Looking first at the programming language interpretation, we would really like a more formal way of saying that there is a family of pair operations, one for every type following the pattern A ->B ->and A B, with corresponding fst and snd operations for each choice of A and B. A function like pair is called polymorphic; it can be applied to arguments of many types. To describe this, we introduce type variables, variables which range over types (as opposed to variables which range over terms of a given type.) We will generally use capital letters (A, B, C) to denote type variables. (Note that this agrees with “propositions as types” – we have been using A, B, C to range over propositions.) These will now be part of our term language.

We can fit the idea of a family of pairing functions into our functional framework if we think of pair as a function which first takes two types as arguments, and then returns a pairing function of the appropriate type, so that

                            pair A B: A ->B ->and A B

i.e. the first two arguments determine the type of the resulting function.

To express the type of this version of pair, we can say

                         pair : ∀A ∀B. A ->B ->and A B.

In other words, for all types A and B, we have a pairing function of type A ->B ->and A B. The Lego notation for this is

                          {A:Prop}{B:Prop}A->B->and A B

(usually simplified to {A,B:Prop}A->B->and A B.) This is just another way of describing a function type – the type A->B is the same as {x:A}B if B does not contain x. In the case of pair, the type of the result depends on the arguments A and B, so we must preserve their names.

An element of this type (i.e. a pairing function) would look like:

              [A:Prop][B:Prop][x:A][y:B] (something which pairs x and y)

We can treat all the other axiom schemes above in the same way, and this is how Lego does it. If you check the definition of pair in Lego, its type is {A,B|Prop}A->B->and A B. The use of the bar (|) in {A,B|Prop} instead of the colon (:) in {A,B:Prop} means that you don’t usually need to give these arguments to pair explicitly; Lego will try to work them out on its own from the types of the other arguments. If it can’t, it will prompt you to supply the types explicitly.

Universal quantification rules

We can make this more precise by adding introduction and elimination rules for quantified formulas. This is more complicated than it appears – to do this correctly, we would have to roughly double the number of rules we already have. We will do this eventually; however, the following rules should give you the basic idea.

We extend the set of assumptions G to include assumptions of the form A: Prop for propositional variables. Until now, this kind of assumption has been implicit in the formal system, but now we explicitly declare all propositional variables. In Lego, we have already seen this – the declarations like [A,B:Prop] are global versions of these assumptions.

Given such assumptions, the rules for introducing and eliminating the universal quantifier are:

                             \frac{G, A:Prop ⊢ M:B}{G ⊢ [A:Prop]M :\{A:Prop\}B}

                         \frac{G ⊢ M: \{x:Prop\}B    G ⊢ N: Prop}{G ⊢ M N:B[N/x]}

The first rule allows us to create quantified formulas. The propositional variable A will generally appear in the formula B, but this is not necessary. The formula A may also appear in M. Using the rules we’ve seen so far, it can only appear as the type of a variable abstracted by the ->- introduction rule, but later on this will become more general.

Example:

                              A : Prop, x:A ⊢ x :  A
                             A : Prop ⊢ [x:A]x :  A->A
                         ⊢ [A:Prop][x:A]x : {A:Prop}A->A

The second rule allows us to instantiate a quantified formula by substituting a particular proposition for the propositional variable. To be complete, we would have to add more rules for proving statements of the form A: Prop, for example:

                            \frac{G ⊢ A: Prop   G ⊢ B: Prop}{G ⊢ and A B: Prop}

but for now we won’t worry about this.

Example:

                B :Prop ⊢ B:Prop

                                      A : Prop, x:A ⊢ x :  A
                                     A : Prop ⊢ [x:A]x :  A->A
                                  ⊢ [A:Prop][x:A]x : {A:Prop}A->A
                        B : Prop ⊢ ([A:Prop][x:A]x)B : B->B

Notice that the substitution takes place immediately in the proved formula, but not in the proof term itself.

Just as the rules for ->introduction and elimination are represented in Lego by intros and Refine, so are the rules for universal quantification. Here are the examples above in Lego:

Lego> Goal {A:Prop}A->A;
Goal
  ?0 : {A:Prop}A->A
Lego> intros;
intros (2)
  A : Prop
  H : A
  ?1 : A
Lego> Refine H;
Refine by  H
Discharge..  H A
*** QED ***
Lego> Save Ident;
"Ident"  saved as global, unfrozen
Lego> Ident;
value of Ident = [A:Prop][H:A]H
type  of Ident = {A:Prop}A->A
Lego> Goal {B:Prop}B->B;
Goal
  ?0 : {B:Prop}B->B
Lego> intros B;
intros (1) B
  B : Prop

  ?1 : B->B
Lego> Refine Ident B;
Refine by  Ident B
Discharge..  B
*** QED ***
Lego> Save Ident2;
"Ident2"  saved as global, unfrozen
Lego> Ident2;
value of Ident2 = [B:Prop]Ident B
type  of Ident2 = {B:Prop}B->B

Expanding the definition of Ident in the proof Ident2 gives us

value of Ident2 = [B:Prop]([A:Prop][H:A]H) B

Typed lambda calculus and Hilbert systems

Don’t worry if you don’t follow the argument in this section right away – we won’t be using this result. It demonstrates the computational connection between natural deduction for constructive implicational logic and a Hilbert system for the same logic. It’s worth looking at this later if you skip it now.

To prove that all closed typed lambda terms (in the implicational calculus) can be expressed using only S and K, we will give an algorithm for translating terms into terms containing only S and K. For convenience, we will use I = SKK as an abbreviation for the identity function.

We use two functions to define the compilation.

C compiles a term into S, K and I. A is used by C to abstract a variable from a term.

C[ MN ] = C[ M ] C[ N ]
C[ [x]M ] = A x [C[ M ]]
C[ v ] = v ( v a variable)

Note that the arguments to A contain no lambda abstractions.

A x [MN] = S(A x [M])(A x [N])
A x [x] = I
A x v = Kv (v a variable other than x or v = S, K, I)

A x M abstracts x from M by moving the λ abstraction inwards until either [x]x or [x]y is reached. The S in the first rule takes care of copying the x which would otherwise have been copied during substitution.

Exercise* Prove that if M contains no free variables, C[M] also contains no free variables.

Note that the types are not used in the translation. In fact, this scheme works for the untyped λ calculus as well, though untypable terms will be translated into untypable terms (i.e. we would not be able to assign consistent types to S, K, and I).

Exercise Work out the translation of the untyped term [x]xx and see that the resulting instances of S, K, and I cannot be typed consistently.

Exercise* Show that if t is a typed λ term, then all instances of S, K, and I in C[t] can be typed.

The translation I’ve given is from chapter 16 of The Implementation of Functional Programming Languages, by Simon Peyton Jones. A friendly introduction to combinatory logic can be found in To Mock a Mockingbird, by Raymond Smullyan, in particular the second half of the book.