?

Log in

No account? Create an account

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

« previous entry | next entry »
Nov. 29th, 2009 | 03:59 am
posted by: kassalanche in sfedu_ctseminar

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

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

Введение. Для начала, докладчик знакомил слушателей с основными понятиями КЛ: переменная, комбинатор, применение, терм. Были рассмотрены примеры комбинаторов:
1) I x = x,
2) K x y = x,
3) S x y z = x z (y z).
Показано, что I может быть построен через K и S.
4) B x y z = x (y z)
5) С x y z = x y z
6) W x y = x y y

Полнота. Сформулировали теорему о том, что исчисление комбинаторов полно по Тьюрингу. Сказали, что для доказательства достаточно показать эквивалентность КЛ и лямбда-исчисления (которое, как известно полно по Тьюрингу), для чего придумать правила, переводящие любой терм КЛ в лямбда-терм и наоборот. В одну сторону (из КЛ в лямбда) это оказывается тривиальным. Правила же перехода из λ-исчисления в КЛ:
1. T[x] => x
2. T[(E_1 E_2)] => (T[E_1] T[E_2])
3. T[λx.E] => (K T[E]) (если x связно в E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (если x свободно в E)
6. T[λx.E_1 E_2] => S T[λx.E_1] T[λx.E_2]
вызвали значительно больше обсуждений. В частности, обсуждалась эквивалентность 3-его и 6-ого правил для терма вида λx.E_1 E_2, где x — связная переменная в E_1 E_2. Затруднения вызвал тот факт, что, можно обозначить E_1 E_2 как E и тогда, сторого говоря, непонятно какое из правил (третье или шестое) применять.
На этом обсуждение доказательства завершилось.

Пример. В качестве примера рассмотрели λ-терм λx.λy.yx и его перевод в КЛ:
T[λx.λy.yx] = ... = S (K (S I)) (S (K K) I)
При проведении вычислений заметили, что не хватает правила: T[P] => P (где P - комбинатор), несмотря на это, не преминули им воспользоваться.
То что получилось, применили к x y. Оказалось, этот терм просто меняет местами два своих параметра:
S (K (S I)) (S (K K) I) x y = ... = y x
К уже существующим правилам добавили это:
7. T[(λx.Ex)] => T[E].
Оно выводится из первых 6, но может упростить вычисление T.
Ещё пример.
S I I x = I x (I x) = I x x = x x.
Рассмотрим S I I ( S I I) x. Нетрудно видеть, что попытка вычислить такой терм приводит к зацикливанию. Терм S I I ( S I I) обозначили через Ω — традиционно. Прозвучало замечание о том, что, если бы в исчислении не было бы зацикливающихся вычислений, оно не могло бы быть полным по Тьюрингу.

Условная операция. Рассмотрели понятие условной операции, уделив внимание корректности её определения. Обозначение true и false как K и K I соответственно повергло часть публики в замешательство.

Проблема останова. Сказали, что в линейном λ-исчислении редуцирование всегда приводит к НФ, если она есть. После чего была сформулирована теорема: не существует комбинатора, который для любого комбинатора может определить редуцируемый он или нет. Доказательство проводилось от противного. В предположении о существовании такого комбинатора, мы обозначили его N, рассмотрели некоторый конкретный комбинатор Z и убедились, что для него N работает некорректно. Получили противоречие.

Базис. Красной нитью шли толки о том, что S и K образуют базис. В преддверии завершения встречи докладчиком был озвучен интересный факт о существовании одноточечного базиса X:
X x = x S K.
Разумеется (т.к. это базис) S и K также выражаются через X:
X(X(X X)) = K
X(X(X(X X))) = S


Материал для доклада был взят из книги В. Э. Вольфенгаген «Комбинаторная логика в программировании» и статьи Combinatory logic из английской википедии.
Tags:

Link | Leave a comment |

Comments {18}

(no subject)

from: kassalanche
date: Nov. 29th, 2009 01:05 am (UTC)
Link

> Обозначение 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

Reply | Thread

(Deleted comment)

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 10:31 am (UTC)
Link

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

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

Reply | Parent | Thread

(Deleted comment)

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 11:19 am (UTC)
Link

А, это да.

Reply | Parent | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 06:20 am (UTC)
Link

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

> 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 отправил под кат (тег <lj-cut text="Краткое содержание доклада"> или кнопочка в Визуальном редакторе).

Reply | Thread

(no subject)

from: kassalanche
date: Nov. 29th, 2009 01:10 pm (UTC)
Link

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

> Решили к уже существующим правилам добавить это:
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]

Reply | Parent | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 06:25 am (UTC)
Link

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

Reply | Thread

(Deleted comment)

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 11:18 am (UTC)
Link

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

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

Reply | Parent | Thread

ghbdtn.mp

(no subject)

from: ghbdtn.mp
date: Nov. 29th, 2009 09:44 am (UTC)
Link

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

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

Reply | Thread

(Deleted comment)

ghbdtn.mp

(no subject)

from: ghbdtn.mp
date: Nov. 29th, 2009 10:12 am (UTC)
Link

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

Reply | Parent | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 10:33 am (UTC)
Link

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

Reply | Parent | Thread

ghbdtn.mp

(no subject)

from: ghbdtn.mp
date: Nov. 29th, 2009 12:10 pm (UTC)
Link

Да, выходит. Тут такая проблема: либо, как ниже Осман говорит, "это бета-редукция (что и так уже давно ясно)". Либо "выходит за рамки".

Что еще можно было бы из того, что в рамках... Рассматреть спецификацию "категорной абстрактной машины" - так она концептуально ничего нового не содержит. А что Вам было бы интересно?

Reply | Parent | Thread

ghbdtn.mp

(no subject)

from: ghbdtn.mp
date: Nov. 29th, 2009 12:10 pm (UTC)
Link

"рассматреть"="рассмотреть"
(увы, пора в первый класс)

Reply | Parent | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 01:33 pm (UTC)
Link

Мне было бы интересно рассмотреть КАМ. Рассуждать так широко: «концептуально ничего нового» — я не готов. Много всего не содержит концептуально, но интересно.

Reply | Parent | Thread

(Deleted comment)

ghbdtn.mp

(no subject)

from: ghbdtn.mp
date: Nov. 29th, 2009 12:04 pm (UTC)
Link

Конкретно этот текст - да, как в мультфильме: "слон есть плохо, справка есть карашо!"
Но к нему список литературы интересный.

Reply | Parent | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Nov. 29th, 2009 11:20 am (UTC)
Link

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

Reply | Thread

(no subject)

from: kassalanche
date: Nov. 29th, 2009 01:16 pm (UTC)
Link

А также упоминался язык программирования, который использует единственный комбинатор X. Это lota.

Reply | Thread

Pavel Samolisov

(no subject)

from: chelcoder
date: Jun. 20th, 2010 01:10 pm (UTC)
Link

Все же в правиле вывода (3) лучше указать, что х должна не входить как свободная переменная, а не должна быть связанной переменной (как указано сейчас). В примере T[λx.λy.yx] = ... = S (K (S I)) (S (K K) I) (см. статью на википедии) на 4-м шаге выражение T[λy.x] сводится к (K x) по правилу 3, однако переменная y вообще не входит в тело терма λy.x, т.е. не может быть связанной переменной тела этого терма.

Reply | Thread

ulysses4ever

(no subject)

from: ulysses4ever
date: Jun. 20th, 2010 04:12 pm (UTC)
Link

Да, Барендрегт дваждует вас истово.

Reply | Parent | Thread