<p>I think $\lambda$-calculus has contributed in many ways to this field, and still contributes to it. Three examples follow, and this is not exhaustive. Since I am not a specialist in $\lambda$-calculus, I certainly miss some important points.</p>

<ul>
<li><p>First, I think having different models of computation that turn out to represent the exact same set of functions was at the origin of the <a href="https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis">Church-Turing thesis</a>, and $\lambda$-calculus played a major role, alongside with Turing machines and $\mu$-recursive functions.</p></li>
<li><p>Second, regarding functional programming language, I do not understand as a <em>not valid contribution</em>: Basically, all our models of computations were invented <em>long before</em> anything happened in Computer Science! Thus $\lambda$-calculus brought another view of computation, in some sense orthogonal to Turing machines, that is very fruitful in the field of programming languages (which is part of the field of theory of computation).</p></li>
<li><p>Finally, and as a more specific example, I think of Implicit Computational Complexity which aims at characterizing complexity classes by means of dedicated languages. The first results such as <em>Bellantoni-Cook's Theorem</em> were stated in terms of $\mu$-recursive functions, but more recent results use the vocabulary and techniques of $\lambda$-calculus. See this <a href="http://link.springer.com/chapter/10.1007/978-3-642-31485-8_3">Short introduction to Implicit Computational Complexity</a> for more and pointers, or the proceedings of the <a href="http://perso.ens-lyon.fr/patrick.baillot/DICE/">DICE workshops</a>.</p></li>
</ul>

CC BY-SA 3.0
2014-03-24T08:38:35.160Z
2014-03-24T08:38:35.160Z
Bruno
<p>Apart from the foundational role of the $\lambda$-calculus, which was mentioned in all other answers, I would like to add something on</p>

<blockquote>
  <p>What exactly did the lambda calculus do to advance the theory of CS?</p>
</blockquote>

<p>I believe that <strong>concurrency theory</strong> is one field of CS which has been tremendously influenced by the compositional view mentioned by Martin Berger.  Of course, the $\lambda$-calculus itself is not a concurrent language, but its "algebraic spirit" permeates the definition and development of modern <a href="http://en.wikipedia.org/wiki/Process_calculus" rel="noreferrer">process calculi</a>.  I think it is fair to say that process algebras are descendants of the $\lambda$-calculus more than they are of automata and Turing machines and, in general, concurrency theory wouldn't be what it is today without the import of the $\lambda$-calculus.</p>

<p>Besides concurrency, I am happy to see <strong>implicit computational complexity</strong> (ICC) mentioned in one of the answers (it is a field in which I am personally involved).  However, it must be said that, so far, ICC has no use in CS theory outside of programming languages and, in a very limited way, software verification.  This is just an example of a more general situation: the modular, compositional, highly structured view of computation underlying the $\lambda$-calculus and predominant in "Theory B" seems to bring little insight into the deep problems of interest in "Theory A".  Why this is so is, for me, an interesting and at the same time frustrating subject of reflection.  (See <a href="https://cstheory.stackexchange.com/questions/944/solid-applications-of-category-theory-in-tcs">this question</a> for a related discussion).</p>

<p>(As a side note, let me mention that, thanks to its deep connections with proof theory (Curry-Howard), the $\lambda$-calculus has interesting applications also outside of CS "proper", in particular in set theory.  I am especially alluding to recent work on classical realizability, a research program developed from the early 2000s onward by <a href="http://www.pps.univ-paris-diderot.fr/~krivine/" rel="noreferrer">Jean-Louis Krivine</a> (and several other people now, such as Alexandre Miquel, the lectures found on his <a href="http://perso.ens-lyon.fr/alexandre.miquel/" rel="noreferrer">web page</a> are an excellent introduction to the subject).  From the model-theoretic standpoint, classical realizability may be seen as a "non-commutative" generalization of Cohen's forcing, yielding models of set theory impossible to obtain with forcing).</p>

CC BY-SA 3.0
2014-03-24T12:57:23.673Z
Good point about concurrency theory: the development of types for interacting systems, pursued mostly by K. Honda and his coworkers, is, to a substantial part, about rephrasing types for $\lambda$-calculi as types for interactive systems. The key bridge that makes this all work is Milner's [Functions as processes](http://hal.inria.fr/inria-00075405/en/), giving a translation from $\lambda$ to $\pi$. This lead to a reverse technology transfer already: most Hoare logics for ML-like programming languages were born as logics for typed $\pi$-fragments, and then pushed back via Milner's encoding.
Martin Berger
CC BY-SA 3.0
2014-03-24T16:28:00.663Z
If I could clone myself, I would make a duplicate to look into P/NP using BLL and realizability. Logical relations seem to not be "natural proofs", the linear type discipline ensure you cannot relativize, and BLL's polytime completeness theorems seem to let you avoid worrying about whether or not there are classes of algorithms you've missed. The relationship between linearity and representation theory suggest connections to GCT, too. I suppose all this is why you are tantalized and frustrated, though. :)
Neel Krishnaswami
CC BY-SA 3.0
2014-03-24T16:52:58.043Z
Hey @NeelKrishnaswami could you please point me towards reading material that relates BLL (bounded linear logic) and natural proofs?
Martin Berger
CC BY-SA 3.0
2014-03-24T18:32:59.157Z
Re B vs. A: lambda-calculus is only about structuring the same computations better, but can't, for instance, produce better algorithms. By cut-elimination and the subformula property on the result, any program with a first-order type can be written without first-class functions. But cut-elimination corresponds to duplicating code: so we find again that you don't need higher-order functions if you are willing to do enough copy-pasting.
(Reynolds's defunctionalization allows you to avoid even the copy-pasting, but is a global transformation, so it's better left to a compiler).
Blaisorblade
CC BY-SA 3.0
2014-03-24T18:38:11.627Z
Anecdotally speaking, my comment is motivated by programming with an algorithmist — he's great, but he does seem to abstract much less than I find desirable. I don't claim that's general, but I claim that abstraction in the code is often not needed/emphasized when writing algorithms. (Consider how many quicksort implementations inline the partition function — I find that inacceptable).
Blaisorblade
CC BY-SA 3.0
2014-03-24T11:33:44.530Z
2014-06-09T08:56:53.223Z
2017-04-13T12:32:28.053Z
Damiano Mazza
<p>Your questions can be approached from many sides. I'd like to leave the historical and philosophical aspects on the side and address your main question, which I take to be this:</p>

<blockquote>
  <p>What's the point of lambda calculus? Why go through all these functions/reductions?</p>
</blockquote>

<p>What is the point of Boolean Algebra, or Relational Algebra, or First-Order Logic, or Type Theory, or some other mathematical formalism/theory? The answer is that they have no <em>inherent</em> purpose to them, even if their designers created them for some purpose or another. Leibniz, when erecting the foundations of Boolean Algebra, had a certain philosophical <a href="http://en.wikipedia.org/wiki/Characteristica_universalis">project</a> in mind; Boole studied it for his own reasons. de Morgan's work on Relational Algebra also was motivated by various projects of his; Peirce and Frege had their own motivations for creating modern logic.</p>

<p>The point is: whatever reason Church may have had when creating lambda calculus, the point of lambda calculus varies from one practitioner to another. </p>

<ul>
<li><p>To someone it's a convenient <em>notation</em> for talking about computations; an alternative to Turing Machines, and so on. </p></li>
<li><p>To another it's a solid <em>mathematical basis</em> on which to build a more sophisticated programming language (e.g. McCarthy, Stanley).</p></li>
<li><p>To a third person it's a <em>rigorous tool</em> for giving the semantics of natural as well as programming languages (e.g. Montague, Fitch, Kratzer).</p></li>
</ul>

<p>I think Lambda calculus is a formal language that is worth studying for its own sake. You can learn the fact that in untyped lambda calculus we have these little beasts called 'Y-combinators', and how they help us define recursive functions and make the proof of undecidability so elegant and simple. You can learn the amazing fact that there is an intimate <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">correspondence</a> between <a href="http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus">simply typed lambda calculus</a> and a type of <a href="http://en.wikipedia.org/wiki/Intuitionistic_logic">intuitionistic logic</a>. There are many other interesting topics to explore (e.g. how should we give the <a href="http://en.wikipedia.org/wiki/Lambda_calculus#Semantics">semantics</a> of lambda calculus? how can we turn lambda calculus into a deductive system like FOL?) </p>

<hr>

<p>Check out Hindley &amp; Seldin's <a href="http://rads.stackoverflow.com/amzn/click/0521898854"><em>Introduction to Combinators and &lambda;&ndash;Calculus</em></a> for an introduction. Barendregt's <a href="http://rads.stackoverflow.com/amzn/click/0444875085"><em>The Lambda Calculus</em></a> is the bible, so if you're hooked after Hindley &amp; Seldin, there are lots of topics of both semantical and syntactical nature in there to explore.</p>

CC BY-SA 3.0
2014-03-23T21:16:28.237Z
I am not buying this "for its own sake" argument. The point of a mathematical formalism is to elucidate our understanding of some concept. What is elucidated may develop over time, but unless a formalism helps us think more clearly about some idea, it usually dies out. In that sense it's valid to aks how does lambda calculus elucidate the concept of computation in a way that is not subsumed by TMs.
Sasho Nikolov
CC BY-SA 3.0
2014-03-23T21:32:18.563Z
I think one *can* study lambda calculus without ever thinking of reduction and substitution as computation. If I'm right and that is in fact possible, then we can have interest in lambda calculus even if we're not interested in computation at all. But thanks for your comment; I'll try to edit my answer accordingly as soon as I get a chance.
Hunan Rostomyan
CC BY-SA 4.0
2019-06-26T07:36:07.367Z
@GabrielL. If you read the entire sentence, it says "how does lambda calculus *elucidate* the concept of computation in a way that is not subsumed by TMs". Two mathematical definitions that are formally equivalent may still elucidate the same underlying concept in different and complementary ways. My comment meant that it's reasonable to ask what clarity is gained by expressing computability in terms of lambda calculus, rather than in terms of TMs. This is not at all about formal equivalence.
Sasho Nikolov
CC BY-SA 4.0
2019-06-26T20:31:29.643Z
Got it – managed to miss the key word there somehow. Thanks for the reply.
Gabriel L.
CC BY-SA 4.0
2019-06-25T18:23:48.177Z
@SashoNikolov — "in a way that is not subsumed by TMs." By definition, that is impossible, as LC and TMs are equivalent. Anything you can express or prove with one, you can with the other (and vice-versa). So they make each other redundant (as they both do with general recursive theory, yet another TM-equivalent formalism). Does that mean we should throw out all TM-equivalent systems but TM itself? I wouldn't say so, since sometimes things are *easier* to express in LC than TM or vice-versa. It's just another way of talking about computability.
Gabriel L.
CC BY-SA 3.0
2014-03-23T20:12:19.147Z
2014-03-23T20:12:19.147Z
Hunan Rostomyan
<p>Turing argued that Mathematics can be reduced to a combination of reading/writing symbols, chosen from a finite set, and switching between a finite number of mental 'states'. He reified this in his Turing Machines, where symbols are recorded in cells on a tape and an automaton keeps track of the state.</p>

<p>However, Turing's machines are not a constructive proof of this reduction. He argued that any 'effective procedure' can be implemented by some Turing Machine, and showed that a Universal Turing Machine can implement all of those other machines, but he didn't actually give a set of symbols, states and update rules which implement Mathematics in the way that he argued. In other words, he did not propose a 'standard Turing Machine', with a standard set of symbol which we can use to write down our Mathematics.</p>

<p>Lambda Calculus, on the other hand, is precisely that. Church was specifically trying to unify the notations used to write down our Mathematics. Once it was shown that LC and TMs are equivalent, we could use LC as our 'standard Turing Machine' and everyone would be able to read our programs (well, in theory ;) ).</p>

<p>Now, we could ask why treat LC as a primitive, rather than as a TM dialect? The answer is that LC's semantics are <em>denotational</em>: LC terms have 'intrinsic' meaning. There are Church numerals, there are functions for addition, multiplication, recursion, etc. This makes LC very well aligned with how (formal) Mathematics is practiced, which is why many (functional) algorithms are still presented directly in LC.</p>

<p>On the other hand, the semantics of TM programs are <em>operational</em>: the meaning is defined as the behaviour of the machine. In this sense, we can't cut out some section of tape and say "this is addition", because it is context-dependent. The machine's behaviour, when it hits that section of tape, depends on the machine's state, the lengths/offsets/etc. of the arguments, how much tape will be used for the result, whether any previous operation has corrupted that section of tape, etc. This is a horrendous way of working ("Nobody wants to program a Turing Machine"), which is why so many (imperative) algorithms are presented as pseudocode.</p>

CC BY-SA 3.0
2014-04-01T09:42:42.090Z
2014-04-01T09:42:42.090Z
Warbo
<p>other answers are good, here is one additional angle/reason for consideration that meshes with others yet might be even more definitive, nevertheless may be harder to keep clearly in mind as the old origins are lost somewhat in the sands of time:</p>

<p><em><strong>historical precedence!</em></strong></p>

<p><a href="http://en.wikipedia.org/wiki/Lambda_calculus" rel="noreferrer">Lambda calculus</a> was introduced <em>at least</em> as early as <strong>1932</strong> in the following ref:</p>

<ul>
<li>A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).</li>
</ul>

<p>the <a href="http://en.wikipedia.org/wiki/Turing_machine" rel="noreferrer">Turing Machine</a> was introduced in <strong>~1936</strong>, so Lambda Calculus predates the appearance of the TM by several years!</p>

<ul>
<li>Turing, A.M. (1936). "On Computable Numbers, with an Application to the Entscheidungs problem". Proceedings of the London Mathematical Society. 2 (1937) 42: 230–265. <a href="http://dx.doi.org/10.1112%2Fplms%2Fs2-42.1.230" rel="noreferrer">doi:10.1112/plms/s2-42.1.230</a></li>
</ul>

<p>so in other words a basic answer is that Lambda Calculus is in many ways the ultimate <em>legacy system</em> of TCS. its still around in much the same way that <a href="http://en.wikipedia.org/wiki/Cobol" rel="noreferrer">Cobol</a> is even though not as much new development goes on in the language! it appears to be the earliest <a href="http://en.wikipedia.org/wiki/Turing_complete" rel="noreferrer">Turing Complete computation system</a> introduced and even predates the fundamental idea of Turing Completeness. it was only later retrospective analysis that showed that Lambda Calculus, Turing machines, and the Post Correspondence Problem were equivalent and introduced the concept of Turing equivalence and the <a href="http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis" rel="noreferrer">Church-Turing thesis</a>.</p>

<p>Lambda calculus is simply the way to study computation from a <a href="http://en.wikipedia.org/wiki/Logic" rel="noreferrer"><em>logic-centric</em></a> pov more in terms of representing it as math theorems &amp; logical formula derivations etcetera. it also shows the deep relationship between computing and <a href="http://en.wikipedia.org/wiki/Recursion" rel="noreferrer">recursion</a> and the further tight coupling with <a href="http://en.wikipedia.org/wiki/Mathematical_induction" rel="noreferrer">mathematical induction</a>.</p>

<p>this is a somewhat remarkable factoid because it suggests that in many ways the (at least <em>theoretical</em>) origins of computing were fundamentally in <em>logic/mathematics</em>, a thesis advanced/expanded in detail by Davis in his book <a href="http://rads.stackoverflow.com/amzn/click/0393322297" rel="noreferrer">Engines of Logic/Mathematicians and the origins of the computer</a>. (of course the origins &amp; fundamental role of <a href="http://en.wikipedia.org/wiki/Boolean_algebra" rel="noreferrer">Boolean algebra</a> also further reinforce that conceptual historical framework.)</p>

<p>hence, dramatically, one might even say Lambda calculus is a bit like a <em>pedagogical time machine</em> for exploring the origins of computing!</p>

CC BY-SA 3.0
2014-03-25T01:48:21.977Z
addendum, Lambda calculus also seems to have been highly influenced by [Principia mathematica](http://en.wikipedia.org/wiki/Principia_Mathematica) by Whitehead/Russell which also was a major inspiration for [Godels thm](http://en.wikipedia.org/wiki/Godels_theorem). some of this research was also inspired by [Hilberts 10th problem](http://en.wikipedia.org/wiki/Hilberts_tenth_problem) at turn of century which asked for an _algorithmic solution_ before _"algorithm"_ was precisely (mathematically) defined, and in fact that quest is largely what lead to the later precise technical definition.
vzn
CC BY-SA 3.0
2014-03-25T15:46:23.340Z
btw/clarification/iiuc it was actually [Post canonical systems](http://en.wikipedia.org/wiki/Post_canonical_system) that were studied 1st by Post and apparently the simpler [Post Correspondence Problem](http://en.wikipedia.org/wiki/Post_correspondence_problem) is a special case. also it was Kleene who was instrumental in developing the concept of Turing completeness (not nec under that name) by helping prove all 3 major systems interchangeable/equivalent (TM, Lambda Calculus, Post canonical system).
vzn
CC BY-SA 3.0
2014-03-25T15:47:17.113Z
see also [History of the Church-Turing thesis](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis) wikipedia that traces many historical details/interrelations
vzn
CC BY-SA 3.0
2014-03-27T01:24:26.217Z
I'm having a hard time not being offended at the Cobol comparison.
Neil Toronto
CC BY-SA 3.0
2014-03-24T21:59:47.623Z
2014-03-24T22:23:14.903Z
2014-03-24T22:23:14.903Z
vzn
<p>I have just come across this post and despite my post being rather late in the day (year!), I thought that perhaps my "penny's worth" may be of some use. </p>

<p>Whilst studying the subject at university, I had a similar thought on the matter; so, I posed the question of "why" to the lecturer and the response was: "compilers". As soon as she mentioned it, the power behind reduction and the art of assessing how best to manipulate it suddenly made the whole purpose of why it was and still is a potentially useful tool.</p>

<p>Well, that so to speak was my "aha" moment.</p>

<p>In my opinion, we often consider high level languages, patterns, automata, algorithm-complexity etc. useful because we can relate them to the 'task' at hand; whereas lamdba calculus seems a bit too abstract. However, there are still those out there who work with languages at a low level - and I imagine lambda calculus, object calculus and other related formalisations have helped them to understand and perhaps develop new theories and technologies from which the average programmer can then benefit. Indeed, it is probably not a core module for that reason, but (for the reasons I have stated) there will be the odd few - other than academics - who may find it integral to their chosen career path in computing.</p>

CC BY-SA 3.0
2014-12-19T08:51:38.590Z
What was the "aha" on *compilers*?
PhD
CC BY-SA 3.0
2014-12-19T09:27:23.637Z
Your last paragraph seems entirely speculative and you never actually explain why the one word "compilers" answers the question.
David Richerby
CC BY-SA 3.0
2015-01-08T13:16:09.350Z
@PhD: Beta-reduction & substitution aren't used when running programs, but are used inside optimizing compilers. That's not *the* main importance of lambda-calculus, but it's a very concrete application.
Blaisorblade
CC BY-SA 3.0
2014-12-19T02:19:45.817Z
2014-12-19T02:19:45.817Z
user30412
<p>$\lambda$-calculus has two key roles.</p>

<ul>
<li><p>It is a simple mathematical foundation of sequential, functional, higher-order
computational behaviour.</p></li>
<li><p>It is a representation of proofs in   constructive
logic.</p></li>
</ul>

<p>This is also known as the <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="noreferrer">Curry-Howard correspondence</a>.  Jointly,
the dual view of $\lambda$-calculus as proof and as (sequential,
functional, higher-order) programming language, strengthened by the algebraic feel
of $\lambda$-calculus (which is not shared by Turing machines), has lead
to massive technology transfer  between logic, the foundations of mathematics, and programming.
This transfer is still ongoing, for example in <a href="http://homotopytypetheory.org" rel="noreferrer">homotopy type theory</a>.  In
particular the development of programming languages in general, and
typing disciplines in particular, is inconceivable without
$\lambda$-calculus. Most programming languages owe some degree of debt to
Lisp and ML (e.g. garbage collection was invented for Lisp), which are direct descendants of the $\lambda$-calculus. A
second strand of work strongly influenced by $\lambda$-calculus are
<a href="http://en.wikipedia.org/wiki/Proof_assistant%E2%80%8E" rel="noreferrer">interactive proof assistants</a>.</p>

<p>Does one have to know $\lambda$-calculus to be a competent programmer, or
even a theoretician of computer science?    No. If you are not interested
in types, verification and programming languages with higher-order
features, then it's probably a model of computation that's not
terribly useful for you. In particular, if you are interested in complexity theory, then
$\lambda$-calculus is probably not an ideal model because the basic
reduction step $$(\lambda x.M) N \rightarrow_{\beta} M[N/x]$$ is powerful: it can make an arbitrary number of copies on $N$, so
$\rightarrow_{\beta}$ is an unrealistic basic notion in accounting for
the microscopic cost of computation. I think this is the main reason why
Theory A is not so enamoured of $\lambda$-calculus. Conversely, Turing machines are not terribly inspirational for programming language development, because there are no natural notions of machine composition, whereas with $\lambda$-calculus, if $M$ and $N$ are programs, then so is $MN$. This algebraic view of computation relates naturally to programming languages used in practice, and much language development can be understood as the search for, and investigation of novel program composition operators.</p>

<p>For an encyclopedic overview of the history of $\lambda$-calculus see <a href="http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf" rel="noreferrer">History of Lambda-calculus and Combinatory Logic by Cardone and Hindley</a>.</p>

CC BY-SA 3.0
2014-03-24T05:41:32.127Z
This is a very nice answer.
Suresh Venkat
CC BY-SA 3.0
2014-03-24T11:42:44.170Z
Concerning the "unrealism" of $\beta$-reduction: Beniamino Accattoli and Ugo Dal Lago recently proved a [surprising result](https://sites.google.com/site/beniaminoaccattoli/beta-invariance.pdf?attredirects=0) stating that the number of $\beta$-steps to normal form in any standard reduction strategy (e.g., leftmost-outermost) is an invariant complexity measure. This means that, even if implementing $\beta$-reduction *per se* is expensive, counting the number of reductions is not an unrealistic complexity measure (for instance, it would not affect the definition of the class $\mathsf P$).
Damiano Mazza
CC BY-SA 3.0
2014-03-24T13:02:31.937Z
@DamianoMazza Since it's a new result, it could not have been influential in the history of Theory A. In addition, I think this resuld holds only for some notions of reduction. IIRC Asperti's paper [P = NP, up to sharing](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=484032BD603CAD977553C0849FA5D40E?doi=10.1.1.52.1414&rep=rep1&type=pdf) shows that P and NP collapse if you have an 'optimal' reduction strategy in the sense of J.-J. Levy.
Martin Berger
CC BY-SA 3.0
2014-03-24T16:15:38.760Z
@MartinBerger: yes of course. My comment was meant to add information on the complexity of $\beta$-reduction, not at all to "correct" your statement about the lack of influence on Theory A (which I repeated in my answer).  By the way, Accattoli and Dal Lago's result holds for usual, leftmost-outermost $\beta$-reduction (*cf.* p.2, c.2, l.11 of their paper). That's why it's so interesting (and worth mentioning). Asperti's result concerns, as you say, Lévy-optimal reduction, which is not a $\beta$-reduction strategy (in particular, leftmost-outermost is not Lévy-optimal).
Damiano Mazza
CC BY-SA 3.0
2014-03-23T20:25:54.653Z
2017-06-14T14:19:41.317Z
2017-06-14T14:19:41.317Z
Martin Berger
<p>I'm just reading up on lambda calculus to "get to know it". I see it as an alternate form of computation as opposed to the Turing Machine. It's an interesting way of doing things with functions/reductions (crudely speaking). Some questions keep nagging at me though: </p>

<ul>
<li>What's the point of lambda calculus? Why go through all these functions/reductions? What is the purpose?</li>
<li>As a result I'm left to wonder: What exactly did lambda calculus do to advance the theory of CS? What were it's contributions that would allow me to have an "aha" moment of understanding the need for its existence?</li>
<li>Why is lambda calculus not covered in texts on automata theory? The common route is to go through various automata, grammars, Turing Machines and complexity classes. Lambda calculus is only included in the syllabus for SICP style courses (perhaps not?). But I've rarely seen it be a part of the core curriculum of CS. Does this imply it's not all that valuable? Maybe not and I maybe missing something here?</li>
</ul>

<p>I'm aware that functional programming languages are based on lambda calculus but I'm not considering that as a valid contribution, since it was created much before we had programming languages. So, really what is the point of knowing/understanding lambda calculus, w.r.t. its applications/contributions to theory?</p>

CC BY-SA 3.0
2014-03-24T07:29:47.840Z
A related set of answers explain the difference in power between the $\lambda$-calculus and TMs: http://cstheory.stackexchange.com/questions/1117/realizability-theory-difference-in-power-between-lambda-calculus-and-turing-mac
Suresh Venkat
CC BY-SA 3.0
2014-03-24T08:45:56.947Z
Maybe the discussion of [Historical reasons for adoption of Turing Machine as primary model of computation](https://cstheory.stackexchange.com/questions/3650/historical-reasons-for-adoption-of-turing-machine-as-primary-model-of-computatio/3680#3680) is of interest, too.
Martin Berger
CC BY-SA 3.0
2014-03-24T10:21:31.783Z
In a way, its contribution was to **create** the field. Don't forget that Church came up with lambda calculus first, but it wasn't at first seen as a universal model of computation.
Dan Hulme
CC BY-SA 3.0
2014-03-25T12:50:04.150Z
In my core studies I had `Functional Programming` which discussed Haskell and a little bit of Lisp.  The successor to that was `Principles of Programming Languages`, which used ML and introduced lambda calculus.  As some answers show, that's really where lambda calculus belongs: in a class about programming languages, typing, etc.
Shaz
CC BY-SA 3.0
2014-03-25T15:14:01.530Z
this question is similar [relationship between TMs & Lambda calculus](http://cstheory.stackexchange.com/questions/625/relationship-between-turing-machine-and-lambda-calculus) & also discusses Lambda calculus historical precedence
vzn
<soft-question><big-picture><lambda-calculus><ho.history-overview>
What is the contribution of lambda calculus to the field of theory of computation?
PhD
# What is the contribution of lambda calculus to the field of theory of computation?

(Asked by: username_0 on 2014-03-23)

I'm just reading up on lambda calculus to "get to know it". I see it as an alternate form of computation as opposed to the Turing Machine. It's an interesting way of doing things with functions/reductions (crudely speaking). Some questions keep nagging at me though:

* What's the point of lambda calculus? Why go through all these functions/reductions? What is the purpose?
* As a result I'm left to wonder: What exactly did lambda calculus do to advance the theory of CS? What were it's contributions that would allow me to have an "aha" moment of understanding the need for its existence?
* Why is lambda calculus not covered in texts on automata theory? The common route is to go through various automata, grammars, Turing Machines and complexity classes. Lambda calculus is only included in the syllabus for SICP style courses (perhaps not?). But I've rarely seen it be a part of the core curriculum of CS. Does this imply it's not all that valuable? Maybe not and I maybe missing something here?

I'm aware that functional programming languages are based on lambda calculus but I'm not considering that as a valid contribution, since it was created much before we had programming languages. So, really what is the point of knowing/understanding lambda calculus, w.r.t. its applications/contributions to theory?

**Tags:** soft-question, big-picture, lambda-calculus, ho.history-overview
> **Comments:**
> **username_1**: A related set of answers explain the difference in power between the $\lambda$-calculus and TMs: http://cstheory.stackexchange.com/questions/1117/realizability-theory-difference-in-power-between-lambda-calculus-and-turing-mac  
> **username_2**: Maybe the discussion of [Historical reasons for adoption of Turing Machine as primary model of computation](https://cstheory.stackexchange.com/questions/3650/historical-reasons-for-adoption-of-turing-machine-as-primary-model-of-computatio/3680#3680) is of interest, too.  
> **username_3**: In a way, its contribution was to **create** the field. Don't forget that Church came up with lambda calculus first, but it wasn't at first seen as a universal model of computation.  
> **username_4**: In my core studies I had `Functional Programming` which discussed Haskell and a little bit of Lisp.  The successor to that was `Principles of Programming Languages`, which used ML and introduced lambda calculus.  As some answers show, that's really where lambda calculus belongs: in a class about programming languages, typing, etc.  
> **username_5**: this question is similar [relationship between TMs & Lambda calculus](http://cstheory.stackexchange.com/questions/625/relationship-between-turing-machine-and-lambda-calculus) & also discusses Lambda calculus historical precedence  

---

## 7 answers

### Answer by username_2 on 2014-03-23. Score: 105 | Accepted answer

$\lambda$-calculus has two key roles.

* It is a simple mathematical foundation of sequential, functional, higher-order
  computational behaviour.
* It is a representation of proofs in constructive
  logic.

This is also known as the [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence). Jointly,
the dual view of $\lambda$-calculus as proof and as (sequential,
functional, higher-order) programming language, strengthened by the algebraic feel
of $\lambda$-calculus (which is not shared by Turing machines), has lead
to massive technology transfer between logic, the foundations of mathematics, and programming.
This transfer is still ongoing, for example in [homotopy type theory](http://homotopytypetheory.org). In
particular the development of programming languages in general, and
typing disciplines in particular, is inconceivable without
$\lambda$-calculus. Most programming languages owe some degree of debt to
Lisp and ML (e.g. garbage collection was invented for Lisp), which are direct descendants of the $\lambda$-calculus. A
second strand of work strongly influenced by $\lambda$-calculus are
[interactive proof assistants](http://en.wikipedia.org/wiki/Proof_assistant%E2%80%8E).

Does one have to know $\lambda$-calculus to be a competent programmer, or
even a theoretician of computer science? No. If you are not interested
in types, verification and programming languages with higher-order
features, then it's probably a model of computation that's not
terribly useful for you. In particular, if you are interested in complexity theory, then
$\lambda$-calculus is probably not an ideal model because the basic
reduction step $$(\lambda x.M) N \rightarrow\_{\beta} M[N/x]$$ is powerful: it can make an arbitrary number of copies on $N$, so
$\rightarrow\_{\beta}$ is an unrealistic basic notion in accounting for
the microscopic cost of computation. I think this is the main reason why
Theory A is not so enamoured of $\lambda$-calculus. Conversely, Turing machines are not terribly inspirational for programming language development, because there are no natural notions of machine composition, whereas with $\lambda$-calculus, if $M$ and $N$ are programs, then so is $MN$. This algebraic view of computation relates naturally to programming languages used in practice, and much language development can be understood as the search for, and investigation of novel program composition operators.

For an encyclopedic overview of the history of $\lambda$-calculus see [History of Lambda-calculus and Combinatory Logic by Cardone and Hindley](http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf).

> **Comments:**
> **username_1**: This is a very nice answer.  
> **username_7**: Concerning the "unrealism" of $\beta$-reduction: Beniamino Accattoli and Ugo Dal Lago recently proved a [surprising result](https://sites.google.com/site/beniaminoaccattoli/beta-invariance.pdf?attredirects=0) stating that the number of $\beta$-steps to normal form in any standard reduction strategy (e.g., leftmost-outermost) is an invariant complexity measure. This means that, even if implementing $\beta$-reduction *per se* is expensive, counting the number of reductions is not an unrealistic complexity measure (for instance, it would not affect the definition of the class $\mathsf P$).  
> **username_2**: @DamianoMazza Since it's a new result, it could not have been influential in the history of Theory A. In addition, I think this resuld holds only for some notions of reduction. IIRC Asperti's paper [P = NP, up to sharing](http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=484032BD603CAD977553C0849FA5D40E?doi=10.1.1.52.1414&rep=rep1&type=pdf) shows that P and NP collapse if you have an 'optimal' reduction strategy in the sense of J.-J. Levy.  
> **username_7**: @MartinBerger: yes of course. My comment was meant to add information on the complexity of $\beta$-reduction, not at all to "correct" your statement about the lack of influence on Theory A (which I repeated in my answer).  By the way, Accattoli and Dal Lago's result holds for usual, leftmost-outermost $\beta$-reduction (*cf.* p.2, c.2, l.11 of their paper). That's why it's so interesting (and worth mentioning). Asperti's result concerns, as you say, Lévy-optimal reduction, which is not a $\beta$-reduction strategy (in particular, leftmost-outermost is not Lévy-optimal).  

---

### Answer by username_6 on 2014-03-24. Score: 29

I think $\lambda$-calculus has contributed in many ways to this field, and still contributes to it. Three examples follow, and this is not exhaustive. Since I am not a specialist in $\lambda$-calculus, I certainly miss some important points.

* First, I think having different models of computation that turn out to represent the exact same set of functions was at the origin of the [Church-Turing thesis](https://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis), and $\lambda$-calculus played a major role, alongside with Turing machines and $\mu$-recursive functions.
* Second, regarding functional programming language, I do not understand as a *not valid contribution*: Basically, all our models of computations were invented *long before* anything happened in Computer Science! Thus $\lambda$-calculus brought another view of computation, in some sense orthogonal to Turing machines, that is very fruitful in the field of programming languages (which is part of the field of theory of computation).
* Finally, and as a more specific example, I think of Implicit Computational Complexity which aims at characterizing complexity classes by means of dedicated languages. The first results such as *Bellantoni-Cook's Theorem* were stated in terms of $\mu$-recursive functions, but more recent results use the vocabulary and techniques of $\lambda$-calculus. See this [Short introduction to Implicit Computational Complexity](http://link.springer.com/chapter/10.1007/978-3-642-31485-8_3) for more and pointers, or the proceedings of the [DICE workshops](http://perso.ens-lyon.fr/patrick.baillot/DICE/).


---

### Answer by username_7 on 2014-03-24. Score: 22

Apart from the foundational role of the $\lambda$-calculus, which was mentioned in all other answers, I would like to add something on

> What exactly did the lambda calculus do to advance the theory of CS?

I believe that **concurrency theory** is one field of CS which has been tremendously influenced by the compositional view mentioned by Martin Berger. Of course, the $\lambda$-calculus itself is not a concurrent language, but its "algebraic spirit" permeates the definition and development of modern [process calculi](http://en.wikipedia.org/wiki/Process_calculus). I think it is fair to say that process algebras are descendants of the $\lambda$-calculus more than they are of automata and Turing machines and, in general, concurrency theory wouldn't be what it is today without the import of the $\lambda$-calculus.

Besides concurrency, I am happy to see **implicit computational complexity** (ICC) mentioned in one of the answers (it is a field in which I am personally involved). However, it must be said that, so far, ICC has no use in CS theory outside of programming languages and, in a very limited way, software verification. This is just an example of a more general situation: the modular, compositional, highly structured view of computation underlying the $\lambda$-calculus and predominant in "Theory B" seems to bring little insight into the deep problems of interest in "Theory A". Why this is so is, for me, an interesting and at the same time frustrating subject of reflection. (See [this question](https://cstheory.stackexchange.com/questions/944/solid-applications-of-category-theory-in-tcs) for a related discussion).

(As a side note, let me mention that, thanks to its deep connections with proof theory (Curry-Howard), the $\lambda$-calculus has interesting applications also outside of CS "proper", in particular in set theory. I am especially alluding to recent work on classical realizability, a research program developed from the early 2000s onward by [Jean-Louis Krivine](http://www.pps.univ-paris-diderot.fr/~krivine/) (and several other people now, such as Alexandre Miquel, the lectures found on his [web page](http://perso.ens-lyon.fr/alexandre.miquel/) are an excellent introduction to the subject). From the model-theoretic standpoint, classical realizability may be seen as a "non-commutative" generalization of Cohen's forcing, yielding models of set theory impossible to obtain with forcing).

> **Comments:**
> **username_2**: Good point about concurrency theory: the development of types for interacting systems, pursued mostly by K. Honda and his coworkers, is, to a substantial part, about rephrasing types for $\lambda$-calculi as types for interactive systems. The key bridge that makes this all work is Milner's [Functions as processes](http://hal.inria.fr/inria-00075405/en/), giving a translation from $\lambda$ to $\pi$. This lead to a reverse technology transfer already: most Hoare logics for ML-like programming languages were born as logics for typed $\pi$-fragments, and then pushed back via Milner's encoding.  
> **username_8**: If I could clone myself, I would make a duplicate to look into P/NP using BLL and realizability. Logical relations seem to not be "natural proofs", the linear type discipline ensure you cannot relativize, and BLL's polytime completeness theorems seem to let you avoid worrying about whether or not there are classes of algorithms you've missed. The relationship between linearity and representation theory suggest connections to GCT, too. I suppose all this is why you are tantalized and frustrated, though. :)  
> **username_2**: Hey @NeelKrishnaswami could you please point me towards reading material that relates BLL (bounded linear logic) and natural proofs?  
> **username_9**: Re B vs. A: lambda-calculus is only about structuring the same computations better, but can't, for instance, produce better algorithms. By cut-elimination and the subformula property on the result, any program with a first-order type can be written without first-class functions. But cut-elimination corresponds to duplicating code: so we find again that you don't need higher-order functions if you are willing to do enough copy-pasting. (Reynolds's defunctionalization allows you to avoid even the copy-pasting, but is a global transformation, so it's better left to a compiler).  
> **username_9**: Anecdotally speaking, my comment is motivated by programming with an algorithmist — he's great, but he does seem to abstract much less than I find desirable. I don't claim that's general, but I claim that abstraction in the code is often not needed/emphasized when writing algorithms. (Consider how many quicksort implementations inline the partition function — I find that inacceptable).  

---

### Answer by username_10 on 2014-03-23. Score: 14

Your questions can be approached from many sides. I'd like to leave the historical and philosophical aspects on the side and address your main question, which I take to be this:

> What's the point of lambda calculus? Why go through all these functions/reductions?

What is the point of Boolean Algebra, or Relational Algebra, or First-Order Logic, or Type Theory, or some other mathematical formalism/theory? The answer is that they have no *inherent* purpose to them, even if their designers created them for some purpose or another. Leibniz, when erecting the foundations of Boolean Algebra, had a certain philosophical [project](http://en.wikipedia.org/wiki/Characteristica_universalis) in mind; Boole studied it for his own reasons. de Morgan's work on Relational Algebra also was motivated by various projects of his; Peirce and Frege had their own motivations for creating modern logic.

The point is: whatever reason Church may have had when creating lambda calculus, the point of lambda calculus varies from one practitioner to another.

* To someone it's a convenient *notation* for talking about computations; an alternative to Turing Machines, and so on.
* To another it's a solid *mathematical basis* on which to build a more sophisticated programming language (e.g. McCarthy, Stanley).
* To a third person it's a *rigorous tool* for giving the semantics of natural as well as programming languages (e.g. Montague, Fitch, Kratzer).

I think Lambda calculus is a formal language that is worth studying for its own sake. You can learn the fact that in untyped lambda calculus we have these little beasts called 'Y-combinators', and how they help us define recursive functions and make the proof of undecidability so elegant and simple. You can learn the amazing fact that there is an intimate [correspondence](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) between [simply typed lambda calculus](http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus) and a type of [intuitionistic logic](http://en.wikipedia.org/wiki/Intuitionistic_logic). There are many other interesting topics to explore (e.g. how should we give the [semantics](http://en.wikipedia.org/wiki/Lambda_calculus#Semantics) of lambda calculus? how can we turn lambda calculus into a deductive system like FOL?)

---

Check out Hindley & Seldin's [*Introduction to Combinators and λ–Calculus*](http://rads.stackoverflow.com/amzn/click/0521898854) for an introduction. Barendregt's [*The Lambda Calculus*](http://rads.stackoverflow.com/amzn/click/0444875085) is the bible, so if you're hooked after Hindley & Seldin, there are lots of topics of both semantical and syntactical nature in there to explore.

> **Comments:**
> **username_11**: I am not buying this "for its own sake" argument. The point of a mathematical formalism is to elucidate our understanding of some concept. What is elucidated may develop over time, but unless a formalism helps us think more clearly about some idea, it usually dies out. In that sense it's valid to aks how does lambda calculus elucidate the concept of computation in a way that is not subsumed by TMs.  
> **username_10**: I think one *can* study lambda calculus without ever thinking of reduction and substitution as computation. If I'm right and that is in fact possible, then we can have interest in lambda calculus even if we're not interested in computation at all. But thanks for your comment; I'll try to edit my answer accordingly as soon as I get a chance.  
> **username_12**: @SashoNikolov — "in a way that is not subsumed by TMs." By definition, that is impossible, as LC and TMs are equivalent. Anything you can express or prove with one, you can with the other (and vice-versa). So they make each other redundant (as they both do with general recursive theory, yet another TM-equivalent formalism). Does that mean we should throw out all TM-equivalent systems but TM itself? I wouldn't say so, since sometimes things are *easier* to express in LC than TM or vice-versa. It's just another way of talking about computability.  
> **username_11**: @GabrielL. If you read the entire sentence, it says "how does lambda calculus *elucidate* the concept of computation in a way that is not subsumed by TMs". Two mathematical definitions that are formally equivalent may still elucidate the same underlying concept in different and complementary ways. My comment meant that it's reasonable to ask what clarity is gained by expressing computability in terms of lambda calculus, rather than in terms of TMs. This is not at all about formal equivalence.  
> **username_12**: Got it – managed to miss the key word there somehow. Thanks for the reply.  

---

### Answer by username_13 on 2014-04-01. Score: 12

Turing argued that Mathematics can be reduced to a combination of reading/writing symbols, chosen from a finite set, and switching between a finite number of mental 'states'. He reified this in his Turing Machines, where symbols are recorded in cells on a tape and an automaton keeps track of the state.

However, Turing's machines are not a constructive proof of this reduction. He argued that any 'effective procedure' can be implemented by some Turing Machine, and showed that a Universal Turing Machine can implement all of those other machines, but he didn't actually give a set of symbols, states and update rules which implement Mathematics in the way that he argued. In other words, he did not propose a 'standard Turing Machine', with a standard set of symbol which we can use to write down our Mathematics.

Lambda Calculus, on the other hand, is precisely that. Church was specifically trying to unify the notations used to write down our Mathematics. Once it was shown that LC and TMs are equivalent, we could use LC as our 'standard Turing Machine' and everyone would be able to read our programs (well, in theory ;) ).

Now, we could ask why treat LC as a primitive, rather than as a TM dialect? The answer is that LC's semantics are *denotational*: LC terms have 'intrinsic' meaning. There are Church numerals, there are functions for addition, multiplication, recursion, etc. This makes LC very well aligned with how (formal) Mathematics is practiced, which is why many (functional) algorithms are still presented directly in LC.

On the other hand, the semantics of TM programs are *operational*: the meaning is defined as the behaviour of the machine. In this sense, we can't cut out some section of tape and say "this is addition", because it is context-dependent. The machine's behaviour, when it hits that section of tape, depends on the machine's state, the lengths/offsets/etc. of the arguments, how much tape will be used for the result, whether any previous operation has corrupted that section of tape, etc. This is a horrendous way of working ("Nobody wants to program a Turing Machine"), which is why so many (imperative) algorithms are presented as pseudocode.


---

### Answer by username_5 on 2014-03-24. Score: 6

other answers are good, here is one additional angle/reason for consideration that meshes with others yet might be even more definitive, nevertheless may be harder to keep clearly in mind as the old origins are lost somewhat in the sands of time:

***historical precedence!***

[Lambda calculus](http://en.wikipedia.org/wiki/Lambda_calculus) was introduced *at least* as early as **1932** in the following ref:

* A. Church, "A set of postulates for the foundation of logic", Annals of Mathematics, Series 2, 33:346–366 (1932).

the [Turing Machine](http://en.wikipedia.org/wiki/Turing_machine) was introduced in **~1936**, so Lambda Calculus predates the appearance of the TM by several years!

* Turing, A.M. (1936). "On Computable Numbers, with an Application to the Entscheidungs problem". Proceedings of the London Mathematical Society. 2 (1937) 42: 230–265. [doi:10.1112/plms/s2-42.1.230](http://dx.doi.org/10.1112%2Fplms%2Fs2-42.1.230)

so in other words a basic answer is that Lambda Calculus is in many ways the ultimate *legacy system* of TCS. its still around in much the same way that [Cobol](http://en.wikipedia.org/wiki/Cobol) is even though not as much new development goes on in the language! it appears to be the earliest [Turing Complete computation system](http://en.wikipedia.org/wiki/Turing_complete) introduced and even predates the fundamental idea of Turing Completeness. it was only later retrospective analysis that showed that Lambda Calculus, Turing machines, and the Post Correspondence Problem were equivalent and introduced the concept of Turing equivalence and the [Church-Turing thesis](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis).

Lambda calculus is simply the way to study computation from a [*logic-centric*](http://en.wikipedia.org/wiki/Logic) pov more in terms of representing it as math theorems & logical formula derivations etcetera. it also shows the deep relationship between computing and [recursion](http://en.wikipedia.org/wiki/Recursion) and the further tight coupling with [mathematical induction](http://en.wikipedia.org/wiki/Mathematical_induction).

this is a somewhat remarkable factoid because it suggests that in many ways the (at least *theoretical*) origins of computing were fundamentally in *logic/mathematics*, a thesis advanced/expanded in detail by Davis in his book [Engines of Logic/Mathematicians and the origins of the computer](http://rads.stackoverflow.com/amzn/click/0393322297). (of course the origins & fundamental role of [Boolean algebra](http://en.wikipedia.org/wiki/Boolean_algebra) also further reinforce that conceptual historical framework.)

hence, dramatically, one might even say Lambda calculus is a bit like a *pedagogical time machine* for exploring the origins of computing!

> **Comments:**
> **username_5**: addendum, Lambda calculus also seems to have been highly influenced by [Principia mathematica](http://en.wikipedia.org/wiki/Principia_Mathematica) by Whitehead/Russell which also was a major inspiration for [Godels thm](http://en.wikipedia.org/wiki/Godels_theorem). some of this research was also inspired by [Hilberts 10th problem](http://en.wikipedia.org/wiki/Hilberts_tenth_problem) at turn of century which asked for an _algorithmic solution_ before _"algorithm"_ was precisely (mathematically) defined, and in fact that quest is largely what lead to the later precise technical definition.  
> **username_5**: btw/clarification/iiuc it was actually [Post canonical systems](http://en.wikipedia.org/wiki/Post_canonical_system) that were studied 1st by Post and apparently the simpler [Post Correspondence Problem](http://en.wikipedia.org/wiki/Post_correspondence_problem) is a special case. also it was Kleene who was instrumental in developing the concept of Turing completeness (not nec under that name) by helping prove all 3 major systems interchangeable/equivalent (TM, Lambda Calculus, Post canonical system).  
> **username_5**: see also [History of the Church-Turing thesis](http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis) wikipedia that traces many historical details/interrelations  
> **username_14**: I'm having a hard time not being offended at the Cobol comparison.  

---

### Answer by username_15 on 2014-12-19. Score: -2

I have just come across this post and despite my post being rather late in the day (year!), I thought that perhaps my "penny's worth" may be of some use.

Whilst studying the subject at university, I had a similar thought on the matter; so, I posed the question of "why" to the lecturer and the response was: "compilers". As soon as she mentioned it, the power behind reduction and the art of assessing how best to manipulate it suddenly made the whole purpose of why it was and still is a potentially useful tool.

Well, that so to speak was my "aha" moment.

In my opinion, we often consider high level languages, patterns, automata, algorithm-complexity etc. useful because we can relate them to the 'task' at hand; whereas lamdba calculus seems a bit too abstract. However, there are still those out there who work with languages at a low level - and I imagine lambda calculus, object calculus and other related formalisations have helped them to understand and perhaps develop new theories and technologies from which the average programmer can then benefit. Indeed, it is probably not a core module for that reason, but (for the reasons I have stated) there will be the odd few - other than academics - who may find it integral to their chosen career path in computing.

> **Comments:**
> **username_0**: What was the "aha" on *compilers*?  
> **username_16**: Your last paragraph seems entirely speculative and you never actually explain why the one word "compilers" answers the question.  
> **username_9**: @PhD: Beta-reduction & substitution aren't used when running programs, but are used inside optimizing compilers. That's not *the* main importance of lambda-calculus, but it's a very concrete application.  

---

