Путаница в лямбда - исчислении и церковных цифрах

Question

Я пытаюсь понять основы лямбда-исчисления и церковных цифр.Я много читал и практиковался, но, похоже, я все время зацикливаюсь на попытках понять, как работают некоторые функции.

Пример, на котором я застрял, выглядит следующим образом.Возможно, кто-нибудь сможет объяснить, где я ошибся.

Церковная цифра , обозначающая 1 , может быть представлена следующим образом:

λf. λx. f x

Функция возведения в степень для церковных цифр (mⁿ) может быть задан как:

λm. λn. n m

Все, что я хочу сделать, это показать, что, применяя функцию возведения в степень к 1 и 1, я получаю обратно 1, поскольку 1¹ = 1.Я делаю это, чтобы лучше понимать, как работают эти функции.Моя работа заключается в следующем, и я каждый раз застреваю:

// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)

И вот тут я застрял.Я потерял и то, и другое f's, оставшийся с xэто единственный, и у меня нет 1 ответного.Где я иду не так, как надо?

Answer 1

Где я иду не так, как надо?

Нигде!С тобой покончено.Помните, что имена переменных не важны;важна именно структура.Имена f или x2 не имеют смысла.Имеет значение только то, как они используются.Церковная цифра , обозначающая 1 , равна

λf. λx. f x

и у вас есть

λx2. (λx1. x2 x1)

Переименовать x2 Для f и x1 Для x и вуаля!У вас есть

λf. (λx. f x)
= λf. λx. f x