<< стр. 6(всего 10)СОДЕРЖАНИЕ >>
By definition, an internal adjunction < F, G, f > : cВ®d is given by two internal functors F:
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

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
 << стр. 6(всего 10)СОДЕРЖАНИЕ >>