DemonScript: Пространственные отношения

Введение

Рассмотрим отношения, составляющие топологическую основу описания относительного расположения объектов в пространстве:

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

Примеры

Ниже приведен пример для отношений 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# обладает следующими четырьмя свойствами:

Древесность означает, что Z не может находится одновременно и внутри X, и внутри Y, если они, в свою очередь, не являются вложенными (см. выше разрешённый пример с ящиками B,C,E на последнем графе).

В 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 {...} - это узел a графа, где в фигурных скобках перечислены все рёбра, которые исходят из узла. Пока у нас есть только два типа рёбер in# и in. После их имён, в квадратных скобках идёт перечисление узлов в которые эти рёбра направлены. Если перед именем узла стоит восклицательный знак, это означает, что данное отношение ложно.

Например, 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)

Заключительные замечания

  • Приведенная аксиоматика не учитывает размерности пространства. В большинстве случаев это не критично. Однако иногда может оказаться важным. Например, если ввести отношения слева, справа, спереди, сзади в 2-мерном пространстве (прямоугольники), при помощи 4-х объектов можно "зажать" между ними пятый. В 3-мерном пространстве для этого необходимо ещё два объекта и отношения above, below.

  • Отношение above более общее, чем on (включает его), а in# - более общее, чем in. В посылках правил надо стремиться к наиболее общим отношениям (тогда они будут справедливы и для частных). Большая общность означает, что данное отношение выполняется на большем числе моделей. Например X above Y может быть истинно, и когда X on Y ложно, но не наоборот.

  • При генеративном порождении значений отношений (применяем аксиомы, пока граф не перестаёт изменяться), необходимо учесть, что если есть аксиома F -> G, то также справедливо и !G -> !F. В объекте Mind это автоматически учитывается, так как все формулы представляются в КНФ. В частности аксиома F -> G имеет вид !F | G. Аналогично, если в посылке два атома, то аксиомы утраиваются. Например: 
          A & B -> C    <=>     !С & B -> ! A       <=>     A & !C -> В.
    Однако все они имеют одинаковую КНФ: !A | !B | С, поэтому достаточно в Mind добавить только одну запись этой аксиомы.

  • Рассмотренные в этом документе примеры можно найти в скрипте: in_on_above.ds