«Теория категорий и теория вычислений»

[kassalanche]

Вчера Александр Батальщиков положил начало цикла встреч, посвященного разбору четвертой части Rosetta Stone «Computation».

Первый семинар в этом направлении прошёл под общим заголовком комбинаторная логика (КЛ).

Comments

[ulysses4ever]

Хорошее описание, спасибо. Есть пара замечаний.

> 3. T[λx.E] => (K T[E]) (если x свободно в E)
На самом деле, связано в E.

> Условный оператор.
В русской традиции это более правильно называть условной операцией. Операция (operator) - это то, что возвращает значение, а оператор (statement, инструкция) это средство управление порядком вычислений. Условная операция в КЛ это, кстати, аналог операции ?: в C/C++ или операции if-then-else в Haskell (обратите внимание, что else обязательно именно потому, что это операция, у условного оператора в императивных языках его обычно можно опускать).

> мы обозначили его N (на самом деле условный оператор)
Эээ Не понял, какой же он условный: условный по значению булевского условия возвращает первое или второе, а этот, наоборот, по аргументу возвращает булевское значение. То есть это предикат, если хотите.

> Рассмотрим S I I ( S I I) x
Его ещё (без x) потом обозначили Ω - традиционно.

> Решили к уже существующим правилам добавить это:
7. T[(λx.Ex)] => T[E]
... который выводится из первых 6, но может повышать эффективность вычисления T.

Я бы всё от слова Введение до X(X(X(X X))) = S отправил под кат (тег или кнопочка в Визуальном редакторе).

[kassalanche]

Больше спасибо за замечания. Я все исправила.

> Решили к уже существующим правилам добавить это:
7. T[(λx.Ex)] => T[E]
... который выводится из первых 6, но может повышать эффективность вычисления T.
Даже из первых трёх:
T[(λx.Ex)] = (3) = K T[Ex] = (2) = K T[E] T[x] = (1) = K T[E] x = (K) = T[E]