Volume 6: January - December 1996

Issue 3: June 1996

Abstract


Inclusions and subtypes I: first-order case

  • Inclusions and subtypes I: first-order case
  • N. Marti-Oliet and J. Meseguer SRI International, Menlo Park, CA 94025, USA and Center for the Study of Language and Information, Stanford University, Stanford, CA 94305, USA. Email: {narciso,meseguer}@csl.sri.com

    ABSTRACT

    The failure to make explicit two different notions of subtype, a subtype as inclusion notion orginally proposed by Goguen and a subtype as implicit conversion notion originally proposed by Reynolds, leads to unsatisfactory situations in present approaches to subtyping. Here, it is argued that choosing either notion at the expense of the other would be mistaken and limiting, and a framework is proposed in which two subtype relations [tau] <= [tau]' (inclusion) and [tau] <= : [tau]' (implicit conversion) are distinguished and integrated. Part I generalizes the first-order equational logic with subtypes as inclusions and overloaded function symbols from its usual set-theoretic semantics to a categorical semantics in the style of Lawvere. This provides a much more general notion of model and supports interpretations of a logic with subtypes in any category having a suitable canonical notion of model and supports interpretations of logic with subtypes in any category having a suitable canonical notion of subobject. Soundness and completeness of the logic in the categorical setting are proved, and the classifying category of a theory, which is the initial model in this context, is constructed in detail. The adjunction between theory presentations and model categories is also proved, shedding light on subtleties of operation overloading not present in the unsorted and many-sorted cases. All this sets the stage for the higher-order categorical semantics of subtypes developed in Part II.

    Keywords: subtype, inclusion, coercion, overloading, categorical logic

    Pages: 409 - 438

    Part of the OUP Journal of Logic and Computation WWW service


    General Information

    Click here to register with OUP.

    This page is maintained by OUP admin

    Last updated 23 Jul 96

    Part of the OUP Journals World Wide Web service.


    Copyright Oxford University Press, 1996