The Type Of Intersection And The Standardized Nature Of ?-calculus

The lambda calculus is a theory of functions as formulas.It is a system for manipulating functions as expressions.It has some connections with computability,computer science,logic and mathematics.It is equal to Turing machine and it is the basis of functional programming.Moreover,it has corresponding relationship with logic according to Curry-Howard isomorphism.Mathematicans can build various math models by lambda calculus.Therefore,the study of A-calculus plays an important roles in computability theory,programming language designing,logic and mathematics.Normalizing,Church-Rosser theorem,standardization and separation ect.are important properties for studing ? calculus.Simple typed lambda calculus assigns a type(atomic or func-tion type)to each term.But some terms cannot be typed in simple type calculus,such as ?x.xx.Intersection types are introduced as extension to simple types,?-terms corresponding to correct programs not typeable in the standard curry-style simple type system are typeable with intersec-tion type.Intersection types are first introduced to provide a characterization of strongly normal-izing ?-terms,and then are used to prove various properties of ? calculus and its variants.The?-calculus has many variants so far.For example,??,?Gtz are extensions of A-calculus from the view of Curry-Howard isomorphism.?? is an extension of ??y-calculus which is correspond-ing to classical natural deduction.?Gtz is corresponding to intuitionistic sequent calculus.We put attention to the normalization property of ??-calculus and ?Gtz-calculus.The works of this dissertation are as follows:1.The normalizing theorem for ?-calculus states that the leftmost reduction strategy is nor-malizing and is always used in proving that a term has no normal form.It was demonstrated by Curry which is based on Church-Rosser theorem and standardization theorem,of which proofs are likely quite complex.In this paper,we give a different method which is only based on simple properties of the typing system.We utilize the intersection type assign-ment system to verify the normalizing theorem.We show that terms typeable in a certain intersection type assignment system is normalizable by leftmost reduction.2.?? is proposed to recover the separation property of ?? and the property is proved by Saurin.In this paper,we present a new type assignment system for ??-calculus using intersection and product types,and define the perpetual strategy for ??-calculus.We show that the system satisfies the subject reduction and weak subject expansion properties for perpetual strategy.Moreover,we show that the type assignment system characterizes those terms which are strong normalizing.3.Intersection type can be idempotent or non-idempotent according to whether A?A =A.They have been used in a series of papers for characterizing strong normalization in natu-ral deduction style.Regarding the sequent calculus,only idempotent type systems have been used so far.Characterization results by idempotent intersection types are always proved by reducibility techniques or lifting the characterization result for the middle cal-culus whose results are known to the new extended calculus.These methods are always complex and undirect.In this paper,we introduce a non-idempotent intersection system for ?Gtz-calculus,which is in sequent calculus style.We show that a ?Gtz-term is typeable if and only if it is strongly normalizing directly.Non-idempotent intersection type sys-tems are just based on the decrease of a non-negative integer measure.They are usually considered as simpler.