SN combinators and partial combinatory algebras

We introduce an intersection typing system for combinatory logic. We prove the soundness and completeness for the class of partial combinatory algebras. We derive that a term of combinatory logic is typeable iff it is SN. Let F be the class of non-empty filters which consist of types. Then F is an extensional non-total partial combinatory algebra. Furthermore, it is a fully abstract model with respect to the set of SN terms of combinatory logic. By F, we can solve Bethke-Klop’s question; “find a suitable representation of the finally collapsed partial combinatory algebra of P”’. Here, P is a partial combinatory algebra, and is the set of closed SN terms of combinatory logic modulo the inherent equality. Our solution is the following: the finally collapsed partial combinatory algebra of P is representable in F. To be more precise, it is isomorphically embeddable into F.