λ-Representability of Integer, Word and Tree Functions

Article type: Research Article

Authors: Madry, Małgorzata

Affiliations: Instytut Informatyki Uniwersytetu Jagiellońskiego, ul. Nawojki 11, 30-072 Kraków, Poland

Abstract: Six λ-languages over function-types between algebras B, N and Υ are considered. Type N=(0→0)→(0→0) is called a non-negative integers type; B=(0→0)→((0→0)→(0→0)) is called a binary words type; Υ=(0→(0→0))→(0→0) is called a binary trees type. These associations come from the isomorphism between the types and corresponding algebraic structures. Closed terms whose types are the above mentioned function-types represent unary functions of appropriate types. The problem is: what class of functions is represented by the closed terms of the examined type. It is proved that for B→N, N→B, Υ→N, Υ→B there exists a finite base of functions such that any λ-definable function is some combination of the base functions. The algorithm which, for every closed term, returns the function in the form of a combination of the base functions is given. For two other types, B→Υ and N→Υ, a method of constructing λ-representable functions using primitive recursion is shown.

DOI: 10.3233/FI-1992-17306

Journal: Fundamenta Informaticae, vol. 17, no. 3, pp. 253-270, 1992