Computer Science – Logic in Computer Science
Scientific paper
2000-11-23
Computer Science
Logic in Computer Science
26 pages, no figure
Scientific paper
We characterize those intersection-type theories which yield complete intersection-type assignment systems for lambda-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the intersection constructor set-theoretic inclusion, and by taking the interpretation of the arrow constructor a' la Scott, with respect to either any possible functionality set, or the largest one, or the least one. These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Secondly, the characterizations are all given just in terms of simple closure conditions on the preorder relation on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Lastly, we do not restrict attention just to lambda-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted lambda-calculi. Nevertheless the characterizations we give can be tailored just to the case of lambda-models.
Alessi F.
Dezani-Ciancaglini Mariangiola
Honsell Furio
No associations
LandOfFree
A Complete Characterization of Complete Intersection-Type Theories does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Complete Characterization of Complete Intersection-Type Theories, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Complete Characterization of Complete Intersection-Type Theories will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-729552