Editing Lambda calculus (section)

== Complexity ==
The notion of [[computational complexity theory|computational complexity]] for the lambda calculus is a bit tricky, because the cost of a β-reduction may vary depending on how it is implemented.<ref>{{cite book |last1=Frandsen |first1=Gudmund Skovbjerg |last2=Sturtivant |first2=Carl |title=Functional Programming Languages and Computer Architecture: 5th ACM Conference. Cambridge, MA, USA, August 26-30, 1991. Proceedings |chapter=What is an efficient implementation of the λ-calculus? |series=Lecture Notes in Computer Science |date=26 August 1991 |volume=523 |pages=289–312 |publisher=Springer-Verlag|doi=10.1007/3540543961_14 |isbn=9783540543961 |citeseerx=10.1.1.139.6913|contribution-url=https://scholar.archive.org/work/i7pfbnat3vdwfgalk5l6pkvbze}}</ref> 
To be precise, one must somehow find the location of all of the occurrences of the bound variable {{Mono|''V''}} in the expression {{Mono|''E''}}, implying a time cost, or one must keep track of the locations of free variables in some way, implying a space cost. A naïve search for the locations of {{Mono|''V''}} in {{Mono|''E''}} is [[Big O notation|''O''(''n'')]] in the length ''n'' of {{Mono|''E''}}. [[Director string]]s were an early approach that traded this time cost for a quadratic space usage.<ref>{{cite journal|first1=F.-R.|last1=Sinot|url=http://www.lsv.fr/Publis/PAPERS/PDF/sinot-jlc05.pdf|title=Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting|journal=Journal of Logic and Computation|volume=15|number=2|pages=201–218|year=2005|doi=10.1093/logcom/exi010}}</ref> More generally this has led to the study of systems that use [[explicit substitution]].

In 2014, it was shown that the number of β-reduction steps taken by normal order reduction to reduce a term is a ''reasonable'' time cost model, that is, the reduction can be simulated on a Turing machine in time polynomially proportional to the number of steps.<ref>{{cite book |last1=Accattoli |first1=Beniamino |last2=Dal Lago |first2=Ugo |title=Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |chapter=Beta reduction is invariant, indeed |date=14 July 2014 |pages=1–10 |doi=10.1145/2603088.2603105 |arxiv=1601.01233 |isbn=9781450328869 |s2cid=11485010}}</ref> This was a long-standing open problem, due to ''size explosion'', the existence of lambda terms which grow exponentially in size for each β-reduction. The result gets around this by working with a compact shared representation. The result makes clear that the amount of space needed to evaluate a lambda term is not proportional to the size of the term during reduction. It is not currently known what a good measure of space complexity would be.<ref name=Reasonable>{{cite journal |last1=Accattoli |first1=Beniamino |title=(In)Efficiency and Reasonable Cost Models |journal=Electronic Notes in Theoretical Computer Science |date=October 2018 |volume=338 |pages=23–43 |doi=10.1016/j.entcs.2018.10.003 |doi-access=free}}</ref>

An unreasonable model does not necessarily mean inefficient. [[Reduction strategy#Optimal reduction|Optimal reduction]] reduces all computations with the same label in one step, avoiding duplicated work, but the number of parallel β-reduction steps to reduce a given term to normal form is approximately linear in the size of the term. This is far too small to be a reasonable cost measure, as any Turing machine may be encoded in the lambda calculus in size linearly proportional to the size of the Turing machine. The true cost of reducing lambda terms is not due to β-reduction per se but rather the handling of the duplication of redexes during β-reduction.<ref name=Asperti>{{cite arXiv |last1=Asperti |first1=Andrea |title=About the efficient reduction of lambda terms |date=16 Jan 2017 |class=cs.LO |eprint=1701.04240v1}}</ref> It is not known if optimal reduction implementations are reasonable when measured with respect to a reasonable cost model such as the number of leftmost-outermost steps to normal form, but it has been shown for fragments of the lambda calculus that the optimal reduction algorithm is efficient and has at most a quadratic overhead compared to leftmost-outermost.<ref name=Reasonable/> In addition the BOHM prototype implementation of optimal reduction outperformed both [[Caml]] Light and Haskell on pure lambda terms.<ref name=Asperti/>