Talk:Lambda calculus

Note on readability

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 resummarise 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)

Mix-up of 0 and 1

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

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

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

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

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.

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

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)

Lambda Expressions. Clarification of the term expression.

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

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

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)

Priorities on fixes

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

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)

Cut 2nd paragraph?

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)

Capture Avoiding Substitutions

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.