On principal types of combinators

• Type: Article in International Scientific Journal
• Date: 2000

Authors

Broda, S (Author) FCUP; Damas, L (Author) FCUP

Journal

Title: Theoretical Computer Science

Vol. 247

Pages: 277-290

ISSN: 0304-3975

Publisher: Elsevier

Indexing

ISI Web of Knowledge - 1 Citation

Scopus - 3 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-000-YYV

DOI: 10.1016/s0304-3975(99)00086-9

Abstract (EN): In this paper we study (in some cases) the relationship between the combinatory completeness of a set of typable combinators, with simple types, for a system of lambda-calculus and the axiomatic completeness, under substitution and modus ponens, of the respective set of principal types for the corresponding logical system. We show that combinatory completeness is a necessary, but not sufficient, condition for axiomatic completeness in the lambda k- and in the lambda g-calculus, while the two problems become equivalent for the BCK-lambda- as well as for the BCI-lambda-calculus. Furthermore, we present an algorithm which, whenever (B, alpha) is a principal pair for some normal BCK-lambda-term M, reconstructs M up to a-conversion and which fails if there is no normal BCK-lambda-term for which (B,alpha) is a principal pair. From the correctness proof of the algorithm we also obtain another proof for the fact that each BCK-lambda-term in normal form is completely determined by its principal pairs.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 14