On principal types of combinators

• Tipo: Artigo em Revista Científica Internacional
• Data: 2000

Autores

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

Revista

Título: Theoretical Computer Science

Vol. 247

Páginas: 277-290

ISSN: 0304-3975

Editora: Elsevier

Indexação

ISI Web of Knowledge - 1 Citação

Scopus - 3 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 14