| A Complete Characterization of Complete Intersection-Type Preorders (2007) | |||||||||||||||||
Abstract | |||||||||||||||||
| this paper we solve completely the characterization problem as far as the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics [Scott 1975] and the F-semantics [Scott 1980b]. These are the semantics which arise by interpreting types as subsets of applicative structures, and by taking as interpretation of the preorder relation, set-theoretic inclusion, as interpretation of the intersection constructor, set-theoretic intersection, and by taking the interpretation of the arrow constructor, a la Scott, as a logical predicate, with respect to either any possible functionality set, or the largest one, or the least one. More precisely, the simple semantics of types associates to each arrow type A B the set of elements which applied to an arbitrary element in the interpretation of A return an element in the interpretation of B | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||