Как определить функцию с цифрами Чёрча в лямбда-терминах?
Как я могу выразить следующую функцию с помощью лямбда-члена?
f(n) = T, если n != 0. F, если 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?
Ответы 1
Нет, вам дан срок для 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
....
ах, отлично. так было notZero тогда. :)
Большое спасибо. Поскольку я искал функцию, которая возвращает F, если n равно 0, в противном случае T, мне просто нужно переключить T и F в вашем решении.