Y combinator: Some functions do not have fixed points

Question

The W combo article on Y combinator contains the following JavaScript implementation of Y combinator:

function Y(f) { return ( (function (x) { return f(function (v) { return x(x)(v); }); }) (function (x) { return f(function (v) { return x(x)(v); }); }) ); } 

The existence of a Y combinator in JavaScript should mean that every JavaScript function has a fixed point (since for each function g , Y(g) and g(Y(g)) must be equal).

However, it is easy to come up with functions without fixed points that violate Y(g) = g(Y(g)) (see here ). Even some functionals do not have fixed points (see here ).

How is the proof that each function has a fixed point consistent with these counter examples? Is JavaScript an untyped lambda calculus that uses the proof that Y(g) = g(Y(g)) ?

Answer 1

The problem with lambda expressions is that they cannot be interpreted as functions in a mathematical sense, i.e. mappings from one set to another.

The reason is that the power of a set of functions from a set A itself is always greater than the power of A , so not all functions from A to A can be an element of A That is, there exists a function f: A -> A for which the expression f(f) does not make sense.

This is like a “set of all sets that do not contain themselves”, which logically does not make sense.

JavaScript is not a lambda calculus model.

The problem with your example is that

 (lambda xg(xx)) (lambda xg(xx)) 

should be equivalent

 g((lambda xg(xx)) (lambda xg(xx))) 

but this is not in your JavaScript program, where g is the indicator function 0 .

xx always undefined . Therefore, the first line evaluates to g (undefined) = 0 . The second line evaluates to g (g (undefined)) = g (0) = 1 . That means your lambda calculus JavaScript model is not actually a model.

Since for every nonempty set D there exists a function from D to D without a fixed point, obviously, there can be no model of lambda calculus. I think it should even be possible to prove that there cannot be an implementation of Y-combinator in any Turing language.

Answer 2

As far as I understand the Wikipedia article, nowhere is it implied that “every JavaScript function has a fixed point”, and this example just shows how to implement Y combinator for functions that have it according to their specification.

And no, according to the definitions in this article and the fixed-point article , JavaScript cannot be an untyped lambda calculus, because it can formulate functions that obviously do not perform a “fixed-point” test, for example, function f(x){ return x + 1 } or x ^ 1 if you want to include non-numbers and thus do not perform the check "every function has at least one fixed point".

Answer 3

The theory of fixed points comes in flavors. Those for programming languages ​​are studied under the heading of denotational semantics . They depend on the values ​​forming a structured counting set with special properties. Lattices and Full partial orders are two examples. All of these sets have a "bottom" element, which turns out to be a fixed point, which means "no useful result." In fact, the only fixed point operators that interest you in computer programs are the least fixed point operators: those that find a unique minimum fixed point that is the lowest in a structured set of values. (Note that all integers are on the same level in these structured sets. Only the bottom element lives below. The rest of the layers are made up of more complex types such as types of functions and tuples, i.e. Structures.) If you have a discrete math is very good. The Tarski fixed point theorem actually says that every function, monotonous (or alternately continuous), has a fixed point. See the above link for definitions. In operating computer programs, the bottom element corresponds to a non-determinative calculation: infinite recursion.

The fact is that if you have a strict mathematical model of calculations, you can start to prove interesting things about type systems and the correctness of a program. This is not just an academic lesson.