Editing Lambda calculus (section)

== Additional programming techniques ==
There is a considerable body of [[programming idiom]]s for lambda calculus. Many of these were originally developed in the context of using lambda calculus as a foundation for [[semantics (computer science)|programming language semantics]], effectively using lambda calculus as a [[low-level programming language]]. Because several programming languages include the lambda calculus (or something very similar) as a fragment, these techniques also see use in practical programming, but may then be perceived as obscure or foreign.

=== Named constants ===
In lambda calculus, a [[library (computing)|library]] would take the form of a collection of previously defined functions, which as lambda-terms are merely particular constants. The pure lambda calculus does not have a concept of named constants since all atomic lambda-terms are variables, but one can emulate having named constants by setting aside a variable as the name of the constant, using abstraction to bind that variable in the main body, and apply that abstraction to the intended definition. Thus to use {{Mono|''f''}} to mean ''N'' (some explicit lambda-term) in ''M'' (another lambda-term, the "main program"), one can say
: {{Mono|(λ''f''.}}''M''{{Mono|)}} ''N''
Authors often introduce [[syntactic sugar]], such as {{Mono|let}},{{efn|{{Mono|(λ''f''.}}''M''{{Mono|)}} ''N'' can be pronounced "let f be N in M".}} to permit writing the above in the more intuitive order
: {{Mono|1=let ''f'' =}} ''N'' {{Mono|in}} ''M''
By chaining such definitions, one can write a lambda calculus "program" as zero or more function definitions, followed by one lambda-term using those functions that constitutes the main body of the program.

A notable restriction of this {{Mono|let}} is that the name {{Mono|''f''}} may not be referenced in ''N'', for ''N'' is outside the scope of the abstraction binding {{Mono|''f''}}, which is ''M''; this means a recursive function definition cannot be written with {{Mono|let}}. The {{Mono|letrec}}{{efn|name=ariola|1= Ariola and Blom<ref name= AB94 /> employ 1) axioms for a representational calculus using ''well-formed cyclic lambda graphs'' extended with {{Mono|letrec}}, to detect possibly infinite unwinding trees; 2) the representational calculus with β-reduction of scoped lambda graphs constitute Ariola/Blom's cyclic extension of lambda calculus; 3) Ariola/Blom reason about strict languages using [[#callByValue|§ call-by-value]], and compare to Moggi's calculus, and to Hasegawa's calculus. Conclusions on p. 111.<ref name= AB94 >Zena M. Ariola and Stefan Blom, ''Proc. TACS '94'' Sendai, Japan 1997 [http://ix.cs.uoregon.edu/~ariola/cycles.pdf (1997) Cyclic lambda calculi] 114 pages.</ref>}} construction would allow writing recursive function definitions, where the scope of the abstraction binding {{Mono|''f''}} includes ''N'' as well as ''M''. Or self-application a-la that which leads to {{Mono|'''Y'''}} combinator could be used.

=== Recursion and fixed points ===
{{Further|Fixed-point combinator}}
{{See also|SKI combinator calculus#Self-application and recursion}}
[[Recursion]] is when a function invokes itself. What would a value be which were to represent such a function? It has to refer to itself somehow inside itself, just as the definition refers to itself inside itself. If this value were to contain itself by value, it would have to be of infinite size, which is impossible. Other notations, which support recursion natively, overcome this by referring to the function ''by name'' inside its definition. Lambda calculus cannot express this, since in it there simply are no names for terms to begin with, only arguments' names, i.e. parameters in abstractions. Thus, a lambda expression can receive itself as its argument and refer to (a copy of) itself via the corresponding parameter's name. This will work fine in case it was indeed called with itself as an argument. For example,  {{Mono|(λ''x''.''x'' ''x'') ''E'' {{=}} (''E E'')}} will express recursion when ''E'' is an abstraction which is applying its parameter to itself inside its body to express a recursive call. Since this parameter receives ''E'' as its value, its self-application will be the same {{Mono|(''E E'')}} again.

As a concrete example, consider the [[factorial]] function {{Mono|F(''n'')}}, recursively defined by

: {{Mono|1=F(''n'') = 1, if ''n'' = 0; else ''n'' × F(''n'' − 1)}}.

In the lambda expression which is to represent this function, a ''parameter'' (typically the first one) will be assumed to receive the lambda expression itself as its value, so that calling it with itself as its first argument will amount to the recursive call. Thus to achieve recursion, the intended-as-self-referencing argument (called {{Mono|''s''}} here, reminiscent of "self", or "self-applying") must always be passed to itself within the function body at a recursive call point:

: {{Mono|1=E := λ''s''. λ''n''.(1, if ''n'' = 0; else ''n'' × (''s'' ''s'' (''n''−1)))}}
::: with  {{Mono|1=''s s n'' = F ''n'' = E E ''n''}}  to hold, so  {{Mono|''s'' {{=}} E}}  and
: {{Mono|1=F := (λ''x''.''x'' ''x'') E = E E}}

and we have

: {{Mono|1=F = E E = λ''n''.(1, if ''n'' = 0; else ''n'' × (E E (''n''−1)))}}

Here {{Mono|''s s''}} becomes ''the same'' {{Mono| (E E)}} inside the result of the application {{Mono| (E E)}}, and using the same function for a call is the definition of what recursion is. The self-application achieves replication here, passing the function's lambda expression on to the next invocation as an argument value, making it available to be referenced there by the parameter name {{Mono|''s''}} to be called via the self-application {{Mono|''s'' ''s''}}, again and again as needed, each time ''re-creating'' the lambda-term {{Mono| F {{=}} E E}}. 

The application is an additional step just as the name lookup would be. It has the same delaying effect. Instead of having {{Mono| F}} inside itself as a whole ''up-front'', delaying its re-creation until the next call makes its existence possible by having two ''finite'' lambda-terms {{Mono| E}} inside it re-create it on the fly ''later'' as needed.

This self-applicational approach solves it, but requires re-writing each recursive call as a self-application. We would like to have a generic solution, without the need for any re-writes:

: {{Mono|1=G := λ''r''. λ''n''.(1, if ''n'' = 0; else ''n'' × (''r'' (''n''−1)))}}
::: with  {{Mono|1=''r'' ''x'' = F ''x'' = G ''r'' ''x''}}  to hold, so  {{Mono|1=''r'' = G ''r'' =: FIX G}}  and
: {{Mono|1=F := FIX G}}  where  {{Mono|1=FIX ''g'' = (''r'' where ''r'' = ''g'' ''r'') = ''g'' (FIX ''g'')}}
::: so that  {{Mono|1=FIX G = G (FIX G) = (λ''n''.(1, if ''n'' = 0; else ''n'' × ((FIX G) (''n''−1))))}}

Given a lambda term with first argument representing recursive call (e.g. {{Mono|G}} here), the ''fixed-point'' combinator {{Mono|FIX}} will return a self-replicating lambda expression representing the recursive function (here, {{Mono|F}}). The function does not need to be explicitly passed to itself at any point, for the self-replication is arranged in advance, when it is created, to be done each time it is called. Thus the original lambda expression {{Mono|(FIX G)}} is re-created inside itself, at call-point, achieving [[self-reference]].

In fact, there are many possible definitions for this {{Mono|FIX}} operator, the simplest of them being:

: {{anchor|Y}} {{Mono|1='''Y''' := λ''g''.(λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x''))}}

In the lambda calculus, {{Mono|'''Y''' ''g''}}  is a fixed-point of {{Mono|''g''}}, as it expands to:

: {{Mono|'''Y''' ''g''}}
: {{Mono|~> (λ''h''.(λ''x''.''h'' (''x'' ''x'')) (λ''x''.''h'' (''x'' ''x''))) ''g''}}
: {{Mono|~> (λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x''))}}
: {{Mono|~> ''g'' ((λ''x''.''g'' (''x'' ''x'')) (λ''x''.''g'' (''x'' ''x'')))}}
: {{Mono|<~ ''g'' ('''Y''' ''g'')}}

Now, to perform the recursive call to the factorial function for an argument ''n'', we would simply call {{Mono|('''Y''' G) ''n''}}. Given ''n'' = 4, for example, this gives:
{{smalldiv|1=
: {{Mono|('''Y''' G) 4}}
: {{Mono|~> G ('''Y''' G) 4}}
: {{Mono|1=~> (λ''r''.λ''n''.(1, if ''n'' = 0; else ''n'' × (''r'' (''n''−1)))) ('''Y''' G) 4}}
: {{Mono|1=~> (λ''n''.(1, if ''n'' = 0; else ''n'' × (('''Y''' G) (''n''−1)))) 4}}
: {{Mono|1=~> 1, if 4 = 0; else 4 × (('''Y''' G) (4−1))}}
: {{Mono|~> 4 × (G ('''Y''' G) (4−1))}}
: {{Mono|1=~> 4 × ((λ''n''.(1, if ''n'' = 0; else ''n'' × (('''Y''' G) (''n''−1)))) (4−1))}}
: {{Mono|1=~> 4 × (1, if 3 = 0; else 3 × (('''Y''' G) (3−1)))}}
: {{Mono|~> 4 × (3 × (G ('''Y''' G) (3−1)))}}
: {{Mono|1=~> 4 × (3 × ((λ''n''.(1, if ''n'' = 0; else ''n'' × (('''Y''' G) (''n''−1)))) (3−1)))}}
: {{Mono|1=~> 4 × (3 × (1, if 2 = 0; else 2 × (('''Y''' G) (2−1))))}}
: {{Mono|~> 4 × (3 × (2 × (G ('''Y''' G) (2−1))))}}
: {{Mono|1=~> 4 × (3 × (2 × ((λ''n''.(1, if ''n'' = 0; else ''n'' × (('''Y''' G) (''n''−1)))) (2−1))))}}
: {{Mono|1=~> 4 × (3 × (2 × (1, if 1 = 0; else 1 × (('''Y''' G) (1−1)))))}}
: {{Mono|~> 4 × (3 × (2 × (1 × (G ('''Y''' G) (1−1)))))}}
: {{Mono|1=~> 4 × (3 × (2 × (1 × ((λ''n''.(1, if ''n'' = 0; else ''n'' × (('''Y''' G) (''n''−1)))) (1−1)))))}}
: {{Mono|1=~> 4 × (3 × (2 × (1 × (1, if 0 = 0; else 0 × (('''Y''' G) (0−1))))))}}
: {{Mono|~> 4 × (3 × (2 × (1 × (1))))}}
: {{Mono|~> 24}}
}}
Every recursively defined function can be seen as a fixed point of some suitably defined higher order function (also known as functional) closing over the recursive call with an extra argument. Therefore, using {{Mono|'''Y'''}}, every recursive function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication, and comparison predicates of natural numbers, using recursion.

When [[Fixed-point combinator|Y combinator]] is coded directly in a [[strict programming language]], the applicative order of evaluation used in such languages will cause an attempt to fully expand the internal self-application <math>(x x)</math> prematurely, causing [[stack overflow]] or, in case of [[tail call optimization]], indefinite looping.<ref>{{cite web |last1=Bene |first1=Adam |title=Fixed-Point Combinators in JavaScript |url=https://blog.benestudio.co/fixed-point-combinators-in-javascript-c214c15ff2f6 |website=Bene Studio |publisher=Medium |access-date=2 August 2020 |language=en |date=17 August 2017}}</ref> A delayed variant of Y, the [[Z combinator]], can be used in such languages. It has the internal self-application hidden behind an extra abstraction through [[#η-conversion|eta-expansion]], as <math>(\lambda v.x x v)</math>, thus preventing its premature expansion:<ref>{{cite web |title=CS 6110 S17 Lecture 5. Recursion and Fixed-Point Combinators |url=https://www.cs.cornell.edu/courses/cs6110/2017sp/lectures/lec05.pdf |website=Cornell University |at=4.1 A CBV Fixed-Point Combinator}}</ref>
: <math>Z = \lambda f.(\lambda x.f (\lambda v.x x v)) \ (\lambda x.f (\lambda v.x x v))\ .</math>

=== Standard terms ===
Certain terms have commonly accepted names:<ref>{{cite web |last1=Ker |first1=Andrew D. |title=Lambda Calculus and Types |url=https://www.cs.ox.ac.uk/andrew.ker/docs/lambdacalculus-lecture-notes-ht2009.pdf#page=18|page=6 |access-date=14 January 2022}}</ref><ref>{{cite book |last1=Dezani-Ciancaglini |first1=Mariangiola |last2=Ghilezan |first2=Silvia |title=Rewriting and Typed Lambda Calculi |chapter=Preciseness of Subtyping on Intersection and Union Types |series=Lecture Notes in Computer Science |date=2014 |volume=8560 |page=196 |doi=10.1007/978-3-319-08918-8_14|hdl=2318/149874 |isbn=978-3-319-08917-1 |chapter-url=http://www.di.unito.it/~dezani/papers/dg14.pdf#page=3 |access-date=14 January 2022}}</ref><ref>{{cite journal |last1=Forster |first1=Yannick |last2=Smolka |first2=Gert |title=Call-by-Value Lambda Calculus as a Model of Computation in Coq |journal=Journal of Automated Reasoning |date=August 2019 |volume=63 |issue=2 |pages=393–413 |doi=10.1007/s10817-018-9484-2 |s2cid=53087112 |url=https://www.ps.uni-saarland.de/Publications/documents/ForsterSmolka_2018_Computability-JAR.pdf#page=4 |access-date=14 January 2022}}</ref>

: {{anchor|I}} {{Mono|1='''I''' := λ''x''.''x''}}
: {{anchor|S}} {{Mono|1='''S''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' (''y'' ''z'')}}
: {{anchor|K}} {{Mono|1='''K''' := λ''x''.λ''y''.''x''}}
: {{anchor|B}} {{Mono|1='''B''' := λ''x''.λ''y''.λ''z''.''x'' (''y'' ''z'')}}
: {{anchor|C}} {{Mono|1='''C''' := λ''x''.λ''y''.λ''z''.''x'' ''z'' ''y''}}
: {{anchor|W}} {{Mono|1='''W''' := λ''x''.λ''y''.''x'' ''y'' ''y''}}
: {{anchor|omega}} {{Mono|1='''ω''' or '''Δ''' or '''U''' := λ''x''.''x'' ''x''}}
: {{anchor|Omega}} {{Mono|1='''Ω''' := '''ω ω'''}}

{{Mono|'''I'''}} is the identity function. {{Mono|'''SK'''}} and {{Mono|'''BCKW'''}} form complete [[combinator calculus]] systems that can express any lambda term - see 
[[#Abstraction elimination|the next section]]. {{Mono|'''Ω'''}} is {{Mono|'''UU'''}}, the smallest term that has no normal form. {{Mono|'''YI'''}} is another such term.
{{Mono|'''Y'''}} is standard and defined [[#Y|above]], and can also be defined as {{Mono|'''Y'''{{=}}'''BU(CBU)'''}}, so that {{Mono|'''Y'''g{{=}}g('''Y'''g)}}. {{Mono|TRUE}} and {{Mono|FALSE}} defined [[#Logic and predicates|above]] are commonly abbreviated as {{Mono|'''T'''}} and {{Mono|'''F'''}}.

=== Abstraction elimination ===
{{Further|Combinatory logic#Completeness of the S-K basis}}
If ''N'' is a lambda-term without abstraction, but possibly containing named constants ([[combinatory logic|combinators]]), then there exists a lambda-term ''T''({{Mono|''x''}},''N'') which is equivalent to {{Mono|λ''x''.}}''N'' but lacks abstraction (except as part of the named constants, if these are considered non-atomic). This can also be viewed as anonymising variables, as ''T''({{Mono|''x''}},''N'') removes all occurrences of {{Mono|''x''}} from ''N'', while still allowing argument values to be substituted into the positions where ''N'' contains an {{Mono|''x''}}. The conversion function ''T'' can be defined by:
: ''T''({{Mono|''x''}}, {{Mono|''x''}}) := '''I'''
: ''T''({{Mono|''x''}}, ''N'') := '''K''' ''N'' if {{Mono|''x''}} is not free in ''N''.
: ''T''({{Mono|''x''}}, ''M'' ''N'') := '''S''' ''T''({{Mono|''x''}}, ''M'') ''T''({{Mono|''x''}}, ''N'')
In either case, a term of the form ''T''({{Mono|''x''}},''N'') ''P'' can reduce by having the initial combinator '''I''', '''K''', or '''S''' grab the argument ''P'', just like β-reduction of {{Mono|(λ''x''.}}''N''{{Mono|)}} ''P'' would do. '''I''' returns that argument. '''K''' throws the argument away, just like {{Mono|(λ''x''.}}''N''{{Mono|)}} would do if {{Mono|''x''}} has no free occurrence in ''N''. '''S''' passes the argument on to both subterms of the application, and then applies the result of the first to the result of the second.

The combinators '''B''' and '''C''' are similar to '''S''', but pass the argument on to only one subterm of an application ('''B''' to the "argument" subterm and '''C''' to the "function" subterm), thus saving a subsequent '''K''' if there is no occurrence of {{Mono|''x''}} in one subterm. In comparison to '''B''' and '''C''', the '''S''' combinator actually conflates two functionalities: rearranging arguments, and duplicating an argument so that it may be used in two places. The '''W''' combinator does only the latter, yielding the [[B, C, K, W system]] as an alternative to [[SKI combinator calculus]].