| dc.description |
We give a denotational semantics to a calculus λ⊗ with overloading and subtyping. In λ⊗, the interaction between overloading and subtyping causes self application, and non-normalizing terms exist for each type. Moreover, the semantics of a type depends not on that type alone, but also on infinitely many others. Thus, we need to consider infinitely many domains, which are related by an infinite number of mutually recursive equations. We solve this by considering a functor category from the poset of types modulo equivalence to a category in which each type is interpreted. We introduce a categorical constructor corresponding to overloading, and formalize the equations as a single equation in the functor category. A semantics of λ⊗ is then expressed in terms of the minimal solution of this equation. We prove the adequacy theorem for λ⊗ following the construction in Pitts (1994) and use it to derive some syntactic properties. |
