[Haskell] Re: lambda calculus theory

[Greg Woodhouse]

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  Church-Rosser theorem. In lambda calculus, on "computes" by reducing lambda expressions according to one of three basic rules:
 
alpha reduction - allows renaming of free variables
beta - reduction - allows uniform substitution
eta reduction - allows irrelevevent abstractions to be dropped
 
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.
 
Another way to look at it is that pure functional languages do not fix an order in which "statements" are "executed", but 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.
 
I hope this helps.

"Marc A. Ziegert" <coeus at gmx.de> wrote:
(this duplicates that inquiry from glasgow-haskell-users@ to haskell@)



Am Sonntag, 6. November 2005 15:53 schrieb Hans N Beck:
> Hi,
> 
> I'm searching for a good mathematical oriented introduction to the 
> theory of lambda calculus or other theoretical foundations of Lisp/ 
> Haskell, i.e. monads or such (of course in the web there are much 
> hints, but what is the best for mathematicans foreign to this field)
> 
> Regards
> 
> Hans
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> 
> 



Hi Hans,

i'm searching for such lectures/papers/scripts, too.
well, untill there is a better answer, i send you some links, which i think could be interesting to you.
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.
beside that, i attended a german lecture about Algebraic Topology. one chapter was about cathegory theory. it was not that much, but interesting.


lambda:

()
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.

functor:


monad:
there is a mathematical definition in the paper "The essence of dataflow programming", see 'comonad:' below.

cathegory theory:





arrow:



comonad:



beside these links, do not abstain from reading parts of the haskell library. (Data.Maybe, Data.Monoid, Control.Monad, Data.FunctorM, Control.Arrow)



- marc

_______________________________________________
Haskell mailing list
Haskell at haskell.org
http://www.haskell.org/mailman/listinfo/haskell



===
Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>



"Einstein was a giant. He had his head in the clouds and his feet on the ground."

-- Richard P. Feynman









-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org//pipermail/haskell/attachments/20051107/03c0e1a1/attachment.htm