Finite Combinatory Logic with Intersection Types

Combinatory logic is based on modus ponens and a schematic (polymorphic) interpretation of axioms. In this paper we propose to consider expressive combinatory logics under the restriction that axioms are not interpreted schematically but ,,literally”, corresponding to a monomorphic interpretation of types. We thereby arrive at

finite combinatory logic

, which is strictly finitely axiomatisable and based solely on modus ponens. We show that the provability (inhabitation) problem for finite combinatory logic with intersection types is

Exptime

-complete with or without subtyping. This result contrasts with the general case, where inhabitation is known to be

Expspace

-complete in rank 2 and undecidable for rank 3 and up. As a by-product of the considerations in the presence of subtyping, we show that standard intersection type subtyping is in

Ptime

. From an application standpoint, we can consider intersection types as an expressive specification formalism for which our results show that functional composition synthesis can be automated.