DemonScript: Пространственные отношения
Введение
Рассмотрим отношения, составляющие топологическую основу описания относительного расположения объектов в пространстве:
- X in Y - объект Х непосредственно находится в объекте Y (если мы заглянем в Y, то увидим Х). При этом Y полностью окружает своей оболочкой объект Х (Х не "выглядывает" наружу). Если X in Y, то при перемещении объекта Y в пространстве, вместе с ним переместится и объект Х.
- X in# Y - объект X находится где-то внутри объекта Y. Для этого отношения выполняется свойство транзитивности, т.е. подразумевается возможность вложения объектов подобно матрёшкам (если ключ в шкатулке, а шкатулка в сундуке, то ключ внутри сундука). Отношение in# является транзитивным замыканием для отношения in. В примере выше "ключ in сундук" ложно, хотя "ключ in# сундук" - истинно.
- X оn Y - объект Х находится на горизонтальной поверхности объекта Y, имея с ней контакт, внутри которого нет других объектов.
- X оn# Y - объект Х "опирается" на объект Y, возможно через другие объекты (транзитивное замыкание для on)
- X above Y - все части объекта Х находятся выше всех частей объекта Y. Выше понимается в обыденном смысле — выше по вертикали против направления силы гравитации.
- X below Y - все части объекта Х находятся ниже всех частей объекта Y. Очевидно, что X below Y <-> Y above Х.
Данные определения не всегда совпадают с практикой применения аналогичных предлогов в естественном языке. Например, "яблоко в миске" может "выглядывать" за края миски, а "монета на блюдце" - нет. Тем не менее, подобная формализация позволит сформулировать логические правила (аксиомы) понимания интеллектуальной системой взаимосвязи этих отношений. При помощи аксиом можно будет решать различные задачи, в том числе и в условиях неполноты исходной информации.
Примеры
Ниже приведен пример для отношений in# и in (a в b, b в c и d вне всех остальных). Справа от рисунка записаны пары объектов для которых отношения истинны (первая колонка) и для которых они ложны (вторая колонка). Ложное отношение, как обычно, помечается восклицательным знаком "!":

Например, (a in# c) истинно (транзитивность). В тоже время (a in c) ложно (a находится не непосредственно в c, а через вложение в b). Аналогичны примеры для отношений above, on:

Объекты выше изображены прямоугольниками, символизирующими некоторые ящики. Это может быть реальный ящик (коробка, сундук) или воображаемый параллелепипед, полностью окружающий объект. Подчеркнём, что эти отношения применяются к закрытым ящикам. В частности, для истинного отношения X in Y, объект X не может выглядывать за Y. Если один ящик ставится на другой (X on Y), то он не "проваливается вниз" (у Y есть крышка). Наконец, отношение X above Y будет ложным, если хотя-бы часть объекта Х не выше объекта Y.
Для закрытых ящиков возможны вполне корректные (и многочисленные) модели в которых данное отношение ложно (ниже первые три примера). Однако, можно нарисовать картинки, которые в 2D запрещены в принципе (последние два примера):

Для двух ящиков Х и Y существует 9 вариантов расположения (X непосредственно в Y, X вложен внутрь Y и т.д.):

На второй картинке ящик Х окружён пунктиром. Это подчеркивает, что в общем случае между ним и ящиком Y могут быть другие ящики, вложенные друг в друга. Аналогично для Y на четвёртой картинке. Мы не ограничиваем относительных размеров ящиков (за исключением возможности их вложения in, in#). Поэтому в последнем примере, при ложности X above Y и Y above Х, не принципиально кто из ящиков больше или "чуть выше" (они нарисованы одинаковыми и на одном уровне).
True, False и Undef
Задание отношений не всегда однозначно фиксирует модель. Это означает, что данному множеству отношений может удовлетворять несколько различных "картинок" (= моделей). Например, пусть известно, что Y непосредственно находится в Z, а X - выше Y. Этой информации удовлетворяет пять моделей:

Ящик Х, находящийся выше Y, может быть как в Z, так и не вне его (но выше Y). Отношения, приведенные справа от рисунков, в одних моделях истинные, а в других ложные. Поэтому для них используется значение "возможно"= Undef. Истинность такого отношения при данных посылках недоказуема, но не доказуема и его ложность.
Аксиом, связывающих отношения, достаточно много. Добавление новых отношений ещё сильнее увеличивает их количество. Поэтому необходимо некоторым образом упорядочить процесс перечисления аксиом. Воспользуемся следующей стратегией. Начнем с базового отношения in#. Затем будем добавлять по одному отношению, учитывая только специфичные для него аксиомы, используя также некоторые предыдущие отношения.
Аксиоматика отношения in#
Отношение in# образует строгий древесный порядок. Ниже на рисунке приведена система вложенных друг в друга ящиков. Если нарисовать отношение непосредственного вложения in, то получится древесный граф. С учётом транзитивности, в графе отношения in# добавляются ещё рёбра A-E и B-E (последний рисунок):

Графы выше приведены в традиционном для математики виде (указаны только истинные рёбра). Первый граф является диаграммой порядка для отношения in# (не рисуются рёбра транзитивности), а второй - графом отношения in# на котором указаны все True рёбра отношения.
Напомним, что в трёхзначной логике (True, False, Undef) мы придерживаемся, вообще говоря, иного соглашения. Если значение отношения известно (True или False) ребро рисуется явным образом (и для False помечается восклицательным знаком). Если же ребра нет, это означает Undef (не известно значение отношения, но аксиомы не запрещают ни значения True, ни значения False).
Строгий древесный порядок in# обладает следующими четырьмя свойствами:
- (1) in# антирефлексивно: сам внутри себя не находится;
- (2) in# асимметрично: если X внутри Y, то Y внутри X не находится;
- (3) in# транзитивно: если истинно, что Х внутри Z и Z внутри Y, то истинно, что Х внутри Y;
- (4) in# древесно: если Z внутри Х и Y, то, либо Х внутри Y, либо Y внутри Х, либо Х и Y один ящик.
В DemonScript аксиомы отношения in# запишем следующим образом:
edges in, in#, on, on#, above, below; // декларируем отношения Mind.add ( X !in# X, // (1) антирефлексивность Y in# X -> X !in# Y, // (2) асимметричность X in# Z & Z in# Y -> X in# Y, // (3) транзитивность Z in# X & Z in# Y -> X in# Y | Y in# X | X==Y // (4) деревесность )В объект Mind, при помощи метода add, добавляются аксиомы. Символ -> обозначает логическое следствие, | - логическое ИЛИ (дизъюнкция), & - логическое И (конъюнкция) и ! - отрицание. Аксиомы предполагаются всегда истинными. Поэтому, в частности, антирефлексивность X !in# X означает, что X in# X ложно.
Отметим, что из антирефлексивности и транзитивности следует асимметричность: (1),(3) => (2). Действительно, положив X=Y в аксиоме транзитивности (3) и записав её в КНФ, имеем:
X !in# Z | Z !in# X | X in# X => X !in# Z | Z !in# X => X in# Z -> Z !in# X,где сначала опущен член X in# X как всегда ложный (по первой аксиоме), а затем КНФ снова превращена в импликацию. Аналогично, при Y=X, из асимметричности следует антирефлексивность: (2) => (1):
X in# X -> X !in# X <=> X !in# X | X !in# X <=> X !in# X.Вообще говоря, теоремы, следующие из аксиом, можно не указывать явным образом в Mind. Поэтому, можно опустить (2) или (1). Однако мы этого делать не будем. Дело в том, что Mind может работать в режиме в котором значения различных переменных считаются различными. В этом режиме опускание одной из аксиом приведёт к неполноте аксиоматики отношения.
Аксиоматика отношения in
Добавим отношение непосредственного вложения in, которое в языковых конструкциях будем обозначать предлогом "в", в отличии от предлога "внутри" для отношения in#. В принципе отношение in можно определить через in#:
def in(X,Y): X in# Y & !exists(Z, Z in# Y & X in# Z).Однако, информация о расположении объектов может поступать как в форме "X внутри Y", так и "X в Y". Поэтому удобнее рассматривать in и in# равноправным образом, вводя для отношения X in Y собственную аксиоматику.
Отношение in антирефлексивно и асимметрично однако не обладает транзитивностью (далее опускаем Mind.add):
X !in X, // (5) антирефлексивно Y in X -> X !in Y, // (6) асимметричноТак как транзитивность отсутствует, свойство асимметричности необходимо указать явным образом, однако можно опустить антирефлексивность (что, как указывалось выше, мы делать не будем).
Справедлива ещё одна "аксиома единственности": если истинно, что Х находится в Z, то он не может находится в другом Y, который не есть Z:
X in Z & Z!=Y -> X !in Y, // (7) единственностьПримеры для этой аксиомы приведены ниже на первом рисунке:

Свяжем теперь отношение in с отношением in#. Очевидно, что, если Х непосредственно (in) в Y, то оно находится и где-то внутри (in#) Y (но не наоборот!):
X in Y -> X in# Y, // (8)Эта аксиома эквивалентна X !in# Y -> X !in Y (если не где-то внутри, то тем более и не непосредственно "в"). Должны также выполняться две запрещающие отношение in аксиомы, примеры для которых приведены на рисунках выше:
X in# Z & Z in# Y -> X !in Y, // (9) X in# Z & Y !in# Z & Y != Z -> X !in Y, // (10)На древесных графах отношения in# последние две аксиомы могут показаться избыточными. Однако, мы рассматривем отношения in и in# равноправным образом. Это означает, что граф вложения ящиков друг в друга может быть частично задан отношением in, а частично отношением in#. В этом случае эти аксиомы необходимы. Например, если для трёх ящиков известно, что a in# c; c in# b, то непосредственно применить аксиому единственности (7) нельзя, хотя, очевидно, что при этом истинно a !in b.
Тестируем in и in#
Решим следующую задачу. Пусть известно, что ящик "a" находится где-то внутри ящика "c",
ящик "b" не находится внутри "c". Какие выводы из этой информации можно сделать?
Понятно, что возможны две модели. В одной ящик "b" находится вне ящика "c",
а в другой ящик "c" находится в "b" (и "b",
соответственно, в "c"
также не находится). Эти модели приведены на рисунках справа.
Получим решение при помощи DemonScript:
var G = GRAPH("G") // создаём пустой граф GRAPH = G // делаем его текущим nodes a,b,c // добавляем в него три узла a in# c; // а находится внутри c b !in# c; // b не находится внутри c out G // выводим исходный граф Mind.set_graph(G) // запускаем логический вывод out G // выводим финальный графИсходный граф и граф после проведения логических выводов (метод set_graph) выглядят следующим образом:
G { a { in#: [ c] }, b { in#: [!c] }, c {} }
G { a{ in#: [!a, c], in: [!a,!b], }, b{ in#: [!a,!b,!c], in: [!a,!b,!c], }, c{ in#: [!a,!c], in: [!a,!c], } }
Например, a !in# a или a in# a == False (это сработала аксиома антирефлексивности). Более нетривиальный вывод a !in b, т.е. ящик "a" не может находиться непосредственно внутри "b" (т.к. b не находится в "c", где находится "a"). Ещё один важный вывод: b !in# a ("b" не может находиться в "a").
При этом a in c, в отличии от a in# c, имеет неопределённое значение ("c" отсутствует в массиве a { in: [...] }). Это связано с тем, что информация a in# c; означает, что "a" находится где-то в "c", т.е. не обязательно непосредственно в "c"). Если мир не замкнут (могут существовать другие ящики), то между "a" и "c" может оказаться ящик (а может и не оказаться). Именно поэтому отношение a in c имеет неопределённое значение.
Для аналогичной задачи с отношениями in результат другой. В этом случае условиям соответствует уже три модели.
G.clear_edges() // очищаем рёбра a in c; // а находится непосредственно в c b !in c; // b не находится непосредственно в c

G { a{ in#: [!a, c], in: [!a,!b, c], }, b{ in#: [!b], in: [!b,!c], }, c{ in#: [!a,!c], in: [!a,!c], } }
Аксиоматика отношений on, on#
Отношение on антирефлексивно и асимметрично, но, как и in, транзитивностью не обладает:
X !on X, // (11) антирефлексивно Y on X -> X !on Y, // (12) асимметрично
Отношение on# (транзитивное замыкание для on) образует строгий, частичный порядок (в отличии от in# без аксиомы древесности):
X !on# X, // (13) антирефлексивность X on# Y -> Y !on# X, // (14) асимметричность X on# Z & Z on# Y -> X on# Y, // (15) транзитивностьКак и пара in, in#, отношения on, on# связаны следующим образом:
X on Y -> X on# Y, // (16)Заметим, что не любой частичный порядок описывается отношением on#. В частности, если между Х и Y "вклинивается" третий объект Z (или on-цепочка объектов), то отношение X on Y запрещено:
X on Z & Z on# Y -> X !on Y, // (17)Ниже на первом рисунке ниже приведена иллюстрация к этой аксиоме и пример запрещённого графа частичного порядка для отношения on:

Аналогично запрещают отношение on контейнеры, которые также "вклиниваются" между Х и Y:
X in# Z & Y !in# Z & Y!=Z -> X !on Y, // (18) X !in# Z & Y in# Z & X!=Z -> X !on Y, // (19)
Ещё два правила выглядят понятнее, если их записать не как запрещающие для on, а как разрешающие для in:
X on Z & Z in Y -> X in Y, // (20) Z on X & Z in Y -> X in Y, // (21)
На этом аксиоматика отношений on и on# окончена.
Размерность пространства
Модель объектов, связанных отношениями in, in# всегда можно реализовать как в 2-мерном пространстве (прямоугольники), так и 3-мерном (параллелепипеды). Для отношений on, on# - ситуация иная. Приведём простой пример, который имеет смысл в 3-мерном пространстве, но не возможен в 2-мерном:

Аксиоматика отношения above
Отношения above, как и in#, образует строгий частичный порядок, без древесного ограничения. Оно антирефлесивно, транзитивно (и, следовательно, асимметрично):
X !above X, // (22) антирефлексивно X above Y -> Y !above X, // (23) асимметрично X above Z & Z above Y -> X above Y, // (24) транзитивноСуществует также ряд аксиом, связывающих above с остальными отношениями. Так, очевидно, что:
X in# Y -> X !above Y, // (25) Y in# X -> X !above Y, // (26) X on Y -> X above Y, // (27)
Справедливо также соотношение, аналогичное по смыслу аксиоме (17):
X above Z & Z above Y -> X !on Y, // (28)Кроме этого, для трёх объектов справедливы две разрешающие аксиомы (приводящие к истинности отношения above):
X in# Z & Z above Y -> X above Y, // (29) X above Z & Y in# Z -> X above Y, // (30)Соответствующие этим аксиомам примеры приведены на следующих рисунках:

Аксиоматика отношения below
Для полноты картины добавим также аксиомы для отношения below:
Y above X -> X below Y, // (31) Y below X -> X above Y // (32)Двустороннее следование означает формулу эквивалентности X below Y <-> Y above X.
Тест для всех отношений
G.clear_edges() // очищаем рёбра nodes d // добавляем ещё один узел

a in c; b on c; d below c; Mind.set_graph(G) out G
a{ in#: [!a, c,!d], in: [!a,!b, c,!d], on: [!a,!b,!c,!d], above: [!a,!c, d], below: [!a,!c,!d]}, b{ in#: [!a,!b,!d], in: [!a,!b,!c,!d], on: [!a,!b, c], above: [!b], below: [!b], }, c{ in#: [!a,!c,!d], in: [!a,!b,!c,!d], on: [!a,!b,!c,], above: [!a,!c, d], below: [!a,!c,!d]}, d{ in#: [!a,!c,!d], in: [!a,!d,!c], on: [!a,!d], above: [!a,!c,!d], below: [ a, c,!d]}
Открытый и закрытый мир
Построенная выше аксиоматика пространственных отношений основывается на модели открытого мира. В такой модели могут существовать объекты, которые не упомянуты в исходной информации. В ряде случаев это может оказаться не удобным. Например, если утверждается, что существуют только ящики a,b,c и других нет, то эту информацию также необходимо уметь использовать. Подобная ситуация называется закрытым миром. В модели закрытого мира с двумя ящиками "a" и "b" противоречивыми являются факты a in# b; a !in b. В открытой модели они непротиворечивы и означают существование такого "c", что: a in# c; c in# b.
Чуть более сложный пример. Пусть известно, что
[a, b] in c; d !in c; d in# c;В закрытом мире это означает, что "d" должно находится или в "a" или в "b" (но не в обоих). В открытом мире, кроме этих возможностей следует допустить существование внутри "c" пятого объекта в котором находится "d".
Закрытый мир реализуется при помощи построения всех возможных, полностью определённых моделей. Для этого в Mind существует метод .get_models. Впрочем, часть сгенерённых им моделей, при наличии нескольких отношений, по-прежнему будут "открытыми". Более прямой путь, это "руками" получать все возможные модели, перебрав известные объекты. В примере с четырьмя ящиками a,b,c,d это выглядит так:
out Mind.set_graph(G) // применяем аксиомы для in#, in out "============== Models in# close world:" for X in# (d in X) == Undef { // для всех X в которых d может быть var Tmp = G.copy(); Tmp.d in Tmp.X; // его туда помещаем Mind.set_graph(Tmp) // и ещё раз применяем аксиомы out Tmp // выводим модель } out "============== Models in# open world:" var Models = Mind.get_models(G, in, 0); // генерация моделей для отношения in for M in# Models: out M // выводим эти моделиПервый способ даст две модели (d in a и d in b). Во втором способе дополнительно будет модель d !in a; d in# a, потому, что возможен не упомянутый пятый ящик вокруг ящика d.
Ящики без крышки
Выше рассматривалась модель ящика с крышкой, на которую можно ставить другие ящики. Эту модель можно расширить на ящики без крышки. Для этого введём граф смыслов Sen в котором будет смысл $lid (крышка). При описании конкретных объектов будем определять есть у ящика крышка или нет:
a has Sen.$lid; // у ящика "a" есть крышка b !has Sen.$lid; // у ящика "b" нет крышки
Если у ящика нет крышки, на него нельзя никого поставить:
X !has Sen.$lid -> Y !on X.
Часть аксиом не зависит от наличия или отсутствия крышки. Другие истинны, только при наличии соответствующей информации. Например, аксиому (20) следует модифицировать следующим образом:
X on Z & Z in Y & Y has Sen.$lid -> X in Y, // (20)
Заключительные замечания
A & B -> C <=> !С & B -> ! A <=> A & !C -> В.Однако все они имеют одинаковую КНФ: !A | !B | С, поэтому достаточно в Mind добавить только одну запись этой аксиомы.