Каноническая форма (МБ) (МБ)

Question

Существуют ли лямбда-члены M и B с M =/= B, чтобы MB и (MB) (MB) имели одинаковую каноническую форму?

Является ли проблема, с которой я столкнулся, пока я еще новичок с лямбда-исчислением, я подошел к этому, имея M = λx.x и B = λy.y Μ Β = (λx.x) (λy.y) -> (β) λy.y

(MB) (MB) = ((λx.x) (λy.y)) ((λx.x) (λy.y)) -> (β) (λy.y) ((λx.x) (λy. y)) -> (β) (λx.x) (λy.y) -> (β) λy.y и, таким образом, получаю ту же каноническую форму, но я не уверен, что я прав насчет (MB) (MB),

Answer 1

Размещенные вами сокращения верны.

Следует знать, что вы можете использовать любое имя для связанной переменной в лямбда-термине, поэтому термины \x.x а также \y.y не очень разные; это один и тот же термин. Это называется альфа-эквивалентностью.

Другое дело, что функция \x.x который просто возвращает свой аргумент, называется тождественной функцией, и это очень полезно знать.

Вот ответ на ваш вопрос, где М и Б разные. M может быть функцией, которая игнорирует свой аргумент и возвращает функцию тождества: \x.\y.y, B может быть любым термином, отличным от M. Тогда
(M B) -> \y.y
А также
((M B) (M B)) -> (\y.y \y.y) -> \y.y