lambda abstraction a la Arrows
Fri, 29 Jan 1999 16:00:22 +0100
On Mon, Jan 04, 1999 at 11:06:23PM +0300, RE01 Rice Brian T. EM2 wrote:
> [lambda abstraction without symbols]
There are many ways to achieve the expressivity of lambda-expressions
without using symbols. See
1) combinatory logic: choose a set of combinators that can generate any
function (together with function application as an operator),
the simplest being Schonfinkel's SKI:
I x = x ; K x y = x ; S x y z = (x z) (y z)
The downside is that expressions get very hairy and unreadable/unwritable,
since scoping has to be explicitly maintained in the very structure of
2) lambda-sigma: explicitly use deBruijn indices instead of identifiers;
you have to systematically shift/unshift them when entering/exiting
a lexical scope.
The proof that SKI generates all functions is isomorphic (per Curry-Howard),
in the simply-typed case, to the well-known deduction theorem
for propositional calculus (in constructive logic).
The categorical logic formulation of it is also well-known.
See your usual courses on lambda-calculus for an explanation.
See a file named lambda-foo.scm in the Tunes CVS archive,
for an implementation.
Actually, I think it is interesting to know about all these different
points of view on what seems to be the "same" function space;
each of these views also gives insight on the constraints that
implementors have to face when programming pure objects that give good
modularity instead of impure objects to lead to a conceptual mess.
[ "Faré" | VN: Ð£ng-Vû Bân | Join the TUNES project! http://www.tunes.org/ ]
[ FR: François-René Rideau | TUNES is a Useful, Nevertheless Expedient System ]
[ Reflection&Cybernethics | Project for a Free Reflective Computing System ]
The last good thing written in C was Franz Schubert's Symphony number 9.
-- Erwin Dieterich <firstname.lastname@example.org>