On the representation of data in lambda-calculus

Abstract

We analyse the algorithmic properties of programs induced by the choice of the representation of data in lambda-calculus. From a logical point of view there are two canonical ways of defining the data types: the iterative one and the recursive one. Both define the same mathematical object, but we show that they have a completely different algorithmic content. The essential of the difference appears in the operational properties of two programs: the predecessor and the addition on the type of unary natural numbers (for the type of lists this would be the programs cdr and append). The results we prove in this paper state a fundamental duality between the iterative and recursive representation of data in lambda-calculus.

For the iterative representation of natural numbers (Church numerals) there is a "one-step" addition, but we prove in §3 that there is no "one-step" predecessor (by "one-step" we mean "whose computation requires only number of reduction steps bounded by a constant"). For the recursive representation of natural numbers we have the converse situation: there is a "one-step" predecessor but we prove in §4 that there is no "one-step" addition. For simplicity, we state these results for the type of natural numbers, but they hold in fact for all the usual data types defined as multisorted term algebras. Their practical significance for programming, may be, appears clearer on the type of lists where the predecessor is replaced by the cdr and the addition by append.

In §5, we briefly present a new representation of natural numbers for which we have both, a "one-step" predecessor and a "one-step" addition.