λ-Representability of Integer, Word and Tree Functions
Małgorzata Madry · Fundamenta Informaticae · 1992
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.