оценить лямбда-исчисление - ИЛИ ЛОЖНОЕ ИСТИНА

Question

TRUE = λxy. x

FALSE = λxy. y

IF = λbtf. btf

AND = λxy. ЕСЛИ xy ЛОЖЬ

ИЛИ = λxy. ЕСЛИ x ИСТИНА y

НЕ = λx. ЕСЛИ x ЛОЖНО ИСТИНА

Как я могу использовать лямбда-исчисление для бета-уменьшения выражения ИЛИ ЛОЖНО ИСТИНА? Я не уверен, с чего начать. Мой преподаватель не прошел через это. Вот моя попытка

(\xy.IF x TRUE y)(\xy.y)(\xy.x)
= (\xy.IF x TRUE y)[x := (\xy.y))(\xy.x)
= (\y. IF (\xy.y) TRUE y)(\xy.x)
= (IF (\xy.y) TRUE y)[y := (\xy.x))
= IF (\xy.y) TRUE (\xy.x)

Answer 1

Когда вы работаете с церковными кодировками, я думаю, что лучше оставаться настолько абстрактным, насколько это возможно, то есть вы не должны раскрывать TRUE, FALSE, IF и NOT с нетерпением, но только при необходимости.

Вместо того, чтобы сначала попытаться доказать основные результаты их поведения, это также поможет проверить работоспособность. Для IF вы хотите проверить, что IF TRUE t f = t и IF FALSE t f = f.

IF TRUE t f = TRUE t f   (IF returns its arguments directly)
            = t          (TRUE returns its first argument)

То же самое для IF FALSE.

Сейчас

OR FALSE TRUE = IF FALSE TRUE TRUE

иприменяя удостоверение, которое вы уже доказали, вы сможете сделать вывод.