Editing Lambda calculus (section)

== Explanation and applications ==
Lambda calculus is [[Turing completeness|Turing complete]], that is, it is a universal [[model of computation]] that can be used to simulate any [[Turing machine]].<ref>{{cite journal|first1=Alan M.|last1=Turing|author1-link=Alan Turing|title=Computability and λ-Definability|jstor=2268280|journal=The Journal of Symbolic Logic|volume=2|issue=4|date=December 1937|pages=153–163|doi=10.2307/2268280|s2cid=2317046}}</ref> Its namesake, the Greek letter lambda (λ), is used in lambda expressions and lambda terms to denote [[Free variables and bound variables|binding]] a variable in a [[Function (mathematics)|function]].

{{anchor|untyped lambda calculus}}{{anchor|untypedLambdaCalculus}}Lambda calculus may be ''untyped'' or ''typed''. In typed lambda calculus, functions can be applied only if they are capable of accepting the given input's "type" of data. Typed lambda calculi are strictly ''weaker'' than the untyped lambda calculus, which is the primary subject of this article, in the sense that ''typed lambda calculi can express less'' than the untyped calculus can. On the other hand, typed lambda calculi allow more things to be proven. For example, in [[simply typed lambda calculus]], it is a theorem that every evaluation strategy terminates for every simply typed lambda-term, whereas evaluation of untyped lambda-terms need not terminate (see [[#betaReducIsAcomput|below]]). 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.

Lambda calculus has applications in many different areas in [[mathematics]], [[philosophy]],<ref>{{cite web|first1=Thierry|last1=Coquand|author1-link=Thierry Coquand|title=Type Theory|website=The Stanford Encyclopedia of Philosophy|date=8 February 2006|url=http://plato.stanford.edu/archives/sum2013/entries/type-theory/|editor1-first=Edward N.|editor1-last=Zalta|edition=Summer 2013|access-date=November 17, 2020}}</ref> [[linguistics]],<ref>{{cite book|url=https://books.google.com/books?id=9CdFE9X_FCoC|title=Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus|first1=Michael|last1=Moortgat|publisher=Foris Publications|year=1988|isbn=9789067653879}}</ref><ref>{{Cite book|url=https://books.google.com/books?id=nyFa5ngYThMC|title=Computing Meaning|editor1-last=Bunt|editor1-first=Harry|editor2-last=Muskens|editor2-first=Reinhard|year=2008|publisher=Springer|isbn=978-1-4020-5957-5}}</ref> and [[computer science]].<ref>{{cite book|title=Concepts in Programming Languages|first1=John C.|last1=Mitchell|author1-link=John C. Mitchell|publisher=Cambridge University Press|year=2003|isbn=978-0-521-78098-8|page=57|url=https://books.google.com/books?id=7Uh8XGfJbEIC&pg=PA57}}.</ref><ref>{{cite tech report |last1=Chacón Sartori |first1=Camilo |date=2023-12-05 |title=Introduction to Lambda Calculus using Racket |url=https://www.researchgate.net/publication/376232150 |archive-url=https://web.archive.org/web/20231207230752/https://www.researchgate.net/publication/376232150_Introduction_to_Lambda_Calculus_using_Racket |archive-date=2023-12-07}}</ref> Lambda calculus has played an important role in the development of the [[Programming language theory|theory]] of [[programming language]]s. [[Functional programming]] languages implement lambda calculus. Lambda calculus is also a current research topic in [[category theory]].<ref>{{cite book |last1=Pierce |first1=Benjamin C. |author1-link=Benjamin C. Pierce |title=Basic Category Theory for Computer Scientists |page=53}}</ref>