Technical Report: DCC-2000-4

Habitantes Principais Normais em TA$\lambda$

 Sabine Broda and Luís Damas

DCC-FC & LIACC, Universidade do Porto
R. do Campo Alegre 823, 4150-180 Porto, Portugal
Phone: 351 22 6078830, Fax: 351 22 6003654
E-mail: {sbb,luis}@ncc.up.pt}
  Junho 2000

Abstract

Neste trabalho estudamos o problema de contar e enumerar efectivamente os $\lambda$-termos em forma normal-$\beta$ que são habitantes principais de um dado tipo no $\lambda$-calculus simplesmente tipado. Apresentamos resultados e algoritmos para resolver este problema respectivamente no $\lambda$-calculus completo e nos seus três subsistemas principais. Apresentamos ainda um resultado que permite adaptar para o $\lambda I$-calculus o algoritmo definido por Ben-Yelles em 1979 para contar e enumerar habitantes normais. Com este conjunto de resultados resolvemos cinco problemas em aberto nesta área, ainda recentemente referidos por Hindley em 1997.