Mathematical Institute of the Serbian Academy of Sciences and Arts
|Title:||Semantics for Combinatory Logic With Intersection Types||Journal:||Frontiers in Computer Science||Volume:||4||First page:||792570||Issue Date:||12-Jul-2022||ISSN:||2624-9898||DOI:||10.3389/fcomp.2022.792570||Abstract:||
There is a plethora of semantics of computational models, nevertheless, the semantics of combinatory logic are among the less investigated ones. In this paper, we propose semantics for the computational system of combinatory logic with intersection types. We define extensional applicative structures endowed with special elements corresponding to primitive combinators. We prove two soundness and completeness results. First, the equational theory of untyped combinatory logic is proven to be sound and complete with respect to the proposed semantics. Second, the system of the combinatory logic with intersection types is proven to be sound and complete with respect to the proposed semantics. The usual approach to the semantics for calculi with types that can be found in the literature is based on models for the untyped calculus endowed with a valuation of type variables which enables the interpretation of types to be defined inductively. We propose, however, a different approach. In the semantics we propose, the interpretation of types is represented as a family of subsets that satisfies certain properties, whereas for a given valuation of term variables, the interpretation of terms is defined inductively. Due to the wide applicability of semantics of computational models, the presented approach could be further developed to other computational models and beyond—to current and foreseen application of semantics to large distributed systems and new challenging technologies.
|Keywords:||combinatory logic | completeness | computational systems | equational theory | intersection types | semantics | soundness | type theory||Publisher:||Frontiers Media S.A.|
Show full item record
checked on Mar 23, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.