Title
A characterization of lambda definable tree operations
Abstract
λ-language over simple type structure is considered. Type γ = (O → (O → O)) → (O → O) is called a binary tree type because of the isomorphism between binary trees and closed terms of this type. Therefore any closed term of type γ → (γ → … → (γ → γ) …) represents an n -ary tree function. The problem is to characterize tree operations represented by the closed terms of the examined type. It is proved that the set of λ definable tree operations is the minimal set containing constant functions and projections and closed for composition and the limited version of recursion. This result should be contrasted with the results of Schwichtenberg and Statman, which characterize the λ-definable functions over natural number types (O → O) → (O → O) by composition only, as well as with the result of Zaionc for λ-definable functions over type (O → O) → ((O → O) → (O → O)), which are also characterized by means of composition.
Year
DOI
Venue
1990
10.1016/0890-5401(90)90019-E
Inf. Comput.
Keywords
Field
DocType
lambda definable tree operation
Discrete mathematics,Lambda calculus,Combinatorics,Natural number,Constant function,Binary tree,Isomorphism,Function tree,Mathematics,Recursion,Lambda
Journal
Volume
Issue
ISSN
89
1
Information and Computation
Citations 
PageRank 
References 
2
0.52
2
Authors
1
Name
Order
Citations
PageRank
Marek Zaionc111117.27