TY - GEN

T1 - SN combinators and partial combinatory algebras

AU - Akama, Yohji

PY - 1998/1/1

Y1 - 1998/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=34547316301&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34547316301&partnerID=8YFLogxK

U2 - 10.1007/BFb0052378

DO - 10.1007/BFb0052378

M3 - Conference contribution

AN - SCOPUS:34547316301

SN - 354064301X

SN - 9783540643012

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 302

EP - 316

BT - Rewriting Techniques and Applications - 9th International Conference, RTA 1998, Proceedings

A2 - Nipkow, Tobias

PB - Springer-Verlag

T2 - 9th International Conference on Rewriting Techniques and Applications, RTA 1998

Y2 - 30 March 1998 through 1 April 1998

ER -