Вторая теорема Черча – Россера “Теорема о стандартизации”

Если выражение e0 ->* e1 являющемуся нормальной формой, то существует нормальный порядок редукций из e0 в e1.

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

Теперь определим нормальный порядок редукции.

Он предполагает, что на каждом шаге редукции выполняется самая левая внешняя бета – редукция.

Теперь уточним идеи –левая и внешняя.

Самая левая – в терме (L M) сначало редуцируется L, т.е. надо получить сначало функцию, а когда ее нельзя будет редуцировать то тогда будем ее применять.

Что такое самая внешняя? Это значит в терме

(hx.M) N

Сначала применяется бета – редукция без редуцирования M и N.Вместо N модет стоять амега, это опасно. Сделаем сразу подстановку.

Здесь можно увидеть принцип передачи параметра по имени, аргумент не вычисляется а буквально подставляется….

На практике передача параметров по имени исп в ленивых вычислениях.

Представление данных в лямбда исчислении.

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

На лямда исчислении можно смоделировать все возможности хаскеля.

Представление булевых значений

Для булевых величин должны выполняться условия

If True M N = M

If False M N = N

____ - метасимволы, обозначающие какие – либо термы лямбда исчисления.

Эти равенства выполняются при

True Ξ hx y . x

False Ξ hx y . y

If Ξ hp x y .p x y

Пример.

If True M N

-> (hp x y .p x y) (hx y .x) M N

-> (hx y . x) M N -> M

Представление логических функций.

and Ξ hp q . if p q False

or Ξ hp q . if p True q

not Ξ hp. If p False True

Представление упорядоченных пар

Списки можно представить упорядоченными парами…

Для работы с упор парами нужны три функции

pair Ξ hx y f . f x y // строит пару

fst Ξ hp . p True // лямбда p, берет пару и применяет к терму True

snd Ξ hp . p False

Очевидно что

pair M N -> hf . f M N

то есть “упаковываются в одну функцию”

аргументы в кариерых функциях могут запоминаться.

Пару можно применить к любой функции от двух аргументов вида

h x y . L

В этом случае получится результат

L[M/x][N/y]

Пример

Вычислим

fst (pair M N) -> fst (hf . d M N)

• (hf . f M N) True

• True M N -> M

Анлогично

snd (pair M N) -> N

Числа

Представление натуральных чисел

Черч предложил натуральные числа представлять так

(константа Ξ …………)

0 Ξ h f x. x

1 Ξ h f x. f x

2 Ξ h f x. f (f x)

…

n Ξ h f x. f (…(f x)..) Ξ h f x. fⁿ x

N раз

это представление полезно тем, что каждое число заключает в себе итерацию n раз. получить функцию….применить n раз…

Сложение натуральных чисел

add Ξ h m n f x. m f (n f x)

Пример

add m n Ξ (h m n f x. m f (n f x)) m n

• h f x. m f (n f x)

Ξ h f x. m f ((h f x. fⁿ x) f x)

• h f x. m f (fⁿ x)

Ξ h f x. ((h f x. f^m x) f (fⁿ x)

• h f x. f^m (fⁿ x)

Ξ h f x. f^m+n x Ξ m+n

Умножение натуральных чисел

mult Ξ h m n f. m (n f) x

Пример

mult m n ->h f x. m (n f) x

Ξ h f x. (h f x. f^m x) (n f) x

• h f x. (n f)^m x

Ξ h f x. ((h f x. fⁿ x) f)^m x

• h f x.((h x. fⁿ x)^m x

= h f x.(fⁿ)^m x

Ξ h f x. f^m*n x Ξ m*n

В лямбда исчислении и есть возможность описать рекурсивные функции.

Как представлять рекурсивные функции лямбда исчисления

Рекурсивная функция представляется

f = hx . (… f …)

Для представляения рекурсивных функций нужен беск терм, но дела обстоят не так плохо. Есть способ представления рекурсивных функций, основанный на комбинаторно-рекурсиврованной точки.

Комбинатор – это лямбда терм, не содержащий свободных переменных. Его еще называют замкнутый терм.

Фиксированной точкой функции F называется терм X, для которого выполняется равенство F X = X (F примененное к X дает X). т.е. это такой терм который при отображении через функцию никак не изменится.

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