λ -Representability of Integer,Word and Tree Functions

Abstract

Six λ-languages over function-types between algebras B, N and Υ are considered. Type $\mathit{N}=\mathrm{(}0\to 0\mathrm{)}\to \mathrm{(}0\to 0\mathrm{)}$ is called a non-negative integers type; $\mathit{B}=\mathrm{(}0\to 0\mathrm{)}\to \mathrm{(}\mathrm{(}0\to 0\mathrm{)}\to \mathrm{(}0\to 0\mathrm{)}\mathrm{)}$ is called a binary words type; $\mathrm{{\rm Y}}=\mathrm{(}0\to \mathrm{(}0\to 0\mathrm{)}\mathrm{)}\to \mathrm{(}0\to 0\mathrm{)}$ 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 $\mathit{B}\to \mathit{N}$ , $\mathit{N}\to \mathit{B}$ , $\mathrm{{\rm Y}}\to \mathit{N}$ , $\mathrm{{\rm Y}}\to \mathit{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, $\mathit{B}\to \mathrm{{\rm Y}}$ and $\mathit{N}\to \mathrm{{\rm Y}}$ , a method of constructing λ-representable functions using primitive recursion is shown.