<DIV>A nice elementary treatment of typed lambda calculus can be found in "Types and Programming Languages" by Benjamin C. Pierce. My favorive introduction to compuytability theory is undoubtedly Barry S. Cooper's book, though it's pretty light on the lambda calculus. I understand that the first satisfactory model theoretic approach is due to Dana Scott, though I don't have access to it (yet). What I've been able to glean from more elementary treatments suggest that it focuses on replacing sets with more structured on objects known as domains, allowing recursive definitions to be formalized as fixpoints of continuous functions on lattices. I would love to find a reasonably accessible proof of the&nbsp; Church-Rosser theorem. In lambda calculus, on "computes" by reducing lambda expressions according to one of three basic rules:</DIV>
<DIV>&nbsp;</DIV>
<DIV>alpha reduction - allows renaming of free variables</DIV>
<DIV>beta - reduction - allows uniform substitution</DIV>
<DIV>eta reduction - allows irrelevevent abstractions to be dropped</DIV>
<DIV>&nbsp;</DIV>
<DIV>But, though various evaluation strategies fix the order in which reductions are applied in real implementations, the lambda calculus does not specify any particular order, and the Church-Rosser theorem states that the "normal form" (expression that cannot be reduced further) you reach, if any, is well-defined.</DIV>
<DIV>&nbsp;</DIV>
<DIV>Another way to look at it is that pure functional languages do not fix an order in which "statements" are "executed", but&nbsp;consist of a series of definitions evaluated through reduction. That the result is well-defined in an imperative language is clear because there is usually a straightforward operational semantics. But the functional "machine" is more like a theorem prover, so you need something like a consistency theorem (as in logic) saying that the conclusion you might reach from a set of (conistent) premises is well-defined.</DIV>
<DIV>&nbsp;</DIV>
<DIV>I hope this helps.<BR><BR><B><I>"Marc A. Ziegert" &lt;coeus@gmx.de&gt;</I></B> wrote:</DIV>
<BLOCKQUOTE class=replbq style="PADDING-LEFT: 5px; MARGIN-LEFT: 5px; BORDER-LEFT: #1010ff 2px solid">(this duplicates that inquiry from glasgow-haskell-users@ to haskell@)<BR><BR><BR><BR>Am Sonntag, 6. November 2005 15:53 schrieb Hans N Beck:<BR>&gt; Hi,<BR>&gt; <BR>&gt; I'm searching for a good mathematical oriented introduction to the <BR>&gt; theory of lambda calculus or other theoretical foundations of Lisp/ <BR>&gt; Haskell, i.e. monads or such (of course in the web there are much <BR>&gt; hints, but what is the best for mathematicans foreign to this field)<BR>&gt; <BR>&gt; Regards<BR>&gt; <BR>&gt; Hans<BR>&gt; _______________________________________________<BR>&gt; Glasgow-haskell-users mailing list<BR>&gt; Glasgow-haskell-users@haskell.org<BR>&gt; http://www.haskell.org/mailman/listinfo/glasgow-haskell-users<BR>&gt; <BR>&gt; <BR><BR><BR><BR>Hi Hans,<BR><BR>i'm searching for such lectures/papers/scripts, too.<BR>well, untill there is a better answer, i send you some links,
 which i think could be interesting to you.<BR>the first real mathematical definition of "monad", i read, was in the paper "The essence of dataflow programming". i approve to not omit that paper, if you like both, haskell and that theory.<BR>beside that, i attended a german lecture about Algebraic Topology. one chapter was about cathegory theory. it was not that much, but interesting.<BR><BR><BR>lambda:<BR><HTTP: Lambda_calculus wiki en.wikipedia.org><BR>(<HTTP: wiki Lambda-Kalk%C3%BCl de.wikipedia.org>)<BR>very interesting is the "typed lambda calculus", which allows effective bug-prevention, which you do not have in most variants of lisp (or lisp's derivatives) but in haskell.<BR><BR>functor:<BR><HTTP: CategoryTheory_2fFunctor hawiki haskell.org><BR><BR>monad:<BR>there is a mathematical definition in the paper "The essence of dataflow programming", see 'comonad:' below.<BR><BR>cathegory theory:<BR><HTTP: hawiki haskell.org CategoryTheory><BR><HTTP: hawiki haskell.org
 CategoryTheory_2fPapers><BR><HTTP: wiki en.wikipedia.org List_of_category_theory_topics><BR><HTTP: hsce 2004 ~zednenem www.eyrie.org /><BR><BR>arrow:<BR><HTTP: arrows www.haskell.org /><BR><HTTP: fop.html papers ~ross www.soi.city.ac.uk><BR><BR>comonad:<BR><HTTP: 12171 gmane.comp.lang.haskell.general comments.gmane.org><BR><BR><BR>beside these links, do not abstain from reading parts of the haskell library. (Data.Maybe, Data.Monoid, Control.Monad, Data.FunctorM, Control.Arrow)<BR><HTTP: www.haskell.org libraries html latest docs ghc /><BR><BR><BR>- marc<BR><BR>_______________________________________________<BR>Haskell mailing list<BR>Haskell@haskell.org<BR>http://www.haskell.org/mailman/listinfo/haskell<BR></BLOCKQUOTE><BR><BR><DIV>
<DIV>
<DIV>
<DIV>
<DIV>
<DIV><FONT color=#000080 size=2>
<P><FONT color=#4040ff>===<BR>Gregory Woodhouse&nbsp; &lt;</FONT></FONT><U><FONT size=2><FONT color=#4040ff>gregory.woodhouse@sbcglobal.net&gt;</FONT></U></FONT><FONT color=#000080 size=2><BR><BR><FONT color=#008000 size=2></P><FONT color=#4040ff><FONT color=#008000 size=2>
<P><FONT color=#0000ff>"Einstein was a giant. He had his head in the clouds and his feet on the ground."</FONT></P>
<P><FONT color=#0000ff>-- Richard P. Feynman</FONT></P>
<P></FONT></FONT></FONT></FONT><BR></P></DIV></DIV></DIV></DIV></DIV></DIV>