The main issues, well l-calculus is extremely
important because this notion of b-reduction
formalises the notion of capture avoiding substitution of bound variables.
l-calculus was first used by Church, Turing
and Rosser to formalise the notion of computer algorithm and in fact Church's
thesis originated precisely when Rosser and Church together with Turing
realised that all Turing computable functions are l
definable; and they succeeded to prove also the converse, that is all
l definable functions are Turing computable.
A very interesting point is if this language is the basic, the fundamental
paradigm functional language: how do we represent the recursive functions,
and how do we represent data types?
|
|