This is the
talk page for discussing improvements to the
Lambda calculus article. This is not a forum for general discussion of the article's subject. |
Article policies
|
Find sources: Google ( books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
Archives: 1 |
![]() | This ![]() It is of interest to the following WikiProjects: | |||||||||||||||||||||||||||||||||||||||||||||||
|
Does anyone know why Church chose lambda as the letter symbol? Did it used to stand for something that started with L ? — Preceding unsigned comment added by 87.114.213.103 ( talk) 20:03, 4 September 2014 (UTC)
just wanted to leave a note saying that the article seemed pretty confusing to read at first sight. (there seemed to be good links though and maybe i'll come back after understanding it to make it more readable.) Harshav
I have no idea how to do this and I have no idea what lambda calculus is but the start of the "Imformal Description" where it says "In lambda calculus, every expression is a unary function" but then it says things like "λ y. y + 2;" -- well "y + 2" is an expression which is not a unary function. So, to have the very first sentence be so misleading is pretty bad. Pedzsan ( talk) 13:15, 7 June 2008 (UTC)
Lambda calculus is a method for (or theory about)- I dunno which) expressing (all?) functions ("functions" linked). Lambda calculus represents every mathematical expression as a unary function (linked). The lambda symbol is used to respresent such and such, and this relates to the concept of unary function because of such and such. For instance in the expression of f(x)=x+2 we typically perform such and such... Lambda calculus, instead would express this as such and such... So when we input such and such... the expression is mathematically identical but more verbose. -Michali —Preceding unsigned comment added by 67.142.130.11 ( talk) 06:30, 29 December 2008 (UTC)
Every article I've read about functional programming makes references to lambda calculus (and assumes you understand it), so I came here to try to figure it out. After reading the article and this discussion, lambda calculus still doesn't make any goddamn sense. Thanks guys. Anti-kudos. 150.135.222.63 ( talk) 20:54, 11 February 2009 (UTC)
It may be appropriate to introduce the formal syntax (x.x,λx.t, ts) in conjunction with the conceptual x -> y examples above it. Cackowski
The article mentions alpha-equivalence, but no direct explanation is given. That should probably be changed? Ran4 ( talk) 20:39, 9 April 2010 (UTC)
At the moment, the section "Arithmetic in lambda calculus" says "Note that 1 returns f itself, i.e. it is essentially the identity function, and 0 returns the identity function." If I understand the rest of the section correctly, this sentence has it the wrong way around: 0 is the identity function; 1 returns the identity function. So, I'm swapping the 1 and the 0. I'm definitely not an expert on this subject, though, so go ahead and revert my edit if I'm mistaken. — Saric ( Talk) 20:44, 16 February 2008 (UTC)
01-Nov-2008: I suggest adding a section "Controversy in lambda calculus" because it seems like overkill on fairly useless stuff. I still ponder "Why Johnny can't program" & "Why Johnny can't de-virus" & "Why Johnny can't word search" etc. I think subjects like lambda calculus created a nerd-iverse (re: "universe") that wasted hours on useless math games. Consequently, almost no one had time to focus on important topics, such as multi-word search. Can you believe it's 2008, even Google had copied multi-word search 10 years ago (in 1998), and how many text editors today can search for a multi-word match? As for "Why Johnny can't de-virus" as a 25-year ongoing nightmare, I think the answer lies in the fact that most people would buy a new "better" computer every time a virus killed their old PC: hence, some software companies had a vested interest in prolonging viruses that fostered sales of new software. Even so, Johnny wasn't taught to track & stop viruses that would kill each PC owned by almost everyone he ever met. The Computer Virus Era was 1983-2009?, which seems to be ending with Windows Vista stopping viruses before execution. My view is to cite sources that consider lambda calculus to be a limited concept that thwarted the expansion of computer science in other areas. For example, it has become common knowledge that languages are easier to program when using the standard syntax of algebra (but with words as variable names, not just x/y/z). The vast majority of all software systems originally written in LISP have been re-written in procedural, non-list languages. Simply as a matter of neutral balance, add some broader perspective to the article. - Wikid77 ( talk) 02:22, 1 November 2008 (UTC)
I note that the link ( http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9283) for Barendregt's book takes one to an internet shop. I think that should not be so. Could someone who is up to speed on it replace it with a proper reference with ISBN etc, A link to the text online, if available would also be good. PJTraill ( talk) 14:40, 14 February 2009 (UTC)
Lambda expression is not quite the same as an unnamed procedure without side-effects. It is a first-class citizen in the language design. Historically, this is a very important achievement, as this was the first formal system where such design was explored. In computer science there is an overarching concept of reification, which is roughly speaking the process of making a certain part of the run-time system visible within the language. The reification article has been recently updated, and it contains references to other areas in computer science where this process is used. It is important to make this link, as is one of the key benefits of Wikipedia. On the other hand, there are many resources on the Internet, which contain tutorials on lambda-calculus. This is the case to keep the link in the article.
I meant to argue against Equilibrioception's treatment of reification earlier, but got distracted. Talk the lambda-calculus being about first-class functions is alright, but a bit strange, to talk of it directly reifying any kind of procedure crosses the line from strange into positively perverse: the lambda calculus, though confluent, is a term rewriting system that is in terms of naive space and time resources highly nondeterministic, presumes no notion computational realisation and is not faithfully used in any non-toy implementation. I'm happy with the treatment of these concepts in the LC&PL section, and I think Landin's idea should be promoted to the second paragraph. — Charles Stewart (talk) 08:47, 18 March 2009 (UTC)
I propose merging the various lambda calculus articles into this one. All the other lambda calculus articles are (to me) hard to follow without understanding the lambda calculus ideas in this article. Therefore, I believe the other lambda calculus articles should become sections of this article. I realize this will make this article longer, but the basic concepts share so much in common that I believe it will make the exposition clearer. HowardBGolden ( talk) 04:38, 23 June 2009 (UTC)
References
The fact the 1st section freely mixes lambda expressions with numbers is contributing to the confusion with typed lambda calculi, because neither that section nor the lead explain that those numbers are actually encoded as functions in untyped lambda calculus. Granted, there's a section on that, but that comes way later. WP:LEAD should be observed here, i.e. the lead should summarize the important fact that data types have to be encoded in untyped lambda calculus. Pcap ping 21:29, 5 August 2009 (UTC)
A programming expression must always evaluate to a value as I understand it. E.g. x+3 is an expression since x is a pointer to a memory location with a value.
Therefore λy.y+2 is a function, not a programming expression, since y does not point to any memory location and no value can be evaluated. This lambda function is equivalent to f(y)=y+2. It surely only becomes a lambda expression when you make a function call like (λy.y+2) 3 and specify y so it evaluates to 5. Please see http://en.wikipedia.org/wiki/Expression_(programming).
Neither can λy.y+2 be a mathematical expression since its equivalent functional notation f(y)=y+2 contains an = symbol implying it is an equation not an expression. Please see http://en.wikipedia.org/wiki/Expression_(mathematics).
I think this should be clarified in the article. For example the wording "A lambda expression represents an anonymous function" appears to be misleading according to the above. —Preceding unsigned comment added by 92.39.205.210 ( talk) 21:46, 6 July 2009 (UTC)
After reading more on lambda calculus I think the "Informal description" section in this article is highly misleading to say the least. The term λx.x + 2 used in the section should not be used until both + and 2 have been defined otherwise the reader may think arithmetic terms like + and 2 are included in the lambda calculus by default which they are not. If you want + then it is built up from other operations i.e. λn.λm.(n add1 m) where add1 is λn.λf.λx.f(nfx), and 2 is defined as lf.lx.f(fx) according to Church numerals. The whole section needs redoing, it seriously misled me when I first read it.
As for the "expressions" point above it would be better to replace "lambda expressions" with "lambda terms" throughout to avoid confusion with the programming and mathematical meaning of "expressions" where an expression always evaluates to a value. In lambda calculus there are no values until you first define them using the rules so really the word "expression" doesn't apply to lambda calculus at a foundational level. —Preceding unsigned comment added by 92.39.205.210 ( talk) 12:44, 11 July 2009 (UTC)
The introduction is written as to imply the existence only one typed lambda calculus that Church published circa 1936 (besides the untyped one). This couldn't be more wrong or confusing! First, there's more than one flavor of typed lambda calculus, e.g. simply typed lambda calculus, but also others with more expressive types, System F etc. Church did write a technical report about simply typed lambda calculus, but only in 1940. In [2], p. 33 this is made clear enough (and, by the way, Curry essentially described simply typed lambda calculus in 1934). Also, simply typed lambda calculus is not just some "bug free" version that this article's intro seems to imply it is. The simply typed variant is not Turing complete, and neither are most other typed lambda calculi, which were later discovered by others, whereas the untyped lambda calculus is Turing complete. The fact that you can encode numbers and other types in untyped lambda calculus does not make it typed. Pcap ping 17:02, 5 August 2009 (UTC)
The man in the the sky heard us and fixed the most confusing part. But as Charles Matthews put it here, it is the wrong end of the microscope to delve on the foundational issue in the lead, which is only of historical interest today. Pcap ping 15:11, 20 August 2009 (UTC)
See talk page of the fixed point combinator for details on why "recursive" is meaningless as used in that section; I've fixed the main article, and eventually I'll fix this too. Pcap ping 00:41, 22 August 2009 (UTC)
The article may need clarifying in general but the most important thing is fixing the meaningless example of (λx.x+2) (where neither + nor 2 have been defined inside the theory). It's disconcerting when the very example designed to clarify the subject isn't a valid part of the theory. The writer should have used (λx.x x).
As for clarification, how about starting something like: "Lambda calculus, developed by Alonso Church in the 1930s is a technique for studying mathematic operations. The basic idea is to encode mathematic concepts in a code, and allowing the code to be manipulated in certain rigid ways to mimic the operations. Its importance nowadays is that it lent itself to computerization, inspiring the LISP programming language, and helped develop the general concept of programming functions." At least that's my understanding of it. CharlesTheBold ( talk) 20:21, 1 October 2009 (UTC)
The "informal description" section was far too confusing for the non-lay reader, IMO. I've attempted to rework the section the best I can, by placing an explicit "motivation" section, detailing where some of the concepts in the lambda calculus come from, and reworking the start of the rest of the section. Is this OK with everybody? —Preceding unsigned comment added by 137.195.27.217 ( talk) 14:02, 22 October 2009 (UTC)
(I was the original unsigned editor.)
I don't think we should mention tuples in the informal description. To my mind, that's getting far too picky in a section that's ostensibly aimed at a lay reader. Further, it's only type lambda calculi where tuples are nearly universally taken as primitive; untyped seems to be 50/50 (IME!), and if you go the encoding route, you aren't really contradicting what the article says at the moment (as the encoding is made with single argument functions).
I still think the Informal Description needs a lot more work, too (which I'll attempt when I have more time). DPMulligan ( talk) 15:59, 22 October 2009 (UTC)
FWIW, I only wrote the motivation section, and the first paragraph of the lambda calculus section. I've now rewritten the whole of the lambda calculus section, in order to make the section less confusing and consistent with the rest of what I'd written. I'd appreciate comments on this. One thing: I'm not very good with Wiki markup: the lambda terms, reductions etc. would probably look a lot better spaced out vertically. How does one do this? DPMulligan ( talk) 10:22, 23 October 2009 (UTC)
Also, stuff like a proper reduction arrow, alpha-equivalence symbol: are these available? DPMulligan ( talk) 10:24, 23 October 2009 (UTC)
I'm afraid the Informal Description section is still desperately confusing for a lay reader. I think the problem is that terms (English words & phrases that is, not lambda terms) are used without definition, or with specialised meanings that conflict with everyday usage. Examples:
In fact, I found the Formal Definition section much more digestible, but perhaps I'm just a sucker for BNF. There it helped that meta-variables are distinguished by case, so you can see that x is a <variable>, but M and N are <lambda terms> (which may be variables, applications or other abstractions, ...)
I realise the contributors to a page like this are going to be serious maths nerds, but they need to take a step back and recognise where they are using professional argot that overlaps with vernacular English so much that it cannot be parsed by the uninitiated. Swiveler ( talk) 13:23, 25 November 2009 (UTC)
I feel that all or most of the 2nd paragraph (starting "In the lambda calculus, functions are first-class entities...") should be cut. Do others agree? I can go line by line:
This line is okay, but maybe it can be streamlined and merged into the previous paragraph.
This line is bizarre. I agree with what Charles Stewart wrote above on 18 March 2009. I think it is also unnecessary and misleading to talk about side effects here. The original untyped lambda calculus was "pure" in the sense that it was restricted to function abstraction and application, but it wasn't really about "purity" in the sense of deliberately avoiding state. It wasn't because it couldn't be! As Charles pointed out, the semantics of the lambda calculus is highly nondeterministic, not a realistic model of computation, and so to even talk about state-ful functions you have to make a departure from the "real" lambda calculus. And in fact, all of the functional programming languages mentioned at the bottom of the paragraph (with the arguable exception of Haskell) do make this departure, and allow functions with side effects!
This is good.
The second half is POV, and wrong in my opinion. This fact is what allows for languages like Unlambda, but it is not what makes functional programming important.
What I wrote above -- this line is absolutely wrong for the standard definition of "functional programs", which includes programs witten in Lisp, ML, Scheme, etc.
It does make sense to mention some of the functional languages inspired by lambda calculus. But maybe that can be merged into the first paragraph. And it is absolutely wrong to imply that these languages are stateless! Noamz ( talk) 16:52, 25 October 2009 (UTC)
I agree. Cut the second paragraph, it's muddled and confusing. Merge whatever's salvageable into the first paragraph. DPMulligan ( talk) 23:27, 25 October 2009 (UTC)
There appear to be inconsistencies in this section; it is stated that the following holds: (λx.t)[x := r] = λr.t And yet in an example, ((λx.y)x)[x := y] = ((λx.y)[x := y])(x[x := y]) = (λx.y)y
I'm not sure, but I believe that the assertion that (λx.t)[x := r] = λr.t is erroneous. —Preceding unsigned comment added by 99.255.132.186 ( talk) 22:00, 29 October 2009 (UTC)
Argh. Yes, sorry, that was my fault. I realised I had a name clash with my original naming scheme, so changed the convention I was using halfway through, and thought I'd changed what I'd previously written. Sorry about that! DPMulligan ( talk) 11:06, 3 November 2009 (UTC)
Is this the same as alpha-renaming or alpha-conversion? If it is not, it must be explained why. Else, in Odifreddi (1992) (From Google Books: Piergiorgio Odifreddi. Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Volume 1. Volume 125 of Studies in Logic and the Foundations of Mathematics. ISBN 0444894837, 9780444894830), on page 77, it is defined the alpha-rule (another name for the same stuff?) as "We can rename bound variables: provided y does not occur in M, where M[x/y] indicates the result of the substitution of x by y everywhere". Repair that is replaced by . -- Menegola ( talk) 01:07, 14 December 2010 (UTC)
---
I believe the first part of
if x ≠ y and y is not in the free variables of r
is superfluous since the fact that x is different from y is stated where they are "declared". -- Andreas Lundblad ( talk) 11:18, 9 June 2011 (UTC)
I find the end of the paragraph on eta-conversion lacks some explanation. It states that
This conversion is not always appropriate when lambda expressions are interpreted as programs. Evaluation of λx.f x can terminate even when evaluation of f does not.
Could we have an example where the conversion is not appropriate, and an example where the evaluation of f does not terminate but the evaluation of λx.f x does ? Or are such examples too complicated ? 82.67.7.229 ( talk) 15:33, 8 November 2009 (UTC)
Also the paragraph in eta conversion is wrong. Eta conversion is much weaker than full blown extensionality. --
76.10.153.79 (
talk)
16:56, 2 February 2011 (UTC)
Furthermore, η conversion is not a fundamental aspect of lambda calculus. I think η should have received its separate section. (α-conversion is not fundamental either, but it is usual described with β-reduction, plus it has nothing to do with typing, whereas λx.(f x) implies that f has a functionnal type). Sedrikov ( talk) —Preceding undated comment added 16:22, 30 November 2012 (UTC)
Lambda calculus reads:
Functions are a fundamental concept within computer science and mathematics, as they are rules by which an input may be transformed into some output
this is true in computer science but not in mathematics! As put in Function_(mathematics):
a function is a relation between a given set of elements called the domain and a set of elements called the codomain
A function is the relation itself, not the set of rules that construct it. This distinction is important, because there are functions which cannot be constructed using any set of rules.
I don't know how to fix this without losing the original intent of the phrase. Perhaps the intended meaning becomes inappropiate because of this, so I'm just removing the "and mathematics" part. If you find a better way to reword it, it'd be appreciated :-)
193.153.229.101 ( talk) 19:35, 10 February 2010 (UTC)
I'd like the originator to demonstrate a function that cannot be expressed as a rule, If you can describe it in English, then you can construct a rule. Unless you need to define rule a particular way. I guess I am asking for more justification of the original fix. 65.175.239.50 ( talk) 13:52, 18 March 2010 (UTC)
What is a capture? A fundamental notion in formal languages? Why then does it not have its own WP article? (Or why is it not linked?)-- 217.232.244.191 ( talk) 14:30, 25 February 2010 (UTC)
To which section are you referring? The section on substitutions? 86.177.226.105 ( talk) 10:59, 2 April 2010 (UTC)
I've tried reading this article several times and I have to say, I still don't have a clue what lambda calculus actually is. The opening sentence says that it's "a formal system for function definition, function application and recursion" (and only recursion has a useful wiki link). The article assumes that you already know what a whole bunch of things are and from that, you already know why you'd use lambda calculus. I think that the article would greatly benefit if it included the following things in the lead:
I feel that with these changes, the article would become much more accessible to those who are not at all familiar with it. - Thunderforge ( talk) 17:35, 13 May 2010 (UTC)
Doesn't the informal description section already cover a lot of this? DPMulligan ( talk) 19:38, 13 May 2010 (UTC)
I have similar concerns about this article. I study computer science and mathematics, so I am not completely unfamiliar with terminology, but the whole idea of lambda-calculus is unclear to me. When I was reading article on bound and free variables, the explanation that made most sense to me was a linguistic one. Similarly, the first paragraph here completely throws me off: “a way to formalize mathematics through the notion of functions, in contrast to the field of set theory.” I do not dispute that I may be dumb, but is not the very “notion of function” described via set theory (“to each element of a set (domain) there is one and only one corresponding element of another set (range)”? theUg ( talk) 22:29, 16 February 2012 (UTC)
This page is missing a "History" section. -- a3_nm ( talk) 20:38, 16 October 2010 (UTC)
I'm trying to merge the article AlphaRenaming into this (see its talk page), but I'm not quite sure of the difference (if any) between "alpha conversion" and "alpha renaming". Is there a difference? It seems as though alpha-conversion means "any legal renaming" (as defined formally in this article), while alpha-renaming means "renaming from a term with overlapping scopes to a new term with no overlapping scopes".
For example, is a valid alpha-renaming (and alpha-conversion), whereas is an alpha-conversion but not an alpha-renaming since it didn't fix the overlapping scopes, and is also not alpha-renaming since the scopes weren't overlapping to begin with.
Or the two terms could mean exactly the same thing. I can only find colloquial uses of the term "alpha-rename", meaning "to make non-overlapping scopes", but not a true definition. It could be that the two terms are interchangeable. Anybody got a source? — MattGiuca ( talk) 06:31, 28 October 2010 (UTC)
The function definitions used for encoding booleans and numbers uses a syntax that is not defined. It shows a function containing 2 or more arguments, which is never explained. This should either be introduced prior to this section, or not used.
For example
Instead of what is written:
—Preceding unsigned comment added by 198.36.95.12 ( talk) 19:23, 13 April 2011 (UTC)
Ok, now that you point it out I can see it. This one line is fine for the Formal Definition. But I think an additional section of 1 or 2 examples would make it easier for a new-comer - or just avoid this syntax all together in the examples. This one liner definition is very easy to miss, and when looking for other explanatory examples - none can be found. As a start I updated the Church Encodings of numerals section to show both syntaxes. So now there is at least one set of examples for conversion. —Preceding unsigned comment added by 198.36.94.35 ( talk) 21:22, 21 April 2011 (UTC)
Hello. I refined the lead a bit boldly because I didn't agree with some statements recently introduced.
ComputScientist ( talk) 15:14, 4 January 2012 (UTC)
The definitions of the Church numerals 0..3 are exactly the same between the common and "alterate" notations. They not only appear the same; their source (mark-up) is the same. Macareus ( talk) 18:54, 15 March 2012 (UTC)
I use lambda calculus in the .Net language for anonymous functions. I am not a formal mathematician and found the following example confusing.
( ( X , Y ) → ( X * X + Y * Y ) ( 5 , 2 )
I did not know how to 'read' this statement. It came out in my head as something like: "For variables X and Y, calculate the formula substituting 5 and 2."
For anyone with elementary algebra there is an implied multiplication between the two bracketed terms. Lambda calculus has its own syntax but I believe it should be previously explained possibly, with a simpler example...
( X ) → ( X + 2 ) (6)
(read as ...)
Can someone supply the substitution for "..."?
This was done earlier with the statement:
(read as “the pair of X and Y is mapped to X * X + Y * Y”).
I would have preferred something like( X ) → ( X + 2 ) [6] or ( X ) → ( X + 2 ) {6} but I guess the syntax chosen is the correct formal method. Finally, apologies for not working out how to display the mathematical symbols. — Preceding unsigned comment added by Prcotter ( talk • contribs) 11:56, 20 April 2012 (UTC)
( (X , Y) → (X * X + Y * Y) ) (5 , 2)
( (X) → (X + 2) ) (6)
Guys, maybe the correct AND is AND = lambda p. lambda q. p q FALSE (with FALSE defined above) ? and not with p in the end..
The following is not a Y combinator, but seems to be able to function as one where one is needed: λx.(x x) 12.198.223.226 ( talk) 21:46, 29 June 2012 (UTC)JH
Lambda calculus is of interest to non-mathematicians, particularly to software engineers. In my experience, many intelligent software engineers complain that the topic is hard to learn not because of inherent complexity, but because most presentations of it are in a language that is trivial for mathematicians to understand but hard for engineers.
I attempted to expand a few terse paragraphs and had a 2.5k edit reverted nearly immediately by User:Ruud Koot with the comment undo: "sloppy writing rarely increases readability" (revision 528491773). I do not defend the edits as perfect, but they were significantly easier for a non-mathematician to understand than before.
I have reverted the undo. I am happy to work to come up with wording that preserves the readability of my version and yet corrects any flaws. TJIC ( talk) 12:24, 18 December 2012 (UTC)
I made a first pass copyediting the text. Here are some thought:
— Carl ( CBM · talk) 13:46, 18 December 2012 (UTC)
I plan to update this page with
The changes are primarily editorial in nature, to improve the tone and readability of the article. To this end quite a bit of material has been moved. The goal is to simplify the lambda calculus page and redirect people out to other pages for technical details.
If all goes smoothly after the change I will fix up links to the page.
Thepigdog ( talk) 04:27, 13 November 2014 (UTC)
I am trying to learn this. I do not have any expertise, and therefore the syntax might be fully correct. That being said, the following snippet under the introduction of the transformations confused me:
"For example, λ x.((λ x.x)x) and (λ x.(λ x.x)) x denote different terms (although coincidentally reduce to the same value.)"
If I am understanding correctly, these equations are not coincidentally the same, but must be the same, right? Let's take the two cases, breaking down each step:
λ x.((λ x.x)x): (λ x.x) is just x, so the eqn has become: λ x.(x * x), and then it becomes: x^2
(λ x.(λ x.x)) x: (λ x.x) is just x, so the eqn has become: (λ x.x) x: (λ x.x) is just x again, so now: x * x x^2
As stated, they reduce to the same equation, but he suggests this is coincidental. That's the part I'm missing. They are necessarily identical in all cases, if all I'm doing is merely moving around the parentheses where the lambda functions are performed, thereby introducing an extra identity function.
Stepping back, my real question is on syntax: these equations sometimes require that I put every function in a lambda "wrapper", and sometimes not. Is this allowed? Is it normal? To me, and hence the confusion, the equations necessarily had to be written as such:
1) λ x.((λ x.x) * x) 2) λ x.((λ x.(λ x.x)) * x)
In this way, it becomes obvious that the only difference between the two is that the second one has wrapped another identity function, which, necessarily, does not alter the equation at all. Am I missing something?
This.is.mvw ( talk) 16:53, 23 December 2014 (UTC)
In the section "Functions that operate on functions" an \rightarrow is used to write the identity. I would prefer to have "x \mapsto x", but then again I'm no computer scientist and so can't be sure this is not some sort of standard notation. Could someone who knows this stuff correct it or tell me why I'm wrong? EdvinW ( talk) 12:49, 11 December 2015 (UTC)
It should be made clear in the header what untyped lambda calculus is. I don't know enough about the subject to add anything of much use, sorry.
137.124.161.82 ( talk) 21:19, 16 February 2016 (UTC)
only a proposal, if I understand what is "alpha equivalence" and "beta reduction". how would it be, if it were:
thx for attention 94.219.96.38 ( talk) 22:50, 3 March 2016 (UTC)
The article states right in the beginning that the equivalence of lambda-calculus and Turing machines is the Church-Turing thesis. This affirmation seems to be wrong, though: The CT thesis states that these systems of computation, which had been PROVEN to be equivalent (and thus this equivalence is a theorem and not a thesis), describe, somehow, the human powers of computation. Equivalence in this sense cannot be proven mathematically, that's why it is a thesis. See Wikipedia's own article on the topic as a reference: /info/en/?search=Church%E2%80%93Turing_thesis 85.138.163.71 ( talk) 23:07, 30 May 2016 (UTC)
This comment: "It is a universal model of computation that can be used to simulate any single-taped Turing machine..."
Seems odd because any single-taped Turing machine can simulate any multitape Turing machine. By modus ponens then, shouldn't lambda calculus be able to simulate any multitape Turing machine because it can simulate any single-taped one?
Assuming that's true (and I would appreciate an expert confirming it is just to be sure) then we can probably change the above to "It is a universal model of computation that can be used to simulate any Turing machine..."
Hello fellow Wikipedians,
I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{
Sourcecheck}}
).
An editor has reviewed this edit and fixed any errors that were found.
Cheers.— InternetArchiveBot ( Report bug) 20:49, 12 September 2016 (UTC)
Hello fellow Wikipedians,
I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
This message was posted before February 2018.
After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than
regular verification using the archive tool instructions below. Editors
have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
RfC before doing mass systematic removals. This message is updated dynamically through the template {{
source check}}
(last update: 5 June 2024).
Cheers.— InternetArchiveBot ( Report bug) 02:29, 11 May 2017 (UTC)
If x and y are variables then xy seems to have no direct mathematical meaning. Shouldn't this be discussed? — Preceding unsigned comment added by G. Blaine ( talk • contribs) 21:50, 29 June 2017 (UTC)
The "informal description of lambda calculus" section currently goes into the technicalities of making substitution capture-avoiding, giving the same five definition cases as are later repeated in the formal definition section. I would suggest dropping those technicalities from the informal description—replacing them with just an example of how non-capture-avoiding substitution can go wrong—since these details are by far the most technical and confusing in the definition of the lambda calculus. (There are more confusing stuff you can do with lambda calculus, but the rest of the definition is pretty straightforward.) In view of past discussions, as recorded above on this talk page, I am however reluctant to do that change on just my own volition. 78.73.97.76 ( talk) 22:22, 8 July 2017 (UTC)
(Correction: It is the "Reduction" section that repeats the definition of capture-avoiding substitution, not the "Formal definition" one. Still, the suggestion stands. 78.73.97.76 ( talk) 12:09, 9 July 2017 (UTC))
In section 3.2.2 "Functions that operate on functions", the examples given are not of functions that operate on functions. Some better examples are needed. LoMaPh ( talk) 19:14, 9 November 2017 (UTC)
The use of the term "invention" suggest that the system is not a discovery, as would be held by mathematical Platonists. It also seems a like a pointless choice, given that anyone looking in that category would almost certainly not be looking for a model of computation.
After the example (λx.λy.(λz.(λx.z x) (λy.z y)) (x y)) the article states "Parentheses can be dropped if the expression is unambiguous". I would argue that the expression (λx.z x), which is a sub-expression of the above example is unambiguous. According to the three syntax constructions the expression (λx.z x) can be constructed as ((λx.z) x) or (λx.(z x)). So I believe there is missing information about precedence of the syntax constructions. Does the "." (dot) operator (syntax construction 2) have higher or lower precedence than the " " (space) operator (syntax construction 3)? -- Jarl ( talk) 08:22, 9 March 2019 (UTC)
The story about the lambda symbol arising via a series of typographical errors is implausible on its face, and directly disputed by Dana Scott in this talk. Barendregt does not give any evidence in that 1997 article, and it's not clear where he got it from or if he just meant it as a joke. (The other citation in this section to "Mathematical Methods in Linguistics" does not seem to have any relevance.) I suggest deleting this section. Noamz ( talk) 14:49, 16 May 2019 (UTC)
On further digging, this question is also discussed in Carbone and Hindley's History of Lambda-calculus and Combinatory Logic:
(By the way, why did Church choose the notation “λ”? In [Church, 1964, §2] he stated clearly that it came from the notation “ˆx” used for class-abstraction by Whitehead and Russell, by first modifying “ˆx” to “∧x” to distinguish function-abstraction from class-abstraction, and then changing “∧” to “λ” for ease of printing.
This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and “λ” just happened to be chosen.)
The reference [Church 1964] is an unpublished letter to Harald Dickson (not available online as far as I can tell), but in any case, from the way Carbone and Hindley describe it that original version of the story is pretty different than the version given by Barendregt, which seems like it passed through a couple rounds of telephone (game). So given this and the Dana Scott video, my impression is that the origin story is indeed apocryphal, albeit perhaps with a bit of help from Church himself. Noamz ( talk) 18:06, 22 May 2019 (UTC)
This section explains that the equivalence of two expressions in the lambda calculus is undecidable, though it doesn't cite any references. Which references should be cited here? Jarble ( talk) 16:15, 3 June 2019 (UTC)
Hello, how can operators or constants be brought in by application of these three rules? Are these supposed to be covered by the first rule? If so, the word "variable" is misleading to me. Stefan84556 ( talk) 01:00, 27 July 2020 (UTC)
For example, and denote different terms (although they coincidentally reduce to the same value).
There are too many different uses of for these expressions to be reasonably understood. It's used as the argument for the outer and inner lambdas and, in the second expression, a useless free variable. Something like and , which reduce to and respectively, would be much less confusing. (It may be impossible to make lambda calculus easy to understand, but we can at least not actively make it more difficult.) Nloveladyallen ( talk) 22:33, 2 March 2021 (UTC)
A search directed me to a lambda calculus wikibook. There was only a very wrong short intro with concepts borrowed from some not very formal lisp book. I wrote something with the purpose make it clear that many of what was written was wrong because the lambda calculus is important as a foundation of computing theory. Unfortunately I have no time to work on that enterprise. Maybe this article could be copied in wikibooks to be transform it in a lambda calculus book. I did not check if there were previous attempts to write such wikibook. -- User:2806:106e:b:31b1:3a5f:db9e:42bd:b4bd 00:51, 15 August 2022 (UTC)
From the talk page, it seems like there have been efforts in the past to turn this article into something that is actually helpful as an introduction to the subject that were overriden in favor of the previous unhelpful versions.
This is just a reminder that the current introduction is circular nonsense that only makes sense if a reader is already fully aware of what all of the terms and syntax mean. It should absolutely be rewritten for normal humans, at maximum to a high school reading level. You can get into the circular terminology deeper in the article but the lead, at least, should simply express the general concepts in a way that can be understood by complete neophytes. — LlywelynII 00:59, 21 October 2022 (UTC)
What is a capture? 2402:3A80:1A42:12E8:0:0:4141:250E ( talk) 07:26, 23 November 2022 (UTC)
According to the definition in the Lambda calculus#Lambda terms subsection, is not a lambda term, since x^2+2 is not a lambda term. It seems to me that we should add that x+y and x*y are also lambda terms, if x and y are. Dan Gluck ( talk) Dan Gluck ( talk) 16:44, 7 January 2023 (UTC)
{{
cite book}}
: |journal=
ignored (
help)Anas1712 ( talk) 16:56, 3 April 2023 (UTC)
Let's talk about what is missing in the statement. -- Ancheta Wis (talk | contribs) 16:24, 11 May 2023 (UTC)
This mechanism works well for Algol 60 but in a language in which functions can be returned as results, a free variable might be held onto after the function call in which it was created has returned, and will no longer be present on the stack. Landin (1964) solved this in his SECD machine.
In a functional programming language where functions are first class citizens, this systematic change in variables to avoid capture of a free variable can introduce an error, when returning functions as results.
@WillNess, please refer to (Selinger 2008) for his explanation of the scope of parentheses. Basically Selinger is trying to minimize the use of parentheses, but that does not mean that lambda calculus has no notion of scope, because Selinger is talking about the outermost level of parentheses. -- Ancheta Wis (talk | contribs) 22:04, 12 May 2023 (UTC)
Also, might you please participate in the discussion above ( 05:18, 12 May 2023 ), about D A Turner's ref to Landin's use of closures? If the article needs updating, we need more voices/suggestions. -- Ancheta Wis (talk | contribs) 22:04, 12 May 2023 (UTC)
One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.
should be
what the typed calculus can do Federicolo ( talk) 19:08, 2 October 2023 (UTC)
The section "Functions that operate on functions" contains a discussion on the identity and constant functions, but fails to use them to illustrate the point of the section - functions being used as input or output. VeeIsMe ( talk) 15:55, 4 November 2023 (UTC)
That sentence is supposed to be describing applicative order. I think it is confusing and unnecessary. For starters, a beta reduction is always applied to a redex. What exactly is an "argument" here? If, in that sentence, argument refers to the right side of a redex, then that sentence is false (that interpretation would fit call by value, not applicative order). And if it refers to bound variables, then the sentence is still false, because bound variables are not redexes. I think the most charitable interpretation of the sentence is that given a redex R, before R is reduced, one must reduce every redex U, if U's right side is a bound variable of R's function. Unfortunately, despite that new sentence's verbosity, it is not a complete definition of applicative order reduction. 81.158.160.194 ( talk) 04:14, 29 March 2024 (UTC)
This is the
talk page for discussing improvements to the
Lambda calculus article. This is not a forum for general discussion of the article's subject. |
Article policies
|
Find sources: Google ( books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
Archives: 1 |
![]() | This ![]() It is of interest to the following WikiProjects: | |||||||||||||||||||||||||||||||||||||||||||||||
|
Does anyone know why Church chose lambda as the letter symbol? Did it used to stand for something that started with L ? — Preceding unsigned comment added by 87.114.213.103 ( talk) 20:03, 4 September 2014 (UTC)
just wanted to leave a note saying that the article seemed pretty confusing to read at first sight. (there seemed to be good links though and maybe i'll come back after understanding it to make it more readable.) Harshav
I have no idea how to do this and I have no idea what lambda calculus is but the start of the "Imformal Description" where it says "In lambda calculus, every expression is a unary function" but then it says things like "λ y. y + 2;" -- well "y + 2" is an expression which is not a unary function. So, to have the very first sentence be so misleading is pretty bad. Pedzsan ( talk) 13:15, 7 June 2008 (UTC)
Lambda calculus is a method for (or theory about)- I dunno which) expressing (all?) functions ("functions" linked). Lambda calculus represents every mathematical expression as a unary function (linked). The lambda symbol is used to respresent such and such, and this relates to the concept of unary function because of such and such. For instance in the expression of f(x)=x+2 we typically perform such and such... Lambda calculus, instead would express this as such and such... So when we input such and such... the expression is mathematically identical but more verbose. -Michali —Preceding unsigned comment added by 67.142.130.11 ( talk) 06:30, 29 December 2008 (UTC)
Every article I've read about functional programming makes references to lambda calculus (and assumes you understand it), so I came here to try to figure it out. After reading the article and this discussion, lambda calculus still doesn't make any goddamn sense. Thanks guys. Anti-kudos. 150.135.222.63 ( talk) 20:54, 11 February 2009 (UTC)
It may be appropriate to introduce the formal syntax (x.x,λx.t, ts) in conjunction with the conceptual x -> y examples above it. Cackowski
The article mentions alpha-equivalence, but no direct explanation is given. That should probably be changed? Ran4 ( talk) 20:39, 9 April 2010 (UTC)
At the moment, the section "Arithmetic in lambda calculus" says "Note that 1 returns f itself, i.e. it is essentially the identity function, and 0 returns the identity function." If I understand the rest of the section correctly, this sentence has it the wrong way around: 0 is the identity function; 1 returns the identity function. So, I'm swapping the 1 and the 0. I'm definitely not an expert on this subject, though, so go ahead and revert my edit if I'm mistaken. — Saric ( Talk) 20:44, 16 February 2008 (UTC)
01-Nov-2008: I suggest adding a section "Controversy in lambda calculus" because it seems like overkill on fairly useless stuff. I still ponder "Why Johnny can't program" & "Why Johnny can't de-virus" & "Why Johnny can't word search" etc. I think subjects like lambda calculus created a nerd-iverse (re: "universe") that wasted hours on useless math games. Consequently, almost no one had time to focus on important topics, such as multi-word search. Can you believe it's 2008, even Google had copied multi-word search 10 years ago (in 1998), and how many text editors today can search for a multi-word match? As for "Why Johnny can't de-virus" as a 25-year ongoing nightmare, I think the answer lies in the fact that most people would buy a new "better" computer every time a virus killed their old PC: hence, some software companies had a vested interest in prolonging viruses that fostered sales of new software. Even so, Johnny wasn't taught to track & stop viruses that would kill each PC owned by almost everyone he ever met. The Computer Virus Era was 1983-2009?, which seems to be ending with Windows Vista stopping viruses before execution. My view is to cite sources that consider lambda calculus to be a limited concept that thwarted the expansion of computer science in other areas. For example, it has become common knowledge that languages are easier to program when using the standard syntax of algebra (but with words as variable names, not just x/y/z). The vast majority of all software systems originally written in LISP have been re-written in procedural, non-list languages. Simply as a matter of neutral balance, add some broader perspective to the article. - Wikid77 ( talk) 02:22, 1 November 2008 (UTC)
I note that the link ( http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9283) for Barendregt's book takes one to an internet shop. I think that should not be so. Could someone who is up to speed on it replace it with a proper reference with ISBN etc, A link to the text online, if available would also be good. PJTraill ( talk) 14:40, 14 February 2009 (UTC)
Lambda expression is not quite the same as an unnamed procedure without side-effects. It is a first-class citizen in the language design. Historically, this is a very important achievement, as this was the first formal system where such design was explored. In computer science there is an overarching concept of reification, which is roughly speaking the process of making a certain part of the run-time system visible within the language. The reification article has been recently updated, and it contains references to other areas in computer science where this process is used. It is important to make this link, as is one of the key benefits of Wikipedia. On the other hand, there are many resources on the Internet, which contain tutorials on lambda-calculus. This is the case to keep the link in the article.
I meant to argue against Equilibrioception's treatment of reification earlier, but got distracted. Talk the lambda-calculus being about first-class functions is alright, but a bit strange, to talk of it directly reifying any kind of procedure crosses the line from strange into positively perverse: the lambda calculus, though confluent, is a term rewriting system that is in terms of naive space and time resources highly nondeterministic, presumes no notion computational realisation and is not faithfully used in any non-toy implementation. I'm happy with the treatment of these concepts in the LC&PL section, and I think Landin's idea should be promoted to the second paragraph. — Charles Stewart (talk) 08:47, 18 March 2009 (UTC)
I propose merging the various lambda calculus articles into this one. All the other lambda calculus articles are (to me) hard to follow without understanding the lambda calculus ideas in this article. Therefore, I believe the other lambda calculus articles should become sections of this article. I realize this will make this article longer, but the basic concepts share so much in common that I believe it will make the exposition clearer. HowardBGolden ( talk) 04:38, 23 June 2009 (UTC)
References
The fact the 1st section freely mixes lambda expressions with numbers is contributing to the confusion with typed lambda calculi, because neither that section nor the lead explain that those numbers are actually encoded as functions in untyped lambda calculus. Granted, there's a section on that, but that comes way later. WP:LEAD should be observed here, i.e. the lead should summarize the important fact that data types have to be encoded in untyped lambda calculus. Pcap ping 21:29, 5 August 2009 (UTC)
A programming expression must always evaluate to a value as I understand it. E.g. x+3 is an expression since x is a pointer to a memory location with a value.
Therefore λy.y+2 is a function, not a programming expression, since y does not point to any memory location and no value can be evaluated. This lambda function is equivalent to f(y)=y+2. It surely only becomes a lambda expression when you make a function call like (λy.y+2) 3 and specify y so it evaluates to 5. Please see http://en.wikipedia.org/wiki/Expression_(programming).
Neither can λy.y+2 be a mathematical expression since its equivalent functional notation f(y)=y+2 contains an = symbol implying it is an equation not an expression. Please see http://en.wikipedia.org/wiki/Expression_(mathematics).
I think this should be clarified in the article. For example the wording "A lambda expression represents an anonymous function" appears to be misleading according to the above. —Preceding unsigned comment added by 92.39.205.210 ( talk) 21:46, 6 July 2009 (UTC)
After reading more on lambda calculus I think the "Informal description" section in this article is highly misleading to say the least. The term λx.x + 2 used in the section should not be used until both + and 2 have been defined otherwise the reader may think arithmetic terms like + and 2 are included in the lambda calculus by default which they are not. If you want + then it is built up from other operations i.e. λn.λm.(n add1 m) where add1 is λn.λf.λx.f(nfx), and 2 is defined as lf.lx.f(fx) according to Church numerals. The whole section needs redoing, it seriously misled me when I first read it.
As for the "expressions" point above it would be better to replace "lambda expressions" with "lambda terms" throughout to avoid confusion with the programming and mathematical meaning of "expressions" where an expression always evaluates to a value. In lambda calculus there are no values until you first define them using the rules so really the word "expression" doesn't apply to lambda calculus at a foundational level. —Preceding unsigned comment added by 92.39.205.210 ( talk) 12:44, 11 July 2009 (UTC)
The introduction is written as to imply the existence only one typed lambda calculus that Church published circa 1936 (besides the untyped one). This couldn't be more wrong or confusing! First, there's more than one flavor of typed lambda calculus, e.g. simply typed lambda calculus, but also others with more expressive types, System F etc. Church did write a technical report about simply typed lambda calculus, but only in 1940. In [2], p. 33 this is made clear enough (and, by the way, Curry essentially described simply typed lambda calculus in 1934). Also, simply typed lambda calculus is not just some "bug free" version that this article's intro seems to imply it is. The simply typed variant is not Turing complete, and neither are most other typed lambda calculi, which were later discovered by others, whereas the untyped lambda calculus is Turing complete. The fact that you can encode numbers and other types in untyped lambda calculus does not make it typed. Pcap ping 17:02, 5 August 2009 (UTC)
The man in the the sky heard us and fixed the most confusing part. But as Charles Matthews put it here, it is the wrong end of the microscope to delve on the foundational issue in the lead, which is only of historical interest today. Pcap ping 15:11, 20 August 2009 (UTC)
See talk page of the fixed point combinator for details on why "recursive" is meaningless as used in that section; I've fixed the main article, and eventually I'll fix this too. Pcap ping 00:41, 22 August 2009 (UTC)
The article may need clarifying in general but the most important thing is fixing the meaningless example of (λx.x+2) (where neither + nor 2 have been defined inside the theory). It's disconcerting when the very example designed to clarify the subject isn't a valid part of the theory. The writer should have used (λx.x x).
As for clarification, how about starting something like: "Lambda calculus, developed by Alonso Church in the 1930s is a technique for studying mathematic operations. The basic idea is to encode mathematic concepts in a code, and allowing the code to be manipulated in certain rigid ways to mimic the operations. Its importance nowadays is that it lent itself to computerization, inspiring the LISP programming language, and helped develop the general concept of programming functions." At least that's my understanding of it. CharlesTheBold ( talk) 20:21, 1 October 2009 (UTC)
The "informal description" section was far too confusing for the non-lay reader, IMO. I've attempted to rework the section the best I can, by placing an explicit "motivation" section, detailing where some of the concepts in the lambda calculus come from, and reworking the start of the rest of the section. Is this OK with everybody? —Preceding unsigned comment added by 137.195.27.217 ( talk) 14:02, 22 October 2009 (UTC)
(I was the original unsigned editor.)
I don't think we should mention tuples in the informal description. To my mind, that's getting far too picky in a section that's ostensibly aimed at a lay reader. Further, it's only type lambda calculi where tuples are nearly universally taken as primitive; untyped seems to be 50/50 (IME!), and if you go the encoding route, you aren't really contradicting what the article says at the moment (as the encoding is made with single argument functions).
I still think the Informal Description needs a lot more work, too (which I'll attempt when I have more time). DPMulligan ( talk) 15:59, 22 October 2009 (UTC)
FWIW, I only wrote the motivation section, and the first paragraph of the lambda calculus section. I've now rewritten the whole of the lambda calculus section, in order to make the section less confusing and consistent with the rest of what I'd written. I'd appreciate comments on this. One thing: I'm not very good with Wiki markup: the lambda terms, reductions etc. would probably look a lot better spaced out vertically. How does one do this? DPMulligan ( talk) 10:22, 23 October 2009 (UTC)
Also, stuff like a proper reduction arrow, alpha-equivalence symbol: are these available? DPMulligan ( talk) 10:24, 23 October 2009 (UTC)
I'm afraid the Informal Description section is still desperately confusing for a lay reader. I think the problem is that terms (English words & phrases that is, not lambda terms) are used without definition, or with specialised meanings that conflict with everyday usage. Examples:
In fact, I found the Formal Definition section much more digestible, but perhaps I'm just a sucker for BNF. There it helped that meta-variables are distinguished by case, so you can see that x is a <variable>, but M and N are <lambda terms> (which may be variables, applications or other abstractions, ...)
I realise the contributors to a page like this are going to be serious maths nerds, but they need to take a step back and recognise where they are using professional argot that overlaps with vernacular English so much that it cannot be parsed by the uninitiated. Swiveler ( talk) 13:23, 25 November 2009 (UTC)
I feel that all or most of the 2nd paragraph (starting "In the lambda calculus, functions are first-class entities...") should be cut. Do others agree? I can go line by line:
This line is okay, but maybe it can be streamlined and merged into the previous paragraph.
This line is bizarre. I agree with what Charles Stewart wrote above on 18 March 2009. I think it is also unnecessary and misleading to talk about side effects here. The original untyped lambda calculus was "pure" in the sense that it was restricted to function abstraction and application, but it wasn't really about "purity" in the sense of deliberately avoiding state. It wasn't because it couldn't be! As Charles pointed out, the semantics of the lambda calculus is highly nondeterministic, not a realistic model of computation, and so to even talk about state-ful functions you have to make a departure from the "real" lambda calculus. And in fact, all of the functional programming languages mentioned at the bottom of the paragraph (with the arguable exception of Haskell) do make this departure, and allow functions with side effects!
This is good.
The second half is POV, and wrong in my opinion. This fact is what allows for languages like Unlambda, but it is not what makes functional programming important.
What I wrote above -- this line is absolutely wrong for the standard definition of "functional programs", which includes programs witten in Lisp, ML, Scheme, etc.
It does make sense to mention some of the functional languages inspired by lambda calculus. But maybe that can be merged into the first paragraph. And it is absolutely wrong to imply that these languages are stateless! Noamz ( talk) 16:52, 25 October 2009 (UTC)
I agree. Cut the second paragraph, it's muddled and confusing. Merge whatever's salvageable into the first paragraph. DPMulligan ( talk) 23:27, 25 October 2009 (UTC)
There appear to be inconsistencies in this section; it is stated that the following holds: (λx.t)[x := r] = λr.t And yet in an example, ((λx.y)x)[x := y] = ((λx.y)[x := y])(x[x := y]) = (λx.y)y
I'm not sure, but I believe that the assertion that (λx.t)[x := r] = λr.t is erroneous. —Preceding unsigned comment added by 99.255.132.186 ( talk) 22:00, 29 October 2009 (UTC)
Argh. Yes, sorry, that was my fault. I realised I had a name clash with my original naming scheme, so changed the convention I was using halfway through, and thought I'd changed what I'd previously written. Sorry about that! DPMulligan ( talk) 11:06, 3 November 2009 (UTC)
Is this the same as alpha-renaming or alpha-conversion? If it is not, it must be explained why. Else, in Odifreddi (1992) (From Google Books: Piergiorgio Odifreddi. Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Volume 1. Volume 125 of Studies in Logic and the Foundations of Mathematics. ISBN 0444894837, 9780444894830), on page 77, it is defined the alpha-rule (another name for the same stuff?) as "We can rename bound variables: provided y does not occur in M, where M[x/y] indicates the result of the substitution of x by y everywhere". Repair that is replaced by . -- Menegola ( talk) 01:07, 14 December 2010 (UTC)
---
I believe the first part of
if x ≠ y and y is not in the free variables of r
is superfluous since the fact that x is different from y is stated where they are "declared". -- Andreas Lundblad ( talk) 11:18, 9 June 2011 (UTC)
I find the end of the paragraph on eta-conversion lacks some explanation. It states that
This conversion is not always appropriate when lambda expressions are interpreted as programs. Evaluation of λx.f x can terminate even when evaluation of f does not.
Could we have an example where the conversion is not appropriate, and an example where the evaluation of f does not terminate but the evaluation of λx.f x does ? Or are such examples too complicated ? 82.67.7.229 ( talk) 15:33, 8 November 2009 (UTC)
Also the paragraph in eta conversion is wrong. Eta conversion is much weaker than full blown extensionality. --
76.10.153.79 (
talk)
16:56, 2 February 2011 (UTC)
Furthermore, η conversion is not a fundamental aspect of lambda calculus. I think η should have received its separate section. (α-conversion is not fundamental either, but it is usual described with β-reduction, plus it has nothing to do with typing, whereas λx.(f x) implies that f has a functionnal type). Sedrikov ( talk) —Preceding undated comment added 16:22, 30 November 2012 (UTC)
Lambda calculus reads:
Functions are a fundamental concept within computer science and mathematics, as they are rules by which an input may be transformed into some output
this is true in computer science but not in mathematics! As put in Function_(mathematics):
a function is a relation between a given set of elements called the domain and a set of elements called the codomain
A function is the relation itself, not the set of rules that construct it. This distinction is important, because there are functions which cannot be constructed using any set of rules.
I don't know how to fix this without losing the original intent of the phrase. Perhaps the intended meaning becomes inappropiate because of this, so I'm just removing the "and mathematics" part. If you find a better way to reword it, it'd be appreciated :-)
193.153.229.101 ( talk) 19:35, 10 February 2010 (UTC)
I'd like the originator to demonstrate a function that cannot be expressed as a rule, If you can describe it in English, then you can construct a rule. Unless you need to define rule a particular way. I guess I am asking for more justification of the original fix. 65.175.239.50 ( talk) 13:52, 18 March 2010 (UTC)
What is a capture? A fundamental notion in formal languages? Why then does it not have its own WP article? (Or why is it not linked?)-- 217.232.244.191 ( talk) 14:30, 25 February 2010 (UTC)
To which section are you referring? The section on substitutions? 86.177.226.105 ( talk) 10:59, 2 April 2010 (UTC)
I've tried reading this article several times and I have to say, I still don't have a clue what lambda calculus actually is. The opening sentence says that it's "a formal system for function definition, function application and recursion" (and only recursion has a useful wiki link). The article assumes that you already know what a whole bunch of things are and from that, you already know why you'd use lambda calculus. I think that the article would greatly benefit if it included the following things in the lead:
I feel that with these changes, the article would become much more accessible to those who are not at all familiar with it. - Thunderforge ( talk) 17:35, 13 May 2010 (UTC)
Doesn't the informal description section already cover a lot of this? DPMulligan ( talk) 19:38, 13 May 2010 (UTC)
I have similar concerns about this article. I study computer science and mathematics, so I am not completely unfamiliar with terminology, but the whole idea of lambda-calculus is unclear to me. When I was reading article on bound and free variables, the explanation that made most sense to me was a linguistic one. Similarly, the first paragraph here completely throws me off: “a way to formalize mathematics through the notion of functions, in contrast to the field of set theory.” I do not dispute that I may be dumb, but is not the very “notion of function” described via set theory (“to each element of a set (domain) there is one and only one corresponding element of another set (range)”? theUg ( talk) 22:29, 16 February 2012 (UTC)
This page is missing a "History" section. -- a3_nm ( talk) 20:38, 16 October 2010 (UTC)
I'm trying to merge the article AlphaRenaming into this (see its talk page), but I'm not quite sure of the difference (if any) between "alpha conversion" and "alpha renaming". Is there a difference? It seems as though alpha-conversion means "any legal renaming" (as defined formally in this article), while alpha-renaming means "renaming from a term with overlapping scopes to a new term with no overlapping scopes".
For example, is a valid alpha-renaming (and alpha-conversion), whereas is an alpha-conversion but not an alpha-renaming since it didn't fix the overlapping scopes, and is also not alpha-renaming since the scopes weren't overlapping to begin with.
Or the two terms could mean exactly the same thing. I can only find colloquial uses of the term "alpha-rename", meaning "to make non-overlapping scopes", but not a true definition. It could be that the two terms are interchangeable. Anybody got a source? — MattGiuca ( talk) 06:31, 28 October 2010 (UTC)
The function definitions used for encoding booleans and numbers uses a syntax that is not defined. It shows a function containing 2 or more arguments, which is never explained. This should either be introduced prior to this section, or not used.
For example
Instead of what is written:
—Preceding unsigned comment added by 198.36.95.12 ( talk) 19:23, 13 April 2011 (UTC)
Ok, now that you point it out I can see it. This one line is fine for the Formal Definition. But I think an additional section of 1 or 2 examples would make it easier for a new-comer - or just avoid this syntax all together in the examples. This one liner definition is very easy to miss, and when looking for other explanatory examples - none can be found. As a start I updated the Church Encodings of numerals section to show both syntaxes. So now there is at least one set of examples for conversion. —Preceding unsigned comment added by 198.36.94.35 ( talk) 21:22, 21 April 2011 (UTC)
Hello. I refined the lead a bit boldly because I didn't agree with some statements recently introduced.
ComputScientist ( talk) 15:14, 4 January 2012 (UTC)
The definitions of the Church numerals 0..3 are exactly the same between the common and "alterate" notations. They not only appear the same; their source (mark-up) is the same. Macareus ( talk) 18:54, 15 March 2012 (UTC)
I use lambda calculus in the .Net language for anonymous functions. I am not a formal mathematician and found the following example confusing.
( ( X , Y ) → ( X * X + Y * Y ) ( 5 , 2 )
I did not know how to 'read' this statement. It came out in my head as something like: "For variables X and Y, calculate the formula substituting 5 and 2."
For anyone with elementary algebra there is an implied multiplication between the two bracketed terms. Lambda calculus has its own syntax but I believe it should be previously explained possibly, with a simpler example...
( X ) → ( X + 2 ) (6)
(read as ...)
Can someone supply the substitution for "..."?
This was done earlier with the statement:
(read as “the pair of X and Y is mapped to X * X + Y * Y”).
I would have preferred something like( X ) → ( X + 2 ) [6] or ( X ) → ( X + 2 ) {6} but I guess the syntax chosen is the correct formal method. Finally, apologies for not working out how to display the mathematical symbols. — Preceding unsigned comment added by Prcotter ( talk • contribs) 11:56, 20 April 2012 (UTC)
( (X , Y) → (X * X + Y * Y) ) (5 , 2)
( (X) → (X + 2) ) (6)
Guys, maybe the correct AND is AND = lambda p. lambda q. p q FALSE (with FALSE defined above) ? and not with p in the end..
The following is not a Y combinator, but seems to be able to function as one where one is needed: λx.(x x) 12.198.223.226 ( talk) 21:46, 29 June 2012 (UTC)JH
Lambda calculus is of interest to non-mathematicians, particularly to software engineers. In my experience, many intelligent software engineers complain that the topic is hard to learn not because of inherent complexity, but because most presentations of it are in a language that is trivial for mathematicians to understand but hard for engineers.
I attempted to expand a few terse paragraphs and had a 2.5k edit reverted nearly immediately by User:Ruud Koot with the comment undo: "sloppy writing rarely increases readability" (revision 528491773). I do not defend the edits as perfect, but they were significantly easier for a non-mathematician to understand than before.
I have reverted the undo. I am happy to work to come up with wording that preserves the readability of my version and yet corrects any flaws. TJIC ( talk) 12:24, 18 December 2012 (UTC)
I made a first pass copyediting the text. Here are some thought:
— Carl ( CBM · talk) 13:46, 18 December 2012 (UTC)
I plan to update this page with
The changes are primarily editorial in nature, to improve the tone and readability of the article. To this end quite a bit of material has been moved. The goal is to simplify the lambda calculus page and redirect people out to other pages for technical details.
If all goes smoothly after the change I will fix up links to the page.
Thepigdog ( talk) 04:27, 13 November 2014 (UTC)
I am trying to learn this. I do not have any expertise, and therefore the syntax might be fully correct. That being said, the following snippet under the introduction of the transformations confused me:
"For example, λ x.((λ x.x)x) and (λ x.(λ x.x)) x denote different terms (although coincidentally reduce to the same value.)"
If I am understanding correctly, these equations are not coincidentally the same, but must be the same, right? Let's take the two cases, breaking down each step:
λ x.((λ x.x)x): (λ x.x) is just x, so the eqn has become: λ x.(x * x), and then it becomes: x^2
(λ x.(λ x.x)) x: (λ x.x) is just x, so the eqn has become: (λ x.x) x: (λ x.x) is just x again, so now: x * x x^2
As stated, they reduce to the same equation, but he suggests this is coincidental. That's the part I'm missing. They are necessarily identical in all cases, if all I'm doing is merely moving around the parentheses where the lambda functions are performed, thereby introducing an extra identity function.
Stepping back, my real question is on syntax: these equations sometimes require that I put every function in a lambda "wrapper", and sometimes not. Is this allowed? Is it normal? To me, and hence the confusion, the equations necessarily had to be written as such:
1) λ x.((λ x.x) * x) 2) λ x.((λ x.(λ x.x)) * x)
In this way, it becomes obvious that the only difference between the two is that the second one has wrapped another identity function, which, necessarily, does not alter the equation at all. Am I missing something?
This.is.mvw ( talk) 16:53, 23 December 2014 (UTC)
In the section "Functions that operate on functions" an \rightarrow is used to write the identity. I would prefer to have "x \mapsto x", but then again I'm no computer scientist and so can't be sure this is not some sort of standard notation. Could someone who knows this stuff correct it or tell me why I'm wrong? EdvinW ( talk) 12:49, 11 December 2015 (UTC)
It should be made clear in the header what untyped lambda calculus is. I don't know enough about the subject to add anything of much use, sorry.
137.124.161.82 ( talk) 21:19, 16 February 2016 (UTC)
only a proposal, if I understand what is "alpha equivalence" and "beta reduction". how would it be, if it were:
thx for attention 94.219.96.38 ( talk) 22:50, 3 March 2016 (UTC)
The article states right in the beginning that the equivalence of lambda-calculus and Turing machines is the Church-Turing thesis. This affirmation seems to be wrong, though: The CT thesis states that these systems of computation, which had been PROVEN to be equivalent (and thus this equivalence is a theorem and not a thesis), describe, somehow, the human powers of computation. Equivalence in this sense cannot be proven mathematically, that's why it is a thesis. See Wikipedia's own article on the topic as a reference: /info/en/?search=Church%E2%80%93Turing_thesis 85.138.163.71 ( talk) 23:07, 30 May 2016 (UTC)
This comment: "It is a universal model of computation that can be used to simulate any single-taped Turing machine..."
Seems odd because any single-taped Turing machine can simulate any multitape Turing machine. By modus ponens then, shouldn't lambda calculus be able to simulate any multitape Turing machine because it can simulate any single-taped one?
Assuming that's true (and I would appreciate an expert confirming it is just to be sure) then we can probably change the above to "It is a universal model of computation that can be used to simulate any Turing machine..."
Hello fellow Wikipedians,
I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{
Sourcecheck}}
).
An editor has reviewed this edit and fixed any errors that were found.
Cheers.— InternetArchiveBot ( Report bug) 20:49, 12 September 2016 (UTC)
Hello fellow Wikipedians,
I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:
When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.
This message was posted before February 2018.
After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than
regular verification using the archive tool instructions below. Editors
have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the
RfC before doing mass systematic removals. This message is updated dynamically through the template {{
source check}}
(last update: 5 June 2024).
Cheers.— InternetArchiveBot ( Report bug) 02:29, 11 May 2017 (UTC)
If x and y are variables then xy seems to have no direct mathematical meaning. Shouldn't this be discussed? — Preceding unsigned comment added by G. Blaine ( talk • contribs) 21:50, 29 June 2017 (UTC)
The "informal description of lambda calculus" section currently goes into the technicalities of making substitution capture-avoiding, giving the same five definition cases as are later repeated in the formal definition section. I would suggest dropping those technicalities from the informal description—replacing them with just an example of how non-capture-avoiding substitution can go wrong—since these details are by far the most technical and confusing in the definition of the lambda calculus. (There are more confusing stuff you can do with lambda calculus, but the rest of the definition is pretty straightforward.) In view of past discussions, as recorded above on this talk page, I am however reluctant to do that change on just my own volition. 78.73.97.76 ( talk) 22:22, 8 July 2017 (UTC)
(Correction: It is the "Reduction" section that repeats the definition of capture-avoiding substitution, not the "Formal definition" one. Still, the suggestion stands. 78.73.97.76 ( talk) 12:09, 9 July 2017 (UTC))
In section 3.2.2 "Functions that operate on functions", the examples given are not of functions that operate on functions. Some better examples are needed. LoMaPh ( talk) 19:14, 9 November 2017 (UTC)
The use of the term "invention" suggest that the system is not a discovery, as would be held by mathematical Platonists. It also seems a like a pointless choice, given that anyone looking in that category would almost certainly not be looking for a model of computation.
After the example (λx.λy.(λz.(λx.z x) (λy.z y)) (x y)) the article states "Parentheses can be dropped if the expression is unambiguous". I would argue that the expression (λx.z x), which is a sub-expression of the above example is unambiguous. According to the three syntax constructions the expression (λx.z x) can be constructed as ((λx.z) x) or (λx.(z x)). So I believe there is missing information about precedence of the syntax constructions. Does the "." (dot) operator (syntax construction 2) have higher or lower precedence than the " " (space) operator (syntax construction 3)? -- Jarl ( talk) 08:22, 9 March 2019 (UTC)
The story about the lambda symbol arising via a series of typographical errors is implausible on its face, and directly disputed by Dana Scott in this talk. Barendregt does not give any evidence in that 1997 article, and it's not clear where he got it from or if he just meant it as a joke. (The other citation in this section to "Mathematical Methods in Linguistics" does not seem to have any relevance.) I suggest deleting this section. Noamz ( talk) 14:49, 16 May 2019 (UTC)
On further digging, this question is also discussed in Carbone and Hindley's History of Lambda-calculus and Combinatory Logic:
(By the way, why did Church choose the notation “λ”? In [Church, 1964, §2] he stated clearly that it came from the notation “ˆx” used for class-abstraction by Whitehead and Russell, by first modifying “ˆx” to “∧x” to distinguish function-abstraction from class-abstraction, and then changing “∧” to “λ” for ease of printing.
This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and “λ” just happened to be chosen.)
The reference [Church 1964] is an unpublished letter to Harald Dickson (not available online as far as I can tell), but in any case, from the way Carbone and Hindley describe it that original version of the story is pretty different than the version given by Barendregt, which seems like it passed through a couple rounds of telephone (game). So given this and the Dana Scott video, my impression is that the origin story is indeed apocryphal, albeit perhaps with a bit of help from Church himself. Noamz ( talk) 18:06, 22 May 2019 (UTC)
This section explains that the equivalence of two expressions in the lambda calculus is undecidable, though it doesn't cite any references. Which references should be cited here? Jarble ( talk) 16:15, 3 June 2019 (UTC)
Hello, how can operators or constants be brought in by application of these three rules? Are these supposed to be covered by the first rule? If so, the word "variable" is misleading to me. Stefan84556 ( talk) 01:00, 27 July 2020 (UTC)
For example, and denote different terms (although they coincidentally reduce to the same value).
There are too many different uses of for these expressions to be reasonably understood. It's used as the argument for the outer and inner lambdas and, in the second expression, a useless free variable. Something like and , which reduce to and respectively, would be much less confusing. (It may be impossible to make lambda calculus easy to understand, but we can at least not actively make it more difficult.) Nloveladyallen ( talk) 22:33, 2 March 2021 (UTC)
A search directed me to a lambda calculus wikibook. There was only a very wrong short intro with concepts borrowed from some not very formal lisp book. I wrote something with the purpose make it clear that many of what was written was wrong because the lambda calculus is important as a foundation of computing theory. Unfortunately I have no time to work on that enterprise. Maybe this article could be copied in wikibooks to be transform it in a lambda calculus book. I did not check if there were previous attempts to write such wikibook. -- User:2806:106e:b:31b1:3a5f:db9e:42bd:b4bd 00:51, 15 August 2022 (UTC)
From the talk page, it seems like there have been efforts in the past to turn this article into something that is actually helpful as an introduction to the subject that were overriden in favor of the previous unhelpful versions.
This is just a reminder that the current introduction is circular nonsense that only makes sense if a reader is already fully aware of what all of the terms and syntax mean. It should absolutely be rewritten for normal humans, at maximum to a high school reading level. You can get into the circular terminology deeper in the article but the lead, at least, should simply express the general concepts in a way that can be understood by complete neophytes. — LlywelynII 00:59, 21 October 2022 (UTC)
What is a capture? 2402:3A80:1A42:12E8:0:0:4141:250E ( talk) 07:26, 23 November 2022 (UTC)
According to the definition in the Lambda calculus#Lambda terms subsection, is not a lambda term, since x^2+2 is not a lambda term. It seems to me that we should add that x+y and x*y are also lambda terms, if x and y are. Dan Gluck ( talk) Dan Gluck ( talk) 16:44, 7 January 2023 (UTC)
{{
cite book}}
: |journal=
ignored (
help)Anas1712 ( talk) 16:56, 3 April 2023 (UTC)
Let's talk about what is missing in the statement. -- Ancheta Wis (talk | contribs) 16:24, 11 May 2023 (UTC)
This mechanism works well for Algol 60 but in a language in which functions can be returned as results, a free variable might be held onto after the function call in which it was created has returned, and will no longer be present on the stack. Landin (1964) solved this in his SECD machine.
In a functional programming language where functions are first class citizens, this systematic change in variables to avoid capture of a free variable can introduce an error, when returning functions as results.
@WillNess, please refer to (Selinger 2008) for his explanation of the scope of parentheses. Basically Selinger is trying to minimize the use of parentheses, but that does not mean that lambda calculus has no notion of scope, because Selinger is talking about the outermost level of parentheses. -- Ancheta Wis (talk | contribs) 22:04, 12 May 2023 (UTC)
Also, might you please participate in the discussion above ( 05:18, 12 May 2023 ), about D A Turner's ref to Landin's use of closures? If the article needs updating, we need more voices/suggestions. -- Ancheta Wis (talk | contribs) 22:04, 12 May 2023 (UTC)
One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.
should be
what the typed calculus can do Federicolo ( talk) 19:08, 2 October 2023 (UTC)
The section "Functions that operate on functions" contains a discussion on the identity and constant functions, but fails to use them to illustrate the point of the section - functions being used as input or output. VeeIsMe ( talk) 15:55, 4 November 2023 (UTC)
That sentence is supposed to be describing applicative order. I think it is confusing and unnecessary. For starters, a beta reduction is always applied to a redex. What exactly is an "argument" here? If, in that sentence, argument refers to the right side of a redex, then that sentence is false (that interpretation would fit call by value, not applicative order). And if it refers to bound variables, then the sentence is still false, because bound variables are not redexes. I think the most charitable interpretation of the sentence is that given a redex R, before R is reduced, one must reduce every redex U, if U's right side is a bound variable of R's function. Unfortunately, despite that new sentence's verbosity, it is not a complete definition of applicative order reduction. 81.158.160.194 ( talk) 04:14, 29 March 2024 (UTC)