Tags:combinatory logic, inhabitation problem, intersection types, set-theoretic types and type theory
Abstract:
The idea of combinatory logic synthesis (CLS) is: Given a repository Gamma of combinators typed by intersection types and an intersection type tau, construct combinatory terms M such that M is assigned the type tau wrt. Gamma in Finite Combinatory Logic. A notable weakness of intersection types as synthesis query language is the inability to express negative information. We propose a Boolean extension to CLS, adding the connectives AND, OR, and NOT to the query language. This results in a stratified type system, consisting of finite combinatory logic and (partly) a monomorphic variant of a set-theoretic type system. We implement and compare two distinct inhabitation procedures for the presented stratified type system.
Finite Combinatory Logic Extended by a Boolean Query Language for Composition Synthesis