Editing Lambda calculus (section)

== Reduction strategies ==
{{Further|Reduction strategy#Lambda calculus}}
Whether a term is normalising or not, and how much work needs to be done in normalising it if it is, depends to a large extent on the reduction strategy used. Common lambda calculus reduction strategies include:<ref>{{cite book |last1=Pierce |first1=Benjamin C. |author1-link=Benjamin C. Pierce |title=Types and Programming Languages |year=2002 |publisher=[[MIT Press]] |isbn=0-262-16209-1 |page=56|url=https://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA56}}</ref><ref>{{cite book |last1=Sestoft |first1=Peter |title=The Essence of Computation |chapter=Demonstrating Lambda Calculus Reduction |series=Lecture Notes in Computer Science |date=2002 |volume=2566 |pages=420–435 |doi=10.1007/3-540-36377-7_19 |isbn=978-3-540-00326-7 |chapter-url=http://itu.dk/people/sestoft/papers/sestoft-lamreduce.pdf |access-date=22 August 2022}}</ref><ref>{{cite journal |last1=Biernacka |first1=Małgorzata |last2=Charatonik |first2=Witold |last3=Drab |first3=Tomasz |editor1-last=Andronick |editor1-first=June |editor2-last=de Moura |editor2-first=Leonardo |title=The Zoo of Lambda-Calculus Reduction Strategies, and Coq |journal=13th International Conference on Interactive Theorem Proving (ITP 2022) |date=2022 |volume=237 |pages=7:1–7:19 |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |doi=10.4230/LIPIcs.ITP.2022.7 |doi-access=free |url=https://drops.dagstuhl.de/opus/volltexte/2022/16716/pdf/LIPIcs-ITP-2022-7.pdf |access-date=22 August 2022}}</ref>
; Normal order: The leftmost outermost redex is reduced first. That is, whenever possible, arguments are substituted into the body of an abstraction before the arguments are reduced. If a term has a beta-normal form, normal order reduction will always reach that normal form.
; Applicative order: The leftmost innermost redex is reduced first. As a consequence, a function's arguments are always reduced before they are substituted into the function. Unlike normal order reduction, applicative order reduction may fail to find the beta-normal form of an expression, even if such a normal form exists. For example, the term <math>( \; \lambda x.y \;\; (\lambda z. (z z) \; \lambda z. (z z)) \; )</math> is reduced to itself by applicative order, while normal order reduces it to its beta-normal form <math>y</math>.
; Full β-reductions: Any redex can be reduced at any time. This means essentially the lack of any particular reduction strategy—with regard to reducibility, "all bets are off".

Weak reduction strategies do not reduce under lambda abstractions:
; Call by value{{anchor|callByValue}}: Like applicative order, but no reductions are performed inside abstractions. This is similar to the evaluation order of strict languages like C: the arguments to a function are evaluated before calling the function, and function bodies are not even partially evaluated until the arguments are substituted in.
; Call by name: Like normal order, but no reductions are performed inside abstractions. For example, {{Mono|λ''x''.(λ''y''.''y'')''x''}} is in normal form according to this strategy, although it contains the redex {{Mono|(λ''y''.''y'')''x''}}.

Strategies with sharing reduce computations that are "the same" in parallel:
; Optimal reduction: As normal order, but computations that have the same label are reduced simultaneously.
; Call by need: As call by name (hence weak), but function applications that would duplicate terms instead name the argument. The argument may be evaluated "when needed", at which point the name binding is updated with the reduced value. This can save time compared to normal order evaluation.