INFINITE MULTI-BASES

INFINITE MULTI-BASES

PAULA SEVERI

Dipartimento di Matematica ed Informatica,Universit`a degli Studi di Udine

Γ?λx.M:A→B

246PAULA SEVERI

This rule is not valid ifΓis a multi-basis.We cannot derive thatΓ?λx.M:A→B from Γ,x:A?M:B because there may be some other declaration for x inΓbesides x:A.If the setΓ(x)={x:A1,...,x:A n}of declarations for x inΓis?nite then we could consider the following variant of(→I).

Γ?M:B

(→I’)

.

Γ?Tλx.M:A→B

Since it is not clear when the typing rules will be valid,we also have to be careful how we de?ne typability for multi-bases.We de?ne that a term is typable in a multi-basisΓif it is typable in a?nite basis that is contained inΓ.Having this de?nition in mind,we investigate whether the typing rules are derivable for multi-bases.

In Section1we simplify matters and study in?nite bases(with no multiple declarations for the same variable)for the simply typed lambda calculus.

In Section2we study multi-bases for intersection type assignment systems.We?rst give examples that show that(→I)and(∩I)are not derivable.We,then,show that all rules, except(→I),are derivable if we require that the bases are closed under∩.Finally,we show that the rule(→I”)shown above is indeed derivable.

In Section3,we present an application of our study of multi-bases.We prove that a function onλ-terms satis?es the type semantics property if and only if this function coincides with the usual?lter interpretation onλ-terms.The”only if”is the well-known type semantics theorem which we will prove using multi-bases.The other direction is an interesting obser-vation since it means that there is only one way of de?ning application and abstraction on the set of?lters when the type semantics property holds.

1.Infinite Bases in Simply Typed Lambda Calculus

In this section we recall the de?nition of simply typed lambda calculus[2]where bases are assumed to be?nite.For the extension to in?nite bases,we do not rede?ne the typing system.Instead,we de?ne that a term is typable in an in?nite basis?if it is typable in a ?nite basis that is contained in?.Then,we show a variant of rule(→I)that is derivable. De?nition1.1.Let A be a set of atomic types.The set T of simply types is de?ned by:

T=A|T→T

De?nition1.2.(1)A declaration is a statement of the form x:A with A∈T.

(2)A(singled)basisΓis a set of declarations with all variables distinct,i.e.there is

only one declaration per variable.

De?nition1.3.Let M∈Λ,A∈T andΓa?nite singled basis.The simply typed lambda calculus derives assertionsΓ?M:A by the following axioms and rules.

INFINITE MULTI-BASES247

(ax)Γ?x:A if(x:A∈Γ)

(→I)

Γ,x:A?M:B

Γ?MN:B

De?nition1.4.Let?be a basis that is allowed to be in?nite.We de?ne??M:A i?there exists a?nite basisΓ??such thatΓ?M:A.

Lemma1.5.The axiom(ax)and rule(→E)are derivable when the basisΓis in?nite. Since the basisΓcan contain all variables,the rule(→I)is derivable for in?nite bases only if it is reformulated in the following way.

Lemma 1.6.LetΓbe a possible in?nite basis.The following variant of rule(→I)is derivable:

Γx,x:A?M:B

A≤C (incl L)A∩B≤A(incl R)A∩B≤B (glb)

C≤A C≤B

248PAULA SEVERI

De?nition2.4.Let M∈Λ,A∈T∩andΓa?nite singled basis.The(intersection)type assignment system over an intersection type theory T derives assertionsΓ?T M:A by adding the following rules to the axioms and rules of De?nition1.3.

Γ?T M:AΓ?T M:B

(∩I)

Γ?T M:B

De?nition2.5(Multiplication of bases).

Γ?Γ′={x:A∩B|x:A∈Γand x:B∈Γ′}

∪{x:A|x:A∈Γand x∈Γ′}

∪{x:B|x:B∈Γ′and x∈Γ}.

For example,{x:A,y:B}?{x:C,z:D}={x:A∩C,y:B,z:D}.

Lemma2.6.The following rules are admissible in all intersection type assignment systems.

Γ,x:B?T M:A C≤T B

(≤?T L)

Γ1?Γ2?T M:A

De?nition2.7.A multi-basisΓis a set of declarations,in which the requirement that

x:A,y:B∈Γ?x≡y?A≡B

is dropped.Then,the setΓ(x)is de?ned as{A|x:A∈Γ}.

For an in?nite multi-basisΓ,the setΓ(x)could be in?nite.

De?nition2.8.Let?be a(possibly in?nite)multi-basis.We de?ne??T M:A i?there exists a singled(only one declaration per variable)basisΓ??such thatΓ?T M:A. Let CDS be the smallest intersection type theory over the set A={α1,α2,...}∪{U}of atoms originally de?ned in[4].The following examples show that the rules(∩I),(→E)and (→I)are not derivable for multi-bases.

Example2.9.Rule(∩I)is not derivable.

x:α1,x:α2?CDS x:α1∩α2.

Example2.10.Rule(→E)is not derivable:

x:α1→α2,x:α1?CDS xx:α2.

Example2.11.Rule(→I)is not derivable.

ConsiderΓ={x:α1∩α2,x:α1};

A=α2;

B=(α1→α2→α3)→α3;

M=λy.yxx.

We have thatΓ,x:A?CDS M:B,butΓ?CDS(λx.M):(A→B).

De?nition2.12.We say that a multi-basisΓis closed under∩if for all x∈dom(Γ)the setΓ(x)is closed under∩,i.e.A,B∈Γ(x)?A∩B∈Γ(x),up to equality of types in the type theory T under consideration.

INFINITE MULTI-BASES249 Theorem2.13.All the typability rules of the de?nition of type assignment,except for

(→I),are derivable for(possibly in?nite)multi-bases that are closed under∩.

Proof.We only prove that rule(→E)is derivable.The other cases are similar or simpler.Let Γbe a(possible in?nite)multi-basis.AssumeΓ?T M:A→B andΓ?T N:A.There exist ?nite singled basesΓ1,Γ2?Γsuch thatΓ1?T M:A→B andΓ2?T N:A.By Lemma 2.6,applying rule(multiple weakening),we getΓ1?Γ2?T M:A→B andΓ1?Γ2?T N:A. Then,applying rule(→E)on?nite bases,we have thatΓ1?Γ2?T MN:B.SinceΓis closed under∩,Γ1?Γ2?Γ.Hence,Γ?T MN:B.

De?nition2.14.LetΓbe a multi-basis.We de?ne the replacement of all declarations of x inΓby a set X?T∩as follows.

Γ[x:=X]={y:A|A∈Γ(y)&y=x}∪{x:B|B∈X}.

The condition of being closed under∩is not strong enough to ensure that rule(→I)is derivable for in?nite multi-basis.Take,for instance,X=T∩,the set of all types.Then the premisse of(→I)isΓ[x:=T∩]?T M:B does not give any information about the type A that has been used to type the free variables of M.

Theorem2.15.LetΓbe a(possible)in?nite multi-basis.The following variant of(→I) using principal?lters is derivable

Γ[x:=↑A]?T M:B

(→I”)

250PAULA SEVERI

We de?ne F T={X?T∩|X is a?lter over T}.

Lemma3.2.IfΓ(x)is a?lter thenΓ(x)={A|Γ?x:A}.

De?nition3.3.Let D?P(T∩),ρ∈V→D and fρ∈Λ→D.

(1)Γρ={x:A|A∈ρ(x)}.

(2)We say that f satis?es the type semantics property in?T if

fρ(M)={A|Γρ?T M:A}for all M∈Λ,ρ∈V→D

Next we de?ne the notion of?lter interpretation[4,3,5].A?lter interpretation may not be aλ-model[1]since it may not satisfyβ-reduction.

De?nition 3.4.Let T be an intersection type theory andρ∈V→F T.The?lter interpretation[[]]ρis a function fromΛto F T de?ned as follows.

[[x]]ρ=ρ(x)

[[λx.N]]ρ=↑{B→C|C∈[[N]]ρ(x:=↑B)}

[[NP]]ρ=↑{B|?C∈[[P]]ρ.(B→C)∈[[N]]ρ}

We now prove that a function that satis?es the type semantics property coincides with the ?lter interpretation.This means that the only way of interpreting the abstraction and the application on F T is the one given in De?nition3.4.

Theorem3.5.The function f satis?es the type semantics property in?T if and only if D?F T and fρ=[[]]ρfor allρ∈V→D.

Proof.

(?)If f satis?es the type semantics property in?T then it is easy to prove that fρ(M)is a?lter using the de?nition of?T.

Letρ∈V→D.We prove that fρ(M)=[[M]]ρfor all M∈Λby induction on M.

(1)Case M=x.

fρ(x)={A|Γρ?T x:A}by the type semantics property

=Γρ(x)by Lemma2.16

=ρ(x)

=[[x]]ρ

(2)Case M=λx.N.

fρ(λx.N)={A|Γρ?Tλx.N:A}by the type semantics property

={A| n i=1(B i→C i)≤A&Γρ[x:=↑B i]?T N:C i}by Lemma2.16

=↑{B→C|Γρ[x:=↑B]?T N:C}

=↑{B→C|C∈fρ(x:=↑B)(N)}by the type semantics property

=↑{B→C|C∈[[N]]ρ(x:=↑B)}by induction hypothesis

=[[λx.N]]ρ

(3)The case of the application is similar to the previous one.

(?)We prove that[[M]]ρ={A|Γρ?T M:A}by induction on M.

(1)The case M=x follows from Lemma3.2.

INFINITE MULTI-BASES 251

(2)If M =λx.N ,then

[[λx.N ]]ρ=↑{B →C |C ∈[[N ]]ρ(x :=↑B )}

=↑{B →C |Γρ[x :=↑B ]?T N :C }by induction

hypothesis ={A | n i =1(B i →C i )≤A &Γρ[x :=↑B i ]?T N :C i }

={A |Γρ?T λx.N :A }by Lemma 2.16

(3)The case M =NP is similar to the previous one.

Acknowledgement

The author wishes to acknowledge useful comments and discussions with Mariangiola Dezani-Ciancaglini,Furio Honsell and Fer-Jan de Vries.

References

[1]H.P.Barendregt The Lambda Calculus:Its syntax and semantics .North-Holland Publishing co.,Ams-

terdam,1984.

[2]https://www.wendangku.net/doc/0311193757.html,mbda calculi with types.In Abramsky Gabbai and Maibaum,editors,Handbook

of Logic in Computer Science ,volume II.Oxford University Press,1992.

[3]H.Barendregt,M.Coppo,and M.Dezani-Ciancaglini.A ?lter lambda model and the completeness of

type assignment.J.Symbolic Logic ,48(4):931–940,1983.

[4]M.Coppo and M.Dezani-Ciancaglini.An extension of the basic functionality theory for the λ-calculus.

Notre Dame J.Formal Logic ,21(4):685–693,1980.

[5]M.Coppo,M.Dezani-Ciancaglini and G.Longo.Applicative information systems.In CAAP ’83

(L’Aquila,1983),pages 35–64.Springer,Berlin,1983.

[6]M.Coppo,M.Dezani-Ciancaglini,F.Honsell,and G.Longo.Extended type structures and ?lter lambda

models.In Logic Colloquium ‘82,pages 241–262.North-Holland,1984.

[7]M.Dezani-Ciancaglini,F.Honsell,and https://www.wendangku.net/doc/0311193757.html,positional characterization of λ-terms using

intersection https://www.wendangku.net/doc/0311193757.html,put.Sci.,304(3):459–495,2005.

Cambridge