Я пытаюсь понять основы лямбда-исчисления и церковные цифры. Я много читаю и тренируюсь, но, похоже, я все время пытаюсь понять, как работают некоторые функции.
Пример, который я застрял, выглядит следующим образом. Возможно, кто-то может объяснить, где я поступил неправильно.
Церковная цифра для 1 может быть представлена как:
λf. λx. f x
Функция экспоненциации на церковных числителях (m ^ n) может быть задана как:
λm. λn. n m
Все, что я хочу сделать, это показать, что, применяя функцию экспоненциации к 1 и 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", оставил только "x", и у меня нет 1 назад. Где я ошибаюсь?
