403
правки
Изменения
Нет описания правки
{{Определение
|definition=''Неподвижной точкой'' лямбда-функции <tex>f</tex> назовём такую функцию <tex>x</tex>, что
<tex>f\ x \to_\beta ^* x</tex>.
}}
<tex>\operatorname{fix} = \lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x))</tex>
Заметим, что <tex>\operatorname{fix} \to_\beta ^* \lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))</tex>.
Или, что то же самое,
<tex>\lambda f \to (\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)) \to_\beta^*</tex>
<tex>\lambda f \to f\ ((\lambda x \to f\ (x\ x))\ (\lambda x \to f\ (x\ x)))</tex>
<tex>\operatorname{fact'} = \lambda f \to \lambda x \to \operatorname{if}\ (\operatorname{isZero}\ x)\ \bar 1\ (\operatorname{mult}\ x\ (f\ (\operatorname{pred}\ x)))</tex>
Как было показано выше, <tex>\operatorname{fix} f \to_\beta ^* f\ (\operatorname{fix} f)</tex>, то есть, <tex>\operatorname{fix}\ \operatorname{fact'} \to_\beta ^* \operatorname{fact}</tex>, где <tex>\operatorname{fact}</tex> {{---}} искомая функция, считающая факториал.
<tex>\operatorname{fact} = \operatorname{fix}\ \operatorname{fact'}</tex>
