Как определить функцию с цифрами Чёрча в лямбда-терминах?

Как я могу выразить следующую функцию с помощью лямбда-члена?

f(n) = T if n != 0. F if n = 0.

n обозначает число Черча.

Я знаю, что 0 := λf.λx.x, где λx.x — тождественная функция, а все остальные натуральные числа могут быть выражены как n := λf.λx.f (f ... (f x)), которое содержит f в n раз больше чем 0-член. Например. 3 := λf.λx.f (f (f x)).

Но как я могу получить действительный λ-член для функции выше? Думаю, мне тоже нужен y, чтобы получить T/F. Следовательно, я могу выразить число n через λf.(λxy.fxy), верно? А как же F и T? Является ли следующее правым λ-термом для указанной выше функции? λf.(λxy.fxy(yFT)) где T=λxy.x и F=λxy.y?


function computation-theory church-encoding lambda-calculus computability
person user3351676    schedule 22.12.2020    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Нет, вам дан срок для n. Это функция, которая ожидает два аргумента, f и z:

isZero n = n ( ;; f, a function, expecting x
               ;;       or the result of (f (f ... (f x) ...))
               λx.
               ;; but we know what we want it to return, always: it is:
                  F    ;; false, for n is _not_ 0
             )
             ( ;; the initial x, in case n is ......... 0!
               ;; so we know what we want it to be, in case n is 0:
               T       ;; true, for n _is_ 0
             )

и поэтому

isZero = λn.n(λx.F)T

Если n равно 0, isZero n вернет T; а иначе F:

{0}(λx.F)T = T
{1}(λx.F)T = (λx.F)T = F
{2}(λx.F)T = (λx.F)((λx.F)T) = F
{3}(λx.F)T = (λx.F)((λx.F)((λx.F)T)) = F
....
person Will Ness    schedule 22.12.2020
comment
Большое спасибо. Поскольку я искал функцию, которая возвращает F, если n равно 0, в противном случае T, мне просто нужно переключить T и F в вашем решении. - person user3351676; 28.12.2020
comment
ах, отлично. так это было notZero тогда. :) - person Will Ness; 28.12.2020