Talk:Lambda calculus
|
|
Maybe I'm being really dumb but isn't (λ x. x 3) (λ x. x+2) identical to 3?? (λ x. x 3) is the constant function 3, applying it to (λ x. x+2) still gives you 3? Kuratowski's Ghost 15:28, 23 Nov 2004 (UTC)
- The constant function you mean is (λ x. 3) which is different from (λ x. x 3). See the difference? :-) -- Jan Hidders 15:50, 23 Nov 2004 (UTC)
- Nope what I'm saying is that my understanding of (λ x. x 3) is that it is identical to writing (λ x. x) 3 which is 3. The article seems to treat it as meaning λ x.( (x) 3) in other words its treating function application as having precendence over λ quantification. I've never seen that before and can't find any mention of it, all the texts I have include parentheses to avoid ambiguity, I've never really seen something like (λ x. x 3) which can even be misinterpreted as multiplication of x by 3. :P Kuratowski's Ghost 00:10, 24 Nov 2004 (UTC)
- The precedence rules are later explained in the section that gives the formal definition, right after the syntax. These are AFAIK the common conventions when using the dot notation. I agree if you say that we shouldn't apply those rules before we have actually introduced them. I leave it to you to add brackets to disambiguate. -- Jan Hidders 12:38, 24 Nov 2004 (UTC)
- I'm trying to find a good rigorous source on the subject. Some of the stuff I have does naughty things like relying on the fact that people know that f and g are functions and that x and y are numbers so that fx is function application while xy is multiplication :) Kuratowski's Ghost 15:25, 24 Nov 2004 (UTC)
- I don't think that's a good idea. We should be consistent in this article and if you simulate numbers in pure calculus you cannot tell the difference. The best reference is the work by Barendregt, but that's probably not what you are looking for. For an introduction google for "introduction lambda calculus barendregt barendsen". -- Jan Hidders 23:03, 24 Nov 2004 (UTC)
- It looks quite good, still not rigourous enough for my liking ;) Kuratowski's Ghost 17:26, 30 Nov 2004 (UTC)
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.html 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)
- There's a bit on it now, but it needs work.
Great article! I'll point my students to it. -- Ellen Spertus
TODO: connection between lambda calculus and natural language semantics Kowey 08:01, 27 Nov 2003 (UTC)