Computer Aided Formal Reasoning Fall, 1995 Lecture notes 4 Judith Underwood

Propositional Logic II

Let us look at the logic we defined last time from a slightly different perspective. We will first define the simply typed λ calculus, and then augment it with operators to deal with pairing and disjoint union types.

Simply typed lambda calculus

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

\begin{aligned}A & = & p & (p ∈ P) \\ & | & A->A \end{aligned}

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 well-typed 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 1.

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 – treating them as schemas means we don’t have to deal with quantification just yet.)

   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 is considered to be one of the founders of formalism.)

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 typed 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 constant functions 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:

    A ->B ->and A B
    and A B ->A
    and A B ->B
    A ->or A B
    B ->or A B
    (or A B) ->(A ->C) ->(B ->C) ->C
    absurd ->A

We can think of the corresponding 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 lecture notes 3. 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.

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 does demonstrate 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.

Background notes

These are some notes I wrote for another course. I have not changed the notation, so that where you see λx : A.y or λx^{A}.y, this is the same as [x:A]y in Lego. Here I cover just the implicational case in more detail, and explain the notation a bit more carefully. At the end is the (very important!) meditation exercise I gave in class.

Introduction to the Curry-Howard isomorphism

There is a clear analogy between the process of writing programs and the process of proving theorems. Generally speaking, to write a program, the programmer decides what the program must do, chooses an algorithm, and breaks the algorithm down into small computational steps until the program compiles. To prove a theorem, a mathematician formulates a statement of the theorem, chooses a proof technique, and breaks the argument down into small logical steps until the proof is accepted by the referees.

The Curry-Howard isomorphism is one way of formalizing this analogy. It amounts to a formal correspondence between “what the program must do” (as expressed by its type) and “what the theorem proves,” for a simple programming language (namely, simply typed λ-calculus) and a simple logic. We’ll begin with the logic.

Implicational logic

Consider the following deduction system, which is a subsystem of intuitionistic propositional logic. Formulas are constructed from propositional variables from a set P according to the grammar

\begin{aligned}A & = & p & (p ∈ P) \\ & | & A→A \end{aligned}

In each rule below, the construction

Γ ⊢ A

is called a sequent, where Γ is a set of formulas (the hypotheses) and A is a single formula (the conclusion). This sequent can be thought of as stating, “Under the set of assumptions Γ, we can conclude A.”

Axiom The axioms of the system are sequents of the form Γ, A ⊢ A.

→-introduction Given a sequent of the form Γ, A ⊢ B, we can conclude the sequent Γ ⊢ A→B. We say the hypothesis A has been discharged. This rule may also be written

{Γ, A ⊢ B \atop Γ ⊢ A→B}

→-elimination (modus ponens) If we have sequents of the form Γ ⊢ A→B and Γ ⊢ A, then we can conclude the sequent Γ ⊢ B. This rule is written

{Γ ⊢ A→B Γ ⊢ A \atop Γ ⊢ B}

A proof tree is a tree formed by application of these rules to axioms, which form the leaves of the tree. A proof tree in which the final sequent is of the form

⊢ A

(i.e. where Γ is empty) is a proof of A. An example of a proof is

{A, B ⊢ A \atop A ⊢ B→A} ; ⊢ A→(B→A)

Typed λ-calculus

We can interpret the formulas in implicational logic as describing types in simply typed λcalculus. We will show that proof trees then correspond to terms in the calculus.

More formally, we show how to build terms in the typed λ-calculus in the same way as proofs are built. We assume we have a collection TermVar of term variables x, y, …, each associated with a type, i.e. a formula as described above, built from base types which are the propositional variables.

We begin with the axioms in the proof system. With each formula in a sequent

A_{1}, …, A_{n} ⊢ A_{i}

we associate a term variable of that type, i.e.

x_{1} :A_{1}, …, x_{n}:A_{n} ⊢ x_{i}:A_{i}.

The sequent is now read as “Under the typing assumptions x_{1} : A_{1} … x_{n}: A_{n}, conclude that x_{i} has type A_{i}.”

The →-introduction rule corresponds to a typing rule for λ-abstractions.

{x_{1} :H_{1}, …, x_{n}:H_{n}, y:A ⊢ t:B \atop x_{1} :H_{1}, …, x_{n}:H_{n} ⊢ λy^{A}.t:A→B}

(The notation y^{A} is equivalent to y:A; I use it when the presence of too many colons would make parsing a term difficult.)

Finally, the →-elimination rule corresponds to a typing rule for function applications.

{x_{1} :H_{1}, …, x_{n}:H_{n} ⊢ t:A→B x_{1} :H_{1}, …, x_{n}:H_{n} ⊢ a:A \atop x_{1} :H_{1}, …, x_{n}:H_{n} ⊢ ta:B}

Just as a term of type A→B is a function from terms of type A to terms of type B, we see that the modus ponens rule explains a proof of A→B as a function from proofs of A to proofs of B.

In each of these cases, we read the final sequent as describing the type of the term in the conclusion, given the typing assumptions for the variables listed in the hypothesis. Note that because proofs begin with axioms, all free variables in the term in the conclusion are in the hypothesis list. A proof ⊢ A, then, can be interpreted as constructing a term t which has type A under an empty set of typing assumptions. In other words, the term has no free variables.

For example, the proof above becomes

{x:A, y:B ⊢ x:A \atop x:A ⊢ λy^{B}.x:B→A} ; ⊢ λx^{A}.λy^{B}.x:A→(B→A)

Thus, this proof can be represented by the term

λx^{A}.λy^{B}.x

of type A→(B→A). In general, we can consider a proof of ϕ in the implicational logic described above as defining a closed term in the simply typed λ calculus which has type ϕ. Furthermore, the extraction of the term from the proof is completely automatic.

More formally, a well-typed λ term is defined as something constructed on the right side of a turnstile ( ⊢) in a well-formed derivation.

Comments

This system formalizes a particular notion of type. A type is inherent in a term since, given a term, we can construct its type automatically and there is only one type it may have. Next time we shall see how to generalize these types.

First, let us consider some of the implications of this approach. We began with an implicational logic, then used this to describe a typing system for λ calculus where propositions in the logic became types for λ terms. Furthermore, the terms can be interpreted as representing proofs, and vice versa. This leads to the slogans “propositions as types” and “proofs as programs”. Programs (λ-terms) can be considered to be merely another notation for proofs. This idea can be extended to many constructive logics, and, to some degree, non-constructive logics as well.

We have not yet mentioned anything about computation. If proofs are programs, then we may compute with proofs just as we compute with programs. Thus, we can consider issues of normalization, etc for proof transformations which correspond to program reductions.

Exercise: Meditate on the three kinds of implication expressed in the proof rule

{Γ, A ⊢ B \atop Γ ⊢ A → B}