Lambda Calculus

http://safalra.com/science/lambda-calculus/

by jacquesm • 17 years ago

45 23 17 years ago

jacquesm8• 17 years ago

I posted this because I'm trying to get my head wrapped around this subject and it is one of the most concise and clear explanations that I've found so far.

I want to get a more complete understanding of functional programming, and that seems to start with understanding the lambda calculus.

camccann• 17 years ago

Understanding modern functional programming via pure lambda calculus is somewhat like understanding C++ via raw assembly. Which is to say, you'll have a great low-level understanding to build on but a long, long road ahead.

It is a lot of fun, though. I once spent a delightful afternoon puzzling out how to subtract Church numerals knowing only that it was possible to do so, having previously worked out the far simpler addition and multiplication functions. Highly recommended!

jacquesm8• 17 years ago

I figure you can't really say you understand a programming language until you can re-implement it from the ground up.

So that's my intermediate goal.

Spot on about C/C++ through the assembler route by the way, if there is one excellent way to really grok those then it is via the -S flag.

Agent101• 17 years ago

I find lambda calculus needed when you get into some of the subjects that functional programming languages are a gateway to. It definitely helps when trying to read the Coq manual.

baddox• 17 years ago

I don't know that the lambda calculus is necessary for functional programming. It can't hurt, but I don't think it's vital. I basically just think of the l.c. as another equivalent model for general purpose computing, just like Turing machines.

clemesha• 17 years ago

This page: http://safalra.com/science/lambda-calculus/recursion/ contains exactly the phrase "Y combinator", which I found exciting. Still trying to understand many other bits of the article.

jacquesm8• 17 years ago

Recursion in pure functional programming has me stumped. I can't see how in practice it would ever 'end' the recursion, in other words, if I try to envision the recursion I see an endless loop in there.

In practice something needs to decide to end the recursion.

Can somebody shed some light on this ?

procrastitron2• 17 years ago

The Y combinator only works in languages with either a lazy or call-by-name evaluation strategy. If you run it in a language with an eager evaluation strategy then it actually would result in an infinite loop. For those languages you would have to use the Z combinator or an equivalent. The z-combinator is just the Y combinator with the argument wrapped in a thunk to prevent premature evaluation.

Darmani2• 17 years ago

This page looks like it gives a very nice introduction to "programming" in the pure-untyped lambda calculus. But reading this, one would have no idea that a "meatier" side to lambda calculus existed. Just understanding the Church-Rosser theorem and its consequences, for example, would give a far deeper understanding than anything shown here. One thing that saddens me is that it shows construction of the combinators used to compute partial-recursive functions, but makes no discussion of the significance of this (the partial-recursive functions are an important computational class, and this is essentially a proof that they're lambda computable. Throw in a 6th type of combinator, and you've just proved lambda calculus capable of emulating one of the major models of computation).

It's certainly cool, but there's only so much to be gained from knowing that you can implement the factorial function with (λf .(λx .f (xx ))(λx .f (xx ))) (λfn.((λn.n(λu.λxy .y )(λxy .x ))n)(λfx .fx ) ((λmnf .m(nf ))n(f ((λnfx .n(λgh.h(gf ))(λu.x )(λu.u))n)))) .

bitdiddle• 17 years ago

I also think this article is lacking. Something also about domain[1] theory and categorical models could be discussed. Particular the latter as they relate to abstract machines, .eg. Curien's thesis work on combinators and functional programming. I'm not saying one can explore these in depth, but at least throw them out there for further reading to help provide a roadmap for the "meatier" side.

One could also cite a few programming constructs, .eg. (let (... and show how lisp is essentially syntactically sugared lambda calculus.

I should also add Carl Gunter's excellent "Semantics of Programming Languages: Structures and Techniques", as a good intro to this area.

[1] http://en.wikipedia.org/wiki/Domain_theory)

Lambda Calculus

Related Stories