Semantics for Combinatory Logic With Intersection Types

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.