Giuseppe Longo
email: longo@ens.ens.frem@lfcs.ed.ac.uk

Eugenio Moggi

CONSTRUCTIVE NATURAL DEDUCTION AND ITS "ω-SET" INTERPRETATION

Various Theories of Types are introduced, by stressing the analogy "propositionsas-types" : from propositional to higher order types (and Logic).

In accordance with this, proofs are described as terms of various calculi, in particular of polymorphic (second order) λcalculus.

A semantic explanation is then given by interpreting individual types and the collection of all types in two simple categories built out of the natural numbers (the modest sets and the universe of ω -sets). The first part of this paper (syntax) may be viewed as a short tutorial with a constructive understanding of the deduction theorem and some work on the expressive power of first and second order quantification. Also in the second part (semantics, §.6-7) the presentation is meant to be elementary, even though we introduce some new facts on types as quotient sets in order to interpret "explicit polymorphism".

(The experienced reader in Type Theory may directly go, at first reading, to §.6-7-8).

Content.

Remarks on "mathematical semantics" 1. Minimal deductions 2. Constructive PN o 3. Reductions of proofs and terms 4. First order logic or types depending on terms 5. Second order logic and explicit polymorphism 6. Semantic interpretation 7. Products and intersections 8. The product Π is the (internal) right adjoint of the diagonal functor __________________

explanations of Type Theory, based on the solid grounds of a strictly finitistic approach to Mathematics: only finite or finitistically defined structures are allowed, functions are just effective procedures in some formalized language.... This is clearly expressed in Nördstrom [1986].

Indeed, the strict interaction between meaning and denotation, both growing out of a proposal for a constructive foundation of Mathematics, suggested at several stages new systems or variations of previous ones, all embedded into a unifying philosophical perspective.

A further motivation for this understanding of types and terms goes back to the same observation which makes formal systems for computations refer to constructive approaches to Logic: computers, which are finite machines, run (finite) programs for computable functions, thus any programming construct should be explained in these terms. This seems less convincing, as the meaning of software should be provided also to human beings, who may (fortunately) have a variety of approaches to life and understanding. As long as our brains will not be entirely computerized, the understanding of a strictly constructive, but complicated system may also derive from highly non constructive, but conceptually simple, intellectual experiences.

The point is that programming languages are getting almost as complicated as real life and the more approaches we have to their semantics the better we may hope to deal with their unexpected riches. Thus, everybody must welcome the fruitful direct interaction between denotation and meaning provided by finitistic view points in semantics, but one should also appreciate the deep insight given by the limit or ideal objects in Mathematics, particularly when they aid in understanding the complicated stepwise constructions of automated computing. Functions in extenso do not need to exist, but everybody understands by a one second sketch on a blackboard the asymptotic behaviour of the logarithmic function, say, much better than by looking at the effective generation of a hundred thousand outputs. This is simply because our geometric intuition is based on the most solid grounds of over two thousands years of mathematical thinking, since Nemecmo.

Similarly, the sketchy design of a partially ordered set or of a tree, even with limit points, provides an excellent intuition of what it is meant by the notion of approximation or by order completeness and a secure guidance to descriptions by constructive formalizations. On the other hand, when a formal system is given and the issue of its "meaning" is raised, a most informative semantics may easily come from approaches which are based on entirely different grounds. Relevant scientific explanations are precisely provided when apparently unrelated systems are brought toghether and unexpected links are suggested. By this, semantic explanations in terms of topologies or categories enrich our knowledge in both the source and target areas, guarranty the relative consistency of complicated formal systems and suggest extensions or even the design of original systems. Indeed, this is the story of the most relevant applications of Scott-Strachey denotational semantics, to which, for example, the design of Edinburgh language ML is endebted (see [START_REF] Plotkin | LCF as a programming language[END_REF], [START_REF] Milner | A theory of type polymorphism in programming[END_REF]), and it seems to be the intellectual itinerary which brought Girard from system F to Linear Logic as a growing system.

It should be clear that the perspective above gives a major role to informal explanations and intuitive meaning, possibly based on a vaguely defined "mathematical insight" into structures (topological, algebraic...). However, this costumary informality of Mathematics always hides complete rigor and restricts constructions and understanding to the limited cage of mathematical formalism: lack of ambiguities and precision in meaning is the core of it. In other words, it is intended that any informal understanding can be made very precise, if time allows. The formal systems and their semantics below is a typical example of this method and of the forceful formalist environment.

Minimal deductions.

The general idea on which Gentzen-Prawitz systems are based is the concept of derivation as a formalization of the mathematical practice of theorem proving by stepwise deductions. The "atomic" step in a derivation is given by the application of a deduction rule. Each inference rule describes the deduction of certain consequences from given premises. The premises may be formulae, which are assumed, or deductions, i.e. compositions of inference rules. Thus they may have the structure:

A 1 A 2 A n : A 1 A 2 A n B ______________ ____ C C
In the latter case a fundamental concept may be used, the concept of "cancellation". To explain it, assume that you have deduced that if it rains, then it is humid. In a semiformal way, this let syou infer "rain → humidity". Now, the latter implication is "true" independently of the truth of the assumption "it rains"; namely, as an implication, it holds even when you mention it as an obvious meteoreological remark in a sunny day. Thus, you may omit or cancel "rain" when infering "rain → humidity".

We first discuss one of the simplest deductive systems, the Positive Natural calculus (PN o ), as a basis and paradigm for stronger logical extensions. PN o is also known as Minimal Logic.

PN o is only based on implication ("→") as a key concept in deductions. Formulae are inductively defined as follows.

An atomic predicate is a formula. If A and B are formulae, then (A → Β) is a formula.

The inference rules introduce or eliminate "→" from formulae and, thus, tell us how the only connective is formally handled.

Introduction rule Elimination rule

[A] : B A A → B (→I) _____ (→E) ____________ A → B B
In (→I), A is "cancelled".

We are now in the position to define formally derivations as trees. The rigorous reader may view the definitions of inference rule and of derivation as given by combined induction.

1.1 Definition .

(1) The one element tree {A} is a derivation for all predicates A.

A [A] (2 →) If : is a derivation , then : B B ______ is a derivation. A → B D D' D D' If A and A→ B are derivations, then A A → B ___________ is a derivation .

B

The root or bottom formula of a derivation is the conclusion. In this Natural Deduction system, the provability relation Γ  Α between lists of formulae and formulae is defined as follows.

1.2 Definition. Γ  Α if there is a derivation, according to the rules above, with all (uncancelled) hypotheses included in Γ and with conclusion A.

If Γ Α , we say that A is derivable from Γ. Note that, by definition, Γ may contain several copies of the same formula and superfluous "hypotheses", i.e. if Γ ⊇ ∆ A , then Γ Α . Γ,A stands for Γ∪{A}. If Γ = ∅ , we write  A and say that A is a theorem. Sometimes, the system above is equivalently presented by defining directly Γ Α , that is by

(A) _______ for A in Γ Γ  A Γ,A  B Γ  A Γ  A → B (→I) ____________ (→E) ______________________ Γ  A → B Γ  B .

Constructive PN o .

We shall soon see the relevance for functional languages of the very weak system PN o . PN o though is just the implicative fragment of the propositional part of a well known logical system: Intuitionistic Logic. This Logic was formalized by Heyting in the 30's as a logical basis for Brouwer's approach to Mathematics. In Brouwer's view, only the subjective intuition of the stepwise generation of the natural numbers could serve as a basis for mathematical reasoning. That reasoning, moreover, could only be safe if based on finitistic notions and structures, the only ones perfectly handled by the human mind. In particular, given a finite structure and a property one could safely check the truth of the latter in the structure, by finite inspection; while this cannot be done over infinite structures, where the truth of an assertion would require an infinite verification. However, assertions on infinite structures can be made, provided that they are based on finite descriptions and arguments: finitary languages and finite proofs only make sense. In other words, an assertion is true when it comes toghether with a (finitistic) proof. As a consequence of this strict finitism or constructivism, following Brouwer (and Heyting), the truth of A∨ ~A holds only if it is verified over a finite set; in general, A∨ ~A strictly requires a proof, namely a proof of A or a proof of ~A . Similarly, A→B is true if finitistically provable, where a proof of A→B means an effective procedures that converts any proof of A into a proof of B .

In this section we formalize the concept above : C holds iff there is a proof c of C . In this case we write c : C. In particular, the proof c of an implicative assertion A → B must be an effective procedure which takes any proof of A into a proof of B . This will be the key idea in the rewriting below of (→I) and (→E) in an explicitly constructive way, where proofs are handled as part of the language.

For this purpose, we construt a language for proofs. This language contains variables, as x : A means that there is an "hypothetical" proof of A and it is used in (possibly cancelled) assumptions. Suppose, for example, that, if an hypothetical proof x of A is assumed, x : A , then a proof b of B may be derived, b : B . By (→I) , one has A → B and, now, also a proof of it; namely, a transformation λx:A.b which takes any proof of A into a proof of B . The independence of A → B from A , which is cancelled, corresponds to the fact that the function λx:A.b does not depend on the (name of the) variable x .

Indeed, the variable binder λ is an "abstraction operator" such as {x |....} in {x  A(x)}, or as ∀x in a quantified formula ∀x.A(x) : the set or the formula do not depend on the bound variable

x. Thus, the variable binder λ is introduced in the presence of cancelled assumptions : In our contructive approach it says that from a proof a : A and a proof c : A → B we may obtain a proof of B ; indeed, such a proof is constructed from c and a.

Let's write (ca) for it. That is :

a : A c : A → Β (→ E) _____________________ ca : B
In conclusion the language of proofs of PN 0 is based only on variables x,y,z,... , a variable binder λ and on application. Indeed, a typed language, as a:A also means that "a has type A". By this, PN o is really the first step in the analogy between types and formulae: the intuitive meaning of λx:A.b : A → B is that λx:A.b is a function from (the meaning of) A to B ; indeed, a computable function as it is explicitly defined by a finitistic syntax. Then λx:A.b can be applied to a term a of type A and gives an output of type B. Note that λ is a variable binder and binds variables in cancelled assumptions; thus a term does not depend on (the name of) a bound variable similarly as an implication does not depend on the truth of the premise. Conversely, if a term or proof of a proposition contains free variables, then that proposition depends on uncalled hypotheses or, correspondingly, those free variables must have an (uncancelled or) explicit type declaration.

We notice now that, at this stage, proofs and terms may be viewed in a slightly different way. Namely, one may simply write λx.b as a proof of A → B by erasing all type information (by induction, i.e. also in b ) in λx:A.b . This is possible, at this stage, by the strong decidability properties mentioned in the Remark below (on typability). The advantage is twofold. First, it sets the base for ML programming styles, where one may write type-free programs which are typed at compile time by the system. Second, a term "proves" many proposition: e.g. λx.x proves A → A , or has type A → A , for all intances of A (whereas λx:A.x is a different term for each type A ). By this, we have a notion of type-schema corresponding to the notion of (axiom) schema in Logic. This is not possible in the higher order systems described in the sequel. More formally, then terms and types are defined as follows:

2.1 Definition: λ -terms are inductively defined as :

Lemma

: PN o  λxy.x : A → ( B → A ) PN o  λxyz.xz(yz) : A → ( B → C ) → (( A → B ) → ( A → C )) Proof : [ x : A] [y : B] __________________ x : A _____________ (→ I) λy.x :B→ A ____________________ (→ I) λxy.x : A → ( B → A ) [z : A ] [x : A → ( B → C )] [z : A] [y : A → B] _____________________________ (→ Ε) ____________________ (→Ε) _________________________________________ (→ Ε) xz(yz) : C ________________ (→ Ε) λz.xz(yz) : A → C ______________________________ (→ Ι) λyz.xz(yz) : ( A → B ) → ( A → C ) ______________________________________________ (→ Ι) λ xyz.xz(yz) : A → ( B → C ) → (( A → B ) → ( A → C ))
∆ Notation : K λ ≡ λxy.x ; S λ ≡ λxyz.xz(yz).

Note that λ-terms code proofs of PN o : each λ corresponds to the use of an (→ Ι) rule, each application to (→ E) rule. Thus by looking at a term, with the right perentheses, one may reconstruct the theorem it proves.

Remark (On typability). Not all terms, as defined, have a type (e.g. xx ). However, it is decidable whether a type-free term has a type and one can uniformely effectively generate its "most general" type (principal type schema; see [START_REF] Hindley | The principal type-scheme of an object in Combinatory Logic[END_REF], [START_REF] Milner | A theory of type polymorphism in programming[END_REF]). These facts are the core of type-inference and type-checking systems in functional programming. This is why it is worth looking both at the typed and the type free calculi, in the PN o case (see §.6, the paragraph on "Semantics of type assignement and of typed terms").

The rest of the first part of this paper will be mostly concerned with the language of proofs in 2.1 and its extensions; when defined by a collection of axioms, which specify how terms reduce to each other, it is also known as the λ-calculus (see 3.3). However, it may be worth spending a few lines on a simple variant, which actually originated the topic by the work of Shönfinkel and Curry in the 20's and 30's. The correspondence between these two systems also clarifies the correspondence between the deductive approach of Natural Deduction and Hilbert's axiomatic systems. We assume that the reader is familiar with the classical Hilbert style presentation of Propositional Calculus; that is with the system of Logic based on axioms and inference rules. Indeed, Hilbert's presentation of Logic differs from Gentzen-Prawitz in that it assumes some generally valid truth (the axioms or axiom schemata) and deduces other truth from these by means of inference rules. As it should be clear, no assumptions are made in the system PN o , which only relies on the concept of inference. The two different perspectives will suggest below two different calculi of proofs. We recall one of the many equivalent axiomatic systems for a fragment of Hilbert's Propositional Calculus.

Definition:

The Positive Propositional Calculus (PP o ) is given by the following axioms and rule:

Ax.1) A → ( B→ A ) Ax.2) A → ( B→ C ) → (( A → B ) → ( A → C )) A A → B (MP) ___________ B .
In this case, of course, derivability is defined w.r.t. the given axioms.

Recall that PN o makes no assumptions, except for the structure of deductions, while PP o relies on two axioms, i.e. on two underived assumptions. This corresponds to having constants in the language of proofs. That is, in the constructive positive case, it is assumed once and for all that there are "proofs" of the two propositions (or schemata) in Ax.1 and 2. Let's call K and S these (constant) proofs (cf. K λ and S λ in 2.3) :

(K) K: A→ (B→A) (S) S: A→ (B→C) → ((A→B)→(A→C))
2.5 Definition: Combinators are inductively defined as :

x,y,z,... are combinators K and S are combinators (ca) is a combinator, when c,a are combinators.

Variables should be understood as proofs of hypothetical assumptions, if needed. K and S are constant as above and application (ca) is motivated by (→E). The crucial point is that one can get rid of variables in any compound combinator and this will be exactly the deduction theorem below.

Recall now that by axiom we actually mean axiom schema. Thus, K and S are proofs of any formula obtained from ax.1 and ax. 2 by consistent instantiation. Or, equivalently, they have the type schema described in (K) and (S) .

Lemma. PP o | SKK : A→A .

Proof. In the proof, the types of S and K are instantiated as to allow the application of (MP) , i.e. of the rule (→E) . For the reader familiar with Shoenfinkel-Curry's abstraction algorithms, by which one may embed λ-terms into combinators, it should be clear that they are just a constructive investigation of the classical Deduction Theorem, as pointed out by the last two results (see also [START_REF] Huet | Formal Structures for Computation and Deduction[END_REF]).

Reductions of proofs and terms.

In the previous section we were able to look at proofs as terms of a very simple language, indeed a functional language. By this, the inhabited types of that language turned out to be exactly the theorems of PN o . The first application of this analogy is now a connection between reducing proofs and terms. Let's define formally the usual mathemathical concept of instantiation :

3.1 Definition : Let b be a λ-term or a S-K term , then the term [a/x]b is inductively defined , with a free for x in b , in the following way :

-b ≡ x then [a/x]b ≡ a -x ∉ FV(b) then [a/x]b ≡ b -b ≡ λy.c then [a/x]b ≡ λy.[a/x]c -b ≡ c d then [a/x]b ≡ ([a/x]c) ([a/x]d)
(As usual, a free for x in b if there is no free occurence of x in b, which is in the scope bound by a variable free in a ). This passage corresponds to the following practice in Mathemathics. In order to obtain a proof [a/x]b of B , depending on a specific proof a of A , one may more easily prove in general that, "for any x : A " , b : B can be deduced and, then, apply the general proof λx.b of A → Β to the specific proof a of A.

Remark

However, this indirect argument, logically reduces to the derivation of [a/x]b : B from a : A.

In conclusion, the proof (P.1) reduces to (P.2) and the terms (λx.b) a , [a/x]b respectively code these proofs; this suggests a calculus of proofs axiomatizing this concept.

Definition

: λ-calculus (λβ > or λ ο )
is the calculus of proofs defined as λ-terms and axiomatized by α) and β) plus the inference rules below which turn ">" into a reflexive, transitive and substitutive relation :

α) λx.a > λy.[y/x]a β) (λx.b)a > [a/x]b provided that a is free for x in b Rules: (ρ) a > a a > b b > c (τ) __________________ a > c a > b a' > b' a > b (µν) ___________________ (ξ) _________ a a' > b b' λx.a > λx.b
Conventions: Recall that λ is a variable binder and bound variables may be freely renamed, by (α). Therefore, given a , x and b , we may always consider b free for x in a , by renaming of bound variables in a .

Remark. Consider the following derivation:

c : A → Β [ x : A ] (→Ε) ______________________________ (P.3) cx : B (→ Ι) ___________ λx.cx : A → Β
Similarly as before, one shows that λx.cx is a proof of A → B , under the uncancelled assumption that c : A → Β . Thus, one may simplify (P.3) to c : A → Β (P.2) This corresponds to the λβη > calculus which has the extra axiom: η) λx.cx > c provided that x is free in c.

Definition

: A λ-term a is in normal form iff it doesn't contain subterms of the form (λx.b)c.

Definition : A λ-term a has normal form iff there exists a term a' in normal form

such that a > a'.

In Natural Deduction we say that a proof is in normal form if does not contain a (→ I) rule followed by a (→ E) rule. This corresponds exactly to say that a term, viewed as a code for a proof, cannot have subterms such as (λx.b)c . Indeed, (λx.b)c is formed first by abstraction, Analogously : S λ abc ≡ (λxyz.xz(yz))abc > (λyz.az(yz))bc > (λz.az(bz))c > ac(bc).

2) Let a be a closed term in normal form whose type-scheme is : A→(Β→Α). Since a is in normal form, it has one of the forms :

xb 1 ...b n or λx.b (n≥0)
The first form is impossible , since a is closed. Hence , for some b , a ≡ λx.b ; that is, (→Ι) has been used in the deduction of type-scheme of a : The "=" relation is the simmetric and transistive closure of ">" . In the calculi below we will directly define equality between terms.

First order logic or types depending on terms.

As usual in Logic and Mathematics, most relevant facts are expressed by an essential use of assertions on arbitrary elements (of a given set or type). That is, mathematical pratice relies on the use of predicates which include variables and on quantification with respect to variables. A Typetheoretic foundation of this common practice has been given by the work of Martin-Löf. This method, of course, is widely used also in Computer Science (see Bruce&Longo[1988] for a recent application to the description and interpretation of "record types"). As before, we only describe the logic "core" of first order Natural Deduction.

The expressions of the language we are going to define are terms and types (or formulae). They will be defined by combined induction as terms may contain types and types may contain terms. We write capital letters for expressions which are types. A:Tp is short for "A is a type". In contrast to the propositional case, we only consider typed terms (see the Remark on typability, in §2).

The base is given by a collection of variables x, y, z.... and of atomic types or predicates.

Conventions: λ, ∀, ∃ are variables binders. An unbound variable x in exp is free in exp (notation: x∈FV(exp)). The substitution of a for x in exp is defined by induction, provided that a is free for x in exp, as usual.

Here is a (combined) inductive definition of term and type expressions. The formation and deduction rules below will select the (well) typed and well formed terms and types.

Well formed assumptions:

(Empty) ∅ ok (the empty assignment is well formed)

Γ ok Γ | _ A : Tp (Context) ________________ for x∉FV( Γ) Γ(x:A) ok Γ ok (Assump) _______ for (x : A)∈Γ Γ | _ (x:A)
Circular clashes are avoided by the assignement rules, e.g. {(x:A(y)),(y:B)} is not an ok assignement.

Equality "=" is a reflexive, symmetric and transitive relation, which is congruent w.r.t. types according to the following rules:

a : A A = B : Tp (Congr.1) ________________ a : B a = b : A A = B : Tp (Congr.2) ___________________ a = b : B (Congr) ________________________ Γ | _ [b /x]J
The last rule is needed, as may others below, since atomic types may contain term variables, and, hence, type expressions may do so. Substitution of variables by terms (or terms by equal terms) for atomic types (i.e. predicates) will be discussed in the general setting of mathematical extensions of the system below (see the Intermezzo).

Type Formation and Equality:

A :Tp ∆

Intermezzo (on mathematical theories)

We presented so far only the "logical rules" for propositional and first order systems, within the constructive perspective of Type Theory. Mathematical practice, though, and the needs of Computer Science require the investigation and use of specific extensions of these core theories. At this regards, in Constructive Natural Deduction, i.e. in this type-theoretic fomalization of first order deduction, one has more expressive power than in the usual approaches to Natural Deduction. Besides "proof terms", a crucial difference is in the representation of sorts and propositions both as types, while sorts and formulae are different entities in Logic.

Observe that the extensions are usually given by adding constant symbols, i.e. predicates and functions, of various sorts, whose behaviuor is given by telling their "arity" and by a bunch of axioms. That is, sorts, predicates, functions and axioms of a first order theory can be represented in a signature (Σ , say) in the following way (see Harper&al[1987]). Judgements, then, depend also on signatures .

Judgements:

Σ ok ; Σ | _ Γ ok ; Σ, Γ | _ A : Tp ; Σ, Γ | _ A = B : Tp ; Σ, Γ | _ a : A ; Σ, Γ | _ a = b :
A ; X : [...]A gives the "arity" of X.

Well formed signatures:

(Axiom) ∅ ok (the empty signature is well formed)

Σ | _ Γ ok (Sign.1) ____________ for X not in Σ Σ (X : [Γ]Tp) ok Σ, Γ | _ A : Tp (Sign.2) ____________ for X not in Σ Σ (X : [Γ]A) ok

Constants:

Sorts : X: [ ]Tp Predicates : X : [x 1 :A 1 , ..

. , x n :A n ]Tp

where A i : Tp , for all i ≤ n ; Functions :

X : [x 1 :A 1 , ... , x n :A n ]A 0 where A i : Tp , for all i ≤ n ;

Axioms : X : [ ]A

where A : Tp with no free variables

The various formation, elimination and introduction rules follow the pattern below, where K : Tp or K = Tp and the constant X appears as X : [x 1 :A 1 , ... , x n :A n ]K in Σ : In conclusion, the rules (∃E) 2 , (∃E=) 2 , (∃β) 2 and (∃η) 2 instead of the corresponding rules for PN 1 above, give an equivalent systems, which is strictly stronger than the usual Natural Deduction approach to existential quantification.

Σ ok Σ, Γ | _ a i : [a 1 /x 1 , ... , a i-1 /x i-1 ]A i 1≤ i ≤ n (X) ________________________________________ Σ, Γ | _ X(a 1 , ... , a n ) : [a 1 /x 1 , ... , a n /x n ]K Σ ok Σ, Γ | _ a i = b i : [a 1 /x 1 , ... , a i-1 /x i-1 ]A i 1≤ i ≤ n (X=) ____________________________________________ Σ, Γ | _ X(a 1 , ... , a n ) = X(b 1 , ... , b n ) : [a 1 /x 1 , ... , a n /x n ]K .

Second order logic and explicit polymorphism.

The working mathematician often makes assertions concerning arbitrary functions in a given collection (when describing integration, say) or even about arbitrary sets within a given category or class of sets (all c.p.o.'s have a least element...). In the previous section we have been dealing with a language for higher type functions. Functional abstraction (i.e. λx.... ) was defined w.r.t. to variables ranging over ground elements, functions, functionals and so on, in any finite higher type. Note that functional abstraction may be understood as a form of quantification; thus, as each boolean valued function determines a set, abstracting w.r.t. a variable which ranges over boolean valued functions is like quantifying over sets of a given type. However, we were not allowed to quantify explicitly over types. Indeed, there is some implicit quantification over types in the systems mentioned so far. Church-Curry types are defined as type schemata: e.g. the identity λx.x has type schema α→α , i.e. λx.x has type σ→σ for any type σ, or the collection of its possible types is obtained by consistently instantiating α in α→α by every type. Mathematical practice and this implicit use of quantification suggest a language where one could explicitly consider all types: thus, a higher order language, with quantification over types. This language is the core of the nowadays widely known approach to "modularity" in functional programming via second order or "explicit" polymorphism.

The expressions of the language, i.e. terms and types (or formulae), will be defined by simultaneous induction as before, with the further possibility of including the expression Tp in their formation. We write capital letters to stress that an expression is a type; lower-case letters, though, may also be types. A : Tp is short for "A is a type". The base is given by a collection of variables x, y, z.... X, Y, Z... and of atomic types or predicates. We mantain the usual conventions on variable binders ( λ and ∀ ), free variables and substitution. A definition, by combined induction, of term and type expressions is first given, as in the first order case. The rules pick up the legal ones. The judgements and related conventions are the same as for PN 1 . As PN 2 below is a proper extension of PN 1 , we only summarize the new rules.

Well formed assumptions:

Γ ok

(Context 2 ) _________ for X∉FV( Γ) Γ(X : Tp) ok Γ ok (Assump 2 ) _________ for (X : Tp)∈Γ Γ | _ (X : Tp)
Equality "=" is a congruence as in the I order case. The II order type formation rules include the following crucial impredicative cases:

Type Formation and Equality: 5.1 Definition: PN 2 is the deductive system defined above and λP 2 is the calculus of its proofs (as terms) .

II order dependent products (introduction, elimination, equality):

The system PN 2 is a (revisited) fragment of Coquand-Huet's "Calculus of Constructions" (see Hyland&Pitts[1987]).

Remark:

(i) -When (∀I) is used w.r.t. to a non empty list Γ of assumptions, X is not free in uncancelled assumptions, by the same argument as in (4.1). (ii) If there are no atomic types with free variables, λP 2 coincides with Girard-Reynolds' second order λ-calculus, since A→B ≡ ∀x:A.B .

The very elegant and relevant fact, in second order logic, is that also the connetives {∧,∨, ∃} and the absurdum ⊥ , are derivable in this purely implicative fragment, PN 2 , based only on ∀ and →. This was discovered, in Logic, long ago. Observe that second order quantification is essential for this.

Definition: ⊥ ≡ ∀X : Tp.X .

It is sound to consider ⊥ the "absurdum" or constantly false predicate, in view of the following theorem. It proves that "ex falso quodlibet" (1) and that "if one can prove any proposition (type) then one can prove falsum" (2). In either case, the intuitive meaning of "∃" may be understood by instantiating Y by ⊥.

Theorem

Informally, if ~A (≡ A→ ⊥) is the negation of A :

∃X : K.A ≅ ~ ∀X : K.~A
for K : Tp or K = Tp . However, if defined in this way , i.e. by using " ~ ", "∃" would not give the results below! (i) For derived second order existential quantifier it is not possible to obtain projections at all, in the sense, say, of the first order (∃E) in §.4. As for the first projection, one should take C ≡ Tp and c ≡ X , but the result would not be in the language. The second projection is impossible since one should take C ≡ A , which may depend on X, (cf. 4.4).

Note that, if one does not have predicates with free (term) variables, as in Girard's system F , then, after erasing proof terms, (∃ 2 E) becomes exactly the second order rule for existential elimination in Natural Deduction. where, now, z may occur in C and, hence, C depends indirectly on X , x . By this, (∃ 2 E) 2 is not derivable. Clearly, then, the behaviour of the (Let ... in ...) terms must be formalized by rules analogue to the (∃E=), (∃β), (∃η) rules in remark 4.4 (where, again, A is Tp and the dependence of C on X, x must be made indirect as above). By this indirect dependence, though, one cannot have either projection.

5.14 Remark. (On first order "there exists elimination" rules).

Following remark 5.9.2, one may derive a first order "there-exists-elimination" rule by taking K However, these rules are weak and there is no way to derive the second projection, in contrast to the (∃E), (∃β) rules given in §.4 for the first order case, since A may depend on x' , and, hence, one cannot set C ≡ A . Similarly, one cannot derive an analogue to (∃η). Note also that, if one does not have predicates with free (term) variables, than (w∃E), with no proof terms, is exactly the first order rule for existential elimination in Natural Deduction.

Mathematical extensions are handled similarly as for PN 1 , by taking into account that one has higher order arities and sorts.

Semantic interpretation

As already mentioned, we just presented the core Theory of "propositions-as-types". However, this is where (most of) the semantic challanges come in. The point now is to define or construct sets, categories, objects or alike, in a way that the formal, linguistic, notions introduced so far will be enriched by meaning and consistency over these structures, which have an independent foundation from Type Theory.

It is clear that if we can do so for the last theory of types examined, then we would be able to interpret also the other theories, as the latter is an extension of all of them. Moreover, λP 2 presents a very challenging problem: the definition of types is impredicative, or PN 2 is an impredicative theory of types or propositions. In short, when defining proper second order types, the quantified types are defined by using quantification over all types, including the one which is being defined. Indeed, recall Since we want to focus only on the semantic understanding of impredicativity and keep the presentation elementary, in the sequel we will restrict ourselves to Girard's system F, i.e. to the second order fragment of PN 2 , and we will not discuss here the interpretation of dependent types, i.e. of PN 1 . To be precise, system F, as a pure theory, is equivalent to λP 2 . The ideas presented in this paper brought again to the limelight the "realizability interpretation" of impredicative type theory, as pointed out in in [START_REF] Hyland | A small complete category[END_REF].

A full categorical account of dependent types, including the theory of constructions, can be now found in Hyland &Pitts [1987] (see also [START_REF] Ehrhard | A Categorical Semantics of Constructions[END_REF] and Robinson[1989]).

Call now M the interpretation of Tp. Then (∀ 2 I) roughly means that the interpretation of (∀X:Tp.B) must be an element of M, even though its definition may use M itself, as (∀X:Tp.B) contains Tp . Thus, it may not seem possible to construct the entire set or structure M stepwise, i.e. by defining first its elements, as we may know them only after knowing all of M (see (0) below).

The method below for understanding this circularity examplifies a crucial point of "meaningful (and informative) interpretations": the impredicative calculus λP 2 is given meaning in the familiar powerset of a (countable) set. As discussed in the introduction, this is meant to provide a conceptual environment for an explanation of impredicative Type Theory, since we understand it independently and better, we claim, than (∀X:Tp.B) : Tp .

Semantics of type assignement and of typed terms.

A distinction must be made when discussing the semantics of systems like those described in the previous sections. In §.2 types are assigned to type-free terms: rule (→I) , say, derives type schema (A→A) for the term λx.x , the functional program computing the identity function. λx.x , though, carry no type information: it is a type-free term and (→I) tells us that it has all types whose schema is (A→A).

Thus, the meaning of an assignement of types must be given over a model for the type-free calculus, (D, . ), as one needs to interpret first untyped terms. Then a derivation | _ a:A will hold in D iff the interpretation in D of the type-free term a is in the interpretation of the type A as a subset (or a substructure) of D .

We will not get into the semantics of type assignement as this is a well settled part of the connection between type-free and classically typed λ-calculus (Barendregt&al[1983] first proved a completeness result, [START_REF] Hindley | The completeness theorem for typing lambda-terms[END_REF] gives an alternative tidy presentation; see [START_REF] Barendregt | A filter lambda model and the completeness of type assignment[END_REF], [START_REF] Longo | Computability in higher types, Pω and the completeness of type assignement[END_REF], Hindley&Seldin[1986], [START_REF] Mitchell | A type-inference approach to reduction properties and semantics of polymorphic expressions[END_REF][START_REF] Mitchell | Polymorphic Type Inference and containement[END_REF] for further references).

In contrast to λ o , the terms of the calculi of proofs of PN 1 and PN 2 are typed. Then rules such as (∀I) specify their types (or select the legal terms of the typed laguage toghether with their types). For example, by (∀I) in PN 1 one may deduce (λx:A.x) : (A → A) from the derivation [x:A] ...x:A ; that is for any type A , λx:A.x is the typed identity of type A→A.

In the second order case, λP 2 , the metalinguistic or implicit derivation we just made can be explicitly formalized. That is the deduction "for any type A, λx:A.x is the typed identity of type A → A" becomes [X:Tp] ..... (λx:X.x) : (X → X)

and (∀ 2 I) gives (λX:Tp.λx:X.x) : (∀X:Tp.X → X) .

Next we will discuss the meaning of the later syntactic constructs. The model investigated is built out of a type-free structure: Kleene's applicative (ω, . ) . However, the construction works over any partial Combinatory Algebra, and, thus, on any model of the type-free λ-calculus; in this case the model would yield a complete semantics also for type assignement, as described by PN o (see [START_REF] Scott | Data types as lattices[END_REF], [START_REF] Hindley | The completeness theorem for typing lambda-terms[END_REF], were the modest sets are called "the quotient semantics of types").

Types as modest sets.

There are several general definitions of what the semantics of impredicative II order types should be (see Bruce&al[1986], [START_REF] Seely | Categorical semantics for higher order polymorphic lambda calculus[END_REF]). In this section, we first consider a very simple interpretation of λP 2 , which satisfies the requirements in Bruce&al [1986] and is based on the early work of [START_REF] Girard | Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types[END_REF]Troelstra[1973]. In §.6 -7, though, we also set the basis for a more elaborate understanding of λP 2 as described in §.8. There the meaning of (the impredicative core of) PN 2 will be better given by providing a category-theoretic explanation of the (impredicative part of) the previous construction. This is done within a model of IZF (Intuitionistic Set Theory), which allows a "set-theoretic" understanding of a calculus which has no classical set-theoretic model. Let's informally summarize the main steps of the abstract notion and hint the "naïve" interpretation. Later we will construct the model, which is informative even naive idea, can be found in [START_REF] Pitts | Polymorphism is Set Theoretic, constructively[END_REF] and Meseguer[1989]). [START_REF] Reynolds | Polymorphism is not set-theoretic[END_REF] has shown that this naïve approach leads to a paradox, by an informative result on models of λP 2 (see also

Reynolds&Plotkin [1988]). The following is a simple cardinality argument.

Assume that a naive interpretation of λP 2 could be given, as above. That is, that there is a set N such that A→B∈N for A,B∈Ν Π e∈N g(e)∈N for g: N → N .

The interpretation would be non trivial if there were a set A∈N such that #A > 1 . Define then F: Ord → N by

F(0) = A F(α + 1) = F(α) → F(α) F(γ) = Π B∈N g(B)
for a limit ordinal γ, where g(B) = if B∈{F(α) | α < γ} then B, else A . By this α < β ⇒ # F(α) < # F(β) , which is impossible, as Ord is not a set. Therefore for any A∈N , one has #A ≤ 1 . And the model trivializes (similarly as in any naïve attempt to find in Set a model for the type-free λ-calculus).

However, both the simple arguments above and the more complex one in [START_REF] Reynolds | Polymorphism is not set-theoretic[END_REF] are given in classical ZF and do not hold in IZF.

In §.8, we prove that the naïve interpretation of second order types as indexed products can be recovered provided that the model is turned into an internal category of a suitable topos theoretic model of IZF, namely the effective topos Eff of Hyland (see Hyland[1982[START_REF] Hyland | A small complete category[END_REF], [START_REF] Pitts | Polymorphism is Set Theoretic, constructively[END_REF]).

In that frame, products are isomorphic to intersections (theorem 7.4). For convenience, in the exposition, we may avoid any explicit use of Topos Theory by using as categorical frame the category ω-Set below, which has a "concrete" description as a category of sets with a realizability relation (the correctness of this replacement is explained in §.8). By this we intend to provide an elementary categorical justification of the nowadays well known interpretation of types as quotient subsets of ω , the natural numbers. Let's first review this interpretation of types, simply and modestly, as quotient sets, esentially due to Kreisel, Girard, Troelstra and Scott. The current understanding of the higher order types by quotient sets and internal categories, which we develop here, has been first suggested by Moggi and widely developped by several authors in Category Theory [START_REF] Rosolini | About Modest Sets[END_REF], [START_REF] Hyland | A small complete category[END_REF], Hyland&al[1987], Carboni&al [1987], [START_REF] Bainbridge | Functorial Polymorphism[END_REF], Robinson[1989], Asperti&Longo[1990]...)

The objects of the category PER below are equivalence relations on subsets of the natural numbers or partial equivalence relations (p.e.r.'s). Morphisms are defined by Kleene's application: n . p is the result of the application of the n-th partial recursive function to the number p . By n . p∈A we always mean that n . p is defined. < , > with inverses pr 1 , pr 2 is any Morphisms in PER are "computable" in the sense that they are fully described by partial recursive functions which are total on the domain of the source relation. Note also that the intersection of any collection {A i } i∈I of objects in PER is still in PER, by viewing them as sets of pairs (of numbers), that is,

n (∩ i∈I A i ) m iff ∀i∈I (n A i m ) .
The model may be defined by saying how to interpret Tp , individual types and type constructors. Then the interpretation of terms, as "functions" in their types, is given by describing the applicative behaviour of elements of p.e.r.'s, i.e. of equivalence classes. A key point is the mathematical meaning, given in 5 below, of the application of a term to a type (rule (∀ 2 E) ).

Definition (the λ 2 -model of partial equivalence relations):

1 -[Tp] = PER, 2 -→: ( PER×PER ) → PER is the function such that m (R→S) n ⇔ ∀p,q ( p R q ⇒ m . p S n . q ), 3 -∀:

(PER → PER ) → PER is the function such that ∀(F) = ∩ R∈ PER F(R), 4 -eval R,S ({n} R→S ,{m} R ) = {n . m} S where R,S ∈ PER , 5 -eval F ({n} ∀(F) , R) = {n} F(R) where F: PER → PER (polymorphic application).
The definition of polymorphic application in 5 was suggested by Moggi in a discussion on computer mail [START_REF] Moggi | Message on "Types" elettronic mailing list[END_REF]). This model and similar ones (see [START_REF] Mitchell | A type-inference approach to reduction properties and semantics of polymorphic expressions[END_REF], BreazuT.&Coquand[1987]) have been also used to answer consistency questions for extensions of λP 2 (see the Conclusion), for which it is essential to allow models with also empty types (see Meyer&al [1987]). However, the first basic ideas for a λ 2 -model HEO 2 (with all types non empty), based on partial equivalence relations, is due to Girard (see also Troelstra[1972]).

What needs to be done now is to relate the above interpretation of polymorphic types as intersections (in 4) to the set theoretic intuition of polymorphic types as indexed products. Indexed over PER itself, as it should be clear by now. Observe first that there is no way to look at PER as an object of PER itself (for cardinality reasons!). Indeed, we never required, in the formal theory, that Tp is a type, although in some models (e.g. in Amadio&al [1986] or [START_REF] Taylor | Recursive Domains, Indexed Category Theory and Polymorphism[END_REF]) this is so. In any case, we must be able to deal with Tp in some "uniform" way, as we need to interpret universal quantification over types and over Tp . For this purpose we consider the following extension of PER . The category PER is isomorphic to a full subcategory of ω-Set. In fact, for every partial equivalence relation (per) A we can define an ω-set In(A) = (Q(A), ∈ A ) , where Q(A) are the equivalence classes of A , as disjoint subsets of ω, and ∈ A is the usual membership relation restricted to ω×Q(A) . Clearly, this defines a realizability relation in the sense of 6.3 and the embedding is full.

Definition:

Since categorical constructions are defined up to isomorphisms, it is more convenient to consider a full subcategory of ω-Set whose objects are exactly the ω-sets X for which there exists a per A s.t. X is isomorphic to In(A). This category is defined as follows. In view of (SV), (In,Out) is an equivalence between the categories PER and M, which cuts down to an isomorphism between p.e.r.'s and ω-sets of the form (Q(A), ∈ Α ).

example, [START_REF] Mitchell | A type-inference approach to reduction properties and semantics of polymorphic expressions[END_REF], Bruce&Longo[1988]). (Intuitionistic) Set Theory could be used, because the internal category we construct lives inside a model of IZF, the Effective Topos, which extends Kleene's realizability interpretation of Intuitionistic Logic.

It is an easy exercise to check that both M and ω-Set are Cartesian Closed. A key fact is that M is equivalent to an internal category of ω-Set, where an internal category is a pair of objects, one representing the collection of objects, such as M o , the other the morphisms, and a few morphisms between them (see 8.4 below; for example, a category is small when it is an internal category of Set, i.e. its collections of objects and morphisms are sets). The categorical constructions in ω-Set that will be used in the sequel are gathered in the following remark. (The formal treatment has been quite elementary up to this point: it will be based on some more technicalities in this final section). Moreover, ω-Set is just a "piece" of Hyland's Effective Topos Eff, a model for IZF:

8.2 Remark. M and ω-Set may be characterized within Eff, namely M is equivalent to the category of "effective objects" and ω-Set is equivalent to the category of "~~-separated objects" (Hyland[1982], [START_REF] Rosolini | About Modest Sets[END_REF]). The embedding functor from ω-Set to Eff is easily given: just take (A,| __ A ) to (A,= A ) where a = A b := if a = b then {n| n | __ A a} else ∅ . Recall now that, given a category C and an object A∈C, C/A , the slice over A, is the comma category, whose objects are the morphisms with target A. Corollary 8.3 below proves that ω-Set is lCCC and its embedding in Eff preserves such a structure, i.e. the full embedding of any ω-Set/A in Eff/A preserves the CCC structure. Thus, the kind of "constructions" we consider commute w.r.t. the embedding functor from ω-Set to Eff and, hence, we can safely use ω-Set instead of Eff. (to Hyland[1982]). Both M and ω-Set are Locally Cartesian Closed categories, where finite limits and Π-types are "computed" as in Eff.

Corollary

commonly understood as the formalization of Analysis. System F , in turn, suggested the above mentioned strong property of the partial equivalence relation on a (sufficiently rich) applicative structures, i.e. their closure under (suitable) products indexed over the set of p.e.r.'s itself, as well as its general category theoretic understanding (in the sense of §.8 and Carboni&al[1987], [START_REF] Hyland | A small complete category[END_REF], Hyland&al[1987], [START_REF] Pitts | Polymorphism is Set Theoretic, constructively[END_REF], Hyland&Pitts [1987]).

It is worth mentioning that this most recent history was developed by work in Computer Science. Even though they originated in Logic, types as quotient sets or the various categories of "modest sets" were strongly advocated by Dana Scott in various papers and lectures; without his work and stimulating activity, not much would be known about these structures. Moreover, the present model construction originated as an answer to a very reasonable question in Theory of Programming, raised by Albert Meyer: can we extend λP 2 (which is the core of functional languages with explicit polymorphism) by a couple of axioms imposing that there are only two booleans? It is good in programming to know that there will be no rubbish in the type of booleans, i.e. in ∀X:Tp.X→(X→X) . Moggi, by using PER in [START_REF] Moggi | Message on "Types" elettronic mailing list[END_REF], showed that such an extension is consistent. As an exercise, the reader may check that the interpretation in M of the type ∀X:Tp.X→X of the II order identity λX:Tp.λx:X.x contains only the identity function (or the collection of its indices).

Further "consistency questions" for interesting extensions of polymorphic languages, such as those related to the issues on "inheritance" and subtypes, may be the most likely applications of the present interpretation of higher order types (see Bruce&Longo[1988]). This is because types are just (and modestly) sets of numbers and behave very naturally as far as set inclusion and related properties are concerned.

Aknowledgement. Longo is endebted to Roberto Amadio, P.L. Curien, Roger Hindley for numerous discussions. In particular, with P.L. Curien he had a chance to have long and helpful discussions on the categorical approach to higher order typing and on Moggi's understanding of "polymorphic application". Pino Rosolini made comments and suggested changes in several messages on computer mail.

  .b : A → B Consider now (→ E), i.e. Modus Ponens.

S

  SKK, then I is a proof of A→A. Its intended meaning is the identity function of type A→A (see later), Note that combinators code proofs in PP o . For example A → A is proved by first applying (→E) to (an instance of) axiom S to axiom K : this gives (SK). Then apply (→E) again to the theorem coded by (SK) and to axiom K : this gives ((SK)K), a proof of A→A. 2.7 Lemma ("Constructive" Deduction Theorem for PP o ) Let Γ, x: A | __ b : Β then there exists a term [x].b , such that x∉FV([x].b) and Γ | __ [x]. b : A→B. Proof (By induction on the structure of b) 1. b ≡ x Then A ≡ B . Recall that I : A→A and set [x].b ≡ I 2. x∉ FV(b) . Then the assumption x : A is not used in the derivation, i.e. Γ | b: B. Now K: B→(A→B), thus Γ | Kb : A→B and set [x].b = Kb. (Clearly, the case b ≡ y ≠ x could suffice for the inductive proof). 3. b ≡ cd. Then c . Observe that, by induction, [x].c : A→(D→B) and [x].d : A→D . Thus S : A→(D→B)→((Α→D)→(A→B)) [x].c : A→(D→ B) _______________________________________________ S ([x].c) : (A→D)→(A→B) [x].d : A→D __________________________________________________ S ([x].c) ([x].d) : A→B . Set then [x].b = S ([x].c) ([x].d). ∆ 2.8 Theorem . If PP o | a : A , then there exists a closed λ-term a' s. t. PN o | a' : A . Conversely, if PN o | a : A, then there exists a closed SK-term a° s.t. PP o | a° : A . Proof. Use K λ and S λ to translate combinators into λ-terms. For the converse, translate λx.... by [x].... and use induction and the lemma. ∆

  is "any hypothetical proof of A" and x may occur in b , this simplifies (reduces) to :

  i.e. (→ I) , then by application, i.e. (→ E). Notice now that, if a term a is in normal form , there are only two possibilities: (i) a ≡ xb 1 ......b n with b 1 ......b n in normal form, (ii) a ≡ λx.b with b in normal form. 3.6 Proposition : 1) K λ ab > a , S λ abc > ac(bc) 2) Let a and b be closed terms in normal form. Assume that a : (A→(B→Α)) and b : (A→(Β→C))→((Α→Β)→(Α→C)) . Then a ≡ K λ and b ≡ S λ . Proof 1) By sequential applications of the (β) axiom : Κ λ ab ≡ (λxy.x)ab > (λy.a)b > a .

  b) : A→(Β→Α) Since x has a type A which may be atomic, x must occur in b in a non function-position, i.e. b cannot be of the form (xc 1 ...c m+1 ) . On the other hand, b cannot be of the form (λy.c)c 1 ...c m+1 as it would not be in normal form; nor of the form zc 1 ...c m because z would be free in b , while we assumed that b contains at most x free. Hence b has one of the forms : -b ≡ x -b ≡ λy.c , then the deduction coded by a had to be : .c : B→Α (→Ι) __________________ a ≡ λxy.c : A→(Β→Α) Consider now the structure of c. It cannot be of the form (λw.d) because it would give a composite type-scheme. In addition c must be in normal form, because a is in normal form ; it must not contain free variables different from x and y because it has to be closed. Thus c ≡ x or c ≡ y. Let's suppose that c ≡ y , then a ≡ λxy.y : A→(Β→Β) since : λx.y : B→B _____________________ a ≡ λxy.y : (A→(B→B))which is impossible. Thus c ≡ x and then a > λxy.x ≡ Κ λ .(Analogously for S λ ). ∆Thus K λ and S λ are the only closed normal forms of type schemas corresponding to the axioms for PP o . 3.6.1 gives their operational behaviour. In accordance to these facts, define the theory of proofs of PP 0 as follows.3.7 Definition : Combinatory Logic (CL >) is the calculus of proofs of PP 0 axiomatized by: Kab > a Sabc > ac(bc) plus inference rules (ρ), (µν) and (τ) in 3.3.3.8 Corollary: Let [x].b be defined as in 2.7 . Then ([x].b)a > [a/x]b . Proof: (By induction on the structure of b ). Consider the possible cases for b and use the constructive version of the deduction theorem in PP 0 . -If b = x then [x].b ≡ SKK ≡ I , thus (SKK)a > Ka(Ka) > a = [a/x]b . -If x∉FV(b) then [x].b ≡ Kb and Kba > b ≡ [a/x]b . -b = cd; then [x].b ≡ S([x].c)([x].d) and S([x].c)([x].d)a > ([x].c)a(([x].d)a) > [a/x](cd) . ∆

  Term expressions: a := var | fst a | snd a | (aa) | <a,a> | (λvar:A.a) Type expressions: A := Atomic | (∀var:A.A ) | (∃var:A.A ) The derivations from lists of assumptions (or assignement of types to variables, see below) are summarized as judgements, following Martin-Löf terminology. Γ(x:A) stands for the ordered list Γ extended with (x:A). Judgements: Γ ok ; Γ | _ A : Tp ; Γ | _ A = B : Tp ; Γ | _ a : A ; Γ | _ a = b : A .

  A . B) : Tp (*) (∃x : A . B) : Tp (*) A . B) = (∀x : C . D) : Tp (∃x : A . B) = (∃x : C . D) : Tp Remark: As for (*) , observe that in B there is no free variable whose type depends on x. Conventions: 1 -If x∉FV(B), set A→B for ∀x:A.B and A×B for ∃x:A.B . 2 -In the rules we are only writing the part of the assumptions which is discharged in the conclusion. Thus a jugement J in a rule stands for Γ | _ J (see 4.1(ii)). Dependent products (introduction, elimination, equality): [x:A] | _ b : A.b)a = [a/x]b : [a/x]= c : ∃x:A.B 4.1 Remarks: (i) -By the rules, x:A is allowed in judgements only if x∉FV(A).(ii) -Note that (∀I) could be equivalently written asΓ | _ A : Tp Γ(x:A) | _ a : B (∀I) ______________________ Γ | _(λx : A. a) : (∀x : A. B) thus, by the rules, when (∀I) is applied, x is not free in uncancelled hypothesis. Similarly in the related cases. (iii) One may equivalently define PN 1 as an extension of PN o , but the expressions and rules of PN o may be derived from the presentation just given. Since, for x∉FV(B), A→B ≡ ∀x:A.B , one has that (→I) and (→E) in PN o are special cases of (∀I) and (∀E) . Observe that, if there are no atomic types with free variables, PN 1 would coincide with PN o .4.2 Definition:PN 1 is the deductive system defined above and λP is the calculus of its proofs (as terms) .The reader may recognize two familiar properties of first order Logic in the theorems in Proposition 4.3: Proposition 4.3 explicitely gives their constructive proofs. 4.3 Proposition. 1) If x∉FV(B) , then exists c such that : PN 1 | _ c : (∀x : A.(B→C))→(Β→∀x : A.C). 2) If x∉FV(C) , there exists c such that : PN 1 | _ c : (∀x : A.(B→C))→((∃x : A.B)→C) . B.λx : A.zxy) : (B→(∀x : A.C)) ________________________________________________________________ (→Ι) (λz : (∀x : A.(B→C)).λy : B.λx : A.zxy) : (∀x : A.(B→C))→(Β→(∀x : A.C)) where y is a fresh variable s.t. y∉FV(BCA) ; (*) x∉FV(B) as (y:B) follows, in the ordered set of assumptions, (x:λy : (∃x : A.B).z(fst y)(snd y) : ((∃x : A.B)→C) ______________________________________________________________ (→Ι) λz : (∀x : A.(B→ C)).λy : (∃x : A.B).z(fst y)(snd y) : (∀x : A.(B→C))→((∃x : A.B)→C) (**) by assumption x∉FV(C) .

4. 4

 4 Remark. Another aspect of the greater expressive power of Type Theory, is given by the (∃E) rule. The "there exists elimination" rule is usually formalized in Natural Deduction as ∃x:A.B B | _ C (∃E) 1 _____________ with x∉FV(C) C while the (∃E) in dependent sums above is equivalent to a : ∃x:A.B x : A, y : B | _ c : [<x,y>/z]C (∃E) 2 _______________________________ (Let <x,y> = a in c) : [a/z]C where z may occur free in C . Thus (∃E) 2 is much stronger than (∃E) 1 , since, by the proof terms, one has both first and second projections, as in (∃E). This requires a little proof. First observe that, rules corresponding to (∃E=), (∃β), (∃η) for the (Let..... in...) may be easily given, e.g. <a,b> : ∃x:A.B x : A, y : B | _ c : [<x,y>/z]C (∃β) 2 ___________________________________ (Let <x,y> = <a,b> in c) = [a/x,b/y]c: [<a,b>/z]C c: ∃x:A.B (∃η) 2 ___________________________ (Let <x,y> = c in <x,y> ) = c: ∃x:A.B . (∃E=) is obvious. Then define, for a: ∃x:A.B , fst a = Let <x,y> = a in x : A snd a = Let <x,y> = a in y : [fsta/x]B . What needs to be proved is that (snd a) is well typed. Indeed, x:A, y:B | _ x = fst<x,y> : A by (∃β) 2 x:A, y:B | _ B = [fst<x,y>/x]B : Tp by B = [x/x]B x:A, y:B | _ y : B x:A, y:B | _ y : [fst<x,y>/x]B , which is identical to [<x,y>/z][fstz/x]B.

  var | (aa) | (aA) | (λvar:A.a) | (λVar:Tp.a) Type expressions: A := Var | Atomic | (∀var:A.A ) | (∀Var:Tp.A )

  Tp . B) = (∀X : Tp . D) : Tp (*) In B there is no free variable whose type depends on X .

  Tp. fx) = f : (∀X : Tp . B)

  Tp.b) : ⊥ Proof. Indeed, we can give a constructive version of (1) , the absurdum rule of Intuitionistic Logic, as a derived rule. 1) Let a : (∀X : Tp.X) ≡ ⊥ , fixed a generic A : Tp ,we have: second inference is just a trivial application of (∀ 2 Ι). ∆5.5 Definition: A ∧ B ≡ ∀Y : Tp.((A →(Β→Y))→Y) A ∨ B ≡ ∀Y : Tp.((A→Y) ∧ (B→Y)→Y) . λp : (A→(B→X)).pab : (A→(B→X))→X _______________________________________________ (∀ 2 I) λX : Tp.λp : (A→(B→X)).pab : (∀X : Tp.((A→(B→X))→X)) 2) Analogously : a : (∀X : Tp.((A→(B→X))→X)) A : Tp ________________________________________ (∀ 2 E) aA : (A→(B→A))→Α K λ : A→(Β→A) _________________________________________________________ (→E) aAK λ : A Note that A is a generic type and K λ is uncancelled because its type-scheme is a theorem . Use K λ I to obtain the second projection. ∆ 5.7 Definition: ∃X : Tp.A ≡ ∀Y : Tp.((∀X : Tp.(A→Y))→Y) . More generaly, one may derive also a first order existential quantifier, by setting, for B : Tp , ∃x : B.A ≡ ∀Y : Tp.((∀x : B.(A→Y))→Y) .

5. 8

 8 Definition: <a,b> A ≡ λY : Tp.λx : (∀X : Tp.A→Y).xab . 5.9 Remarks: 1 -Note that [a,b] ≡ λx.xab is the classical type-free pairing and may be obtained from <a,b> A by erasing all type information.. As in the type-free case, the second order typed pairing is not surjective, i.e. for no projections fst([a,b]) and snd([a,b]) one has that [fst([a,b]), snd([a,b])] = [a,b]. 2 -Definition 5.8 and the theorems below are only stated for K = Tp . They also hold for K:Tp. In particular, <a,b> A ≡ λY : Tp.λx : (∀x : C.A→Y).xab , for C : Tp , is a first order pairing. (∀X : Tp.A→Y).xBb) : ((∀X : Tp.A→Y)→Y) _________________________________________________________ (∀ 2 I) (λ Y : Tp.λx : (∀ X : Tp.A→ Y).xBb) : (∀ Y : Tp.(∀ X : Tp.A→ Y)→ Y) ∆ Also (∃ 2 E) is a derived rule : 5.11 Theorem. a : ∃X : Tp.A [X : Tp , x : A] | __ c : C (∃ 2 E) ____________________________________________ if x,X∉FV(C) aC(λX : Tp.(λx : A.c)) : C . Proof. Let a ≡ <B,b> A ≡ λY : Tp.λx : (∀X : Tp.A→Y).xBb , i.e. a : (∃X : Tp.A) ≡ ∀Y : Tp.(∀X : Tp.A→Y)→Y) , where B : Tp and b is a term. ∀X : Tp.(A→C)→C) λX : Tp.(λx : A.c) : (∀X : Tp.(A→C)) (∀ 2 E)* ______________________________________________________________________ aC(λX : Tp.(λx : A.c)) : C * Note that in these derivations we used the hypothesis X,x∉FV(C), as we applied (∀I) ≡ (→I) and (∀E) ≡ (→E). ∆ 5.12 Corollary. <B,b> A C (λX : Tp.λx : A.c) = [B/X,b/x]c : C Proof. (λY : Tp.λx : (∀X : Tp.A→Y).xBb) C (λX : Tp.λx : A.c) for Y∉FV(A) = (λx : (∀X : Tp.A→C).xBb) (λX : Tp. λx : A.c) = (λX : Tp.λx : A.c) Bb = [B/X,b/x]c . ∆ 5.13 Remark. (On second order "there exists elimination" rules).

  (ii) However, one may consistently extend PN 2 by a stronger rule. Namely, define pairing <,> , as an independent function symbol, by rules such as (∃I) and (∃I=) in §.4 (where A becomes Tp). Then set a : (∃X : Tp.B) [X : Tp , x : B] | __ c : [<X,x>/z] C (∃ 2 E) 2 _______________________________________________ X,x∉FV(C) (Let <X,x> = a in c) : [a/z]C

  = B : Tp. Then 5.11 proves <b,a> A : (∃x': B.A) [x': B, x : A] | __ c : C (w∃E) ________________________________________ with x',x∉FV(C) . (<b,a> A )C(λx': B.(λx : A.c)) : C By corollary 5.12, also a corresponding (w∃β) is derivable and one may obtain the first projection. Just take c ≡ x' and C ≡ B , which is possible, as B cannot depend on x', x . Then, by 5.11 and 5.12, one has (<b,a> A )C(λx': B.(λx : A.x)) = b : B .

  : [A/X]B where (λX:Tp.a) : (∀X:Tp.B) summarizes also that (∀X:Tp.B) : Tp (see §.5).

  without a general presentation of what a model should be. (Notation: unless otherwise stated, f : A → B or f∈(A → B) is an arbitrary function from the set (or class) A to the set (or class) B . Indeed, we first argue in the category Set of sets and functions) The intended operational meaning of second order types is that a term (λX:Tp.a) of type (∀X:Tp.B) is a procedure which takes a type C, say, as input and gives as output the term [C/x]a of type [C/x]B. This is exactly what (∀ 2 E) says. As for the interpretation over a mathematical structure, assume that Tp is interpreted as the set M. Then: 1 -Write first (∀X:Tp.B) as ∀(λX:Tp.B) , i.e. understand ∀ as a map from (Tp → Tp) to Tp, as it turns the map λX:Tp.B in (Tp → Tp) into a type. Thus the interpretation of ∀ should be a map from M→M to M . 2 -Define [c] ξ as the interpretation of the type or term c under environment ξ and set f = [(λX:Tp.a)] ξ . Then, by (∀ 2 E) and the way we understood it before, f: M → ∪ C∈M [B] ξ[C/X] , with f(C)∈ [B] ξ[C/X] . This idea corresponds to the notion of dependent or indexed product in Set Theory: any f as above is an element of the set-theoretic product Π C∈M [B] ξ[C/X] , indexed over the set M of types. In short, assume that g∈(M→M) interprets λX:Tp.B : (Tp → Tp) , then f∈Π C∈M g(C) = Π C∈M [B] ξ[C/X] and Π C∈M [B] ξ[C/X] is an element of M, i.e. a type. Thus, one has to find a set, M, with the following closure property: it must be closed by products indexed over the set M itself. That is, for all functions g: M → M we want (0) Π e∈M g(e) ∈ M . This property interprets in M the circularity of (∀X:Tp.B) : Tp , the crucial judgement of impredicative Type Theory. In categorical terms (w. r. t. the category Set), this means that we want a full subcategory M of Set which is cartesian closed, has all products indexed by the set M o of objects of M and the embedding of M in Set preserves function spaces, finite products and M o -indexed products. (For a general definition of categorical model for system F, along this

(

  effective) and bijective coding of pairs. (Notation: Let A be a symmetric and transitive relation on ω. Set then: n A m iff n is related to m by A , dom(A) = {n | n A n }, {n} A = {m | m A n } the equivalence class of n w.r.t. A , Q(A) = {{n} A | n ∈ dom(A)} ) 6.1 Definition: The category PER has as objects: A∈PER iff A is a symmetric and transitive relation on ω, morphisms : f∈PER[A,B] iff f : Q(A) → Q(B) and ∃n ∀p (pAp ⇒ f({p} A ) = {n . p} B ).

6. 4

 4 Definition. The category M , of the modest sets, is the subcategory of ω-Set whose objects (X, | __ ) have a single valued relation " | __ " ; that is, " | __ " satisfies (SV) ∀a,b∈X n | __ a ∧ n | __ b ⇒ a = b. Morphisms are defined as for ω-sets . If A is a p.e.r., then In(A) is clearly a modest set, since the elements of Q(A) are disjoint (non empty) subsets of ω . Therefore, In defines an embedding from PER into M. Conversely, for every modest set (X, | __ ) we define a p.e.r. Out(X), by nOut(X)m ⇔ ∃a∈X n,m | __ a .

8. 1

 1 Remark.In ω-Set products are defined in the obvious way: just use a coding of pairs for the natural numbers. 6.3 suggests how to define function spaces:[A → B] = ({f: A → B | f∈ω-Set [A,B] }, | __ A→ B ) .Observe that [A → B] is also obtained from ([Π a∈A g(a)], | __ ) in 6.5, when g is costantly equal to B . The terminal object is simply (1, | __ 1 ) , where 1 is the singleton set and | __ 1 = ω×1 .Equalizers are given by ({a∈A | f(a) = g(a)} , | __ fg ) where n| __ fg a iff n| __ A a .

Remark:The following rules are admissible. For any judgement J ,Γ | _ a : A Γ,(x:A) | _ J (Sub) ______________________ Γ | _ [a/x]J Γ | _ a = b : A Γ | _ [a/x]J

Research supported in part by the Joint Collaboration Contract # ST2J-0374 -C (EDB) of the European Economic Communitee. This paper is based on an invited lecture delivered at the workshop "Semantics of Natural and Computer Languages" Half-Moon-Bay (Stanford), March 1987. (*) On leave from Dipartimento di Informatica, Universita' di Pisa, Italy. This author's work has been made possible also by the generous hospitality of the Computer Science Dept. of Carnegie Mellon University, while teaching in this University during the academic year 1987/88, and by the support of the french CNRS during summer 1990.

With the help of M we explain the relation among certain products in ω-Set and the interpretation of universal quantification in the model defined in 6.2 . The crucial point is to look at PER also as an object of ω-Set by setting:

M o = (PER,| __ M )∈ω-Set where | __ M = ω× M .

(If there is no ambiguity, we call PER also the set of objects of the category PER).

This idea will be developped more rigorously in §.8, where we turn PER into an internal category M' of ω-Set, whose "object of objects" is M o , and prove that the product below, or the intersection of p.e.r.'s, is the object component of an internal product functor.

There is a straightforward way to define a naïve product in ω-Set. Remark. Clearly, ([Π a∈A g(a)], | __ ) in 6.5 is a well defined object of ω-Set. In categorical terms, ([Π a∈A g(a)], | __ ) is an indexed product in ω-Set "indexed over" itself. However, we may avoid, here, the general notion of indexed category and indexed product and keep the presentation fairly elementary.

What is nice is that, as soon as the range of g is restricted to M, this product lives in M:

6.6 Theorem. Let (A, | __ A )∈ω-Set and g: A → M .

Then ([Π a∈A g(a)], | __ Π,g )∈M .

Proof: Let | __ Π,g be defined as in 6.5. All what we need to show is that, under the assumptions, | __ Π,g satisfies (SV) above. Hence,

In §.7, we show the relation between this notion of indexed product (over M o ) and intersection of p.e.r.'s, used in the model defined 6.2.

Products and intersections.

Recall that each X∈M corresponds exactly to the partial equivalence relation Out(X). By an abuse, we identify objects X of M and the corresponding p.e.r. Out(X), when this helps in the presentation. Then, the product in 6.6, for (A, | __ A )∈ω-Set and g: A → M , may be equivalently written as n [Π a∈A g(a)] m iff ∃f∈Π a∈A g(a) ∀a∈A ∀p,q | __ A a n . p,m . q | __ g(a) f(a) iff ∀ a ∈ A ∀ p,q | __ A a n . p g(a) m . q (7.1).

Observe now that the first order types are interpreted in Troelstra[1973] as follows: We are now in the position to explain how this intersection fits with the (naïve) meaning of universal quantification as indexed product. (This also hints (naïvely) to a unified framework, which includes the first order quantification, in view of the relation between (7.1) and (7.2)). Surprisingly enough, the intersection over M in 7.3 is indeed a product. This may be shown when working in ω-Set, as "frame" category. More precisely, theorem 7.4 below shows that the intersection and the product in 6.5, for M o = (PER, | __ M )∈ω-Set and g: M o → M, are isomorphic in M. Thus, the intersection interpretation of second order types fits with their interpretation as products. Moreover, by 6.6 and 7.4, the meaning of functional types (more generally, of first order quantification) and second order quantification turns out to be given by the same kind of product. §.8 will complete the required category-theoretic explanation of the notion of product we are talking about. Then, when universally quantified types are interpreted as intersections, terms of these types are interpreted as equivalence classes in the intersections. Thus G({n} S )(a) = {n} g(a) tells us how to apply {n} S to (the interpretation of) a type a.

Theorem. Let (A, | __ A )∈ω-Set be such that | __

Next we prove that the intersection is the object component of a product functor (over M o ) for the intended internal category. This provides a categorical justification of λP 2 , by using the notion of internal category. As we do not have space to get into a complete treatment of indexed categories, we refer to [START_REF] Hyland | A small complete category[END_REF] and [START_REF] Ehrhard | A Categorical Semantics of Constructions[END_REF] for the categorical understanding of both first and second order quantification and, in the following section, we focus only on the crucial impredicative case, the second order products or quantification over types. §.8 Π is the right adjoint of the diagonal functor

As already mentioned, the point of the present interpretation is its naïve "set-theoretic" flavour, an helpful aspect in applications to the denotational semantics of programming constructs (see, for

Proof. The category of effective objects is a full sub-lCCC of Eff (see Hyland[1982, §.7]), i.e.

it is a full subcategory of Eff and inherits the structure of lCCC from Eff. Since M and the category of effective objects are equivalent (and the lCCC structure of a category is preserved by equivalences), M inherits the lCCC structure via the equivalence. A similar argument can be carried out for ω-Set (use Hyland[1982;§.6]). ∆

In particular the category Cat(ω-Set) of internal categories and internal functors of ω-Set is a full sub CCC of Cat(Eff). We now explicitly give the internal version M'∈Cat(ω-Set) of M.

Lemma. If <F,τ,G>∈ω-Set[M o ,M 1 ] then ∃n ∀A∈PER τ(A) = {n} F(A)→G(A) .

Proof. Suppose that m | __ <F,τ,G>. Since 0 | __ A for any A∈PER , then take n = m . 0 and observe that n | __ <F(A),τ(Α),G(A)>. Thus τ(A) = {n} F(A)→G(A) . ∆ 8.6 Remark. As a matter of fact, some function spaces in ω-Set are surprisingly small. For example, while for all A∈ω-Set, ω-Set[A,M o ] contains all functions from A to PER, when B is a modest set, ω-Set[M o ,B] is just the set of the constant functions from PER to B . The reader may have recognized in this a consequence of the validity of the Uniformity Principle (UP) in Eff. Indeed, this principle was implicitly used in 7.4 . The relevance of (UP) is stressed in [START_REF] Rosolini | About Modest Sets[END_REF], where a generalized version of 7.4 is stated for any index object satisfying (UP).

In definition 6.5 we gave a notion of "product", [Π a∈A F(a)] , over an ω-set (A, | __ A ) (thus, in particular, over M o ). This is the natural candidate for the object part in the definition of the product functor. In view of theorem 7.4, it is clear now that one can equivalently use intersection as product. This makes the connection with the PER model in 6.2 more apparent (and simplifies the computation of a realizer for Π 1 ).

Definition (The product functor

8.8 Fact. Π in 8.7 is well defined. In particular, Π 1 is realized by any number p such that , for all m , p . m = m . 0 . = m (cf. 7.4 and 8.8).

Just for curiosity, if one defines Π 1 by using Π o (F) = [Π a∈PER F(a)], then Π 1 is realized by s , with s . p . q . r = p . r . (q . r) , the other basic combinator of Combinatory Logic. The reader may find a detailed analysis of the completeness properties of the internal category M', necessary to turn it into a model of construction, in [START_REF] Hyland | A small complete category[END_REF], [START_REF] Ehrhard | A Categorical Semantics of Constructions[END_REF] and Robinson[1989]. The definition of model for system F , by internal categories, originally due to Moggi, is described and related to other approaches in Asperti&Longo[1990].

Remark:

There is another property of the right adjoint that has to be verified in order to guaranty that substitution is well-behaved, namely the Beck-Chevalley condition (see [START_REF] Hyland | A small complete category[END_REF], Hyland&Pitts [1987]). However, this condition is automatically true when quantification is restricted to M o , because the only right-adjoint required for the interpretation are

Conclusion: methods and applications.

Going back to the introductory discussion on "denotation and meaning", one may argue that the syntax is largely used in the semantics: the partial recursive functions, which define the morphisms in PER, M and ω-Set, are exactly the lambda definable functions! However, one may use the good old λ o as a computing device and explain by this λP 2 , as it is above. Moreover, one may hide computability in the background or avoid it, as the definition of all the three categories can be relativized to any (partial) Combinatory Algebra or model of the type-free Combinatory Logic in 3.7 (see Hyland [1982], Longo&Moggi[1989]). Thus, one may take a model of λ o constructed by topological tools, as done in [START_REF] Scott | Continuous lattices" Toposes, algebraic Geometry and Logic[END_REF][START_REF] Scott | Data types as lattices[END_REF], and understand λP 2 in terms of continuous functions.

The case discussed in this paper is an example of an interesting interaction between structural meaning and formal systems. Mathematical structures suggested formal calculi of (typed) functions or the proof theory related to the various lambda calculi. For example, Girard's system F was invented for the proof theoretic investigation of second order Arithmetic, which is