An Adequate Left-Associated Binary Numeral System in the lambda-Calculus (Revised Version)

<p>This paper introduces a sequence of lambda-expressions modelling the binary expansion of integers. We derive expressions computing the test for zero, the successor function, and the predecessor function, thereby showing the sequence to be an adequate numeral system. These functions can be computed efficiently. Their complexity is independent of the order of evaluation.</p><p><br />Keywords: Programming calculi, lambda-calculus, functional programming.</p>

Gödelisation in the lambda-Calculus (Extended Version)

<p>Gödelisation is a meta-linguistic encoding of terms in a language.<br />While it is impossible to define an operator in the lambda-calculus which<br />encodes all closed lambda-expressions, it is possible to construct restricted<br />versions of such an encoding operator modulo normalisation. In this<br />paper, we propose such an encoding operator for proper combinators.</p><p><br />Keywords: Programming Calculi; lambda-Calculus; G¨odelisation.</p>

Solving Equations in the lambda-Calculus using Syntactic Encapsulation

<p>Syntactic encapsulation is a relation between an expression and one of<br />its sub-expressions, that constraints how the given sub-expression can<br />be used throughout the reduction of the expression. In this paper, we<br />present a class of systems of equations, in which the right-hand side of<br />each equation is syntactically encapsulated in the left-hand side. This<br />class is general enough to allow equations to contain self-application,<br />and to allow unknowns to appear on both sides of the equation. Yet<br />such a system is simple enough to be solvable, and for a solution<br />(though of course not its normal form) to be obtainable in constant<br />time.</p><p><br />Keywords: lambda-calculus, programming calculi.</p>

An Adequate Left-Associated Binary Numeral System in the lambda-Calculus

<p>This paper introduces a sequence of lambda-expressions, modelling the binary<br />expansion of integers. We derive expressions computing the test<br />for zero, the successor function, and the predecessor function, thereby<br />showing the sequence to be an adequate numeral system. These functions<br />can be computed efficiently. Their complexity is independent of<br />the order of evaluation.</p><p><br />Keywords: Programming calculi, lambda-calculus, functional programming.</p>