Authors: Ghilezan, Silvia 
Kašterović, Simona
Affiliations: Computer Science 
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
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

Page view(s)

checked on Nov 27, 2022

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.