History

Please fill in your query. A complete syntax description you will find on the General Help page.
A domain-theoretic semantics of lax generic functions. (English)
Theor. Comput. Sci. 294, No. 1-2, 307-331 (2003).
Summary: The semantic structure of a polymorphic calculus $λ_m$ is studied. $λ_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), $λ_m$ has syntactic properties lying between those of calculi with ad hoc generic functions and coherent generic functions studied by {\it H. Tsuiki} [Math. Struct. Comput. Sci. 8, 321‒349 (1998; Zbl 0917.68139)]. That is, although $λ_m$ allows for 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 $λ_m$ following the construction of Pitts and use it to derive some syntactic properties.