A domain-theoretic semantics of lax generic functions

摘要

The semantic structure of a polymorphic calculus λ{sub}m is studied. λ{sub}m is defined over a hierarchical type structure, and a function in this calculus, called a generic function, can be composed from more than one lambda expression and the ways it behaves on each type are weakly related in that it lax commutes with the coercion functions defined from the subtypes to the supertypes. Since laxness is intermediate between ad hocness (behaviors on each type are not related) and coherency (commuting with the coercion functions), λ{sub}m has syntactic properties lying between those of calculi with ad hoc generic functions and coherent generic functions studied in Tsuiki (Math. Struct. Comput. Sci. 8 (1998) 321). That is, although λ{sub}m allows self application and thus is not normalizing, it does not have any unsolvable terms. For this reason, all the semantic domains are connected by mutually recursive equations and, at the same time, they do not have the least elements. We solve them by considering fibrations and expressing the equations as a recursive equation about fibrations. We also show the adequacy theorem for λ{sub}m following the construction of Pitts and use it to derive some syntactic properties.