FW: lambda abstraction a la Arrows

[RE01 Rice Brian T. EM2]

> 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!
> 
> yes, i've looked at various views on the lambda calculus, some using
> simple proof-generation equivalence (via modus ponens and function
> application) of a lambda statement, others using information-update (i.e.
> dynamic) logic.  all of these lend themselves well to intensional
> representations, and all are useful.
> 
>