Talk:Lambda calculus

From Wikipedia, the free encyclopedia
Jump to: navigation, search
          This article is of interest to the following WikiProjects:
WikiProject Computing (Rated B-class, Low-importance)
WikiProject icon This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
B-Class article B  This article has been rated as B-Class on the project's quality scale.
 Low  This article has been rated as Low-importance on the project's importance scale.
 
WikiProject Mathematics (Rated B-class, Mid-importance)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
B Class
Mid Importance
 Field: Foundations, logic, and set theory
One of the 500 most frequently viewed mathematics articles.
This article has comments.
WikiProject Philosophy (Rated B-class, Low-importance)
WikiProject icon This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.
B-Class article B  This article has been rated as B-Class on the project's quality scale.
 Low  This article has been rated as Low-importance on the project's importance scale.
 
 
WikiProject Computer science (Rated B-class, Top-importance)
WikiProject icon This article is within the scope of WikiProject Computer science, a collaborative effort to improve the coverage of Computer science related articles on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
B-Class article B  This article has been rated as B-Class on the project's quality scale.
 Top  This article has been rated as Top-importance on the project's importance scale.
 
This article has an assessment summary page.

Note on readability[edit]

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

Agreed. The introduction just seemed to ramble on (rather than the snappy thoughts that many good Wikipedia entries have). Usually this problem is limited to the mathematics pages of Wikipedia, not so much the computing ones (because a lot of geeks contribute and improve it). Shall I slap an "unreadable, please resummarize me" icon on the top of the page? Whophd 08:32, 12 April 2007 (UTC)

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)

"+" is a binary function that returns the sum of two arguments, but "λ y. y + 2" specifies a function that takes a single argument and adds 2 to it. A B Carter (talk) 02:20, 8 June 2008 (UTC)
    • Yeah definitely try to make this introduction easier to understand. I would do it, obviously, but I came here to understand it myself. Do not start using expressions such as the lambda symbol until we understand what its being used for. And try to cut it up to some clear propositions. Allow me to give a layout:

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.xx.t, ts) in conjunction with the conceptual x -> y examples above it. Cackowski

Alpha-equivalence[edit]

The article mentions alpha-equivalence, but no direct explanation is given. That should probably be changed? Ran4 (talk) 20:39, 9 April 2010 (UTC)

Mix-up of 0 and 1[edit]

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)

No, it was right before. Think of this this way: (3 f) is a function that applies f three times to its argument. That is, ((3 f) x) is (f (f (f x))). Similarly, (1 f) is a function that applies f once to its argument: ((1 f) x) is (f x). So (1 f) is the same as f, and so 1 itself is nothing more than the identity function. (0 f) applies f zero times to its argument, so ((0 f) x) is x. So (0 f) is the identity function, and 0 itself is not the identity function, but the constant function that always returns the identity function. Hope this helps. -- Dominus (talk) 21:11, 16 February 2008 (UTC)
Oh, so it was already discussed here. ComputerScientist, read Dominus' answer to get the question you stated in your change comment anwsered. I agree with removing that confusing sentence altogether. Daniel5Ko (talk) 12:52, 18 May 2009 (UTC)
Cheers. Sorry, wasn't thinking. But hold on: I think you need eta equivalence to get (1 f) = f. ComputScientist (talk) 13:17, 18 May 2009 (UTC)
I think so too. (And sorry for misspelling your user name) Daniel5Ko (talk) 13:27, 18 May 2009 (UTC)
I disagree that it was confusing. So far all three of you have correctly understood what the article was trying to communicate, which is that 1 is the identity function, and 0 is the function that always returns the identity function. The problem here is not that you misunderstood what the article was saying, but rather that you understood it correctly and didn't believe it. So I am going to put back the offending sentence. —Dominus (talk) 18:14, 18 May 2009 (UTC)
This was correct up until an anonymous editor screwed it up in the edit of 08:54, 1 December 2008. —Dominus (talk) 18:20, 18 May 2009 (UTC)
Causing confusion and being correct are completely orthogonal. I still believe the sentence shouldn't be in its current context, but instead maybe moved somewhere else or removed. What's the value of it? Daniel5Ko (talk) 21:43, 18 May 2009 (UTC)
I am not sure what the value is. We could instead say "(0 f) is the identity function, and (1 f) = f". But isn't this obvious from the definition and the previous sentences? [I was initially confused yesterday because I usually think of typed λ-calculi; 1 is not the parametric identity function in system F.] ComputScientist (talk) 06:33, 19 May 2009 (UTC)
Yes that is pretty obvious. And that's where the confusion comes in. The start of the sentence ("Note that...") as well as the actual content seem to imply great importance which just isn't there. In the search for the perceived deep meaning, the casual reader gets lost. (I'm still opting for removal) Daniel5Ko (talk) 21:49, 19 May 2009 (UTC)
I am persuaded; let's get rid of it. —Dominus (talk) 13:20, 20 May 2009 (UTC)

Proposed criticism of lambda calculus[edit]

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)

Hello. I'd like to see your references! I don't think you are criticizing the lambda calculus per se, but rather criticizing "people who spend time studying the lambda calculus". You could levy the same criticism on most advanced mathematical subjects: in part, the lambda calculus is studied for purely intellectual reasons. Another thing: you criticize lisp, but my understanding is that functional languages like Haskell are increasingly useful from a commercial perspective [1]. 87.114.24.216 (talk) 09:43, 1 November 2008 (UTC)
So, the criticism is that people have (in fact) ignored developing certain applications because they're busy playing around with an unhelpful kind of formalism. This criticism seems to misconstrue lambda calculus as developed exclusively for use in computer programming languages with an eye to aiding the development of all useful applications. It is merely a tool, like any other. It also has applications in mathematical logic and linguistics, of which this critic seems to be completely unaware. 145.18.22.149 (talk) 11:11, 16 February 2009 (UTC)

Book link should not be to internet shop[edit]

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)

CiteSeerX is not an internet shop, but repository of free (when freely available) computer science papers. Don't get confused by the "metacart" stuff; you don't have to pay to get what's in it. See their about page. Pcap ping 07:40, 21 August 2009 (UTC)

Lambda-expression and reification[edit]

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.

-- Equilibrioception (talk) 04:32, 18 March 2009 (UTC)
Hi, you are right that the first-class status of functions is important, so I've tried to clarify this now. I just didn't want people to have to know what "reification" meant in order to read the introduction. While the "first-class status" part should be kept, I'm not sure that it is worth mentioning the word "reification" in the introduction. "Reification" means a lot of different things, and I am not sure that the way it is being used here is the most common meaning. I'd be interested to know what others think. ComputScientist (talk) 07:54, 18 March 2009 (UTC)

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)

ComputerScientist, I am ok with the current edit. I'd be looking at the introduction to give me the definition, the general context and the essential details, the significance, and connections to other things. Reification is indeed a more general concept than first-class object, but they are synonyms in the context involving the lambda-expressions. Again, I like the current wording.
Charles Stewart, please note, that the term "reification" is used consistently both in the context of lambda-calculus and in the context of functional programming languages. Personally, I do not see it outrageous to refer to a particular decision in the design of a mathematical object as "reification". Also, I find the concept of a "reified function" (function as a first-class object) and the concept of a higher-order function an important difference between lambda-calculus and TRS.
-- Equilibrioception (talk) 01:31, 19 March 2009 (UTC)
Hi Equilibrioception. Could you give a reference to the word "reification" being used in this way, with regard to the lambda calculus? I don't think I have come across it before. (Charles, I am not quite sure which idea of Landin's you mean, but go ahead and move it up.) Thanks, ComputScientist (talk) 07:23, 19 March 2009 (UTC)
I agree that reification (computer science) is a rather obscure name for a meta-concept, probably coming from the knowledge representation guys, that's most commonly referred to using other terminology in CS (first-class values etc.); I think WP:JARGON applies here, so could link to it, but provide a brief explanation on first use. Pcap ping 15:05, 20 August 2009 (UTC)
I have no problem with using the word "reification" somewhere in the article. However, I hope a simpler word or phrase can be used in the opening of the article. IMO there is enough of a hurdle to understand the concept of lambda calculus without using words the general reader is unlikely to understand. Also, "first-class value" is jargon. In the opening it would be better IMO to use a description like "functions may be passed to other functions as arguments and returned as results." — HowardBGolden (talk) 08:31, 26 October 2009 (UTC)

Merge discussion[edit]

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)

I doubt this will solve any difficulties anyone has with understanding the topic that clearer signposting couldn't. Could you indicate how you would organise the sections, so that the discussion can be more concrete? — Charles Stewart (talk) 07:45, 24 June 2009 (UTC)
(Let me begin by explaining my concept: The subject is really much simpler than most people believe, but this is obscured by notation which is unfamiliar to most people unless they have advanced mathematical training or exposure to a functional programming language. The (unintentional but real) obfuscation starts with the name "lambda calculus," combining a Greek letter (why?) with "calculus" used in an uncommon sense. Also, there is the issue of calculus vs. calculi, since it must be explained that there isn't just one lambda calculus. I think the present article gets much too deep much too early, compounding the inherent difficulties for the reader already contained in the subject. In addition, I think the present article attempts too much, becoming almost a course in itself. Here is how I would begin the article:)
The lambda calculus, also written with the Greek letter λ (lambda), is a minimalist symbolic calculation system (calculus). It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s as part of an investigation into the foundations of mathematics. It starts with only a few simple concepts which are then combined to generate all other mathematical concepts, in the same way the axioms of geometry are used to generate the theorems. Despite its minimal basis, the lambda calculus is capable of expressing all algorithms that a Turing Machine can perform. It has been adopted as the basis for functional computer programming languages. The original lambda calculus of Church has given rise to other calculation systems (calculi) with additional concepts. These are collectively referred to as lambda calculi, some of which are discussed later.[1]
==Informal description==
The lambda calculus consists of a single operation, function application, on lambda expressions. Lambda expressions are built up from functions and variables by applying simple rules described below. All functions are expressed using a notation that begins with the letter λ. In lambda notation, to apply a function to an argument, the function is placed before the argument. No parentheses are used to surround the argument. The reason for this notation will become clear shortly.
It is very helpful to compare how functions are defined in conventional notation vs. the lambda notation. For instance, a numeric add-two function, which adds 2 to its argument, can be expressed in conventional mathematical notation as f such that f(x) = x + 2, or sometimes (using anonymous function notation) as x ⟼ x + 2. In lambda calculus notation, the add-two function would be written as λx.x + 2. Here the letter λ indicates the start of a function definition. The letter x following it is the bound-variable. The point separates the bound-variable from the result expression, in this case x + 2. Please note that this function has no name in the lambda notation.
In conventional mathematical notation, the application of function with the name f to a number 3 is expressed as f(3). In lambda calculus the application of this function to a number 3 can be written as x.x + 2) 3. Note that the parentheses surround the function definition to separate it from the argument, but the argument isn't surrounded by parentheses.
In both conventional notation and lambda notation, function application is performed by substituting the argument wherever the bound variable appears in the expression on the right side of the function definition, so the results of the applications above are both 3 + 2.
(Note that part of what makes this description "informal" is that neither the number 2, nor the + operator, are part of the pure lambda calculus, since it has no constants. This example uses an enhanced lambda calculus which includes constants to make the comparison with conventional notation clearer. Later, it will be shown that numbers and arithmetic (constants) can be fully defined in pure lambda calculus (see arithmetic in lambda calculus)).
(Carrying this kind of simplification throughout the article, my idea is that different lambda calculi can be introduced as variants of the pure lambda calculus. This would include contrasting untyped and typed lambda calculi. I believe this belongs in the section on lambda calculus and programming languages.) - HowardBGolden (talk) 08:35, 13 July 2009 (UTC)
  • I like your summary more than what we have (note that I've fixed a claim: Church had invented the lambda-calculus, in 1928, before he took on Kleene as a student, in 1931). If you can keep the article streamlined, it does make sense to merge them: after all, the link to combinatory logic does go back to the origins of the calculus. — Charles Stewart (talk) 09:40, 13 July 2009 (UTC)
  • I also think your proposal is a good one. Thanks. —Dominus (talk) 14:17, 13 July 2009 (UTC)
  • Which articles do you want to merge into this one, exactly? This article is rather long as it stands. (I also wonder if some of the section on encoding data types should be taken out of this main article.) ComputScientist (talk) 18:31, 15 July 2009 (UTC)
  • I oppose the merge based on the obvious reason that simply typed lambda calculus is an important enough topic in PL theory: Benjamin C. Pierce dedicates the entire chapter 9 of his book Types and Programming Languages to simply typed lambda calculus; that book is widely accepted as the standard introductory monograph in PL type theory. The wikipedians proposing these mergers (all lambda calculus articles in one) basically seem to have little clue what they're talking about, and they admit it too. Their proposal make no sense to someone that took a graduate PL class. Any such mergers will simply spread their confusion to our readers. Pcap ping 12:40, 3 August 2009 (UTC)
  • And if you wonder, the untyped lambda calculus gets its own chapter 5 in the book mentioned above. Having separate articles on untyped and simply typed l.c. is not outlandish. Pcap ping 12:57, 3 August 2009 (UTC)
  • I have Pierce's book on my bookshelf. I will look at chapters 5 and 9 as you suggest. My suggestion for merging the articles is based on my belief about how long and technical articles should get. (It does no good for an article to be so sophisticated that only those who already understand the subject can read the article.) The various lambda calculi are very important to functional programming. That's why I want an article that introduces the subject in a way that will be readable by someone who hasn't taken a graduate programming languages class. At what point should the article defer to Pierce or other texts? (I suspect this sort of discussion has already occurred many times. Please help me by referring me to previous discussions which I will gladly read.)HowardBGolden (talk) 09:10, 4 August 2009 (UTC)
  • This article should be mostly about untyped lambda calculus, i.e. it should describe it reasonable detail, but leave typed lambda calculi, of which there's more than one, to separate articles. See new section about the confusion(s) caused by the manner the intro of this article is written. Pcap ping 17:11, 5 August 2009 (UTC)
  • For the reader unfamiliar with the subject, "lambda calculus" is a single concept. Therefore, IMO, an essential part of an article titled "Lambda calculus" should be to explain that there are many lambda calculi and outline their basic similarities and differences. When I proposed a merger, this is what I wanted to achieve. Due to the length of the article, it is fine with me if the individual calculi are covered in more detail in separate articles. As I stated above, the article currently is (IMO) way too technical and won't be understood by someone who doesn't understand the subject already. The essence of my suggestion is to correct that. — HowardBGolden (talk) 20:33, 5 August 2009 (UTC)
  • Okay, what you're actually proposing is that this article should (also) contain a WP:SUMMARY section highlighting the distinction between untyped lambda calculus and the typed lambda calculi—and I'm perfectly fine with that. From my perspective, the problem with the current article isn't that it's "way too technical", but rather that the technical details are vague to the point of easily being interpreted the wrong way. I've posted some notice on the Math and CS wikiprojects. Let's see what others think before proceeding. Pcap ping 21:21, 5 August 2009 (UTC)

Informal presentation issues[edit]

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)

As someone that yet know lambda calculus, the Informal description section itself seems to not be complete. Although the use of narrative is a helpful one, there seem to be some underlying assumptions made that makes it incomplete for someone unfamiliar with the subject matter. There is a chance it's just me, but I'm comfortable with functional programming, reduction, curried functions etc, but there still seems to be a couple of key concepts assumed from the reader (particularly in the subsections about Lambda terms and Alpha equivalence). It might be useful if someone more could look over it and determine if it is missing something, or just my lack of comprehension. --59.167.232.215 (talk) 11:16, 5 July 2011 (UTC)
Can you elaborate on the sentences you're having problems with? Those subsections seem to tiptoe around variable bindings and scope, but if you're fluent in FP and curring, this surely isn't what you're missing? Diego Moya (talk) 11:57, 5 July 2011 (UTC)
As a lay reader, my problem with this section is that " lambda terms" is discussed but it is never actually defined. The term is simply used repeatedly in that section and the reader is left to infer what " lambda terms" are from context. — Preceding unsigned comment added by 184.175.10.230 (talk) 13:42, 28 September 2011 (UTC)

Lambda Expressions. Clarification of the term expression.[edit]

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)

In your comments I think you have jumped ahead too far by comparing a lambda expression to a programming expression. At the lowest level, lambda calculus is about a symbolic "game" (i.e., set of rules independent of any machine) where the rules allow you to replace some symbols with other symbols. In this sense, there is no concept of "value" inherent in lambda calculus. You are free to assign one. Lambda calculus was designed by Church to be the basis for all mathematics. The remarkable thing (to me) is that simple substitution can generate the magnificent whole. - HowardBGolden (talk) 22:01, 11 July 2009 (UTC)
The more I read about about it the more impressive it becomes, so it is remarkable as you say. You are right about values too, there are none explicitly except those simulated by a combination of lambda terms, e.g. Church numerals, amazing. Even true and false are just two argument functions. Going back to the point about the phrase "lambda expressions" I do still think it is misleading since many will associate an expression as occurring only when there is a value whereas the phrase "lambda expressions" in the article includes say λx.x which is not a simulated value. (λx.x)y = y would be more like a value if the variable y could be taken as pointing to a memory location but I guess y is just a symbol so not a value?

Confusing introduction[edit]

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)

P.S.: I think that some if not all of the "merge all lambda calculus articles into this one" proposal above stem from this basic confusion. Pcap ping 17:05, 5 August 2009 (UTC)
I agree with you that the introduction is confusing. I have suggested another introduction above. Is it a better starting point? Perhaps you could suggest specific wording to accomplish your objective.
My comment on merging the articles is in that section above. — HowardBGolden (talk) 20:20, 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)

No, the man in the sky actually made the article even more confusing/incorrect. So I believe this is how it went (see the Cardone and Hindley article): 1. Church published a bunch of papers on the lambda calculus in the 30s, including the well-cited one from 1936, 2. Kleene-Rosser paradox shows LC can't be used as a logic, 3. Church tries to come up with a consistent logic, and publishes the simply typed lambda calculus in 1940. I've corrected the first paragraph to reflect this, and also done a little bit of tweaking to emphasize the importance of both typed and untyped LC in programming languages. However, I think the introduction still needs a lot of work, and could be better along the lines proposed in Talk:Lambda_calculus#Merge_discussion above. Noamz (talk) 03:44, 24 October 2009 (UTC)
Mea culpa. My edit incorrectly got rid of the distinction between Church's original formulation of the lambda calculus as a logic, and the purely computational language. I've corrected that now. I think the confusion in the original version was contrasting the inconsistency of Church's original logic with the "consistency" of the untyped lambda calculus (with citation to Church-Rosser). Those are different notions of consistency (logical vs equational). Anyways, sorry for the drama. I should know better than to be editing wikipedia pages at 5 in the morning. Noamz (talk) 04:25, 24 October 2009 (UTC)

Rubbish in the fixed point section[edit]

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)

I fixed some of it; needs more work. Potatoswatter (talk) 19:33, 10 March 2010 (UTC)

Priorities on fixes[edit]

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)

Hi Charles. The example λx.x+2 is not meaningless. It makes perfect sense in a typed lambda calculus (and typed calculi are arguably most important in modern computer science). One could also add constants + and 2 to the untyped calculus, or understand them as shorthand for the constructions introduced later in the article. I have had a go at clarifying this, but please someone revert me if it is more confusing. I don't think (λx.x x) is a good first example because that is not a function that the beginner will have seen before (also, it doesn't make sense in most typed calculi). Perhaps the best thing to do is to make a general overview article, and to then have a special article on the untyped calculus. I haven't got time to do this, though. ComputScientist (talk) 07:10, 2 October 2009 (UTC)

Reworked informal description[edit]

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)

Nice. I wonder if we should be a little more careful in saying how functions-that-take-multiple-arguments are dealt with. An alternative to currying is to have a function that accepts a tuple of arguments. Tuples can either be encoded or taken as primitive (most typed calculi have product types). I'm not too sure how to make this point in a nice way, though; maybe we should leave it how it is. ComputScientist (talk) 15:13, 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)

Yes, I agree that we don't want to be too picky. [Small rant: My problem with this article is that it is mostly about the untyped calculus (despite not being called that). Most applications involve typed calculi, and moreover the best way to understand the untyped calculus is arguably as an instance of a typed calculus with a universal type. BUT, then again, I suspect that most of the ~900 daily readers/editors are undergraduates who are looking for help with their courses (presumably untyped).] ComputScientist (talk) 18:41, 22 October 2009 (UTC)
Three points about the revision:
  • It uses "lambda abstraction" at the beginning, but the rest uses "lambda expression." Either the relationship of "abstraction" to "expression" should be explained, or one of the terms (abstraction/expression) should be used throughout.
  • I think it would help a novice to explain that the λ introduces the expression and the dot separates the variable (or variables when using the notational convention) from the result. (For me, this unconventional notation was the biggest stumbling block at first.)
  • The section that begins with "The following expression in the lambda calculus is particularly notable:" doesn't belong in the "Informal description" section, but later in the article.
HowardBGolden (talk) 00:22, 23 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)

Nice. One little thing: it's probably a good idea NOT to precisely define substitution in the "informal" section. A couple of examples don't hurt, but in this quick informal overview we can rely on the reader's intuitions on binding and substitution. As it stands, the discussion of substitution is more than half of the overview, which feels unbalanced. By all means move some of this discussion to the "formal" section. I'm happy to have a go at this, but you're doing a nice job. ComputScientist (talk) 14:00, 23 October 2009 (UTC)
There is a unicode arrow, →, which appears as a button below my editing box. You can also do \lambda x.x and directly type latex. This can translate simple things to unicode html, but bigger things it makes into images which don't look nice inline. ComputScientist (talk) 14:05, 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:

  • the application of input s to some function t: in programming and general algebra, one "applies" a function t to an input s, producing a result r, i.e. r = t(s). Is that what this means? If so, saying "the application of some function t to an input s" might make more sense to most readers. Or how about "feeding an input s to a function t"?
  • functions are first class value: I know roughly what this means in programming languages. But then you explain the effects of being first class on a function, without explaining what "first class" actually means. Can a variable be "first class"? Is there a "second class"? At least link to First-class object.
  • Capture avoiding substitution: is that substitutions that avoid capture? It could be hyphenated (capture-avoiding) to make it clearer. And what is "capture" in this context anyway?
  • a freshness condition: implies that this is not the definition of "freshness condition", but an example of a freshness condition, whatever that may be. Actually, the whole "Capture avoiding substitution" section is horribly difficult to understand, although I found it a bit easier with the examples broken out on separate lines.

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)

Cut 2nd paragraph?[edit]

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:

In the lambda calculus, functions are first-class entities: they are passed as arguments, and returned as results.

This line is okay, but maybe it can be streamlined and merged into the previous paragraph.

Thus lambda expressions are a reification of the concept of an unnamed procedure without side effects.

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!

The lambda calculus can be thought of as an idealized, minimalistic programming language.

This is good.

It is capable of expressing any algorithm, and it is this fact that makes the model of functional programming an important one.

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.

Functional programs are stateless and deal exclusively with functions that accept and return data (including other functions), but they produce no side effects in 'state' and thus make no alterations to incoming data.

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.

Modern functional languages, building on the lambda calculus, include Erlang, Haskell, Lisp, ML, and Scheme, as well as nascent languages like Clojure, F#, Nemerle, and Scala.

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)

Okay so I went ahead and cut the entire second paragraph, as well as the third because it seemed redundant. I spent some time thinking about how to merge a bit of the 2nd paragraph into the 1st, but gave up when I realized the lede would only get more convoluted, and that the alternative lede that HowardBGolden proposed above is in any case much better. Is HowardBGolden still around? Whatever happened to that plan? Noamz (talk) 23:23, 30 October 2009 (UTC)
I'm still around. I haven't proceeded due to some of the alternative ideas and also my lack of attention to this article. I would still like to work on this. Part of the discussion should be about the intended audience. If it includes readers who haven't had any previous exposure to LC, then I think a more discursive approach would help them get past the unusual notation (which was a stumbling block for me for a long time). I also think the article shouldn't become a textbook. Instead, the reader should be referred to a Wikibook or another text. — HowardBGolden (talk) 06:36, 10 November 2009 (UTC)

Capture Avoiding Substitutions[edit]

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)

yes, that's a bug: should be (λx.t)[x := r] = λx.t Noamz (talk) 23:28, 30 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: \lambda x.M \xrightarrow{\alpha} \lambda y.M[x/y] provided y does not occur in M, where M[x/y] indicates the result of the substitution of x by y everywhere". Repair that \lambda x is replaced by \lambda y. --Menegola (talk) 01:07, 14 December 2010 (UTC)

No. Alpha conversion is as you said; we associate the terms of form \lambda x . M with \lambda y . ( M [x:= y] ) provided that y does not occur in M. This is akin to being able to changed the variable in a "for" loop in C from i to j as long as you're not using j for something else; the name of a bound variable doesn't matter. In the capture-avoiding substitution section it's defining the actual substitution operation inductively on terms (what I wrote at M[x:=y] and what you wrote at M[x/y]). The "capture avoiding" part is this can only be done to free variables, so (\lambda x . M)[x:=N] = (\lambda x . M). I'm not quite sure in what context these two would be confused, so if you could elaborate any remaining concerns I'd be happy to try to address them and make appropriate changes. Thanks. Wgunther (talk) 02:53, 14 December 2010 (UTC)
This last statement is insightful and should be considered for the main article. Also, for understandability the free variables for the given functions (r,s,t) should be made explicit. [Cackowski]

---

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)

Sorry I don't know what you mean. The whole condition is necessary. Otherwise (λx.x)[x:=t] becomes λx.t, which is wrong. ComputScientist (talk) 14:31, 9 June 2011 (UTC)
But the whole section starts with Suppose t, s and r are lambda terms and x and y are variables where x does not equal y --Andreas Lundblad (talk) 12:48, 10 June 2011 (UTC)
Thanks, I didn't notice that. I've fixed it now by removing that part at the beginning of the paragraph, which seems more reasonable than the particular clause. Feel free to undo me if you disagree. The same definition appears twice in the article, which is clumsy. ComputScientist (talk) 14:46, 10 June 2011 (UTC)

Expand the Eta-conversion paragraph[edit]

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)

I think what this is getting at is that in many (in fact most) interesting evaluation strategies for functional languages, evaluation never occurs "under a λ", i.e., λx.f x is a value, even though f may express some non-terminating computation (computing a function). Examples of languages with no evaluation under a λ are LISP and ML. (Likewise Haskell, but there the evaluation of plain f is also delayed until it is needed (i.e., applied to an argument), so there is no difference in termination behavior.) But so this is a bit odd way of putting it, because in these languages evaluation of λx.f x will always terminate. Maybe the subjunctive "can" was meant to quantify over different evaluation strategies? In any case, I think it would make more sense to talk about restrictions on βη conversion in the section on different reduction strategies. Noamz (talk) 00:43, 11 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)

Functions aren't rules[edit]

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)

The sentence does not read correctly anymore. "a common task in both disciplines" hangs in the air. —Preceding unsigned comment added by 146.232.75.208 (talk) 14:52, 22 February 2010 (UTC)
I wonder if it really needs fixing. Functions in the lambda-calculus sense certainly are rules. The existence of choice functions and the like could be taken here as outside the scope of the discussion. —Dominus (talk) 15:08, 22 February 2010 (UTC)
Proposal:
"Functions are a fundamental concept within computer science and mathematics. While mathematics in general is concerned with all formal relations, and thus in particular with one-many relations aka functions, computer science investigates those particular functions that can be defined in terms of formal rules that, for any given input of appropriate type (namely, that of the function's arguments), determine a computable output of the same type as the function's values. Computer languages provide a means of specifying such rules in a form that, if represented in a computer's memory, make the rules, and thus the function, effectively computable. It is therefore customary in computer science to refer to the rules themselves as functions."
Please, 193.153.229.101, before you make changes to WP articles next time, read the whole article at least once with an eye on what might be affected by your change. If you intend to make substantial changes, please have a glance at "what links here" as well. Not all WP articles are self-contained. --217.232.244.191 (talk) 15:43, 25 February 2010 (UTC)
I don't understand why this article needs such an elaborate discussion of the philosophy of functions and of the distinction between constructive functions and nonconstructive functions. It seems like a digression from the main point of the article, which is supposed to be about the lambda calculus. —Dominus (talk) 16:17, 25 February 2010 (UTC)
I rewrote this contentious paragraph to stick to what I think are the main points: functions are important, and the lambda calculus provides a simple model of computation with functions. —Dominus (talk) 16:35, 25 February 2010 (UTC)
I am not complaining, but, what parts of my above proposal are philosophical? --217.232.250.74 (talk) 12:58, 26 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)

That's partly the point. A simple counting argument shows that there are functions that cannot be expressed in English and so cannot be described by rules. But noncomputable functions are also examples here. For example, there is no lambda expression which, given another lambda expression as an argument, returns λxy.x if the argument possesses a normal form, and λxy.y if not. —Dominus (talk) 15:28, 18 March 2010 (UTC)

What is a capture?[edit]

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)

What exactly is lambda calculus? I still don't know.[edit]

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:

  • A better definition of lambda calculus that would make sense to people with little to no knowledge of computer science.
  • As part of that definition, any technical words (i.e. something that someone with little to no knowledge in computer science would not be familiar with) that cannot be explained in a simpler way are wikified.
  • A clear summary of why someone would use lambda calculus.
  • A clear summary of the advantages of lambda calculus.
  • A quick and clear delineation between typed and untyped calculus, explained in a way that it would make sense to someone with little to no knowledge in computer science. This can be further explained in a section of the article.
  • A more concise history for the lead, perhaps just saying the date of its invention. Right now, the lead has three different dates and it's very confusing. A more in-depth history would be better suited in a section of the article.

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)

The informal description section is a little better than the led, but I still get lost after it starts talking about anonymous functions (and I have no idea what the point of making a function anonymous is because that article isn't all that user-friendly either). At any rate, I was mostly talking about the lead, which is incredibly difficult to understand for someone without any knowledge of it. That's what most people read when they just want a cursory knowledge of what lambda calculus is and it's just way too confusing at this point. -Thunderforge (talk) 21:57, 13 May 2010 (UTC)
Strongly agree. No, the informal description does not cover it. There is nothing comprehensible in this article that actually explains in a non-technical manner what the lambda-calculus is. I have been visiting it for years in the hope that someone would provide a comprehensible introduction, but it has not improved. I cannot; I am one such non-specialist reader. Even quite technical articles such as the Goldbach conjecture manage this in comprehensible form. I myself wrote a non-specialist intro for Romansh language that provided this, which is still in place years later. This really needs fixing; without it, the articles on Lisp, John McCarthy & various others are incomplete. Liam Proven (talk) 13:49, 19 December 2010 (UTC)
I agree that the article, as is, is generally poorly written, organized, and typeset (in my opinion, both to specialists and non-specialists alike). It's been on my radar for awhile on things I'm going to try to fix up. If anyone wishes to help me with this (or, allow me to help them!) contact me through my talk page. I'll try to get started rolling out some adjustments over the next few weeks, starting with with the non-specialist summary and history sections (arguably the two most poorly written and the two most important sections for an encyclopedia article). Thanks Liam for reminding us. Wgunther (talk) 17:37, 19 December 2010 (UTC)
Happy to help if I am able! Not sure I'm competent, though. I won't be online much from 22-29 Dec '10 due to being on dial-up, though. Liam Proven (talk) 12:35, 20 December 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)

I am in the process of rewriting. The article is not friendly for anyone right now. My userpage has the beginnings of my attempt (which was the rewritten lead). As for your comment regarding the lead, set theory attempts to formalize mathematics with the notion of sets. So in set theory, there is a notion of a function, which is coded in the language of set theory. Lambda Calculus, historically, was an attempt to formalize mathematics with the notion of a function. One would then code math (eg. sets) into that language. Its like, you can code PA in ZFC, but it doesnt mean every natural number is a set. I mean, in PA you can code all of HF (hereditarily finite sets, which is V_\omega, or ZF-infinity) and nobody pretends all such sets are natural numbers. Its just a useful code. Category theory has been much more successful as an alternative to set theory, as far as foundations go. Lambda calculus in foundations was stifiled by the Kleene Rosser paradox early on, and HOL and Q_0 were systems that never really caught on. Wgunther (talk) 23:10, 17 February 2012 (UTC)

History[edit]

This page is missing a "History" section. --a3_nm (talk) 20:38, 16 October 2010 (UTC)

Alpha-conversion versus alpha-renaming[edit]

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, \lambda x. \lambda x. x \Rarr \lambda x. \lambda y. y is a valid alpha-renaming (and alpha-conversion), whereas \lambda x. \lambda x. x \Rarr \lambda y. \lambda y. y is an alpha-conversion but not an alpha-renaming since it didn't fix the overlapping scopes, and \lambda x. x \Rarr \lambda y. y 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)

Hi Matt. I think that "alpha renaming" is indeed sometimes a synonym for "alpha conversion". But perhaps compiler writers use it to mean what AlphaRenaming says. There are no references on the page AlphaRenaming. We should probably find some good references before merging it. (Sorry, I don't have any compiler books with me now.) ComputScientist (talk) 07:07, 28 October 2010 (UTC)
I just checked the purple dragon book; it doesn't mention Lambda calculus or alpha renaming at all (it only barely touches on scope). I have asked around a bit; I'm starting to think the two are interchangeable (which the names suggest anyway). — MattGiuca (talk) 23:30, 28 October 2010 (UTC)
I don't have access to it, but an academic gave me this quote from Turbak and Gifford, Design concepts in programming languages: "Consistently renaming the variables of an expression in a way that preserves its alpha-equivalence class is called alpha-renaming." So I'm going to assume the two terms are equivalent since I am yet to see anybody formally or informally define alpha-renaming as "an α-conversion that makes name resolution trivial by making sure that no name masks a name in a containing scope" outside of the Wikipedia article AlphaRenaming. — MattGiuca (talk) 00:38, 29 October 2010 (UTC)

Syntax of Lambda Calculus[edit]

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

TRUE := λxy.x

Instead of what is written:

TRUE := λxy.x

—Preceding unsigned comment added by 198.36.95.12 (talk) 19:23, 13 April 2011 (UTC)


It's explained in the "Notation" subsection of the "Formal Definition" section. Wgunther (talk) 20:20, 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)

Refined lead[edit]

Hello. I refined the lead a bit boldly because I didn't agree with some statements recently introduced.

  • First, I don't really believe the statement that the lambda calculus is "a formal system for studying ... variable binding and substitution". Primarily, variable binding and substitution are important because they are used in the study of the lambda calculus, rather than the other way round. (Perhaps the editor is keen on HOAS but that's a bit niche for this undergrad level article.)
  • Second, it is wrong to say that "The portion of the lambda calculus relevant to computation is now called the untyped lambda calculus". A typed lambda calculus can be just as relevant to computation, particularly if it has recursive types. Many people believe that the right way to understand that untyped lambda calculus is as a "unityped" calculus with the recursive type U=(U->U).

ComputScientist (talk) 15:14, 4 January 2012 (UTC)

Hi, I'm the author of the changes introducing the wording about binding and substitution. I disagree with your assessment of the lack of centrality of these concepts in the lambda calculus. I am a computer scientist working in the area of type theory and metatheory of formal languages. I am familiar with higher-order abstract syntax, but that has really nothing to do with why I introduced that phrasing. The lambda calculus, in comparison to alternatives such as combinatory logic, is all about variables and substitution. It is arguably the most central concept of the language, codified in the rules, and the method by which computation performs. Perhaps one could argue that the wording should have been changed to "a formal system for expressing computation by way of variable binding and substitution", or some other alternative, on the grounds that variables are not first-class objects in the same way they are in some forms of logical frameworks. However, I think that is a bit of a subtle distinction and one that non-experts should not be too concerned with. In any case, the concepts of binding and substitution deserve to be featured prominently in the lead because it is impossible to understand the lambda calculus without them. I agree with your second comment. 69.92.252.58 (talk) 06:07, 20 January 2012 (UTC)
So, as for your first comment, I disagree with you. Imagine you no nothing about the lambda calculus and you read the current first sentence; it has very little encyclopedic value. Binding and substitution are important because that is a way to formalize the theory of functions, which was the driving force for the invention of the lambda calculus. That should be in the first sentence. As for your second statement, I also disagree with you. The untyped lambda calculus historically is one of the major models of computation. No one should be talking about recursive types in the introduction of this article. The information that you state could be somewhere in the article, but putting it in the introduction hinders people without any background in the area. I will try to correct the lead sometime soon. Wgunther (talk) 18:30, 22 January 2012 (UTC)
Hi. I think that it is possible to be precise while still giving an informal idea. On the first point, I now understand what 69.92.252.58 was getting at and I prefer the alternative wording that he suggests: "a formal system for expressing computation by way of variable binding and substitution". That's very nice. On the second point, I agree that recursive types don't need to be mentioned in the first sentence, but to say "The portion of the lambda calculus relevant to computation is now called the untyped lambda calculus" is to exclude typed calculi as irrelevant to computation, which is very wrong and misleading. It is correct, however, to say that the untyped calculus has played a central role in computability theory. ComputScientist (talk) 13:40, 23 January 2012 (UTC)

Section 6.1 Arithmetic -- alternate notation is no different[edit]

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)

The example structure is not defined for a newbie[edit]

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 (talkcontribs) 11:56, 20 April 2012 (UTC)

The example you cite above is wrong, it's missing a parentheses:

( (X , Y) → (X * X + Y * Y) ) (5 , 2)

Note how the function definition is enclosed completely; this avoids any confussion on precedence. Brackets are not interpreted as algebraic multiplication but as standard function application to arguments, just like f (x); but instead of "f" the name of the function is "(X , Y) → (X * X + Y * Y)".
Similarly, the simpler example should be:

( (X) → (X + 2) ) (6)

should be read as 'apply "the function that adds 2" to the value "6"'. Diego (talk) 13:20, 20 April 2012 (UTC)

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

Y Combinator and workalike[edit]

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

accessibility for non-mathematicians[edit]

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)

There are several issues with the next text. The main one is tone, which is too conversational for an encyclopedia article. For example, words like "we", "you", and "note", and contractions, should be avoided; bold to emphasize stress in sentences should be avoided; sentences that emphasize "software engineers" are out of place; and sentences such as "The formal definition of the syntax of lambda terms is simple." and "Variables need no further explanation." are chatty. I will go through and copyedit the text to make the tone more encyclopedic. — Carl (CBM · talk) 12:55, 18 December 2012 (UTC)
A lot of those edits were sloppy. I was going to revert until I saw someone else did. Two examples. First, you erased a paragraph with quite a lot of content in it, and replaced it with a sentence that begins "for software engineers..." and has very little content in it. Secondly, "The syntax of the lambda calculus means that some expressions are valid lambda calculus statements and some are not..." This sentence is nonsensical, and carries no content. Of course some things are terms and some things aren't. This is like adding to the PA article before the axioms of arithmetic the sentence "the axioms of PA mean that some things are natural numbers and some things aren't." I'll be the first to admit, this article is poorly written for non-mathematicians. A goal of mine has been a rewrite, especially the "informal introduction" section. But making it accessible to software engineers (which I'd even claim your edits do not to) does not make it more encyclopedic. Wgunther (talk) 13:08, 18 December 2012 (UTC)

I made a first pass copyediting the text. Here are some thought:

  • I removed the part about variable renaming because it didn't seem to be the same sort of issue as the issues of anonymous functions and currying. The latter two are about things you cannot do in the simplest lambda calculus: have names for functions or functions of several variables. The former is about things you can do: rename variables.
  • There is a huge amount of duplication between different sections of the article. For example, there are two definitions of the set of lambda terms; two definitions of beta reduction; etc. I would recommend editing the article to merge these together.
  • There is a paragraph about untyped lambda calculus not distinguishing between data types, but that is misleading because there simply are not data types, everything is the same type. This should be edited to be more correct.
  • There are still more uses of "we" and such that need to be reworked; I can only do a few sections in one sitting, so I will come back to them.

— Carl (CBM · talk) 13:46, 18 December 2012 (UTC)

Yes, the "Informal description" and "Formal definition" sections are quite messed up. For example, I don't see a need to go into detail about free variables or capture-avoiding substitutions in the first. It also seems odd that "Substitution" is covered under α-renaming instead of β-reduction. Finally, the section about "Encoding datatypes" should be significantly cut down in size. It duplicates a lot of content from Church encoding and takes up to much space in comparison to its importance. —Ruud 19:01, 18 December 2012 (UTC)

Recent "rewrite" of the article[edit]

I've by now lost any hope that this rewrite is going anywhere, so I've restored the previous incarnation of the article (which is also a very poor one, but alas...) I'm not going to point out any specific issues I have the rewrite: it's simply uniformly poorly written, incomprehensible, or worse.
I don't think the stream of consciousness posted on the talk page is particularity helpful either. —Ruud 18:02, 18 July 2013 (UTC)