MENTAL vs. CHURCH'S LAMBDA CALCULUS

A theoretical model for functional expressions
"Most programming languages have their roots in the lambda calculus" (Peter Landin).

---

The Lambda Calculus, by Church
Fundamental concepts

The lambda calculus, created by the mathematician, logician and philosopher Alonzo Church in the 1930s, is a formal theoretical model for functional expressions, i.e., functions defined from other functions.

Lambda calculus functions are mathematical objects with the following characteristics:

• The functions are unnamed (anonymous).
  
  
• Functions can be arguments of other functions.
  
  
• The result of a function is another function.
  
  
• There is referential transparency: the meaning of a functional expression depends only on the meaning of the functional subexpressions.
  
  
• There is a clear difference between the definition of a function and its application (or evaluation):
  
  
  • The definition of a function consists of two parts. The first part specifies the names of the parameters. The second part specifies the body of the function.
    
    
  • In the application of a function, the parameters of the function are replaced by the values of the arguments.

This distinction becomes necessary, because for example the mathematical expression x+5 does not indicate whether it is a function of the variable x or a calculation with the value of x. This problem is solved by the so-called "lambda notation". In the case of a function of one variable, the notation is λx.f(x), where:

• The symbol λ indicates that it is the definition of a function.
  
  
• The variable x that appears after λ is the formal variable (or parameter).
  
  
• f(x) is an expression in which x (the body of the function) appears.

It is implemented by (λx.f(x))a = f(a) where a is the argument. For example: (λx.axb)3 = a3b

For two variables, the notation is:

• Function definition: λxy.f(x, y)
  
  
• Aplicación: (λxy.f(x, y))(a, b) = f(a, b)
  Example: (λxy.xyx)(3, 4) = 343

In general, for n variables, the notation is:

• Function definition: λx₁ ... x_n.f(x₁, ... , x_n)
  
  
• Aplicación: (λx₁ ... x_n.f(x₁, ... , x_n))(a₁, ... ,a_n) = f(a1, ... , a_n)

The definition of a function is reminiscent of a universally quantified expression, in which λ plays a role similar to ∀ (for all).

The variable names of functional expressions is irrelevant. This is why function variables are said to be dummy or dummy. For example, λxy.x+y and λuv.u+v are equivalent.


Bound and free variables

In a lambda expression, a variable x is bound or free, depending on whether it appears as a parameter or not, respectively, in the function definition. Examples:

1. In the functional expression (λx.xy), x is a bound variable and y is free.
   
   
2. In the functional expression (λxy.xyx), x and y are bound variables.

Variables as functions

The variables x, y, z,... are also considered functions or self-functions, i.e. they apply to themselves and return to themselves. In this sense, the expression f(x) is usually written fx for short, since it is considered to be the application of the function f to the function x. Analogously,

fxy = (fx)y
fxyz = ((fx)y)z (assumes associativity on the left side) ...

Therefore, a functional expression of n variables is usually written λx₁ ... x_n.fx₁...x_n.


Partial evaluation

For any lambda function of n variables, it is possible to define a "curry" version −name coming from the Haskell logic B. Curry− equivalent, in which the arguments are applied serially, one after the other. For example, the curry version of λxyz.xyz is λx.λy.λz.xyz. This process is called "currification". In both cases, the arguments must be specified in the same order and the result is the same, but the syntax is different:

• Normal version, with simultaneous or concurrent application of the arguments:
  
  (λxyz.xyz)abc = abc
  
  
• Curry version:
  
  (λx.λy.λz.xyz)abc
  
  This expression is always interpreted with associativity to the left and where the instantiated variables progressively disappear:
  
  ((((λx.λy.λz.xyz)a)b)c = ((((λy.λz.ayz)b)c = (λz.abz)c = abc

Therefore, in the lambda calculus, all functions of n parameters can be considered as an expression of single-parameter functions.


Substitution of variables for arguments

In the application of a function to some arguments, a substitution of each parameter by its corresponding argument is performed. To indicate this, the lambda calculus uses the notation [N/x]M, which indicates that in the expression M we want to substitute the variable x by the expression N. Examples:

[u/x]x = u
[u/x](x y) = (u y)
[(λx.x)/x]x = (λx.x)

If in M the variable x does not appear, then M remains unchanged: [N/x]M = M. For example, [u/x]y = y.

Evidently, by the very definition of function application, it follows that

(λx.M)N = [N/x]M

It is the so-called "reduction β", "conversion β" or "axiom β" of the lambda calculus.

If the expression N appears in M as a dummy variable, it can be assigned a new name before performing the substitution. For example:

[u/x](λu.x) = [u/x](λz.x) = λz.u

It is the so-called "α conversion" or "α axiom" and is realized by means of

λx.M = λz.[z/x]M (supposes z bound in M).

The "η conversion" expresses the idea that two functions f and g are equal if and only if they give the same result for all possible arguments. That is, fa = ga for every argument a. If x does not appear in the body of f nor that of g, then fx = gx.


Calculations as reductions

Calculations in the lambda calculus are successive reductions, applying at each step the conversion β, until the simplest possible form is reached. An expression that can be reduced is called a "redex" (reduction expression). A redex can contain other redexes. An expression that cannot be reduced (containing no redex) is said to be in "normal form".

The Church-Rosser theorem of the lambda calculus states that the result of a calculus does not depend on the order in which reductions (substitutions β) are applied, i.e., all possible sequences of reductions progress to the same final result, which is the same as that obtained when reductions are applied concurrently.


Examples of simple functions

• Identity (I): I := λx.x
  Example: (λx.x)a = a
  
  
• First (Prim): Prim := λxy.x
  Example: (λxy.x)ab = a
  
  
• Second (Seg): Seg := λxy.y Example: (λxy.y)ab = b
  
  
• Constant (K): K := λx.k Example: (λx.k)a = k
  
  
• Duplication (Dup): Dup := λx.xx Example: (λx.xx)a = aa

Higher order functions

If we have the expression of n variables λx₁ ... x_n.fx₁ ... x_n

• fx₁ ... x_n can be, in turn, a lambda expression.
• The variables x₁ ... x_n can also be lambda expressions.
• Arguments can be lambda expressions.

Then the higher-order functions appear.

A simple example is the composition of two functions is λgfx.g(fx). Which is equivalent to g○f in traditional mathematical notation (first apply f and then apply g). For example:

f := λx.xax   g := λx.bxb
(fg) = λx.xax(λx.bxb) = λx.bxbaλx.bxb
(fg)c = (λx.bxbaλx.bxb)c = bcbabcb
(gf) = λx.bxb(λx.xax) = bλx.xaxb
(gf)c = (bλx.xaxb)c = bcacb

Some laws of function composition are:

• Self-application of the function "identity" (I):
  (I I) = (λx.x)(λx.x) = λx.x = I
  
  
• Self-application of the "duplication" function (Dup):
  (Dup Dup) = (λx.xx)(λx. xx) = (λx.xx)(λx.xx) = (Dup Dup)
  (an infinite loop with the same result is produced)
  
  
• Self-application of the "second" function (Seg):
  (Seg) = (λxy.y)(λxy.y) = (λy.y) = I

Arithmetic

Substituting in λx.fx, x for fx, we have: λfx.f(fx)

This is the definition of a function that, acting on any function fx, produces the same function iterated twice, i.e., f(fx). This is the function identified with the symbol 2 (in bold, to differentiate it from the number 2).

2 = λfx.f(fx)

Analogously,

3 = λfx.f(f(fx))
4 = λfx.f(f(f(fx)))
...

Along with:

0 = λfx.x (function that always returns the variable x)

1 = λfx.fx (identity function: returns the same function)

In general, a number n in the lambda calculus is a function that has as argument another function f and produces as result the n-ary composition of f. These numbers are called "Church numerals". Examples:

(0)(xa) = x
(1)(xa) = xa
(2)(xa) = xaa
(3)(xa) = xaaa
...

A surprising aspect of Church's numerals is the possibility of defining the arithmetic operations of addition, multiplication, and power in terms of functions applied to numerals. Addition is based on the operation Successor (Suc), defined as follows: (Suc n) := λnfx. f(nfx)

• Sum.
  (Suma n₁ n₂ ) = λn₁n₂. n₁(Suc n₂)
  n₁+n₂ is the result of applying the successor function < strong>n₁ veces a n₂.
  Example: (Sum 2 3) = 2+3 = 5
  
  
• Product.
  (Prod n₁ n₂ ) = λn₁n₂. n₁(Suma n₂ 0)
  n₁*n₂ is the result of adding < strong>n₂ y 0, n₁ veces.
  Example: (Prod 2 3) = 2*3 = 6
  
  
• Power.
  (Pot n₁ n₂ ) = λn₁n₂. n₁(Prod n₂ 1)
  n₁^n₂ is the result of multiplying < strong>n₂ y 1, n₁ veces.
  Example: (Pot 2 3) = 2^3 = 9

Just as the successor expression of a numeral (Suc n) is relatively simple, the Predecessor < i>Pn, i.e. n−1, is much more complex:

Pn = λnfx. n(λgh.h(gf)( λu.x)( λu.u)

Logic functions

Logical functions can also be defined by lambda expressions. A logical function is a function that has as parameters the logical values V (true) or F (false) and produces a logical value as a result.

The values V and F are defined as follows:

V := λxy.x (returns first argument)
F := λxy.y (returns the second argument)

And the logical operations are defined as follows:

And: ∧ := λxy.xyF
Or: ∨ := λxy.xVy
Not ¬ := λx.xFV

Examples:

∧VF = (λxy.xyF)VF = VFF = (λxy.x)FF = F

∨VF = (λxy.xVy)VF = VVF = (λxy.x)VF = V

¬V = (λx.xFV)V = VFV = (λxy.x)FV = F

Thanks to the above definitions of V and F as functions one can specify the logical condition If-Then-Else, by means of a lambda expression with 3 variables: b (truth value), t (branch Then) and e (branch Else):

IfThenElse := λb.λt.λe.bte

(IfThenElse V p q) = p (returns branch Then)

(IfThenElseF p q) = qV (returns branch Else)

Predicates

A predicate is defined as a function that returns a truth value. An example of a predicate is the function Z, which has a numeral as parameter and returns V if the argument is the numeral 0, and F if it is any other numeral:

Z := λn.nF¬F
Z0 = (λn. nF¬F)0 = 0F¬F = ¬F = V
Zn = (λn. nF¬F)n = nF¬F = IF = F

Where we have to take into account:

0 = λfx.x
0fa = (λfx.x)fa = a. Therefore, 0F¬ = ¬
Fa = (λfxy.y)a = λy.y = I. Therefore, F¬ = I
nF is the function F applied n times. But according to the above, nF = I.

Recursive functions

We want to calculate, for example, the factorial of a number:

f(n) = (if n=1 then 1 else n*f(n−1)))

The problem is that in the lambda calculus recursive functions are not allowed because the functions are anonymous and therefore cannot call themselves. However, it is possible to define them using the Y combinator (also called "fixed-point combinator" or "paradoxical combinator"), discovered by Haskell B. Curry, which is defined as follows:

Y = λy.(λx.y(x x))(λx.y(x x))

Applying Y to a function R we have:

YR = λx.R(x x)(λx.R(x x x)) = R(λx. R(x x))(λx.R(x x)) = R(YR)

That is, YR is equal to the function R applied to YR. Here recursion appears, since

YR = R(YR) = R(R(R(YR)))...

By means of Y recursive functions can be encoded. For example, to solve the factorial problem, we define a function g (informally):

g = λf. λn.if n=1 then 1 else n*f(n−1)

g(n) returns 1 if n=1 and n*f(n−1) if n≠1.

The recursive function is g(Yg)n. For example, for n=4:

g(Yg)4 = (λn.if n=1 then 1 else n*((Yg)(ni>−1)))4 =
if n=4 then 1 else 4*((Yg)(4−1)))) = 4*((Yg) 3) =
4*(g(Yg) 3) = 4*(λn.if n=1 then 1 else n*(((Yg)(n−1)))3 =
4*(if n=3 then 1 else 3*((Yg)(3−1)))) = 4*(3*(3*(Yg) 2)) =
4*(3*(&1*(g(Yg) 2) =
4*(3*(λn.if n=1 then 1 else n*((Yg)(n−1)))2 =
4*(3*(if n=1 then 1 else 2*((Yg)(2−1)))) = 4*(3*(3*(2*(2*(Yg) 1)) = 4*(3*(3*(2*(λn.if n=1 then 1 else 1*((Yg)(1−1))))1 =
4*(3*(2*(1*))) = 4*3*2*1

The formal solution in lambda calculus consists of replacing conditional expressions and arithmetic expressions by the corresponding lambda expressions based on numerals:

n−1 → Pn (the predecessor of n)
n*(n−1) → (Prod n Pn)
if n=1 then 1 else n*f(n−1) → ((Z Suc(< strong>n)) 1 (Prod n Pn))

Therefore, the recursive expression is g(Yg)n, with

g = λf. ((Z Suc(n)) 1 (Prod n Pn))

MENTAL vs. Lambda Calculus
Paradigmas

Lambda calculation.

It is a single-paradigm theoretical model. Everything is a function: numbers, arithmetic, logic, and so on. Therefore, every information structure has to be created every time it is needed. The only information structure that it contemplates is the sequence within a functional expression, a structure that is not explicit, but implicit.

Church had at first a much more ambitious goal: to build a complete formal system and a universal language to model all of mathematics. But when he saw that Russell's paradox was affecting him, he downgraded his initial goal to focus exclusively on modeling computability by means of functional expressions.

MENTAL.

It is a universal paradigm-theoretic model that contemplates all types of paradigms and all types of expressions, and includes an abstract space where expressions are stored and remain.

With MENTAL, Church's initial goal of creating a universal language for modeling all mathematics is achieved.

Primitives

Lambda calculation.

The lambda calculus is considered a formalism of maximum mathematical conceptual economy, and the simplest theoretical programming language in existence, because it uses only two primitives: 1) the definition of functions; 2) the application of functions by substituting variables for arguments. With these two primitives, the lambda calculus makes it possible to express precisely any computable function.

MENTAL.

There are 12 universal semantic primitives, with corresponding contraries or duals. There is no "function" primitive. Functions are expressions derived from primitives.

Level of abstraction

Lambda calculation.

Using only two primitives implies a low level of abstraction. Everything requires a lot of detail.

MENTAL.

The level of conceptual abstraction is supreme. Everything is simpler, more expressive, more compact and direct, because we work directly with primary archetypes.

Expressions

Lambda calculation.

Only contemplates functional expressions. Function parameters must be explicitly declared in front of the function body. Functions cannot be given names, which leads to serious expression difficulties. Simple functions such as λx.x+1 are not supported either, since arithmetic operations are not primitive.

MENTAL.

Contemplates all types of expressions. The functional expressions equivalent to those of the lambda calculus are parameterized generic expressions. The parameters are declared in bold and within the body of the expression itself. This has the advantage that they can be manipulated like any variable. For example, a parameter can be converted into a normal variable, a variable into parameter, etc. For example:

z = ⟨( f(x y) = x+y+2 )⟩
z/(x=a y=b) // ev. ⟨( f(a b) = a+b+2 )⟩

z = ⟨( f(a b) = a+b+2 )⟩
z/(a=x b=y) // ev. ⟨( f(x y) = x+y+2 )⟩

Any expression can act as a function through the particularization mechanism. For example,

(z = x+y+2)
z/(x=3 y=4) // ev. 9
z/(x=3) // ev. y+5

You can specify named and anonymous functions. For example:


1. ⟨( f(n) = (2*n + 1) )⟩ // definition parameterized named function
f(3) // ev. 7 (application)
   
   
2. f=(2*n + 1) // definition of non-parameterized function with name
f/(n=3) // ev. 7 (application)
   
   
3. (2*n + 1)/(n=3) // ev. 7 (definition and application of unnamed function)

MENTAL's generic expressions go beyond the functional, since they allow to define logical rules, procedures, modal expressions, imaginary expressions, etc. They represent a "meta" level above the "base" expressions. The successive "meta" levels correspond to generic expressions of higher order.

Bound and free variables

Lambda calculation.

Bound variables are specified in front of the body of the expression, in the same way as with the universal quantifier of predicate logic. For example, in λxy.xaxby, the variables x and y are bound, and a and b are free.

MENTAL.

Join the concepts of universal quantization and parameterization. The universal quantifier, which was previously associated with logic, becomes universally applicable to all types of expressions, including functions. The parameters appear inside the generic expression. This implies that the expression is self-sufficient, not depending on something external, and the notation is simpler and more intuitive. For example, in the expression ⟨x+y+z+1⟩, x and y are parameters and z is a non-parameterized variable.

In non-generic expressions, no variable is specified as a parameter. This means more flexibility, because sometimes variables will act as parameters and sometimes they will not.

Arithmetic

Lambda Calculus.

Church's arithmetic operations and numerals are functions.

MENTAL.

The primitive operation is "Addition" (along with its counterpart "Subtraction"), which is of a general type, i.e., it can add all kinds of expressions and not just numbers. The rest of the arithmetic operations are derived.

Church's numerals is a good theoretical exercise, but it is a serious mistake to consider numbers as functions.

β substitution

Lambda calculation.

Substitutes the parameters for the arguments in the function body. Sets the way to substitute in the function body each parameter by its opposite. The rule is:

λx.M N = [N/x]M

MENTAL.

Parameters can be replaced by any other expressions, without restriction. The application of a function to arguments can be done in several ways.


1. f(5)/⟨(f(n) = 2*n + 1)⟩ // ev. 11
2. (2*n + 1)/(n=5) // ev. 11
3. z=(2*n + 1)
4. z/(n=5) // ev. 11

In general, the lambda calculus expression [N/x]M is equivalent in MENTAL to M/(x=N). In the lambda calculus, if x does not exist in M, the result is M. In MENTAL the expression is self-evaluating. For example,

(M = axb)
M/(y=c) // is self-evaluating
M // ev. axb

The "curryfication" can be specified as follows:

(x+y+1)/(x=a)/(y=b) // ev. (a+y+1)/(y=b) ev. a+b+1

The default associativity is to the left.

The equivalent of a redex is an expression that is not self-evaluating. The equivalent of a normal form is an expression that is self-evaluating.

α conversion

Lambda calculation.

The axiom is: λx.M = λz.[z/x]M (suppose z bound in M).
(replace, in M, z by x)

MENTAL.

In a parameterized generic expression, the parameter names can be any. Moreover, they are not confused with normal variables. For example, in the expression ⟨x+x+1⟩, x is a parameter and x is a variable. Therefore, the α conversion is not necessary.

η conversion

The η conversion is not necessary, nor is any special formalism needed, because at the conceptual level it is seen that the following expressions (for example) are the same, and not only functions, but expressions in general:

⟨( f(x y) = (x+y x*y) )⟩
f(2 3) // ev. (5 6)
(x+y x*y)/(x=3 y=3) // ev. (5 6)

Partial evaluation

Lambda calculation.

It is limited to functions and bound variables.

MENTAL.

It can be performed on all types of expressions, with bound or unbound variables. Examples:


1. (x+y+2)/(x=3) // ev. 5+y
   
   
2. ⟨( f(x y) = x+y x*y) )⟩
⟨( g(y) = f(5 y) )⟩ // ev. ⟨( g(y) = 5+y 5*y )⟩
   
   
3. ⟨( f = x+y+2 )⟩
⟨( g(y) = f/(x=5) )⟩ // ev. ⟨( g(y) = 7+y )⟩

Recursion

Lambda calculation.

A function cannot be recursive, that is, it cannot call itself because functions are anonymous. To solve this problem we resort to something complex and artificial such as the fixed-point combinator Y.

MENTAL.

It allows you to assign names (even parameterized) to expressions, thus simplifying expressions and allowing recursion in a natural, direct and intuitive way. For example:

⟨( fac(n) = 1 ← n=1 →' n*fac(n−1) )⟩ // factorial of n

Parallel computing

Lambda computation.

Does not include parallel computing.

MENTAL.

Allows parallel computation in a very simple way through the mere conjunction of processes.

Implementation

Lambda calculation.

The lambda calculus involves treating functions as first-class objects, which makes implementation complex.

MENTAL.

The implementation is simple because it is based on very simple concepts.

Types

Lambda calculation.

Kleene and Rosser (1936) showed that the lambda calculus was inconsistent. Church then developed (1940) a simple functional theory of types, a simpler theory than the one that appeared in Principia Mathematica. Church's original lambda calculus had no types, so that functions could be applied without restrictions. Simple type theory is computationally less powerful but more logically consistent.

In Church's type theory, functional expressions are classified into types, and types restrict the possible combinatorial forms of those expressions. Types are categories of functions and play a role analogous to that of set types in set theory.

MENTAL.

Types are not necessary in any kind of expressions (functions, sets, predicates, etc.) because when there are self-references, the result is a fractal expression, i.e., a descriptive expression of recursive type. Church's type theory like Russell's type theory is unnecessary because paradoxes cannot occur.

Foundation

Lambda calculation.

It is used as a theoretical model for functional programming languages.

MENTAL.

It is a universal theoretical model, a universal language, a universal paradigm and a universal foundation, capable of expressing all kinds of paradigms.

Computational model

Lambda calculation.

Provided a computational model. A function F: n → n between natural numbers is computable if and only if there exists a lambda function f such that if F(n_{1) = n2, entonces fn1 = n2.}

MENTAL.

It is a universal theoretical model.

Conclusions
Church, with the lambda calculus, made numerous contributions to the field of computation, including:

• The formal definition of computability in an abstract way, independent of any concrete implementation. The computational model is based on: 1) two functional primitives (definition and application of functions) that allow to define all kinds of functions: 2) the semantics of function as a process of transformation of arguments into a result.
  
  
• unnamed functions (lambda functions). And the possibility for a function to invoke itself, despite not having a name (recursion).
  
  
• Numbers as functions (Church's numerals) and arithmetic operations as functions.
  
  
• Logical operations as functions.
  
  
• Logical values (V and F) as functions, which allow implementing the logical condition (If-Then-Else).
  
  
• Predicates as functions that return a truth value.

However, the lambda calculus −like the Turing machine and category theory− is an example of non-compliance with Einstein's razor principle: "Everything should be made as simple as possible, but not simpler". It uses as its only concept that of functional expression, with two aspects: definition of a function and application of a function. This leads to serious expressive difficulties. Everything is a function, which causes the derived concepts (numbers, predicates, truth values, arithmetic operations, logical operations, conditions, etc.) to be expressed in a complex and unnatural way.

---

Addenda
Church and his contributions to science

The lambda calculus was developed in the 1930s by Alonzo Church [1941] to formalize computable functions, i.e., to define them precisely: every computable numerical function is computable by the lambda calculus, using the corresponding Church numerals instead of numbers. The lambda calculus is a theoretical model of computation, which has a computational power equivalent to that of a Turing machine.

When lambda calculus was invented, computers did not yet exist. However, it can be considered the first functional programming language in history. It has been the foundation of many functional languages, having had great influence on the design of programming languages in general.

Lisp was the first language to implement the lambda calculus [McCarthy, 1960], making it the oldest and most popular functional language. It is oriented to symbolic computation and is mainly applied to artificial intelligence topics.

Lisp was followed by, among others, Scheme, ML, Miranda and Haskell. Anyway, "pure" functional languages are only Haskell and Miranda. And hybrid languages (functional with other features, usually imperative) are Lisp, Scheme and ML.

Church's main contributions have been two:

1. Church's thesis.
   He asserts that every effectively computable numerical function is recursive and computable by the lambda calculus. It thus replaces the informal notion of "computation".
   
   At the end of 1936, Turing, who had also been working on the subject of computability, published his famous paper "On computable numbers ..." in which he put forward the thesis that every computable function is computable by a theoretical device known today as a "Turing machine". Turing himself proved that both computational models were equivalent. The thesis is called the Church-Turing thesis, a thesis that connects the operational, epistemic and extrinsic aspects of arithmetic with the ontological, intrinsic and abstract aspects. This thesis also establishes the limits of computability, since all computation is limited by the primitives used (by Church or by Turing).
   
   
2. Church's theorem.
   Church, studying "Hilbert's decision problem" (Entscheidungsproblem) led him to what is known as "Church's theorem". This theorem states that there is no algorithm or mechanical procedure capable of deciding whether the propositions of arithmetic are true or false. Therefore, that there is no general solution to the decision problem. This is equivalent to the fact that first-order predicate logic is undecidable.
   
   Church also used the lambda calculus to solve for the first time the problem of knowing whether or not any two functional expressions of the lambda calculus are equivalent. This problem is also undecidable: it cannot be solved by a general functional expression of the lambda calculus itself. This question was raised even before Turing's one-machine halting problem. Church and Turing were greatly influenced by Gödel's incompleteness theorem.

In 1990 a symposium was held in Church's honor at the State University of New York at Bufalo, for his seminal contributions to the foundations of the theory of computation.


Fixed-point combinators

A fixed point of a function f(x) is a value v of x such that f(v) = v. For example, 0 and 1 are fixed points of f(x) = x², because 0² = 0 and 1² = 1. A fixed point of a higher order function f(g) is another function h such that f(h) = h. Since YR = R(YR), then YR is a fixed point of any function R.

Curry's Y fixed-point combinator is not the only one that exists in the lambda calculus. In fact, the type-free lambda calculus has infinite fixed-point combinators. In 2005, Mayer Goldberg [2005] showed that the set of fixed-point combinators of the lambda calculus is recursively numerable. In the lambda calculus with types −more restrictive at the combinatorial level− there is no fixed-point combinator.

The use of fixed-point combinators for recursion is called "anonymous recursion".


Bibliography

• Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics. North Holland, Amsterdam, 1984. [Tratado exahustivo, texto estándar].
  
  
• Church, Alonzo. The Calculi of Lambda Conversion. Annals of Mathematicals Studies, No. 6. Princeton University Press, Princeton, New Jersey, 1941.
  
  
• Goldberg, Mayer. On the Recursive Enumerability of Fixed-Point Combinators. BRICS Report RS-05-1, University of Aarhus, 2005.
  
  
• Hindley, J. Roger; Seldin, Jonathan P. Lambda-Calculus and Combinators. An Introduction. Cambridge University Press, 2008.
  
  
• Landin Peter. A Correspondence Between ALGOL 60 and Church's Lambda-Notation. Communications of the ACM, 8 (2): 89-101, 1965.
  
  
• McCarthy, John. Recursive Functions of Symbolic Expressions and their Computation by machine, Part I. Coms. of the ACM, vol. 3, no. 4, pp. 184-195, April 1960.
  
  
• Michaelson, Greg. An Introduction to Functional Programming Through Lambda Calculus. Dover, 2011. Cambridge University Press, 2009.
  
  
• Revesz, G.E. Lambda-calculus, Combinators and Functional Programming. Cambridge University Press, 2009.
  
  
• Rosser, J.B. Highlights of the history of the lambda calculus. Annals of the History of Computing, 6:4, 337-349, 1984.
  
  
• Stoy, Joseph E. Denotational Semantics. The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, Massachusetts, 1981.