lambda abstraction a la Arrows

[Francois-Rene Rideau]

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
 combinations.
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.

Good luck!

[ "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 <erwin@cvt12.verfahrenstechnik.uni-stuttgart.de>