c®d, G: d®c, and an isomorphism

f : (F´Iddop)*(homd) ® (Idc´Gop)*(homc)

between presheaves on c´dop.

Graphically, the notion of internal adjunction is represented by the following complex diagram:

158

7. Indexed and Internal Categories

where (d1,s0,s1) is the internal hom-functor of d, and (c1,s0',s1') is the internal hom-functor of

c. In particular,

s0 = <DOM,COD> : d1 ® d0´d0 and

s0' = <DOM,COD> : c1 ® c0´c0

respectively represent d1 and c1 as indexed collections of morphisms over d0´d0 and c0´c0.

The formal definition of s1 and s1' is:

s1 = COMP » < p2 » P2, COMP » (id ´0 p1) >0 : d1´0(d1´d1) ® d1

s1' = COMP » < p2 » P2, COMP » (id ´0 p1) >0 : c1´0(c1´c1) ® c1

More intuitively, they are both described by the lambda term lfgh. h » f » g (recall that hom[f,g](h)

= h » f » g).

Note also that DOM: c1´d1® c0´d0 = DOMc´CODd because we are working in c´dop.

X and Y are respectively the pullbacks of

s0 = <DOM,COD> : d1 ® d0´d0 , f0´id : c0´d0 ® d0´d0 and

s0' = <DOM,COD> : c1 ® c0´c0 , id´g0 : c0´d0 ® d0´d0

Thus, informally,

X = { (a,b,h) Î c0´d0´d1 | h : f0(a) ® b } = d[f0(a), b]

Y = { (a,b,k) Î c0´d0´c1 | k : a ® g0(b) } = c[a, g0(b)].

f : X ® Y is the natural isomorphism of the adjunction.

f works on triples of the kind (a,b,h)Îc 0 ´d 0 ´d 1 where h: f0 (a)® b. The first two

components a and b are the indexes of the natural trasformation: since r0'» f = r0, these indexes are

left unchanged by f, and an ’external-like“ writing for f(a,b,h) would be fa,b(h). At the external

level, it is common practice to omit these indexes; the formal complexity of the internal theory is

mostly due to the necessity of coping with these details.

The naturality of f is expressed by the property,

() f » r1 = r1'» f´0id .

Still using our informal notation, by ( ), for all (a,b,h) in X, k in c1 and l in d1, such that : dom

cod(k) = a ( that implies cod(f0(k)) = f0(a) = dom(h) )

dom( l ) = b = cod(h)

cod( l ) = b'

we have

fa',b'( l » h » f1(k) ) = g1( l ) » fa,b(h) » k,

(*)

that is the familiar way the naturality of f is expressed at the external level. Let us show, in this

informal notation, that ( ) implies (*)

fa',b'( l » h » f1(k) ) =

= (PY » f)( a', b' , l » h » f1(k) )

159

7. Indexed and Internal Categories

= (PY » f)( a', b' , s1(h, f1(k), l ) ) by def. of s1

= (PY » f » r1) ((a,b,h), k, l ) by the diagram for the adjunction

= (PY » r1'» f´0id) ( (a,b,h), k, l ) by ( )

= (s1'» PY´0(id´g1) » f´0id) ( (a,b,h), k, l ) by the diagram for the adjunction

= s1'( (PY»f)(a,b,h), k, g1( l ) )

= s1'( fa,b(h), k, g1( l ) )

= g1( l ) » fa,b(h) » k by def. of s1'.

Given an adjunction < F, G, f > : C®D, the arrows fa,F(a)(idF(a)) and fG(b),b-1(idG(b)) are

respectively called Unit and Counit of the adjunction (for a and b). Units and Counits fully specify

the behaviour of f and f-1 since:

f( l ) = f( l » id ) = g1( l ) » f(id) = g1( l ) » Unit

f-1(k) = f-1(id » k) = f-1(id) » F(k) = Counit » F(k) .

These properties allow to give at the external level the well-known equational characterization of the

notion of adjunction. In particular, the definition of Cartesian closed category based on the counits of

the adjunctions, plays a central role in the semantic investigation of the lambda calculus, since it

provides the underlying applicative structure needed for the interpretation. Remember that the counits

of the adjunctions defining products and exponents are respectively the projections associated with

the products and the evaluation functions associated with the function spaces.

Now we show how to mimic the same work at the internal level.

7.A.1 Definition Let < F, G, f > : c®d be an internal adjunction from c to d. Define then:

IDF = <<id,f0>, ID » f0 >0 : c0®X;

IDG = <<g0,id>, ID » g0 >0 : d0®Y;

Unit = PY » f » IDF : c0®c1;

Counit = PX » f-1 » IDG : d0®d1.

Where X and Y are as in the diagram for the definition of adjunction.

Note that IDF takes an element a in c0 and gives the associated identity idF(a) as an element in X.

The definition of Unit, is then clear. As one expects, Unit is an internal natural transformation from I

= (id,id) to G » F, and Counit : d0®d1 is an internal natural transformation from F » G to I =

(id,id). The proof is left as an exercise for the reader.

It is now not difficult to prove that every internal adjunction < F, G, f > : c®d is fully

determined by the following data:

the functor G: d®c;

an arrow f0: c0®d0;

an arrow Unit: c0®c1 such that DOM » Unit = id , COD » Unit = g0 » f0;

160

7. Indexed and Internal Categories

an arrow f-1: Y®X, where X and Y are respectively the pullbacks of

<DOM,COD> : d1®d0´d0, f0´id: c0´d0®d0´d0, and

<DOM,COD> : c1®c0´c0, id´g0: c0´d0®c0´c0;

and, moreover, the previous functions satisfy the following equations:

a. < r0, COMP » < g1 » PX, Unit » p1» r0 >0 >0 » f-1= idY;

b. f-1» < r0, COMP » < g1 » PX, Unit » p1» r0 >0 >0 = idX.

Indeed the arrow f0: c0®d0 can be extended to a functor F = (f0, f1): c®d by

f1 = PX » f-1» << DOM, f0 » COD >, COMP » < Unit » COD, id >0 >0: c1®d1.

The inverse of f-1 is

f = < r0, COMP » < g1 » PX, Unit » p1» r0 >0 >0.

Note that, by (a) and (b), f and f-1 define an isomorphism. The non trivial fact is to prove that

they are morphisms of presheaves (i.e., to prove their naturality), but again the prof is a mere internal

rewriting of the corresponding ’external“ result.

Dually, if we have the following data:

a functor F: c®d;

an arrow g0: d0®c;

an arrow Counit: d0®d1 such that DOM » Counit = f0 » g0 , COD » Counit = id;

an arrow f: X®Y, where X and Y are respectively the pullbacks of

<DOM,COD> : d1®d0´d0, f0´id: c0´d0®d0´d0, and

<DOM,COD> : c1®c0´c0, id´g0: c0´d0®c0´c0;

and, moreover, the previous functions satisfy the following equations:

a. < r0', COMP » < Counit » p2» r0', f1 » PY>0 >0 » f = idX,

b. f » < r0', COMP » < Counit » p2» r0', f1 » PY>0 >0 = idY,

then we define an adjunction < F, G, f > : c®d, in the following way.

The arrow g0: d0®c0 can be extended to a functor G = (g0,g1): c®d, by

g1 = PY» f » << g0 » DOM, COD >, COMP » < id, Counit » DOM >0 >0: d1®c1 .

The inverse of f is

f-1 = < r0', COMP » < Counit » p2 » r0' , f1» PY >0 >0 : Y®X.

We are now in a position to study internal Cartesian closed categories from an ’equational“ point of

view. This work is needed to exploit the applicative structure underlying the notion of an internal

CCC. Recall that an internal Cartesian closed category is a category cÎCat(E) with three adjunctions

1. < O, T, 0 > : c®1, where 1 is the internal terminal category;

2. < D, x, <,> > : c®c´c, where D is the internal diagonal functor;

3. < x, [,] , L > : c®c, where this adjunction has parameters in c.

161

7. Indexed and Internal Categories

By the previous results, we can explicitate the three adjunctions of these definitions by means of their

counits:

7.A.2 Definition An internal terminal object in cÎCat(E) is specified by:

an arrow t0: t ® c0;

an arrow 0: c0 ® Z, where Z is the pullback of

<DOM,COD> : c1 ® c0´c0 ,

id´t0 : c0´t ® c0´c0;

and, moreover,

a. 0 » <g',!Z >0 = 0 » p1» g' = idZ;

b. < g',!Z >0 » 0 = p1» g'» 0 = idc0;

where !Z is the unique morphism in E from Z to the terminal object t .

Intuitively t0: t ® c0 points to that element in c0 that is the terminal object. Z is the subset of

c1 of all those morphisms that have the terminal object as target; Z must then be in a bijective

relation 0 with c0; 0 takes an object a in c0 to the unique morphism !a in Z from a to the

terminal object.

The previous diagram can be greatly simplified. As a matter of fact, it amounts to say that there is

an arrow t0: t®c0 such that the following diagram is a pullback (prove it as an exercise):

The arrow in: c0®c1 is the operation that takes every element a in c0 to the unique arrow !a in c1

whose target is the terminal object; in terms of the previous diagram, in = PZ ° 0 .

162

7. Indexed and Internal Categories

7.A.3 Definition An internal category c has products, iff there exist

an arrow x0: c0´c0 ® c0;

two arrows FST: c0´c0 ® c1, SND: c0´c0 ® c1 such that

DOM» FST = DOM » SND = x0,

COD» FST = p1; COD» SND = p2,

(Notation: FSTa,b = FST» <a,b>; SNDa,b = SND» <a,b>);

an arrow < ,> : X®Y, where X and Y are the pullbacks in the following diagram (D 0 =

<id,id>):

and, moreover,

c0. r' » < , > = r;

c1. (FST» p2 » r) o( P Y » <,> ) = p1 » P X;

c2. (SND » p2 » r) o (P Y » <,> ) = p2 » P X;

d. <,> » < r', < (FST » p2» r') o P Y , (SND» p2» r') o P Y > >0 = idY ,

where f o g = COMP » < f, g >0.

7.A.4 Definition An internal category is Cartesian iff it has a terminal object and products.

As the definition f´g = <f » p1, g » p2> extends ´ to a functor from C´C to C for any Cartesian C,

also the internal x0 can also be extended to morphisms.

7.A.5 Proposition Let x1 : c1´c1 ® c1 be defined by the following:

x1 = P Y » <, >» < <x0» DOM c´c, CODc´c >, <id o (FST» DOM c´c),id o (SND» DOM c´c) >0

where as above, f o g = COMP » <f,g>0 . Then x = (x0, x1): c´c®c is an internal functor.

Proof: Exercise.

Note that, if f,g: e®c1, DOM » f = a, COD » f = c, DOM » g = b, COD » g = d, then: x1» <f,g> =

P Y » <,> » < < x0»<a,b>,<c,d>>,< f o FST a,b , g o SNDa,b > >0.

163

7. Indexed and Internal Categories

7.A.6 Definition An internal Cartesian category has exponents iff there exist :

an arrow [,]0: c0´c0 ® c0;

an arrow EVAL: c0´c0 ® c1 such that

DOM» EVAL = ´0 » <[,]0, p1>,

COD» EVAL = p2 ,

(Notation: EVALa,b = EVAL » <a,b> );

an arrow L: X'® Y', where X' and Y' are the pullbacks in the following diagram:

and, moreover,

e0. s' » L = s (to within the isomorphism (a´b)´c @ a´(b´c) );

e1. (eval » p1» s) o ( x1» < PY' » L, ID » p2 » p1 » s> ) = PX';

f. L » < s', ( eval » p2 » s') o ( x1» < PY', ID » p1» p2 » s'> ) >0 = idY',

where f o g = COMP » < f, g >0 , and x1 is the morphism in proposition A.5.

7.A.7 Definition An internal Cartesian closed category is an internal Cartesian category

with exponents.

References The introduction of indexed notions in Category Theory has been a slow process,

which started to develop into a detailed theory around the beginning of the 1970s, with the

independent work of F. W. Lawvere, J. Penon, J. BŽnabou. The Theory of Indexed Category owes

much of its actual settlement to R. ParŽ and D. Schumacher (1978), and to their introductory book,

written in collaboration with P. T. Johnstone, R. D. Rosebrugh, R. J. Wood and G. C. Wraith.

The first significant study of the Theory of Internal categories is due to R. Diaconescu. Further

developments were made by J. BŽnabou, though, most of the time, they never appeared as published

works. Notions of Internal Category Theory can be found in many books of topos theory, for

instance, in those of Johnstone (1977) and Barr and Wells (1985).

164

7. Indexed and Internal Categories

Our development of the arguments in this chapter has been essentially inspired by ParŽ and

Schumacher (1978), Johnstone (1977), and some private communications of E. Moggi. The

definition of the internal category in definition 7.5.1 has been pointed out to us by B. Jacobs.

165

8. Formulae, Types, and Objects

Chapter 8

FORMULAE, TYPES, AND OBJECTS

During the last two decades, computer science has turned the Proof Theory of mathematical logic

from a philosophical investigation of the foundations of human reasoning into an applied sector of

mathematics. Many important logical systems of the beginning of the 1970s, which ’fifteen years

later“ proved of great relevance for computer science, were invented by logicians such as Girard,

Martin-Lšf and Troelstra, who were mostly interested in constructive approaches to mathematics and

foundational problems. Still in 1975, in the first pages of his book on Proof Theory, Takeuti

introduced ’the formalization of the proofs of mathematics, and the investigation of the structure of

these proofs“ as a mere ’fruitful method in investigating mathematics.“ Moreover, he himself

remarked that ’while set theory has already contributed essentially to the development of modern

mathematics, it remains to be seen what influence proof theory will have on mathematics“.

If not on mathematics, Proof Theory has surely proved since that time his influence on theoretical

computer science. The modern theory of functional languages and lambda calculus owes much of his

actual settlement to mathematical logic, and what until a few years ago was known as the

’denotational semantics of programming languages“ has grown under the direct influence of Proof

Theory, and together with the understanding of the logical aspects of Category Theory. But far from

being only a rich field for applications, computer science has also been for mathematical logic an

inexhaustible source of mutual enrichment. The leading theme of this stimulating relation, as for the

topic presented in this chapter, has been the so called Curry-Howard correspondence, which exploits

the connections between Proof Theory and Type Theory. This correspondence, also known by the

suggestive name of ’formulae-as-types analogy“, has been a main methodological tool both for

understanding the relations between intuitionistic logic and typed lambda calculus, and for the design

of new functional languages with powerful type systems. The main idea of the Curry-Howard

correspondence, is that logical formulae can be interpreted as types in a suitable type theory; a proof

of a formula is then associated with a l-term of the proper type, and the reduction of a proof by cut-

elimination corresponds to the normalization of the associated l-term. As a consequence, if a formula

is derivable in a certain logical system, then the corresponding type is inhabited in the associated type

theory. The Curry-Howard correspondence works only for logical systems of Intuitionistic Logic.

This restriction should be clear, since the constructive, procedural interpretation of the notion of proof

was the very basis of Brower's approach to mathematics, which inspired Heyting's formalization of

intuitionistic logic. Moreover, although the formulae-as-types analogy can also be applied to logical

systems based on axioms and inference rules, such as that of Hilbert, just switching from l-terms to

combinators in the associated type theory, it has a more elegant application to systems of Natural

Deduction. Indeed the procedural understanding of a logical proof is more clear in a system like

166

8. Formulae, Types, and Objects

Natural Deduction, where one proceeds by the method of drawing inferences from assumptions, than

in Hilbert's system, where one draw inferences from axioms. Furthermore, especially in Gentzen's

variant of Natural Deduction, the inference rules of the calculus are closely related to the intuitive

’operational“ interpretation of the logical signs, and this fact allows one to proceed in the construction

of the proof in a certain direct fashion, affording an interesting normal form for deductions which has

no clear counterpart in Hilbert's system.

8.1 l -Notation

Consider the following mathematical definition of the function f: N®N :

f(x) = 5*x + 3 .

Note that it is not ’f“ that has been actually defined, but ’f(x),“ that is the result of the application of

f to a formal parameter x which is supposed to range over the integers.

f(x) is not a function: it is a polynomial, that is, an operational description of the behavior of f

when applied to x. The mechanism that allows us to ’abstract“ from the formal parameter x, and

thus to pass from the knowledge of ’how the function works“ to the knowledge of ’what the function

is,“ is called lambda abstraction (l -abstraction). The function f in the example above is

l

defined by the lambda abstraction of 5x + 3 with respect to x, and is denoted by lx. 5*x+3.

The complementary action to l-abstraction is called application. The application of two terms M

and N is usually represented by their justaposition (MN). From the computational point of view, l-

abstraction and application are related by the following rule, known as b-reduction:

(lx.M)N ® [N/x]M

where [N/x]M means the substitution of N instead of x in the term M.

For example,

(lx. 5*x+3)4 ® 5*4+3 = 23

The lambda notation was explicitly introduced by the logician Alonzo Church in the lambda

calculus (l-calculus), a formalism invented to develop a general theory of computable functions,

and to extend that theory with logical notions providing a foundation for (part of) mathematics.

In computer science, the lambda notation made its first appearance in the programming language

LISP; this was also the first language to use procedures as objects of the language. Like the early

lambda calculus, LISP is an untyped language; that is, programs and data are not distinguished, but

they are all elements of a unique untyped universe: the universe of l-terms for the l-calculus, the

universe of S-expressions for LISP (see next chapter). Anyway, as every computer scientist knows

from his or her own programming practice, types arise naturally, even starting from untyped

universes, when objects are categorized according to their usage and behavior. The ultimate question

is whether it wouldn't be better to consider types as an a priori schema of human knowledge, instead

of an attempt to organize subsets of objects with uniform properties out of an untyped universe. In

167

8. Formulae, Types, and Objects

computer science, the debate about typed and untyped languages is very lively today, since it reflects

the unresolvable conflict between reliability and flexibility of the language. Nowadays, the practical

success of a language is often due to the the more or less successful attempt to compromise security

and freedom; in this respect, the language ML is probably one of the most interesting examples.

Anyway, since the first appearance of types in Algol 60, when typing of variables was introduced to

check at compile time the connections of instances of use with associated declarations, typing has

been considered more and more an essential discipline that must not only help, but guide the

programmer in the design of code.

8.2 The Typed l -Calculus with Explicit Pairs (l b h p t )

l

The collection Tp of type labels, over a ground set At of atomic type symbols, is inductively defined

by

i. At Í Tp;

ii. if A,BÎTp, then A®BÎTp;

iii. if A,BÎTp, then A´BÎTp.

For every type A there exists a denumerable number of variables, ranged over by lower case

letters near the end of the alphabet. We use upper case letters M, N, P, . . . , as metavariables for

terms. The fact that a term M has type A will be denoted with the expression ’M: A.“

The well typed (l -)terms (w.t.t.) and their associated types, are defined according to the

l

following formation rules:

1. every variable x: A is a w.t.t.;

2. if x: A is a variable, and M: B is a w.t.t, then lx:A.M: A®B is a w.t.t.;

3. if M: A®B is a w.t.t and N: A is a w.t.t, then MN: B is a w.t.t.;

4. if M: A is a w.t.t and N: B is a w.t.t, then <M,N>: A´B is a w.t.t.;

5. if M: A´B is a w.t.t, then fst(M): A is a w.t.t.;

6. if M: A´B is a w.t.t, then snd(M): B is a w.t.t.

Given a w.t.t M: B, the set FV(M) of the free variables of M, is defined as follows:

1. if M º x, then FV(M) = {x};

2. if M º lx:A.N, then FV(M) = FV(N)-{x};

3. if M º NP, then FV(M) = FV(N)ÈFV(P);

4. if M º <N,P>, then FV(M) = FV(N)ÈFV(P);

5. if M º fst(N), then FV(M) = FV(N);

6. if M º snd(N), then FV(M) = FV(N).

The substitution [M/x]N: B of a proof M: A for a generic x: A in a proof N: B is defined in

the following way:

168

8. Formulae, Types, and Objects

1. if N: B º x: A then [M/x]N: B º M: A;

2. if N: B º y: A , x¹y , then [M/x]N: B º N: B;

3. if N: B º lx:C.P : B, then [M/x]N: B º lx:C.P : B;

4. if N: B º ly:C.P : B, x¹y, yÏFV(M), then [M/x]N: B º ly:C.[M/x]P : B;

5. if N: B º PQ : B, then [M/x]N: B º [M/x]P[M/x]Q : B;

6. if N: B º <P,Q> : B, then [M/x]N: B º <[M/x]P,[M/x]Q> : B;

7. if N: B º fst(P) : B, then [M/x]N: B º fst([M/x]P) : B;

8. if N: B º snd(P) : B, then [M/x]N: B º snd([M/x]P) : B.

As an easy consequence of the definition above, it follows that if xÏFV(N), then [M/x]N: B º N:

B. Note also that, if xÏFV(N), then [P/x][M/y]N: B º [([P/x]M)/y]N: B .

Given a sequence M = M1 ,..., Mn of terms, and sequence x = x1 , . . . , xn of variables,

[M/x]N denotes the simultaneous substitution of every term Mi for the variable xi in the term N.

We also use the notation [M/x]N to express the simultaneous substitution of the term M for all the

variables in x.

We consider an equational theory of proofs, defined as the minimal congruence relation ’=“ which

satisfies the following axiom schemas:

lx:A.M = ly:A.[y/x]M

(a)

(®b) (lx:A.M)N = [N/x]M

(®h) lx:A.(Mx) = M, if xÏFV(M)

(´ b1) fst(<M,N>) = M

(´ b2) snd(<M,N>) = N

(´ h) <fst(P),snd(P)> = P.

The previous equations may be read from left to right : then one obtains a rewriting system, which

defines the operational semantics of lambda calculus as a programming language. Explicitly, we

define a reduction relation Þ as the minimal relation between with respect to terms such that

(®b) (lx:A.M)N Þ [N/x]M

(´ b1) fst(<M,N>) Þ M

(´ b2) snd(<M,N>) Þ N

M Þ M' implies MN Þ M'N

M Þ M' implies NM Þ NM'

M Þ M' implies lx:A.MÞlx:A.M'

M Þ M' implies fst(M) Þ fst(M')

M Þ M' implies snd(M) Þ snd(M')

(®h) lx:A.(Mx) Þ M, if xÏFV(M)

(´ h) <fst(P),snd(P)> Þ P.

169

8. Formulae, Types, and Objects

The rewriting rules associated with (®b ), (´ b1) and (´ b2) are called b-reductions, and those

associated with (®h) and (´ h) are called h-reductions. We put the h-reductions aside, because of

their lesser computational interest. In the following section we shall see that from the point of view of

the Curry-Howard correspondence both b- and h-reductions have an interpretation in terms of proof

normalization. Also in this context, however, the b-rules play a major role.

A term is in normal form (respectively b-normal form), if it is no more reducible (respectively

b-reducible). The (b-)reduction relation is confluent and noetherian.

Let us now look at some simple examples of programs written in the typed lambda calculus. As

usual, when considering the formal expressiveness of a calculus, we compare it with the problem of

representing integers and arithmetic functions.

Given a type s, we call N s = (s®s)®(s®s) the type of s -iterators (s -numerals). The

s

reason for the name is that in the type (s®s)®(s®s) we have all the terms with the following

structure:

0s º lxs®s lys.y

1s º lxs®s lys.xy

...

ns º lxs®s lys.xny, where xny = x(...(xy)) ’n times“.

The effect of the term ns is to take a function x of type s®s, a term y of type s, and iterate the

application of x to y n times. It is possible to show that if s is an atomic type, then the terms of the

form ns, together with the identity lxs®s.xs®s are the only closed terms in normal form of

type s.

We can now define the function succs º ln: Ns lxs®s lys. x(nxy).

The term succs has type Ns®Ns and its effect is to increase the iteration of one unit. For example,

succs 0s = (ln: Ns lxs®s lys. x(nxy) ) 0s

= lxs®s lys. x( 0sxy)

= lxs®s lys. x(y)

= 1s

Define now adds: Ns´Ns®Ns by adds º lz: Ns´Ns lfs®s lys. fst z f (snd z f y )

For example, we have:

adds <1s,1s> = (lz: Ns´Ns lfs®s lys. fst z f (snd z f y ) ) <1s,1s>

= lfs®s lys. fst <1s,1s> f (snd <1s,1s> f y )

= lfs®s lys. 1s f (1s f y )

= lfs®s lys. f ( f y )

= 2s .

Analogously, mults: Ns´Ns®Ns is given by

mults º lz: Ns´Ns lfs®slys. fst z (snd z f ) y.

As an example of computation, we have

170

8. Formulae, Types, and Objects

mults <2s,2s> = (lz: Ns´Ns lfs®s lys. fst z (snd z f ) y ) <2s,2s>

= lfs®s lys. fst <2s,2s> (snd <2s,2s> f ) y

= lfs®s lys. 2s (2s f ) y

= lfs®s lys. (2s f )( 2s f y )

= lfs®s lys. f ( f( f ( f y ) ) ) )

= 4s .

As a final example, we present a test to 0s. That is, we want to define a term test 0s that takes

two terms M and N of type s and a s-numeral n; if n = 0s then the function yields M as

result; otherwise, it outputs N. Here it is: test 0s º lz: s´s ln: Ns. n( lys.(snd z) )(fst z).

It is possible to prove (see references) that these are essentially all the arithmetic functions we can

compute by the (pure!) simply typed l-calculus, that is, all the functions that are defined by

composition of the previous ones. For example the predecessor function is not representable.

The simply typed l-calculus cannot be considered as a real programming language, but only as a

paradigm for strongly typed (functional) languages, which allow us to point out their main common

properties. In the last section of this chapter we shall consider an extension of the language by

fixpoint operators. The combined use of these operators with a reasonable set of arithmetic primitives

gives to the language its full computational power.

8.3 The Intuitionistic Calculus of Sequents

Among the many variants of intuitionistic logic expressed in systems of Natural Deduction, Gentzen's

calculi of cequents has recently gained much popularity among the computer science community. In

the first place, one of the main aspects of the procedural interpretations of proofs is that of making

explicit the assumptions on which a formula occurrence in a deduction depends, and this is just what

the notion of sequent is meant for. Moreover, since the calculi of sequents can be understood as

metacalculi for the deducibility relation in the corresponding system of natural deduction, it seems to

be the best instrument for the investigation of the structure and the properties of proofs. Note,

however, that even when handling sequents, the dependencies of a formula by its premises can be

quite hard to understand, if one adopts some common choices on the structure of the sequent, such as

avoiding repetitions of formulae in the antecedent, or fixing a certain alphabetic order for them. This

is very clear if we consider a sequent as an effective process for transforming proofs of the premises

into a proof of the consequence. It seems not only reasonable, but fair to guarantee the ability of

handling two or more different proofs for a same formula. In particular, this means allowing

repetitions for a formula in the antecedent of a sequent, each one with an associated hypothetical

distinct proof. From the same point of view, even the idea of an ordering among the formulae does

not make any sense; what one really needs, are rather some explicit rules in the calculus which allow

us ’to move formulae around“ (exchange rules). The presence of repetitions of formulae requires a

171

8. Formulae, Types, and Objects

new rule too, stating that two proofs of a formula can actually be assumed to be the same, and thus

affording to discharge one of them (contraction rule). These rules, together with the so-called

weakening rule, that allows for adding new assumptions to a sequent, are usually referred to as

’structural rules.“ The reason for this name should be clear, since these rules have nothing to do with

logical signs and their meanings, but only with the structures of the derivations in the calculi. This

property of the structural rules has been often misunderstood, and regarded as a sign of their lesser

logical interest: Takeuti called them ’weak inferences,“ with respect to the ’strong inferences“ of

introduction of the logical connectives. The very recent revival of the structural rules, and the analysis

of their impact on the logical systems is mostly due to Girard, and to the invention of linear logic (see

chapter 4).

The calculi of sequents for classical and intuitionistic logic were introduced by Gentzen at the

beginning of the 1930s, who called them L systems. In these systems the elementary statements are

statements of deducibility. Each statement G |- B (called a sequent) has a conclusion B and a

collection G, possibly void, of premises, and it is interpreted as stating the existence of a proof

leading to the stated conclusion and having no uncanceled premises other than some of those stated.

We consider only the subcalculus that deals with the two connectives of conjunction and

implication, and that will be referred to as ’positive calculus.“ The principal connective of the system

is implication; the role of conjunction is rather minor, but its analysis will help in clarifying some

issues we will be concerned with in the rest of this chapter.

The following presentation of the positive intuitionistic calculus of sequents is slightly different

from the usual one. In particular, every formula A will be equipped with an associated proof,

formally represented by a lambda term M: A. This association between proofs (l-terms) and

formulae is defined in the inference rules of the calculus. If there is a derivation of the sequnt G |- M:

B, the proof M keeps a trace of the derivation tree. On the other hand, the so-modified inference

rules can be understood as metarules for proof manipulation. This understanding of the calculus of

sequents as a metacalculus for the deducibility relation is one of the most peculiar aspect of this formal

system.

8.3.1 Logical Alphabet

1. atomic propositions, ranged over by A, B, C, . . .;

2. logical symbols: ´, ® .

8.3.2 W.F.Formulae (Types)

1. every atomic proposition is a formula;

2. if A, B are formulae, then A´B is a formula;

3. if A, B are formulae, then A®B is a formula.

172

8. Formulae, Types, and Objects

There is a bijective correspondence between formulae and types of the typed lambda calculus with

explicit pairs. We can go further, and associate every formula B with a l-term M of the respective

type, which intuitively represents its proofs. In particular, if x1: A1,..., xn: An are the free variables

in M, then M: B is a proof of M depending on the hypothesis A1,..., An. The previous approach

is sound with the intuitionistic interpretation of the notion of proof as an effective procedure that

shows the validity of the conclusion B, as soon as one has a proof of the validity of the premises.

Thus, if M is a proof of B, possibly depending on a generic proof x: A, one gets a proof of A®B

by ’abstraction on x: A,“ that is lx:A.M: A®B. Juxtaposition of proofs corresponds intuitively to

their sequential application. In particular, if we have a proof M: A®B, and we apply it to a proof N:

A, then we obtain a proof MN of B. A proof of A´B is given by a pair of distinct proofs for A

and B. Moreover, having a proof of A´B, one can select the two proofs of A and B by means of

the projections fst and snd .

The inference rules of the calculus exactly formalize this process of constructiing complex proofs

by means of simpler ones.

A (well-typed) term M: A, will be called a proof when it is regarded from a logical viewpoint. A

variable x: A, will be called a generic proof of A.

An intuitionistic sequent has the following syntactic structure:

x1: A1, . . . , xn: An |- M: B

where x1: A1, . . . , xn: An is a finite (possibly empty) list of distinct generic proofs, and M: B is a

proof of B whose free variables are among x1 , . . . , xn . Every formula in the left-hand-side

(l.h.s.) has an associated distinct variable; thus no confusion can arise between formulae, even if they

have the same name.

The intuitive interpretation of the sequent x1: A1, . . . , xn: An |- M: B is that of a process which

builds a proof M of B, as soon as it has proofs for A1, . . . , An, that is, a function f of type

A1´ . . . ´An®B, or equivalently, A1®( . . . (An®B) . . . ), which can be obtained by functional

completeness from the polynomial M.

Since the name of a generic proof is not relevant, we assume that sequents which differ only by a

renaming of variables are syntactically identified. This is consistent with the a-conversion rule of

proofs, in view of the intuitive interpretation of sequents sketched above.

We use Greek capital letters G, D, . . . to denote finite sequences of generic proofs in the left hand

side of a sequent. A sequent thus has the form G |- M: B.

An inference is an expression

S1 S1 S2

____ __________

S S

173

8. Formulae, Types, and Objects

where S1, S2, and S are sequents. S1 and S2 are called the upper sequents and S is called the

lower sequent of the inference. Intuitively, this means that when S1 (S1 and S2) is (are) asserted,

one can infer S from it (them).

We always suppose that the variables in the l.h.s. of the upper sequents are distinct. This is not a

problem, since the variables of the upper sequents S1 and S2 that contribute to form the l.h.s. of the

lower sequent S can be conveniently renamed.

The logical system restricts the legal inferences to those obtained from the following rules.

8.3.3 Axioms and Rules

(axiom) x: A |- x: A

G, x: A, y: B, G1 |- M: C

____________________

(exchange)

G, y: B, x: A, G1 |- M: C

G |- M: B

____________

(weakening)

G, x: A |- M: B

G, x: A, y: A |- M: B

____________________

(contraction)

G, z: A |- [z/x][z/y]M: B

G|- M: A G1, x: A, G2 |- N: B

__________________________

(cut)

G1, G, G2 |- [M/x]N: B

G, x: A |- M: B G1 |- M: A G2, x: B |- N: C

_______________ (®, l ) _________________________

(®, r)

G |- lx:A.M: A®B G1, G2, y: A®B |- [yM/x]N: C

G |- M: A G |- N: B G, x: A |- M: C

_________________

(´, l, 1) _____________________

(´, r)

G |- <M,N> : A´B G, z: A´B |- [fst(z)/x]M: C

G, y: B |- M: C

(´, l, 2) ______________________

G, z: A´B |- [snd(z)/x]M: C

Remark Note the identification of the premises of the upper sequents in the rule (´, r).

174

8. Formulae, Types, and Objects

The formula A in the weakening rule is called the weakening formula (of the inference).

Similarly, we define the cut formula. In the case of the contraction rule we distinguish between the

contracting formulae x: A, y: A and the contracted formula z: A. The formulae A®B and

A´B in the logical rules of introduction of the respective connectives, are called the principal

formulae of the inference; A and B are called the auxiliary formulae.

Unlike the usual approach, we intend the previous definition to refer only to the specific

occurrences of the formulae pointed out in the inference rules. For instance, consider the following

application of the rule (®, l ):

G1 |- M: A w: A®B, x: B |- N: C

______________________________

(®, l )

G1, w: A®B, y: A®B |- [yM/x]N: C

The (occurrence of the) formula A®B associated with the proof y is a principal formula of this

inference, but that associated with w is not.

It is easy to check that, for every rule of inference, the proof in the right-hand side of the lower

sequents is well formed, if those of the upper sequents are as well. A derivation D is a tree of

sequents satisfying the following conditions:

1. the topmost sequents of D are axioms;

2. every sequent in D except the lowest one (the root) is an upper sequent of an inference whose

lower sequent is also in D.

The lower sequent in a derivation D is called the end-sequent of D. A path in a derivation D

from a leaf to the root is called a thread. A derivation without the cut rule is called cut-free.

Examples The following is a derivation:

x: A |- x: A y: B |- y: B

______________ _______________

z: A´B |- fst(z): A z: A´B |- snd(z): B

__________________________________

z: A´B |- <fst(z),snd(z)>: A´B

The sequence

x: A |- x: A

z: A´B |- fst(z): A

z: A´B |- <fst(z),snd(z)>: A´B

is a thread.

175

8. Formulae, Types, and Objects

The tidy display of the introduction of new formulae during a derivation in Gentzen•s calculus of

sequent, allows us to follow the entire ’life“ of a formula, from the moment it is ’created“ (by an

axiom, a weakening, or as a principal formula of a logical rule) to the moment it is ’consumed“ (by a

cut, or as an auxiliary formula in a logical rule). Note in particular that a step of contraction must not

be regarded as a consumption, but as an identification of a formula A in the lower sequent, with two

formulae of the same name in the upper sequent.

Given a thread T and an occurrence of a formula A in the final sequent of T, we call rank of

A in T the number of consecutive sequents in T, counting upward, that contain the same

occurrence of the formula A (or a formula which has been contracted to it).

For instance, consider again the thread

x: A |- x: A

z: A´B |- fst(z): A

z: A´B |- <fst(z),snd(z)>: A´B

of the previous example. The rank of the formula A´B in the l.h.s. of the end sequent is 2, while

the rank of the formula A´B in the r.h.s. is 1.

8.4 The Cut-Elimination Theorem

One of the more interesting properties of Gentzen•s calculus of sequent is the cut-elimination theorem,

also known as Gentzen•s Hauptsatz. This result proves that every derivation in the calculus can be

effectively transformed in a ’natural normal form“ which does not contain any application of the cut

rule. Moreover we show that this process of reduction of the derivations toward a normal form is in

parallel to the b-reduction of the associated proofs.

The identification of the derivations reducible to a same normal form is the base of the so-called

’semantics of proofs,“ and, a posteriori, it provides a justification for the equational theory we have

introduced over the language of proofs (at least for the b-conversions).

The following presentation of the cut-elimination theorem is meant to study the relations between a

derivation ending in the sequent G |- M: A and the proof M: A. Indeed, it should be clear that given

a proof M: A, with FV(M) Í G, it is possible to obtain a derivation of the sequent G |- M: A by

building a sort of ’parse tree“ for the term M: A . Anyway, this correspondence between derivations

and proofs is not a bijection: the problems arise with the structural rules, since their application is not

reflected in the terms. In particular, it is not possible to recover the order in which the structural rules

have been applied during the derivation.

The exact formalization of the equivalence of derivations that differ only in ’structural details“ is

not at all trivial, and it is the main goal of Girard•s research of ’a geometry of interaction“. From this

respect, the language of proofs is a very handy formalism that allows us to abstract from such

structural details.

176

8. Formulae, Types, and Objects

Before the cut-elimination theorem, we state a first, simple result that relates cut-free derivations

and proofs in b-normal form.

8.4.1 Proposition Let G |- M: A be the end sequent of a cut-free derivation. Then the proof M:

A is in b-normal form.

Proof Exercise. Hint: Show, by induction on the length of the derivation, that the proof M: A

cannot contain any of the following subterms:

1. (lx:B.N)P: C

2. fst(<N,P>)

3. snd(<N,P>). ¨

One of the aims of this chapter is to put in evidence the logical aspects underlying functional type

theories. For this reason we state and prove Gentzen•s Hauptsatz and stress the equivalence of the

normalization of a derivation D ending in a sequent G |- M: A and the b-reduction of M.

8.4.2 Theorem (The Cut-Elimination Theorem) Let D be a derivation of the sequent G |-

M: A . Then there exists a cut-free derivation D' of the sequent G |- N: A, where N is the b-normal

form of M.

It is difficult to appreciate at first sight the cut-elimination theorem in its whole meaning. Indeed, it

looks like a mere result about the redundancy of one of the inference rules in the calculus, and one

would expect, as a next step, to drop the cut rule from the logical system. This is not at all the case.

The fact is that the cut rule is a very relevant and deep attempt to express one of the crucial

methodological aspects of reasoning, that is, the decomposition of a complex problem in simpler

subproblems: in order to prove G |- B , we can prove two lemmas G |- A and A |- B. This is very

clear from the computer science point of view, where the emphasis is not on the results - that is, the

terms in normal form - but on the program•s synthesis, and its reduction (computation) when applied

to data.

An important consequence of the cut-elimination theorem is the following. One can easily see that

in any rule of inference except a cut, the lower sequent is no less complicated than the upper

sequent(s). More precisely, every formula occurring in an upper sequent is a subformula of some

formula occurring in the lower sequent. Hence a proof without a cut contains only subformulae of the

formulae occurring in the end sequent (subformula property). From this observation, the

consistency of the logical system immediately follows. Suppose indeed that the empty sequent |-

were provable. Then by the cut-elimination theorem, it would be provable without a cut; but this is

impossible, by the subformula property of cut-free proofs.

177

8. Formulae, Types, and Objects

In order to prove theorem 8.4.2, it is convenient to introduce a new rule of inference called a mix.

The mix rule is logically equivalent to the cut rule, but it helps deal with the contraction rules, whose

behavior during the cut elimination is rather annoying. We shall discuss again this problem at the end

of the proof.

A mix is an inference of the following form:

G|- M: A G1 |- N: B

__________________

G, G1* |- [M/x]N: B

where x is a vector of variables in G1, G1* is obtained from G1 by erasing all the assumption x:

A with xÎx, and [M/x]N denotes the simultaneous substitution of M for all variables in x,

inside the term N.

The previous notion of mix rule is slightly different from the usual one. In particular the formula

A can still appear in the lower sequent G1*.

An occurrence of A in the upper sequents of a mix rule is called a mix formula (of the

inference) if and only if it satisfies one of the two following conditions:

1. it is in the r.h.s. of the left upper sequent;

2. it is in the l.h.s. of the right upper sequent, and it is associated with a proof x:A , with xÎx.

Clearly a cut is a particular case of mix, where the vector x contains only one variable. Moreover,

every mix can be simply obtained by a sequence of exchanges and contractions, a cut, and another

series of exchanges.

Since a proof without a mix is also a proof without a cut, theorem 8.4.2 is proved if we prove the

following:

8.4.3 Theorem (The Mix-Elimination Theorem) Let D be a derivation of the sequent G |-

M: A. Then there exists a mix-free derivation D' of the sequent G |- N: A, where N is the b-

normal form of M.

Theorem 8.4.3 is easily obtained from the following lemma, by induction on the number of the mix

rules occurring in the derivation D.

8.4.4 Lemma Let D be a derivation of the sequent G |- M: A that contains only one cut rule

occurring as the last inference. Then there exists a cut-free derivation D' of the sequent G |- N: A,

where N is the b-normal form of M.

The rest of this section is devoted to the proof of this lemma.

178

8. Formulae, Types, and Objects

We define two scales for measuring the complexity of a proof. The grade of a formula A

(denoted by g(A) ) is the number of logical symbols contained in A. The grade of a mix is the grade

of the mix formula. When a derivation D has only one cut as the last inference, we define the grade

of D (denoted by g(D) ) to be the grade of this mix.

Let D be a derivation which contains a mix

G|- M: A G1 |- N: B

__________________

G, G1* |- [M/x]N: B

as the last inference. We call a thread in D a left (right) thread if it contains the left (right) upper

sequent of the mix. The rank of a thread is the number of consecutive sequents in D (counting

upward from the upper sequents of the cut rule) that contain the mix formula or a formula which has

been contracted to it. The rank of every thread is at least 1. The left (right) rank of a derivation D is

the maximum among the ranks of the left (right) threads in D. The rank of a derivation D is the sum

of its left and right ranks. The rank of a derivation is at least 2.

We prove the lemma by double induction on the grade g and rank r of the derivation D. The

proof is subdivided into two main cases, namely r = 2 and r > 2.

Case 1 : r = 2

We distinguish cases according to the forms of the proofs of the upper sequents of the cut rule.

1.1. The left upper sequent S1 is an initial sequent. In this case D is of the form

y: A |- y: A G |- N: B

____________________

G1* |- [y/x]N: B

And we obtain the same proof by a series of contractions starting from the sequent G |- N: B.

1.2. The right upper sequent S2 is an initial sequent. Similarly.

1.3. Neither S1 nor S2 is an initial sequent, and S1 is the lower sequent of a structural inference.

It is easy to check that, in case r = 2, this is not possible.

1.4. Neither S1 nor S2 is an initial sequent, and S2 is the lower sequent of a structural inference.

The structural inference must be a weakening, whose weakening formula is A. The derivation D

has the structure

179

8. Formulae, Types, and Objects

G1 |- N: B

____________

G |- M: A x: A, G1 |- N: B

________________________

G, G1 |- [M/x]N: B

Since xÏFV(N), [M/x]N º N, and we obtain the same proof N: B as follows:

G1 |- N: B

______________

some weakenings

______________

G, G1 |- N: B

1.5. Both S1 and S2 are the lower sequents of logical inferences. Since the left and right ranks of

D are 1, the cut formulae on each side are the principal formulae of the logical inferences, and the mix

is actually a cut between these two formulae.

We use induction on the grade and distinguish two cases according to the outermost logical

symbol of A.

(®) the derivation D has the structure

G, x: A |- M: B G1 |- N: A G2, y: B |- P: C

_______________ ________________________

G |- lx:A.M: A®B G1, G2, z: A®B |- [zN/y]P: C

___________________________________________

G, G1, G2 |- [lx:A.M/z][zN/y]P: C

where, by assumption, the proofs ending with G, x: A |- M: B, G1 |- N: A or G2, y: B |- P: C do

not contain any cut. Note now that

[lx:A.M/z][zN/x]P: C º [(lx:A.M)N/y]P: C = [ ([N/x]M) /y]P: C,

which also suggests how to build the new derivation.

First consider the derivation

G1 |- N: A G, x: A |- M: B

_________________________

G1, G |- [N/x]M: B

This proof contains only one mix as its last inference. Furthermore, the grade of the mix formula is

less than g(A®B). By induction hypothesis, there exists a derivation D' of the sequent G1, G |-

M': B, where M' is the b-normal form of [N/x]M. Then, with another mix we get

180

8. Formulae, Types, and Objects

G1, G |- M': B G2, y: B |- P: C

______________________________

G, G1, G2 |- [M'/z]P: C

Again we can apply the induction hypothesis, obtaining the requested derivation.

(´) we only consider the case in which the right upper sequent is obtained by a (´,r,1), the other case

being completely analogous. The derivation has the structure

G |- M: A G |- N: B G1, x: A |- P: C

_________________ _____________________

G |- <M,N> : A´B G1, z: A´B |- [fst(z)/x]P: C

_____________________________________________

G, G1 |- [<M,N>/z][fst(z)/x]P: C

where by assumption the proofs ending with G |- M: A , G |- N: B or G1, x: A |- P: C do not

contain any mix. We have

[<M,N>/z][fst(z)/x]P: C º [fst(<M,N>)/x]P: C = [M/x]P: C.

Consider the derivation:

G |- M: A G1, x: A |- P: C

__________________________

G, G1, z: A´B |- [M/x]P: C

This proof contains only one mix as its last inference. Furthermore the grade of the cut formula is less

than g(A´B). By induction hypothesis, we have the requested cut-free derivation D'.

Case 2 : r > 2

The induction hypothesis is that we can eliminate the cut from every derivation D' that contains only

one cut as the last inference, and that satisfies either g(D') < g(D), or g(D') = g(D) and rank(D') <

rank(D).

There are two main cases, namely, rankr(D) > 1 and rankl(D) > 1 (with rankr(D) = 1).

2.1. rankr(D) > 1: we distinguish several subcases according to the logical inference whose lower

sequent is S2.

2.1.1. The sequent S2 is the lower sequent of a weakening rule, whose weakening formula is not

the cut formula. The derivation D has the structure

181

8. Formulae, Types, and Objects

G1 |- N: B

_____________

G |- M: A y: C, G1 |- N: B

___________________________

G, y: C, G1* |- [M/x]N: B

Consider the derivation D'

G |- M: A G1 |- N: B

___________________________

G, G1* |- [M/x]N: B

where the grade of D' is the same of D, namely g(A). Moreover, the two derivations have the

same left rank, while rankr(D') = rankr(D) - 1; thus we can apply the induction hypothesis. With a

weakening and some exchanges we obtain the requested mix-free derivation.

2.1.2. The sequent S2 is the lower sequent of an exchange rule. Similarly.

2.1.3. The sequent S2 is the lower sequent of a contraction rule. This is the main source of problems

with the cut rule (see discussion at the end of the proof). With the mix rule, everything is instead very

easy. For instance, let us consider the case when the contracted formula is a cut formula (the other

case is even simpler). The derivation has the structure

G1, x: A, y: A |- N: B

____________________

G |- M: A G1, z: A |- [z/x][z/y]N: B

_______________________________

G, G1* |- [M/x][z/x][z/y]N: B

where zÎx .

Consider the derivation D'

G |- M: A G1, x: A, y: A |- N: B

______________________________

G, G1* |- [M/x']N: B

where x' is obtained from x by erasing z and adding x, y.

The grade of D' is the same of D, namely g(A). Moreover, the two derivations have the same

left rank, while rankr(D') = rankr(D) - 1; thus we can apply the induction hypothesis, and we obtain

a cut-free derivation D" of G, G1* |- N': B, where N' is the b-normal form of [M/x']N: B. Since

[M/x][z/x][z/y]N: B º [M/x']N: B, the proof is completed.

2.1.4. The sequent S2 is the lower sequent of a logical inference J, whose principal formula is not

a cut formula.

182

8. Formulae, Types, and Objects

The last part of the derivation D looks like

G1 |- N: B

________ J

G |- M: A G2 |- P: C

____________________

G, G2* |- [M/x]P: C

where the derivations of G |- M: A and G1 |- N: B contains no mixes, and G1 contains all the cut

formulae of G2. Consider the following derivation D':

G |- M: A G1 |- N: B

_____________________

G, G1* |- [M/x]N: B

The grade of D' is the same as that of D, namely g(A). Moreover, the two derivations have the

same left rank, while rankr(D') = rankr(D) - 1; thus we can apply the induction hypothesis, and we

obtain a cut-free derivation D" of G, G1* |- N': B, where N' is the b-normal form of [M/x]N: B.

Now we can apply the J rule to get:

G, G1* |- N': B

_____________ J

G, G2* |- P': C

and clearly P' is the b-normal form of [M/x]P: C (the inference rules are sound w.r.t. equality of

proofs).

2.1.5. The sequent S2 is the lower sequent of a logical inference J, whose principal formula is a cut

formula. We treat only the case of the arrow.

(®) the derivation D has the structure

G1 |- N: A G2, y: B |- P: C

________________________

G |- M: A®B G1, G2, z: A®B |- [zN/y]P: C

___________________________________________

G, G1*, G2* |- [M/x][zN/y]P: C

where zÎx.

Let v1, v2 be the variables of x, which are respectively in G1 and G2. Note that v1 and v2

cannot be both empty by the hypothesis about rank.

If v1, v2 are both nonempty, consider the following derivations D1 and D2:

183

8. Formulae, Types, and Objects

D1: D2:

G |- M: A®B G1 |- N: A G |- M: A®B G2, y: B |- P: C

_____________________ _____________________________

G, G1* |- [M/v1]N: A G, G2*, y: B |- [M/v2]P: C

If v1 (v2) is empty, and thus G1 = G1* (G2 = G2*), let D1 (D2) be as follows:

D1: D2:

G1 |- N: A G2, y: B |- P: C

__________ ____________

weakenings weakenings

___________ _______________

G, G1* |- N: A G, G2*, y: B |- P: C

The grade of D1 and D2 is the same as that of D, namely g(A®B). Moreover, rankl(D1) =

rankl(D1) = rankl(D), and rankr(D1) = rankr(D1) = rankr(D) - 1. Hence, by induction hypothesis,

there exist two derivations D1' and D2' respectively ending in the sequents

G, G1* |- N1: A with N1 b-normal form of [M/v1]N: A

G, G2*, y: B |- P1: C with P1 b-normal form of [M/v2]P: C.

Let w be the vector of variables in G, and let w', w" be two vectors of fresh variables of the

same length. Let G' = [w'/w]G, G" =[w"/w]G be the sequences of assumptions obtained by

renaming the variables in G. Let also N1' º [w'/w]N1 and P1' º [w'/w]P1 be the results of the

same operation on the two terms N1 and P1.

Consider the derivation D'

G', G1* |- N1': A G", G2*, y: B |- P1': C

_______________________________________

G', G1*, G", G2*, z: A®B |- [z(N1')/y](P1'): C

G |- M: A®B

_________________________________________________________

G, G', G1*, G", G2* |- [M/z][zN1'/y]P1': C.

The grade of D' is the same of D, namely, g(A®B). Moreover, rankl(D') = rankl(D), and

rankr(D') = 1, since z: A®B is the only cut formula. We can apply again the induction hypothesis,

getting a mix-free derivation of the final sequent

G, G', G1*, G", G2* |- P2: C with P2 b-normal form of [M/z][zN1'/y]P1'.

Identifying by means of contractions (and exchanges) the variables in G, G', G", we get a mix-free

derivation of G, G1*, G2* |- P3: C , where P3 is a b-normal form of [w/w'][w/w"]P2.

Note now that:

[w/w'][w/w"]P2 = [w/w'][w/w"][M/z][zN1'/y]P1'

º [M/z][z([w/w']N1')/y]([w/w"]P1')

184

8. Formulae, Types, and Objects

º [M/z][zN1/y]P1

= [M/z][z([M/v1]N)/y]([M/v2]P)

º [M/z][M/v1][M/v2][zN/y]P

º [M/x][zN/y]P: C.

2.2. rankl(D) > 1 (and rankr(D) = 1)

This case is proved in the same way as is 2.1 above.

This completes the proof of lemma 8.4.4 and, hence, of the cut-elimination theorem. ¨

8.5 Categorical Semantics of Derivations

In this section we will study the categorical semantics of the intuitionistic proof theory developed in

the last section. The main idea is that a formula A is interpreted as an object I(A) in a category C.

A provable sequent B1,..., Bn |- A is then associated with a morphism f: I(B1)„...„I(Bn)®I(A),

where „: C´C®C is a suitable bifunctor that gives meaning to the comma in the l.h.s. of the

sequent. Since the comma is associative and commutative, „ is a symmetric tensor product.

Moreover, we need some sort of projections for the weakening rule, and a diagonal map in the

contraction rule. Actually, all these morphisms, together with a few reasonable equations, turn „

into a categorical product.

Since C |- AÞB iff C, A |- B, it is natural to interpret the implication Þ as the right adjoint to

the functor „.

Also the binary connective ´ is bifunctor of the category. In particular, the fact that C |- A´B iff

(C |- A and C |- B) suggests that ´ should be interpreted as a categorical product. As a

consequence „ and ´ coincide to within isomorphism, that is consistent with the well-known fact

that the comma in the l.h.s. of a sequent has the same logical meaning of a conjunction. Anyway,

since they are different concept, we prefer to maintain the distinction at the semantical level.

8.5.1 Definition A categorical model of the positive intuitionistic calculus is a pair (C,IAt ),

where C is a Cartesian closed category (possibly with two specified products „ and ´ ), and IAt is

a map that takes every atomic formula to an object of C.

Notation In the rest of this chapter, we shall use the same symbols Þ and ´ for indicating both

the connectives of the calculus and the associated functors of the category: the intended meaning is

clear from the context.

185

8. Formulae, Types, and Objects

The analysis of the cut-elimination theorem will provide a more convincing justification for the

previous notion of model. Now we concentrate on the interpretation.

I is extended to all the formulae in the following way:

I(A) = IAt(A) if A is atomic

I(AÞC) = I(A)ÞI(C)

I(A´C) = I(A)´I(C)

The categorical interpretation does not give meanings to sequents, but to derivations. Every derivation

D whose final sequent is B1, . . . , Bn |- A is interpreted by a morphism

I(D) = f: I(B1)„ . . . „I(Bn) ® I(A)

Before giving the details of the interpretation, we recall a few results about Cartesian closed

categories, and fix the notation.

We call weak-lA,B: A„B®B, weak-rA,B: A„B®A the projections associated with the product

„, and fstA,B: A´B®B, sndA,B: A´B®A the projections associated with the product ´.

We have the natural isomorphisms assocA,B,C : (A„B)„C® A„(B„C) and exchA,B :

A„B®B„A, given by the symmetric monoidal structure associated with „. Moreover, we have a

diagonal map DA = <idA,idA>: A®A„A and an the evaluation map evalA,C: (AÞC)„A®C.

The interpretation is given by induction on the length of the derivation. We define it in a somewhat

informal but suggestive (and concise) way, associating with every inference rule of the calculus in

8.3.4 a respective semantic rule. This will be enough as for the categorical meaning of the

intuitionistic system in section 8.3.

8.5.2 Interpretation

(axiom) idA : A ® A

f: A„(B„C) ® D

_________________________

(associativity)

f ° assocA,B,C: (A„B)„C ® D

f: B„A ® C

___________________

(exchange)

f ° exchA,B: A„B ® C

f: B ® C

_____________________

(weakening)

f ° weak-lA,B: A„B ® C

186

8. Formulae, Types, and Objects

f: (A„A)„B ® C

____________________

(contraction)

f ° DA„idB: A„B ® C

f: B ® A g: A„D ® C

______________________

(cut)

g ° f„idD : B„D ® C

f: B„A ® C f: E ® A g: C ® D

(®, r) _____________ (®, l ) _____________________________

L(f): B ® AÞC g ° evalA,C ° id„f: (AÞC)„E ® D

f: C ® A g: C ® B f: A„C ® D

__________________ _________________________

(´, r) (´, l, 1)

<f,g>: C ® A´B f ° fstA,B„idC: (A´B)„C ® D

f: B„C ® D

(´, l, 2) __________________________

f ° sndA,B„idC: (A´B)„C ® D.

8.6 The Cut-Elimination Theorem Revisited

In this section, we look at the cut elimination theorem from the categorical point of view. Our goal is

to provide a more convincing justification of the categorical notion of model, not a further proof of

cut-elimination. Indeed the notion of CCC imposes some identifications between derivations that are

not evident at the logical level of the inference rules. The fact is that we are not interested in giving

semantics to the provability relation among formulae, but more generally to the whole proof system,

with its associated normalization procedures. The point is that the equalities, which define CCC's,

reflect the identity of derivations up to normalization. In particular, we have the following result.

8.6.1 Theorem (The Cut-Elimination Theorem) Let D be a derivation of the sequent A |-

B. Then there exists a cut-free derivation D' whose final sequent is A |- B, and such that in every

model I(D) = I(D').

We do not prove the previous result, but instead analyze in detail some examples of derivations

identified by the cut-elimination process. Our aim is to show that the Cartesian closed structure is

imposed by this identification of proofs up to normalization. The examples are instrumental to this.

187

8. Formulae, Types, and Objects

8.6.2 Example If in the following derivation the left upper sequent A |- A is an initial sequent,

the cut is eliminated by taking the derivation of the right upper sequent

A |- A A |- B

____________________

A |- B

At the semantic level, we have the situation:

idA: A ® A f: A ® B

_____________________

f ° idA: A ® B

thus a model must satisfy the equation f ° idA = f . Analogously, when the right upper sequent is an

axiom, we derive the equation idA ° f = f

8.6.3 Example Consider a derivation whose final part looks like

B |- C

________

D |- A A, B |- C

___________________

D, B |- C

the cut is eliminated in the following way:

B |- C

________

D, B |- C

At the semantic level we have the following situation:

f: B ® C

_____________________

g: D ® A f ° weak-lA,B: A„B ® C

__________________________________

f ° weak-lA,B ° g„idB: D„B ® C

and

f: B ® C

_____________________

f ° weak-lD,B: D„B ® C

thus, for every g: D®A, we must have

weak-lD,B = weak-lA,B ° g„idB : D„B®C (*)

188

8. Formulae, Types, and Objects

The previous equation is clearly true if „ is a categorical product, and weak-lD,B is the associated

right projection.

8.6.4 Example Consider a derivation whose final part looks like

A, A |- B

________

D |- A A |- B

__________________

D |- B

This is the annoying case of the contraction. With the help of a mix rule, the derivation reduces to

D |- A A, A |- B

___________________

D |- B

Regarding the mix as a simple abbreviation of a series of cuts and structural inferences, the previous

derivation is logically equivalent to

D |- A A, A |- B

___________________

D |- A D, A |- B

___________________

D, D |- B

_________

D |- B

At the semantic level we have

f: A„A ® B

______________

g: D ® A f ° DA : A ® B

________________________

f ° DA ° g: D® B

which reduces to

g: D ® A f: A„A ® B

________________________

g: D ® A f ° g„idA : D„A ® B

___________________________________

f ° g„idA ° idA„g : D„D ® B

__________________________

f ° g„g ° DD : D„D ® B

189

8. Formulae, Types, and Objects