Inclusions and subtypes I: First-order case

Narciso Martí-Oliet, José Meseguer

Research output: Contribution to journalArticlepeer-review

Abstract

The failure to make explicit two different notions of subtype, a subtype as inclusion notion originally 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 τ ≤ τ' (inclusion) and τ ≤: τ' (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 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.

Original languageEnglish (US)
Pages (from-to)409-438
Number of pages30
JournalJournal of Logic and Computation
Volume6
Issue number3
DOIs
StatePublished - Jun 1996

Keywords

  • Categorical logic
  • Coercion
  • Inclusion
  • Overloading
  • Subtype

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Arts and Humanities (miscellaneous)
  • Hardware and Architecture
  • Logic

Fingerprint Dive into the research topics of 'Inclusions and subtypes I: First-order case'. Together they form a unique fingerprint.

Cite this