Talk:Lambda calculus

Really excellent work on this. When I saw the initial version, I went ahead and made a stub for Y combinator, admittedly for humor reasons, but perhaps something about some of the combinators would be nice. :) -- EdwardOConnor

---

When this article talks about renaming formal arguments:

(λx. λy. y x) (λx. y)     to     λz. z (λx. y)

It doesn't make sense to me.

- It's an information loss, because we don't know what z is.

- It conflicts with the discussion about normal forms, since then any expression can be transformed to another one just by calling it λ z. z.

But it is a very interesting topic, and I'm certainly learning from this page. -- forgotten gentleman

---

Change of bound variables is known as alpha conversion, and has no effect on the meaning of the λ-expression e.g

 (λ x. f x) 3 is just the same as (λ y. f y) 3  

Your example is moderately interesting, and requires also the use of beta conversion or substitution, which goes as follows:

 
 (λx. λy. y x) (λx. y)
 = (λx.λz.z x)  (λx. y) (by alpha conversion - do this first!)
 = (λz. z (λx.y)) by beta conversion (substitution of (λx. y) for x  )  

This should work this time, because there is no clash on y.

Does that make you happier? User talk:David Martland

I hope that the reordering of the conversion processes now gives the correct results - thanks for the comment re free occurences. This example does seem quite instructive - it ought to be possible to get somewhere going the other way surely ...

The article is veering towards considerable formalism - this is in many ways a good thing, but may also render it less accessible to people who don't have much of an idea about this stuff, and want to learn. Maybe some more examples would help? Sometimes intuitive examples do help. David Martland 22:22 Dec 7, 2002 (UTC)

---

Maybe there should be a note that this is the untyped lambda calculus, and that there are also several typed lambda calculi.

done.

---

I removed this:

Church invented lambda-calculus in order to set up a foundational project restricting mathematics to quantities with "effective procedures". Unfortunately, the resulting system admits Russell's paradox in a particularly nasty way; Church couldn't see any way to get rid of it, and gave up the project.

This is taken from FOLDOC; I don't think it is correct. The motive ascribed to Church (and Kleene) is wrong: they wanted to formalize the notion of computability. Furthermore, the paragraph presents the project of the lambda calculus as a failure; indeed it was a smashing success: it solved the Entscheidungsproblem and defined computable function for the first time cleanly (as the article already explains). It is not that "Church couldn't see any way to get rid of it", but in fact he proved that "there is no way to get rid of it", thus solving the Entscheidungsproblem in the negative. AxelBoldt 08:51 Sep 3, 2002 (PDT)

---

I did a little research and found an article by Henk Barendregt (one of the worlds leading experts on lambda calculus) titled The impact of the lambda calculus in logic and computer science that you can find at http://citeseer.nj.nec.com/barendregt97impact and there he says:

(page 2) As to the representation of proofs, one of Church's original goals had been to construct a formal system for the foundations of mathematics by having a system of functions together with a set of logical notions. When the resulting system turned out to be inconsistent, this program was abandoned by him. Church then separated out the consistent subsystem that is now called the lambda calculus and concentrated on computability. (*1). [...]

At the top of page 5 you can read more about the details. -- Jan Hidders 12:16 Sep 3, 2002 (PDT)

Nice reference; we definitely have to weave this in then. AxelBoldt 14:20 Sep 3, 2002 (PDT)

---

I've written the beginning of an article about Combinatory logic, a variation of lambda calculus that has only application, and no abstraction. It seems to me it should be linked from here, but I'm not sure what to say. -- Mark Jason Dominus

---

To do: De Bruijn discovered a version of the Lambda calculus that avoids the alpha-equivalence difficulties by eliminating all variable names. There should be a paragraph about that. I will write it if someone else doesn't get there first. Dominus 04:18 Nov 30, 2002 (UTC)

---

The discussion of alpha-conversion is not quite correct. For example, it says

The alpha-conversion rule states that

λ V. E == λ W. E[V/W]

where V and W are variables, E is a lambda expression and E[V/W] means the expression E with every free occurrence of V in E replaced with W.

Here is a counterexample: Take V==x, W==y, and E==(x y). Then the definition above asserts that

λ x.(y x) == λ y.(y x)[x/y]

== λ y.(y y)

since I have replaced "every free occurrence of x with y", as instructed. But the equivalence is wrong.

I would like to fix this, following the exposition in section 1.1 of Lectures on the Curry-Howard Isomorphism (http://www.folli.uva.nl/CD/1999/library/pdf/curry-howard.pdf) by Sørenson and Urzyczyn. If nobody objects, I will. As the same time I would add a section about the De Bruijn formulation, which avoids the α-reduction issue entirely. Dominus 00:17 Dec 1, 2002 (UTC)

FWIW that certainly has my blessing (you just have to add that W does not ocurr freely in E and all occurrence of W in E[V/W] should be free) and I would even vote for a separate article on the De Bruijn formulation that explains the why and how of it. -- Jan Hidders 14:46 Dec 1, 2002 (UTC)

---

What about eta conversions? I used to know this stuff, but now it's very hazy. I think there are some circumstances where etas are needed - not just alpha and betas. David Martland 22:51 Dec 10, 2002 (UTC)