Y комбинатор: Некоторые функции не имеют неподвижные точки

Question

Wikipedia article on the Y combinator обеспечивают следующую реализацию JavaScript в 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); }); }) 
    ); 
} 

Существование Y Combinator в JavaScript должен подразумевать, что каждая функция JavaScript имеет неподвижную точку (поскольку для каждой функции g, Y(g) и g(Y(g)) должны быть равны).

Однако нетрудно придумать функции без фиксированных точек, которые нарушают Y(g) = g(Y(g)) (см. here). Даже некоторые функционалы не имеют фиксированных точек (см. here).

Как доказательство того, что каждая функция имеет фиксированную точку, согласуется с данными контр-примерами? Является ли JavaScript не нетипизированным лямбда-исчислением, в котором применяется доказательство того, что применяется Y(g) = g(Y(g))?

Answer 1

Проблема с лямбда-выражениями заключается в том, что они не могут быть интерпретированы как функции в математическом смысле, то есть отображения из одного набора в другой.

Причиной является мощность множества функций из множества A на себя всегда больше, чем мощность A, поэтому не все функции от A к A может быть элементом A. То есть существует функция f: A -> A, для которой выражение f(f) не имеет смысла.

Это как «набор всех множеств, не содержащих себя», что логически не имеет смысла.

JavaScript не является моделью лямбда-исчисления.

Проблемы с вашим примером является то, что

(lambda x.g(x x)) (lambda x.g(x x)) 

должен быть эквивалентен

g((lambda x.g(x x)) (lambda x.g(x x))) 

, но это не в вашей программе JavaScript, где g является индикаторной функцией 0.

x x всегда undefined. Следовательно, первая строка оценивается как g (undefined) = 0. Вторая строка оценивается как g (g (undefined)) = g (0) = 1. Это означает, что ваша модель JavaScript лямбда-исчисления фактически не является моделью.

Так как для каждого непустого множества D есть функция от D к D без неподвижной точки, очевидно, не может быть ни одна модель лямбда-исчислении. Я думаю, что было бы даже возможно доказать, что не может быть реализации Y-комбинатора на любом языке Тьюринга.

Answer 2

Насколько я понимаю, статья Википедии не означает, что «каждая функция JavaScript имеет фиксированную точку», и этот пример просто показывает, как реализовать комбинатор Y для функций, которые имеют его по их спецификации.

И нет, в соответствии с определениями, содержащимися в этой статье и an article on fixed point, JavaScript не может быть нетипизированная лямбда-исчисление, потому что он может сформулировать функции, которые, очевидно, обанкротиться «имеют неподвижную точку» проверить, как function f(x){ return x + 1 } или x^1, если вы хотите включают не-номера и, таким образом, не могут «проверять каждую функцию как минимум на одну фиксированную точку».

Answer 3

Теория с фиксированной точкой поступает в ароматы. Для языков программирования изучаются под заголовком денотационная семантика. Они зависят от значений, образующих структурированный счетный набор со специальными свойствами. Lattices и Complete Partial Orders - два примера. Все эти наборы имеют «нижний» элемент, который оказывается неподвижной точкой, что означает «никакого полезного результата». Фактически, единственными операторами фиксированной точки, которые вас интересуют в компьютерных программах, являются наименьшие операторы с фиксированной точкой: те, которые находят уникальную минимальную фиксированную точку, которая является самой низкой в ​​структурированном наборе значений. (Обратите внимание, что все целые числа находятся на одном уровне в этих структурированных наборах. Только нижний элемент живет ниже. Остальные слои состоят из более сложных типов, таких как типы функций и кортежей, т. Е. Структуры.) Если у вас есть дискретная математика , this очень хорошо. Теорема о неподвижной точке Тарского фактически говорит, что каждая функция, которая имеет , монотонная (или поочередно непрерывная) имеет фиксированную точку. См. Приведенную выше ссылку для определений. В операционных компьютерных программах нижний элемент соответствует несконтерминирующему вычислению: бесконечная рекурсия.

Суть всего в том, что если у вас есть строгая математическая модель вычислений, вы можете начать доказывать интересные вещи о системах типов и правильности программы. Так что это не просто академическое упражнение.