Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts
Đorđe Marković, Marc Denecker
TL;DR
This work addresses expressing subtyping polymorphism in order-sorted logic for knowledge representation by identifying limitations of standard OS logic and first-order logic in conditioning subtyping and quantifying over intensions. It introduces guarded order-sorted intensional logic, combining implicit typing guards with quantification over concepts to model subtyping relationships safely. The paper provides formal definitions for guarded OSL and guarded order-sorted intensional logic, outlines typing rules and semantics, and demonstrates how these constructs yield compact, well-typed representations of polymorphic subtyping. It also discusses well-typedness challenges, connects to dependent-type ideas, and outlines future work on integrating intensional extensions with partial-function reasoning and broader type-theoretic frameworks.
Abstract
Subtyping, also known as subtype polymorphism, is a concept extensively studied in programming language theory, delineating the substitutability relation among datatypes. This property ensures that programs designed for supertype objects remain compatible with their subtypes. In this paper, we explore the capability of order-sorted logic for utilizing these ideas in the context of Knowledge Representation. We recognize two fundamental limitations: First, the inability of this logic to address the concept rather than the value of non-logical symbols, and second, the lack of language constructs for constraining the type of terms. Consequently, we propose guarded order-sorted intensional logic, where guards are language constructs for annotating typing information and intensional logic provides support for quantification over concepts.