r3 - 27 Apr 2008 - 16:43:54 - Artem ShvorinYou are here: TWiki >  XSG Web > TheoryOfEverything

Формальное описание

Данные

Предлагаю некоторое обобщение того, что сейчас есть в XSG. Так будет проще, а для утилитарных целей можно будет опять внести ограничения вплоть до строгой типизации.

Итак, язык не типизированный (забегая вперед скажу, что типизацию, точнее типизации , можно будет добавлять потом). Имеется конечный набор атомов (нет конструкторов фиксированной ненулевой арности), из них можно составлять кортежи произвольной длины. Есть также скобки, с помощью которых строятся деревья произвольной глубины. Кроме того, как и в хаскеле, допускаются деревья актуально бесконечной глубины, которые строятся с помощью специальных связывающих переменных (пока не придумалось хорошего названия для этих переменных, но хочется, чтобы они не смешивались с другими переменными, которые появятся позже).

Всё это выглядит примерно так.

EXPR ::= ATOM
   | TUPLE
   | LINK_VAR

TUPLE ::= '(' EXPR* ')'

BINDING ::= LINK_VAR ':=' EXPR

VALUE ::= EXPR
   | EXPR 'with' BINDING*

Здесь для выражение связывания переменных специально используется слово with , а не where , поскольку where будет использоваться с клэшами. Пока рассматриваем только такие значения, в которых все переменные связаны, при этом запрещены "связывания" типа x := x.

Наличие 1-кортежей (синглетов) и 0-кортежей -- вопрос удобства; для дальнейшего изложения это неважно.

Домены

Далее вводится важное понятие, которое, кажется, явно не было сформулировано в XSG, однако неявно в нем присутствует.

Домен (domain) -- это (перечислимое) множество значений. (Андрей как-то говорил про мультимножества; можно попробовать и их, только не очень ясно, что будет, если добавить отрицания.) Ключевым вопросом является способ задания доменов. Здесь мы получаем набор языков в зависимости от выбора. Однако всякий способ задания должен быть внутренне согласован. Я придумал использовать слово алгебра , которое описывает принципы такого задания.

Алгебра доменов

TODO: RBNF для описания доменов

  1. Существует пустой домен, обозначим его {} .
  2. Существует домен, содержащий конечное число явно заданных значений: {v1 | v2 ... | vn} .
  3. Существует домен-универсуум U , содержащий все возможные значения (вообще-то явное наличие универсуума требуется только для алгебр, содержащих отрицания; речь о них пойдет ниже).
  4. Если заданы домены X1, ... Xn, то можно построить домен { expr(x1, ..., xn) for x1:X1, ..., xn:Xn} , где expr -- выражение со свободными переменными x1, ... xn. Такая конструкция подразумевает наличие квантора всеобщности для переменных, т.е. переменные пробегают все значения из доменов X1, ... Xn.
  5. Обобщением предыдущей конструкции является введение клэшей.
    {expr(x1, ..., xn) for x1:X1, ..., xn:Xn where e1(x1, ..., xn) :=: e1'(x1, ..., xn), ..., em(x1, ..., xn) :=: em'(x1, ..., xn)}
    Здесь e1, e1', ..., em, em' -- выражения со свободными переменными x1, ... xn. Такая конструкция является "неканонической", т.е. задача машины -- избавиться от таких представлений путем решения системы клэшей.

Назовем представление домена рациональным , если он выражен без клэшей, и домены, через которые он определен, также выражены рационально.

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

Вначале я думал ограничиться нерекурсивным заданием доменов, однако для выражения доменов соответствующим SML-ным дататайпам уже требуется рекурсия. Например, пусть есть домен D, описывающий некоторый тип, и нужно построить домен, описывающий список. Это можно сделать так:

ListD = {Nil | Cons x y for x:D, y:ListD}

Как видим, ListD рекурсивно зависит от себя.

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

Роль доменов в языке

Вообще язык по сути служит только для описания доменов, а основным результатом вычислений программы является нахождение рационально представления целевого домена. Кроме того, для всякого домена должен существовать генератор -- алгоритм (вообще говоря, не терминируемый), перечисляющий все элементы домена. Построение генератора также является результатом вычислений; это будет единственно полезным результатом, если рациональное представление недостижимо.

Построение генератора должно является алгоритмически разрешимой задачей в отличие от нахождения рационального представления.

Нужно заметить, что речь пока не идет о функциях. Они будут введены позже. Даже без функций язык уже выглядит достаточно богатым, хотя не является алгоритмически полным. Требуется построить язык таким образом, чтобы алгоритм приведения домена к рациональному виду был терминируем (при отсутствии функций). Это будет одним шагом машины.

Связь с теорией множеств

  • Пересечение:
     D1 & D2 = {x1 for x1:D1, x2:D2 where x1 :=: x2}
  • Объединение:
    D1 | D2 = {x1 | x2 for x1:D1, x2:D2}

Отрицания

TODO: раздел далек от завершения.

Отрицания на доменах вводятся примерно как теоретико-множественное дополнение до U . Слово "примерно" употреблено, потому что скорее всего не удастся точно отобразить операции над классическими множествами на операции над доменами. Например, кажется уместной аксиома

D & ^D = ^D & D = {}
однако скорее всего не удастся включить закон исключенного третьего
D | ^D = U
или закон двойного отрицания
^^D = D

Наивное конструктивное определение отрицания апеллирует к перечислениям (т.е. генераторам) доменов.

  1. ^U = {}; ^{} = U
  2. ^{A} = {^A}, что по определению задает домен с таким же перечислением, как U, в котором только отсутствует A.
  3. ^{(v1 v2)} = {^(v1 v2)} = {(^v1 v2) | (v1 ^v2) | ...}, где на месте многоточия перечислены всевозможные кортежи длины, отличной от 2. При наличии какой-нибудь "внешней" типизации этого многоточия может не быть (т.е. получается дополнение не к U, к классу кортежей длины 2).
  4. ...

Одной из основных проблем здесь является доработка УРА: теперь в системах клэшей на каждую явно введенную переменную x заводится дополнительно ее отрицание -- переменная ^x. Нужно решать систему относительно вдвое большего количества переменных, при наличии дополнительных неявных, новых для нас, связей между x и ^x.

Обрывки мыслей

  • Для рационально представленных доменов верны законы двойного отрицания и исключенного третьего.
  • Процесс вычисления иррационального домена D можно представить как построение последовательностей рациональных доменов D1, D2, ... и D1', D2', ... так чтобы они обе возрастали (в теоретико-множественном смысле), и Di < D; Di' < ^D. Т.е, последовательность Di приближается (боюсь употреблять слово "стремится") к D снизу, и Di' приближается к ^D снизу. Дуально: можно приближение снизу заменить на приближение сверху, для этого надо взять ^Di' и ^Di. Таким образом, на каждом шаге этого процесса можно указать значения, которые гарантированно входят в D, а также значения, которые не входят.
  • Недовычисленные домены можно представлять в виде, аналогичном ДНФ: D = {c1 | c2 | ... | cn | f}, где ci -- "довычесленные" выражения, а f -- недовычесленное, которое будет дальше ветвиться. Дуально: должен быть вид, аналогичный КНФ (монотонно растет набор клэшей; пока неясно...).
  • Должна быть некоторая дуальность между клэшами (:=:) и пайпами (|) в представлениях доменов.

(Продолжение следует...)

-- Artem Shvorin - 27 Apr 2008

Edit | WYSIWYG | Attach | Printable | Raw View | Backlinks: Web, All Webs | History: r3 < r2 < r1 | More topic actions
 
Powered by TWiki

This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback