On the representation of data in lambda-calculus
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.
KeywordsNatural Number Recursion Operator Reduction Sequence Recursive Representation Logical Definition
Unable to display preview. Download preview PDF.
- [BB85]C. BOHM, A. BERARDUCCI, Automatic synthesis of typed A—programs on term algebras, TCS 39 (1985), pp 135–154.Google Scholar
- [FLO83]S. FORTUNE, D. LEIVANT, M. O'DONNELL, Expressiveness of simple and second-order type structures, J.ACM vol 30 (1983), pp 151–185.Google Scholar
- [Gi72]J.Y. GIRARD, Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur, Thèse d'état, Université Paris 7, 1972.Google Scholar
- [Kr87]J.L. KRIVINE, Un algorithme non typable dans le systeme F, CRAS 1987.Google Scholar
- [KP87]J.L. KRIVINE, M. PARIGOT Programming with proofs, FCT 87, Berlin 1987, (to appear in EIK 1990).Google Scholar
- [Le83]D. LEIVANT, Reasoning about functional programs and complexity classes associated with type disciplines, FOCS, 1983, pp 460–469.Google Scholar
- [Ma84]P. MARTIN-LØF, Intuitionistic type theory, Bibliopolis, 1984.Google Scholar
- [Mal]P. MALACARIA, personal communcation.Google Scholar
- [Pa88a]M. PARIGOT, Programming with proofs: a second order type theory, ESOP'88, LNCS 300, pp 145–159.Google Scholar
- [Pa88b]M. PARIGOT, Recursive programming with proofs, preprint 1988.Google Scholar