Теорема о неподвижной точке. Для любого F существует X, такой, что F X = X.
Доказательство. Пусть W ≣ λx.F (x x) и X ≣ W W. Тогда имеем X ≣ W W ≣ (λx.F (x x)) W = F (W W) = F X, что и требовалось доказать…
Теорема… о неподвижной точке - один из основных результатов лямбда-исчисления. Читатель, возможно, заметил одну особенность в доказательстве этой теоремы. Чтобы установить, что F X = X, мы начинаем с терма X и редуцируем его к F X, а не наоборот…
Определение. Комбинатор неподвижной точки - это терм M, такой, что для любого F имеет место M F = F (M F), то есть M F - неподвижная точка для F…
Пусть Y ≣ λf.(λx.f (x x)) (λx.f (x x)). Тогда Y — комбинатор неподвижной точки…
Задача. Построить F, такой, что F x y = F y x F.
Решение. F x y = F y x F следует из равенства F = λxy.F y x F, а оно вытекает из F = (λfxy.f y x f) F. Теперь положим F ≣ Y (λfxy.f y x f), и все в порядке.
Доказательство. Пусть W ≣ λx.F (x x) и X ≣ W W. Тогда имеем X ≣ W W ≣ (λx.F (x x)) W = F (W W) = F X, что и требовалось доказать…
Теорема… о неподвижной точке - один из основных результатов лямбда-исчисления. Читатель, возможно, заметил одну особенность в доказательстве этой теоремы. Чтобы установить, что F X = X, мы начинаем с терма X и редуцируем его к F X, а не наоборот…
Определение. Комбинатор неподвижной точки - это терм M, такой, что для любого F имеет место M F = F (M F), то есть M F - неподвижная точка для F…
Пусть Y ≣ λf.(λx.f (x x)) (λx.f (x x)). Тогда Y — комбинатор неподвижной точки…
Задача. Построить F, такой, что F x y = F y x F.
Решение. F x y = F y x F следует из равенства F = λxy.F y x F, а оно вытекает из F = (λfxy.f y x f) F. Теперь положим F ≣ Y (λfxy.f y x f), и все в порядке.
— «Ламбда-исчисление. Его синтаксис и семантика», Барендрегт Х., 1985 (перевод с английского Г. Е. Минца под редакцией А. С. Кузичева)»
