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

[kassalanche]

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

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

Comments

[kassalanche]

> Обозначение true и false как K и K I соответсвенно повергло часть публики в замешательство.

Здесь (стр. 25) описано использование такого приема (правда, для λ-исчисления) с пояснениями и хорошими примерами. Вообще, нетрудно доказать, что true (λx.λy.x) и false (λx.λy.y) в λ-исчислении переводятся в K и K I соответсвенно):
T[λx.λy.y] = (5) = T[λx.T[λy.y]] = (4) = T[λx.I] = (3) = KT[I] = KI

[ulysses4ever]

А что вы имеете ввиду, когда говорите, что «K и KI это не просто "произвольно взятые" комбинаторы»? По ссылке Кассаланч написано: «Вообще говоря, назвать истиной и ложью можно любые термы, но такой выбор обозначений оказался наиболее удобным».

Скажем так, это произвольно взятые удобные комбинаторы. То есть важно понимать, что никем это категорично не диктуется, что обозначать истиной и ложью, просто если обозначать так, удобно писать if-then-else и прочее. Взяли бы другое, могло бы оказаться более удобно или менее удобно или вообще не получилось бы.

[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, но

[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]

[ulysses4ever]

Мне доклад очень понравился. Единственным темноватым моментом для меня стало понятие (не)редуцируемости комбинаторного терма. Оно как-то неожиданно для меня отличается от того, что есть в λ. Там ситуация более простая, конечно, потому что язык формально более богатый.

[ulysses4ever]

Я посмотрел в книгах Hindley, Seldin, Lambda-calculus and Combinators (2B) и в книге Барендрегта (глава 7). Там как-то проще :) Понятие редуцируемого терма дословно нет. Есть редексы, редукция (или контраакция) и нормальная форма. Редекс это одно из выражений: IX, KXY, SXYZ. Редукция это замена редекса IX на X, KXY на X, SXYZ на XZ(YZ). Терм в нормальной форме это терм, не содержащий редексов.

Соответствующее отношение редукции обладает свойством Чёрча-Россера, так что есть единственность НФ, но нет существования. Всё похоже на лямбду. Хотя про взаимоотношение редукций там и там, если верить Барендрегту, есть отдельные работы - отношения действительно несколько различаются.

[ext_179323]

Как я вижу, на первом семинаре решили рассмотреть вторую половину заголовка, а первую оставили на второй семинар. :)

Можем мы добавить эту ссылку в наш список?
http://math.ucr.edu/home/baez/lics2009

[ext_179323]

Да. При том, что мне бы как раз хотелось видеть там более короткий список - слишком длинный скорее дезориентирует читателя. Но про лямбду у нас сейчас маловато, а здесь именно оно, и самое свежее.

[ulysses4ever]

По-моему, этот список как раз выходит за рамки (нашего) базового списка.

[ulysses4ever]

Кстати, ещё упоминалось про графические языки, выражающие лямбду. Вот ссылка на крокодилов, про которые мы с Татьяной упоминали.