# FW: lambda abstraction a la Arrows

**RE01 Rice Brian T. EM2**
BRice@vinson.navy.mil

*Sun, 31 Jan 1999 02:36:16 +0300*

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