LINUX.ORG.RU
Форум — Talks  

Объясните как работает iszero в λ-исчислении


1

3

Не могу разобраться. Вот есть λn.n(λx.false)true. Можете привести выкладки для λfx.x и, например, для λfx.fx. В книжках пишут, что мол слишком просто, чтоб доказывать. И можно ссылкочку на док-во (а лучше, на какое-нибудь доступное пособие)?

★★★
← Регистрация стандартов. Что делать, куда податься?
Увидел ошибку 500 при попытке открыть Youtube, но ошибка какая-то странная →

Бета-редукция:

iszero zero = (λn. n(λx. F) T) (λf.λx. x) = (λf.λx. x) (λx. F) T = T

iszero one = (λn. n(λx. F) T) (λf.λx. fx) = (λf.λx. fx) (λx. F) T = (λx. F) T = F

Дальше сам.

Apple-ch ★★
()
Ответ на: комментарий от Apple-ch

Все равно не совсем ясно. 

(λх.М)N=М[х <- N]
Так? В первой строке последнее преобразование 
((λf.λx.x)(λx.F))T = (λx.x[f <- λx.F]) T = (λx.x) T = х [x <- T] = T
Как вы это в одно преобразование сделали, или я чего-то не понял? Во второй строке от это не понимаю 
(λf.λx. fx) (λx. F) T = (λx. F) T.

У меня как-то так выходит 

((λf.λx. fx) (λx. F)) T = (λx. fx [f <- λx. F]) T = (λx.(λx. F)x) T=(λx.(F[x <- x])) T = (λx. F) T
Это верно?

LIKAN ★★★
() автор топика
Ответ на: комментарий от LIKAN

Это верно?

Ну конечно верно :) Тут всё настолько просто, что ошибиться малореально.

Бета-редукция — это вычисление, т.е. подстановка переменной(ых) в терм. Ты же понимаешь, что λf.λx. fx можно записать как λfx. fx и подставить обе переменные сразу.

что такое f?

Не понял вопрос. f — это имя переменной, такое же как x.

Apple-ch ★★
()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.
← Регистрация стандартов. Что делать, куда податься?
Talks
Увидел ошибку 500 при попытке открыть Youtube, но ошибка какая-то странная →