Title: An optimal implementation of the lambda-calculus
The lambda calculus is a formal system in which one can express functions. There is a (syntactic) difference between the instruction to compute (like "(lambda x. x + 6) 4") and its result (in this case 4 + 6 or 10). Computations are modelled by the beta-rule, which intuitively feeds arguments to a function. This rule is by no means elementary, that is to say the amount of time it takes to perform it depends (nontrivially) on the "argument" and the "function". As such it provides very little help in actually writing a program which can perform the intended computation. To close this gap one can translate expressions in the lambda-calculus to another system where the rules of reduction are elementary. We shall present such a system and show how to translate back and forth between this system and the lambda calculus.