Editing Lambda calculus (section)

=== 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.