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. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Rehof, J., & Urzyczyn, P. (2011). Finite combinatory logic with intersection types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6690 LNCS, pp. 169–183). https://doi.org/10.1007/978-3-642-21691-6_15
Mendeley helps you to discover research relevant for your work.