Talk:Lambda calculus

Where did the name come from? Why the letter L?

Does anyone know why Church chose lambda as the letter symbol? Did it used to stand for something that started with L ? — Preceding unsigned comment added by 87.114.213.103 (talk) 20:03, 4 September 2014 (UTC)

It's not a letter, it was a typesetting problem. The first idea was to put a ^ on top of x, but the typesetters had a problem doing that. So they changed it to ∧x, which was later changed for convenience to λx. Source: History of λ-calculus and Combinatory Logic” by J. R. Hindley, F. Cardone (Handbook of the History of Logic, 5: 723–817, Elsevier, 2009). Blonkm (talk) 17:38, 7 September 2014 (UTC)

If this is correct, then the lede is wrong. The name derives from the printers' use of the letter Λ (capital lambda) in the character pair ΛX meant to represent any character X with a circumflex glyph (aka hat, roof, house) over it, eg. x̂, ŷ, ẑ. (Numerous Diacritics are used in mathematics to indicate that the underlying variable has been changed in a specified manner, eg. õ, ō, ò, ó, ȯ, ö). I'd assume that the Church? paper's authors' choice of the circumflex was more or less arbitrary, but this would require their verification, the use of that notation may have prescedents. The word "calculus" is often used to describe a system of computation or logic. I wonder why the caret wasn't used (^X) or was it?216.96.78.28 (talk) 23:13, 10 September 2015 (UTC)

And I really wonder what was the title of original Church's manuscript, that was sent to publishers? "What"-calculus was that then, where there was no lambdas in it? — Preceding unsigned comment added by 212.75.255.51 (talk) 11:13, 24 September 2015 (UTC)

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

Alpha-equivalence

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

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)

References

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)

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.

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://wiki.riteme.site/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://wiki.riteme.site/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)

I fixed some of it; needs more work. Potatoswatter (talk) 19:33, 10 March 2010 (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)

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?

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

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

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

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?

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.

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

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

Alpha-conversion versus alpha-renaming

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\Rightarrow \lambda x.\lambda y.y$ is a valid alpha-renaming (and alpha-conversion), whereas $\lambda x.\lambda x.x\Rightarrow \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\Rightarrow \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

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 := λx.λy.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

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

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

I use lambda calculus in the .Net language for anonymous functions. I am not a formal mathematician and found the following example confusing.

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

I did not know how to 'read' this statement. It came out in my head as something like: "For variables X and Y, calculate the formula substituting 5 and 2."

For anyone with elementary algebra there is an implied multiplication between the two bracketed terms. Lambda calculus has its own syntax but I believe it should be previously explained possibly, with a simpler example...

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

(read as ...)

Can someone supply the substitution for "..."?

This was done earlier with the statement:

(read as “the pair of X and Y is mapped to X * X + Y * Y”).

I would have preferred something like( X ) → ( X + 2 ) [6] or ( X ) → ( X + 2 ) {6} but I guess the syntax chosen is the correct formal method. Finally, apologies for not working out how to display the mathematical symbols. — Preceding unsigned comment added by Prcotter (talk • contribs) 11:56, 20 April 2012 (UTC)

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

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

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

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)

Planned change

I plan to update this page with

• User:Thepigdog/Lambda_Calculus

The changes are primarily editorial in nature, to improve the tone and readability of the article. To this end quite a bit of material has been moved. The goal is to simplify the lambda calculus page and redirect people out to other pages for technical details.

• Informal description - gone, replaced with new material (simple description and example of lambda calculus reductions and conversion).
• Formal definition - Moved to Lambda calculus definition
• Encoding datatypes - Replaced duplicated material with results.
• Recursion and fixed points - Gone (duplicated material from Fixed-point combinator).
• Reduction strategies - Moved to Lambda calculus definition

If all goes smoothly after the change I will fix up links to the page.

Thepigdog (talk) 04:27, 13 November 2014 (UTC)

As previously, please don't. —Ruud 09:35, 13 November 2014 (UTC)

OK. But the current article seems arrogant, pretentious and badly written. You fix it. Thepigdog (talk) 10:29, 13 November 2014 (UTC)

Transformations Introduction: the syntax is hard to follow / understand

I am trying to learn this. I do not have any expertise, and therefore the syntax might be fully correct. That being said, the following snippet under the introduction of the transformations confused me:

"For example, λ x.((λ x.x)x) and (λ x.(λ x.x)) x denote different terms (although coincidentally reduce to the same value.)"

If I am understanding correctly, these equations are not coincidentally the same, but must be the same, right? Let's take the two cases, breaking down each step:

 λ x.((λ x.x)x):
 (λ x.x) is just x, so the eqn has become:
 λ x.(x * x), and then it becomes:
 x^2

 (λ x.(λ x.x)) x:
 (λ x.x) is just x, so the eqn has become:
 (λ x.x) x:
 (λ x.x) is just x again, so now:
 x * x
 x^2

As stated, they reduce to the same equation, but he suggests this is coincidental. That's the part I'm missing. They are necessarily identical in all cases, if all I'm doing is merely moving around the parentheses where the lambda functions are performed, thereby introducing an extra identity function.

Stepping back, my real question is on syntax: these equations sometimes require that I put every function in a lambda "wrapper", and sometimes not. Is this allowed? Is it normal? To me, and hence the confusion, the equations necessarily had to be written as such:

 1)  λ x.((λ x.x) * x)
 2)  λ x.((λ x.(λ x.x)) * x)

In this way, it becomes obvious that the only difference between the two is that the second one has wrapped another identity function, which, necessarily, does not alter the equation at all. Am I missing something?

This.is.mvw (talk) 16:53, 23 December 2014 (UTC)

I didn't understand your explanations for the following reasons: There are no equations here, only terms. λx.x is quite different from x. There is no justification for introducing "*" or "^".

The "coincidentally" in the article probably should mean that paranthesation usually does matter, but in this particular example doesn't. Maybe another word would be more accurate, but I have to leave a judgement about this to native English speakers. - Jochen Burghardt (talk) 18:13, 23 December 2014 (UTC)

\rightarrow vs. \mapsto

In the section "Functions that operate on functions" an \rightarrow is used to write the identity. I would prefer to have "x \mapsto x", but then again I'm no computer scientist and so can't be sure this is not some sort of standard notation. Could someone who knows this stuff correct it or tell me why I'm wrong? EdvinW (talk) 12:49, 11 December 2015 (UTC)

Untyped lambda calculus redirects to this page.

It should be made clear in the header what untyped lambda calculus is. I don't know enough about the subject to add anything of much use, sorry.

137.124.161.82 (talk) 21:19, 16 February 2016 (UTC)

maybe you can put α equation and β reduction in the structure of the text

only a proposal, if I understand what is "alpha equivalence" and "beta reduction". how would it be, if it were:

we soon talk about (1) α-equation and (2) β-reduction

(1) about α-equation we talk so and so.

(2) for β-reduction we need to know, what is (a) free variables and (b) capture-avoiding substitutions

(2.a) about free variables we talk so and so.

(2.b) and about capture-avoiding substitutions we talk so and so.

so we can now talk about β-reduction.

thx for attention 94.219.96.38 (talk) 22:50, 3 March 2016 (UTC)

Reference to Church-Turing thesis

The article states right in the beginning that the equivalence of lambda-calculus and Turing machines is the Church-Turing thesis. This affirmation seems to be wrong, though: The CT thesis states that these systems of computation, which had been PROVEN to be equivalent (and thus this equivalence is a theorem and not a thesis), describe, somehow, the human powers of computation. Equivalence in this sense cannot be proven mathematically, that's why it is a thesis. See Wikipedia's own article on the topic as a reference: https://wiki.riteme.site/wiki/Church%E2%80%93Turing_thesis 85.138.163.71 (talk) 23:07, 30 May 2016 (UTC)

I agree, I've just removed the reference to the thesis, keeping the source as it refers to the actual theorem. I think this section is quite poor overall, so it might be worth rewriting it. − Pintoch (talk) —Preceding undated comment added 06:43, 31 May 2016 (UTC)

Single-Taped Turing Machine Simulation?

This comment: "It is a universal model of computation that can be used to simulate any single-taped Turing machine..."

Seems odd because any single-taped Turing machine can simulate any multitape Turing machine. By modus ponens then, shouldn't lambda calculus be able to simulate any multitape Turing machine because it can simulate any single-taped one?

Assuming that's true (and I would appreciate an expert confirming it is just to be sure) then we can probably change the above to "It is a universal model of computation that can be used to simulate any Turing machine..."

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20040823174002/https://www.elsevier.com/wps/find/bookdescription.cws_home/501727/description to http://www.elsevier.com/wps/find/bookdescription.cws_home/501727/description

When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{Sourcecheck}}).

Y An editor has reviewed this edit and fixed any errors that were found.

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 20:49, 12 September 2016 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Lambda calculus. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20011206080336/http://www.jetcafe.org/~jim/lambda.html to http://www.jetcafe.org/~jim/lambda.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 5 June 2024).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 02:29, 11 May 2017 (UTC)

application xy

If x and y are variables then xy seems to have no direct mathematical meaning. Shouldn't this be discussed? — Preceding unsigned comment added by G. Blaine (talk • contribs) 21:50, 29 June 2017 (UTC)

In this context it means that x is a function of some sort and that you should apply it to y. The syntax is clearly discussed at the start of the article and this is just the same syntax. —David Eppstein (talk) 22:20, 29 June 2017 (UTC)

Suggestion: Skip "capture-avoiding" in the informal description

The "informal description of lambda calculus" section currently goes into the technicalities of making substitution capture-avoiding, giving the same five definition cases as are later repeated in the formal definition section. I would suggest dropping those technicalities from the informal description—replacing them with just an example of how non-capture-avoiding substitution can go wrong—since these details are by far the most technical and confusing in the definition of the lambda calculus. (There are more confusing stuff you can do with lambda calculus, but the rest of the definition is pretty straightforward.) In view of past discussions, as recorded above on this talk page, I am however reluctant to do that change on just my own volition. 78.73.97.76 (talk) 22:22, 8 July 2017 (UTC)

(Correction: It is the "Reduction" section that repeats the definition of capture-avoiding substitution, not the "Formal definition" one. Still, the suggestion stands. 78.73.97.76 (talk) 12:09, 9 July 2017 (UTC))

I would even suggest removing the entire "Informal description" section as it has multiple issues, in particular non-traditional notation for terms, use of the same symbol for meta-lambda-abstraction as for lambda-abstraction, and mostly duplicating the same content covered more formally; these issues create confusion. I think it would make more sense to have this article to start with formal definitions right after general description by removing duplicate content there and merging "Explanation and applications" and "History" into it. Codedot (talk) 07:29, 9 July 2017 (UTC)

Examples for "Functions that operate on functions"

In section 3.2.2 "Functions that operate on functions", the examples given are not of functions that operate on functions. Some better examples are needed. LoMaPh (talk) 19:14, 9 November 2017 (UTC)

Putting this in the category "American Inventions" suggests a view on Platonism

The use of the term "invention" suggest that the system is not a discovery, as would be held by mathematical Platonists. It also seems a like a pointless choice, given that anyone looking in that category would almost certainly not be looking for a model of computation.

I'm inclined to agree with you. Removed category for now Poltair (talk) 12:49, 24 February 2019 (UTC)

Unambiguous expressions and operator precedence

After the example (λx.λy.(λz.(λx.z x) (λy.z y)) (x y)) the article states "Parentheses can be dropped if the expression is unambiguous". I would argue that the expression (λx.z x), which is a sub-expression of the above example is unambiguous. According to the three syntax constructions the expression (λx.z x) can be constructed as ((λx.z) x) or (λx.(z x)). So I believe there is missing information about precedence of the syntax constructions. Does the "." (dot) operator (syntax construction 2) have higher or lower precedence than the " " (space) operator (syntax construction 3)? --Jarl (talk) 08:22, 9 March 2019 (UTC)

Formal definition -- Notation states, "The body of an abstraction extends as far right as possible: λx.M N means λx.(M N) and not (λx.M) N." WillNess (talk) 09:36, 21 May 2023 (UTC)

please remove apocryphal story in "Origin of the lambda symbol"

The story about the lambda symbol arising via a series of typographical errors is implausible on its face, and directly disputed by Dana Scott in this talk. Barendregt does not give any evidence in that 1997 article, and it's not clear where he got it from or if he just meant it as a joke. (The other citation in this section to "Mathematical Methods in Linguistics" does not seem to have any relevance.) I suggest deleting this section. Noamz (talk) 14:49, 16 May 2019 (UTC)

it's a very bad quality sound there, but all I could decipher was that Church didn't explain the choice, but said it had no significance. Sounded like he didn't say he chose that symbol. If the talker said "prof. Church said he just picked something at random" that would be meaningful. But again, sound quality is bad. If you could provide transcript at the relevant part of it, with the time stamp, it would be super helpful. WillNess (talk) 07:13, 22 May 2019 (UTC)

The sound quality is not great, but the relevant parts include:

• [0:58-1:23] Church's son-in-law John Addison wrote his father-in-law a postcard with the message: "Dear Prof Church, Russell had the iota operator, Hilbert had the epsilon operator. Why did you choose lambda for your operator?"
• [1:24-1:37] Church's response was: "Eeny, meeny, miny, moe".
• [1:39-1:42] Scott concludes from Church's response that "there is no significance to the choice of lambda".
• [1:43-2:19] Scott goes on to discuss Barendregt's story about the series of typographical errors, but says "that's a completely false story".

WillNess wrote: If the talker said "prof. Church said he just picked something at random" that would be meaningful. Yes, that's exactly what Scott is concluding from Addison's question and Church's response. Noamz (talk) 12:46, 22 May 2019 (UTC)

On further digging, this question is also discussed in Carbone and Hindley's History of Lambda-calculus and Combinatory Logic:

(By the way, why did Church choose the notation “λ”? In [Church, 1964, §2] he stated clearly that it came from the notation “ˆx” used for class-abstraction by Whitehead and Russell, by first modifying “ˆx” to “∧x” to distinguish function-abstraction from class-abstraction, and then changing “∧” to “λ” for ease of printing.

This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and “λ” just happened to be chosen.)

The reference [Church 1964] is an unpublished letter to Harald Dickson (not available online as far as I can tell), but in any case, from the way Carbone and Hindley describe it that original version of the story is pretty different than the version given by Barendregt, which seems like it passed through a couple rounds of telephone (game). So given this and the Dana Scott video, my impression is that the origin story is indeed apocryphal, albeit perhaps with a bit of help from Church himself. Noamz (talk) 18:06, 22 May 2019 (UTC)

this is all highly inconclusive. That the choice is unimportant says nothing about who made it and why. Prof. Scott, again, does not convey the specific words of Church on that matter. His personal impression is irrelevant. Your other sources actually support the story as written in the article: "symbol was needed" why? could be, because of typographers. And the unpublished letter says exactly the same thing: circumflex --> caret --> /\ --> λ (so, not Church picking it at random!!), and it even says "for ease of printing"!! I'd say, definitely a supportive evidence for Barendregt's version. So until clear sources are found that disprove Barendregt (and [Church 1964] himself), the story should stay. WillNess (talk) 08:26, 25 May 2019 (UTC)

I don't mean to be rude, but I suggest that you read the different versions of the story and the video/transcript of Dana Scott's talk more carefully. There is no debate that it was Church who chose to use the λ notation in his original papers on the lambda calculus (where do you see a controversy about that?), the only question is why he chose it. Scott's version corroborates the second paragraph from the Cardone and Hindley article where they say that in later years Church told (at least two) people that his choice of the letter λ was arbitrary. The first paragraph of Cardone and Hindley suggests that Barendregt's (unsourced) anecdote apparently has some basis in something he might have heard sometime, but the version that they describe from the 1964 letter is clearly different, since there Church wrote that he wanted to use a different notation from Principia Mathematica.

I do not think that Barendregt's version of the story merits inclusion in the article. In the interests of being more constructive, I can try to create a new version of the paragraph based on Cardone and Hindley's explanation, including a link to Dana Scott's lecture as well. Noamz (talk) 13:36, 25 May 2019 (UTC)

Done. Noamz (talk) 14:45, 25 May 2019 (UTC)

The question wasn't whether it was he who made the final choice, but whether it was on his on volition or was prompted by the typography demands. Nice straw man there.

So you haven't built consensus and acted (I assume, by your "Done") on your own. WillNess (talk) 14:05, 27 May 2019 (UTC)

Removing (I assume; haven't checked the article yet) a sourced material long present in the article. I.e. acting disruptively. WillNess (talk) 14:07, 27 May 2019 (UTC)

I'm sorry that I mischaracterized your position. If you have a look at the current version of the article, I hope you find it acceptable: I've included both the typography-related explanation quoting directly from Cardone & Hindley (2006), and the arbitrary choice explanation quoting directly from Cardone & Hindley and from Scott. (I actually found another talk where Scott discusses this, so I linked to both.) I removed the citation to Barendregt (1997) because he does not give any sources and his version of the story has discrepancies with the version in Cardone & Hindley (note though that Barendregt's essay is still linked in "Further Reading"). I also removed the citation to "Mathematical Methods in Linguistics" because it seems to be completely spurious. Noamz (talk) 14:31, 27 May 2019 (UTC)

Undecidability of equivalence

This section explains that the equivalence of two expressions in the lambda calculus is undecidable, though it doesn't cite any references. Which references should be cited here? Jarble (talk) 16:15, 3 June 2019 (UTC)

I added a reference to the original proof by Church (1936). Noamz (talk) 10:58, 6 June 2019 (UTC)

Inductive definition of lambda terms unclear

Hello, how can operators or constants be brought in by application of these three rules? Are these supposed to be covered by the first rule? If so, the word "variable" is misleading to me.Stefan84556 (talk) 01:00, 27 July 2020 (UTC)

I understand that this comment is old, but if you're referring to the introduction section, then I think it means that for certain applications (e.g. to analyse a particular programming language or to analyse a particular logical proof), one may extend the rules and syntax to include additional constants and operators. It doesn't mean that the syntax and rules stated allows one to create arbitrary constants and operators. AhoChan (talk) 10:31, 23 November 2020 (UTC)

Confusingly written example

For example, $\lambda x.((\lambda x.x)x)$ and $(\lambda x.(\lambda x.x))x$ denote different terms (although they coincidentally reduce to the same value).

There are too many different uses of $x$ for these expressions to be reasonably understood. It's used as the argument for the outer and inner lambdas and, in the second expression, a useless free variable. Something like $\lambda x.((\lambda y.2x+y)z)$ and $(\lambda x.(\lambda y.2x+y))z$, which reduce to $\lambda x.2x+z$ and $\lambda y.2z+y$ respectively, would be much less confusing. (It may be impossible to make lambda calculus easy to understand, but we can at least not actively make it more difficult.) Nloveladyallen (talk) 22:33, 2 March 2021 (UTC)

someone lost in space started a lambda calculus wikibook; can someone start to turn this article into a wikibook

A search directed me to a lambda calculus wikibook. There was only a very wrong short intro with concepts borrowed from some not very formal lisp book. I wrote something with the purpose make it clear that many of what was written was wrong because the lambda calculus is important as a foundation of computing theory. Unfortunately I have no time to work on that enterprise. Maybe this article could be copied in wikibooks to be transform it in a lambda calculus book. I did not check if there were previous attempts to write such wikibook. --User:2806:106e:b:31b1:3a5f:db9e:42bd:b4bd 00:51, 15 August 2022 (UTC)

Intro

From the talk page, it seems like there have been efforts in the past to turn this article into something that is actually helpful as an introduction to the subject that were overriden in favor of the previous unhelpful versions.

This is just a reminder that the current introduction is circular nonsense that only makes sense if a reader is already fully aware of what all of the terms and syntax mean. It should absolutely be rewritten for normal humans, at maximum to a high school reading level. You can get into the circular terminology deeper in the article but the lead, at least, should simply express the general concepts in a way that can be understood by complete neophytes. — LlywelynII 00:59, 21 October 2022 (UTC)

When attempting to answer the good faith question below, I saw that Simply typed lambda calculus#Syntax has the gist of what I was trying to say. --Ancheta Wis   (talk | contribs) 15:09, 23 November 2022 (UTC)

Computer science

What is a capture? 2402:3A80:1A42:12E8:0:0:4141:250E (talk) 07:26, 23 November 2022 (UTC)

When a variable x is highlighted in a lambda expression (λ x.B), and B is completely general, then x can be freely chosen (i.e. free to mean anything you like in B). x can be renamed to anything else. But if B contains a + sign, or other operator such as parenthesis, then x is no longer free. In that case x has been bound by some mathematical operator (e.g. captured by a + sign, or other operator) which constrains the meaning of the expression B: a + sign in expression B constrains those subexpressions with x. See SECD_machine#Landin's_contribution for avoiding variable capture. --Ancheta Wis   (talk | contribs) 14:47, 23 November 2022 (UTC)

Lambda terms - error in definition?

According to the definition in the Lambda calculus#Lambda terms subsection, $\lambda x.x^{2}+2$ is not a lambda term, since x^2+2 is not a lambda term. It seems to me that we should add that x+y and x*y are also lambda terms, if x and y are. Dan Gluck (talk) Dan Gluck (talk) 16:44, 7 January 2023 (UTC)

See Introduction in Stanford Encyclopedia of Philosophy's entry on Lambda calculus, which uses much the same expression as $x^{2}+2$ and yet claims that expression to be a lambda term.

It may be helpful to use the beta reduction rules, but being mindful that blind substitution doesn't overwrite a bound variable. --Ancheta Wis   (talk | contribs) 20:56, 7 January 2023 (UTC)

Adding some references

• Maraist, John; Odersky, Martin; Turner, David N.; Wadler, Philip (1 January 1995). Call-by-name, Call-by-value, Call-by-need, and the Linear Lambda Calculus (PDF). Vol. 1. pp. 370–392. doi:10.1016/S1571-0661(04)00022-2. ISSN 1571-0661. Retrieved 3 April 2023. {{cite book}}: |journal= ignored (help)
• Ariola, Zena M.; Maraist, John; Odersky, Martin; Felleisen, Matthias; Wadler, Philip (1995). "A call-by-need lambda calculus". Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '95. ACM Press: 233–246. doi:10.1145/199448.199507. Retrieved 3 April 2023.
• Ariola, Zena M.; Felleisen, Matthias (May 1997). "The call-by-need lambda calculus". Journal of Functional Programming. 7 (3): 265–301. doi:10.1017/S0956796897002724. ISSN 1469-7653. Retrieved 3 April 2023.
• Maraist, John; Odersky, Martin; Wadler, Philip (May 1998). "The call-by-need lambda calculus" (PDF). Journal of Functional Programming. 8 (3): 275–317. doi:10.1017/S0956796898003037. ISSN 1469-7653. Retrieved 3 April 2023.
• Chang, Stephen; Felleisen, Matthias (2012). The Call-by-Need Lambda Calculus, Revisited (PDF). Springer. pp. 128–147. arXiv:1201.3907. doi:10.1007/978-3-642-28869-2_7. ISBN 978-3-642-28869-2. Retrieved 3 April 2023.
• Sabel, David; Schmidt-Schauß, Manfred (2016). "A Call-by-Need Lambda Calculus with Scoped Work Decorations". Software Engineering (PDF). S2CID 8139555. Retrieved 3 April 2023.

Anas1712 (talk) 16:56, 3 April 2023 (UTC)

I suggest adding them to Lazy evaluation (target of call-by-need) or maybe expanding the discussion I wrote in Reduction_strategy#Call_by_need_reduction. This article is quite big already and there's not really a good place for it. Mathnerd314159 (talk) 20:41, 11 May 2023 (UTC)

Turner's citation

Let's talk about what is missing in the statement. --Ancheta Wis   (talk | contribs) 16:24, 11 May 2023 (UTC)

I added what I think is the quote being referred to:

This mechanism works well for Algol 60 but in a language in which functions can be returned as results, a free variable might be held onto after the function call in which it was created has returned, and will no longer be present on the stack. Landin (1964) solved this in his SECD machine.

I think the basic issue is that what the article says,

In a functional programming language where functions are first class citizens, this systematic change in variables to avoid capture of a free variable can introduce an error, when returning functions as results.

does not follow from this. It is not capture-avoiding substitution that causes issues, it is the fact that a function partially applied to an argument can outlive its containing function. It's true that the Algol 60 mechanism used capture-avoiding substitution, but every functional programming language avoids unwanted captures in some way. Mathnerd314159 (talk) 20:30, 11 May 2023 (UTC)

And Turner 2012, immediately after his Landin 1964 ref says "Landin (1964) solved this in his SECD machine. A function is represented by a closure, consisting of code for the function plus the environment for its free variables. The environment is a linked list of name-value pairs. Closures live in the heap".

So the function definition (i.e. the lambda abstraction on x where ${\textstyle (\lambda x.M)}$ , has to be augmented by its closure [x, as well as environment y,z   ...] which Turner puts on a heap; ie. in lambda notation we need ${\textstyle (\lambda xyz.}$   $...M)$, in order not to overrun a function call, say application ${\textstyle M}$   $N$. Otherwise we get an indication that the expression evaluation has not yet terminated, and machine application ${\textstyle M}$   $N$ slows. My mental picture is the sequence of twin primes, the output getting slower and slower with each application to successive twins, as the list of divisors y,z,w,   ... (the closures) grow without bound.) -- Ancheta Wis   (talk | contribs) 05:18, 12 May 2023 (UTC)

WillNess is pointing out that there is a problem with the scope of parameters used in intertwining functions (when expressing functions in lambda notation). The problem reminds me of the slogan 'no global variables'.

There must be a way to resolve this, otherwise why use this notation? --Ancheta Wis   (talk | contribs) 22:17, 12 May 2023 (UTC)

I believe something's gone awry. Turner 2012 does not say that capture avoiding substitution introduces errors. The error he is talking about is the Funarg problem, which doesn't require capture-avoiding substitution to occur. He is saying that capture avoiding substitution is one of the basic mechanisms for correct functional programming (it allows passing functions as arguments), but is not enough (the funarg problem means you can't always return functions). The funarg problem has no chance of occurring in the lambda calculus because there is no concept of a stack or other kind of evaluation context; there is never a need to "look up" a variable while evaluating an expression. I have removed the whole statement as I believe it to be irrelevant to the section (if not incorrect or confusing) and will make a similar edits to SECD machine. Howtonotwin (talk) 09:39, 8 January 2024 (UTC)

Parentheses

@WillNess, please refer to (Selinger 2008) for his explanation of the scope of parentheses. Basically Selinger is trying to minimize the use of parentheses, but that does not mean that lambda calculus has no notion of scope, because Selinger is talking about the outermost level of parentheses. --Ancheta Wis   (talk | contribs) 22:04, 12 May 2023 (UTC)

Also, might you please participate in the discussion above ( 05:18, 12 May 2023 ), about D A Turner's ref to Landin's use of closures? If the article needs updating, we need more voices/suggestions. --Ancheta Wis   (talk | contribs) 22:04, 12 May 2023 (UTC)

I apologize that it took me some time to get here. I'm reading through the responses now. WillNess (talk) 10:24, 21 May 2023 (UTC)

typo in a sentence

One reason there are many different typed lambda calculi has been the desire to do more (of what the untyped calculus can do) without giving up on being able to prove strong theorems about the calculus.

should be

what the typed calculus can do Federicolo (talk) 19:08, 2 October 2023 (UTC)

No, this is right, the untyped lambda calculus is more powerful. For example, one can easily write the Y combinator in untyped lambda calculus, whereas many typed lambda calculi (such as the simply typed lambda calculus) do not allow it. Mathnerd314159 (talk) 01:41, 3 October 2023 (UTC)

Ok I agree with you now: I misinterpreted the sentence Federicolo (talk) 16:14, 13 October 2023 (UTC)

"Functions that operate on functions" feels incomplete

The section "Functions that operate on functions" contains a discussion on the identity and constant functions, but fails to use them to illustrate the point of the section - functions being used as input or output. VeeIsMe (talk) 15:55, 4 November 2023 (UTC)

 Done I added function composition. The whole section is a mess; I tried to clean up a little bit. - Jochen Burghardt (talk) 09:44, 5 November 2023 (UTC)

"Intuitively this means a function's arguments are always reduced before the function itself."

That sentence is supposed to be describing applicative order. I think it is confusing and unnecessary. For starters, a beta reduction is always applied to a redex. What exactly is an "argument" here? If, in that sentence, argument refers to the right side of a redex, then that sentence is false (that interpretation would fit call by value, not applicative order). And if it refers to bound variables, then the sentence is still false, because bound variables are not redexes. I think the most charitable interpretation of the sentence is that given a redex R, before R is reduced, one must reduce every redex U, if U's right side is a bound variable of R's function. Unfortunately, despite that new sentence's verbosity, it is not a complete definition of applicative order reduction. 81.158.160.194 (talk) 04:14, 29 March 2024 (UTC)

An argument is the right hand side of an application (this is defined in the lead and mentioned in numerous places). E.g. in M N, M is the function and N is the argument. So what this "intuition" is trying to explain is that for example with A = B = C = λx.x, applicative order will reduce A(BC) to A(C) rather than BC.

The complete definition of applicative order is "leftmost-innermost reduction", it is already pretty concise. Mathnerd314159 (talk) 05:16, 29 March 2024 (UTC)