Ситуационное исчисление

Ситуационное исчисление — это логический формализм, разработанный для представления и рассуждения о динамических областях. Впервые он был введен Джоном Маккарти в 1963 году. ^[1] Основная версия ситуационного исчисления, представленная в этой статье, основана на версии, введенной Рэем Рейтером в 1991 году. За ней следуют разделы о версии Маккарти 1986 года и формулировке логического программирования .

Обзор

Ситуационное исчисление представляет изменяющиеся сценарии как набор формул логики первого порядка . Основные элементы исчисления:

• Действия, которые можно выполнять в мире
• Беглые языки , описывающие состояние мира
• Ситуации

Домен формализуется рядом формул, а именно:

• Аксиомы предварительных условий действия, по одной для каждого действия
• Аксиомы состояния преемника, по одной для каждого текущего
• Аксиомы, описывающие мир в различных ситуациях
• Основополагающие аксиомы ситуационного исчисления

В качестве примера будет смоделирован простой мир роботов. В этом мире есть один робот и несколько неодушевленных предметов. Мир размечен в соответствии с сеткой, так что местоположения могут быть указаны в терминах точек координат. Робот может перемещаться по миру, а также подбирать и ронять предметы. Некоторые предметы могут быть слишком тяжелыми для того, чтобы робот мог их поднять, или хрупкими, так что они разобьются, когда их уронят. Робот также может чинить любые сломанные предметы, которые он держит. ${\displaystyle (x,y)}$

Элементы

Основными элементами исчисления ситуаций являются действия, флюенты и ситуации. В описании мира обычно участвует также ряд объектов. Исчисление ситуаций основано на отсортированной области с тремя сортами: действия, ситуации и объекты, где объекты включают все, что не является действием или ситуацией. Могут использоваться переменные каждого сорта. В то время как действия, ситуации и объекты являются элементами области, флюенты моделируются либо как предикаты, либо как функции.

Действия

Действия формируют своего рода домен. Переменные действия сортировки могут быть использованы, а также функции, результатом которых является действие сортировки. Действия могут быть количественно определены. В примере мира роботов возможными терминами действия будут моделирование перемещения робота в новое место и моделирование подъема роботом объекта o . Специальный предикат Poss используется для указания того, когда действие является исполняемым. ${\displaystyle move(x,y)}$ ${\displaystyle (x,y)}$ ${\displaystyle pickup(o)}$

Ситуации

В ситуационном исчислении динамический мир моделируется как прогрессирующий через ряд ситуаций в результате различных действий, выполняемых в мире. Ситуация представляет собой историю событий действия. В версии ситуационного исчисления Рейтера, описанной здесь, ситуация не представляет собой состояние, вопреки буквальному значению термина и вопреки первоначальному определению Маккарти и Хейса . Этот момент был резюмирован Рейтером следующим образом:

Ситуация — это конечная последовательность действий. Точка. Это не состояние, это не моментальный снимок, это история . ^[2]

Ситуация до выполнения каких-либо действий обычно обозначается ⁠ ⁠ ${\displaystyle S_{0}}$ и называется начальной ситуацией. Новая ситуация, возникающая в результате выполнения действия, обозначается с помощью символа функции do (некоторые другие ссылки ^[3] также используют result ). Этот символ функции имеет ситуацию и действие в качестве аргументов, а также ситуацию в качестве результата, причем последняя является ситуацией, которая возникает в результате выполнения данного действия в данной ситуации.

Тот факт, что ситуации являются последовательностями действий, а не состояний, подтверждается аксиомой, гласящей, что равно тогда и только тогда, когда и . Это условие не имело бы смысла, если бы ситуации были состояниями, поскольку два разных действия, выполненные в двух разных состояниях, могут привести к одному и тому же состоянию. ${\displaystyle do(a,s)}$ ${\displaystyle do(a',s')}$ ${\displaystyle a=a'}$ ${\displaystyle s=s'}$

В примере мира роботов, если первым действием робота является перемещение в местоположение , то первым действием является , а результирующая ситуация — . Если его следующим действием является взятие мяча, то результирующая ситуация — . Такие термины ситуаций, как и обозначают последовательности выполненных действий, а не описание состояния, возникающего в результате выполнения. ${\displaystyle (2,3)}$ ${\displaystyle move(2,3)}$ ${\displaystyle do(move(2,3),S_{0})}$ ${\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))}$ ${\displaystyle do(move(2,3),S_{0})}$ ${\displaystyle do(pickup(Ball),do(move(2,3),S_{0}))}$

Свободно владеет

Утверждения, истинность которых может меняться, моделируются реляционными флюентами , предикатами, которые принимают ситуацию в качестве своего конечного аргумента. Также возможны функциональные флюенты , функции, которые принимают ситуацию в качестве своего конечного аргумента и возвращают зависящее от ситуации значение. Флюенты можно рассматривать как «свойства мира».

В этом примере флюент может использоваться для указания того, что робот несет определенный объект в определенной ситуации. Если изначально робот ничего не несет, то false, а true. Местоположение робота можно смоделировать с помощью функционального флюента , который возвращает местоположение робота в определенной ситуации. ${\displaystyle {\textit {isCarrying}}(o,s)}$ ${\displaystyle {\textit {isCarrying}}(Ball,S_{0})}$ ${\displaystyle {\textit {isCarrying}}(Ball,do(pickup(Ball),S_{0}))}$ ${\displaystyle location(s)}$ ${\displaystyle (x,y)}$

Формулы

Описание динамического мира кодируется в логике второго порядка с использованием трех видов формул: формул о действиях (предпосылок и следствий), формул о состоянии мира и основополагающих аксиом.

Предварительные условия действия

Некоторые действия могут быть невыполнимыми в данной ситуации. Например, невозможно положить предмет, если его не переносишь. Ограничения на выполнение действий моделируются литералами вида , где a — действие, s — ситуация, а Poss — специальный бинарный предикат, обозначающий выполнимость действий. В примере условие, что уронить предмет можно только при его переносе, моделируется следующим образом: ${\displaystyle {\textit {Poss}}(a,s)}$

${\displaystyle {\textit {Poss}}(drop(o),s)\leftrightarrow {\textit {isCarrying}}(o,s)}$

В качестве более сложного примера следующие модели показывают, что робот может переносить только один объект за раз, и что некоторые объекты слишком тяжелы для того, чтобы робот мог их поднять (на это указывает предикат heavy ):

${\displaystyle {\textit {Poss}}(pickup(o),s)\leftrightarrow (\forall z\ \neg {\textit {isCarrying}}(z,s))\wedge \neg heavy(o)}$

Эффекты действия

Учитывая, что действие возможно в ситуации, необходимо указать эффекты этого действия на флюентах. Это делается с помощью аксиом эффекта. Например, тот факт, что поднятие объекта заставляет робота нести его, можно смоделировать следующим образом:

${\displaystyle Poss(pickup(o),s)\rightarrow {\textit {isCarrying}}(o,do(pickup(o),s))}$

Также можно указать условные эффекты, которые зависят от текущего состояния. Следующие модели показывают, что некоторые объекты хрупкие (обозначаются предикатом fragile ) и их падение приводит к их поломке (обозначается текущим broken ):

${\displaystyle Poss(drop(o),s)\wedge fragile(o)\rightarrow broken(o,do(drop(o),s))}$

Хотя эта формула правильно описывает эффект действий, ее недостаточно для правильного описания действия в логике из-за проблемы фрейма .

Проблема рамы

Хотя приведенные выше формулы кажутся подходящими для рассуждений о последствиях действий, у них есть критический недостаток — их нельзя использовать для вывода не-эффектов действий. Например, невозможно вывести, что после поднятия объекта местоположение робота остается неизменным. Для этого требуется так называемая аксиома фрейма, формула типа:

${\displaystyle Poss(pickup(o),s)\wedge location(s)=(x,y)\rightarrow location(do(pickup(o),s))=(x,y)}$

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

Аксиомы состояния-преемника

Аксиомы состояния-последователя «решают» проблему фрейма в исчислении ситуаций. Согласно этому решению, проектировщик должен перечислить в качестве аксиом эффекта все способы, которыми может быть изменено значение конкретного флюента. Аксиомы эффекта, влияющие на значение флюента, можно записать в обобщенной форме как аксиома положительного и отрицательного эффекта: ${\displaystyle F({\overrightarrow {x}},s)}$

${\displaystyle Poss(a,s)\wedge \gamma _{F}^{+}({\overrightarrow {x}},a,s)\rightarrow F({\overrightarrow {x}},do(a,s))}$

${\displaystyle Poss(a,s)\wedge \gamma _{F}^{-}({\overrightarrow {x}},a,s)\rightarrow \neg F({\overrightarrow {x}},do(a,s))}$

Формула описывает условия, при которых действие a в ситуации s делает флюент F истинным в последующей ситуации . Аналогично, описывает условия, при которых выполнение действия a в ситуации s делает флюент F ложным в последующей ситуации. ${\displaystyle \gamma _{F}^{+}}$ ${\displaystyle do(a,s)}$ ${\displaystyle \gamma _{F}^{-}}$

Если эта пара аксиом описывает все способы, которыми текучая F может изменять значение, их можно переписать как одну аксиому:

${\displaystyle Poss(a,s)\rightarrow \left[F({\overrightarrow {x}},do(a,s))\leftrightarrow \gamma _{F}^{+}({\overrightarrow {x}},a,s)\vee \left(F({\overrightarrow {x}},s)\wedge \neg \gamma _{F}^{-}({\overrightarrow {x}},a,s)\right)\right]}$

На словах эта формула гласит: «Учитывая, что возможно выполнить действие a в ситуации s , текущее F будет истинным в результирующей ситуации тогда и только тогда, когда выполнение a в s сделает его истинным, или оно истинно в ситуации s , а выполнение a в s не сделает его ложным». ${\displaystyle do(a,s)}$

В качестве примера, значение текучего сломанного, введенного выше, задается следующей аксиомой состояния-преемника:

${\displaystyle Poss(a,s)\rightarrow \left[broken(o,do(a,s))\leftrightarrow a=drop(o)\wedge fragile(o)\vee broken(o,s)\wedge a\neq repair(o)\right]}$

Штаты

Свойства начальной или любой другой ситуации могут быть определены путем простого указания их в виде формул. Например, факт о начальном состоянии формализуется путем утверждения о (что является не состоянием, а ситуацией ). Следующие утверждения моделируют, что изначально робот ничего не несет, находится в месте , и нет сломанных объектов: ${\displaystyle S_{0}}$ ${\displaystyle (0,0)}$

${\displaystyle \forall z\,\neg {\textit {isCarrying}}(z,S_{0})}$

${\displaystyle location(S_{0})=(0,0)\,}$

${\displaystyle \forall o\,\neg broken(o,S_{0})}$

Основополагающие аксиомы

Основополагающие аксиомы ситуационного исчисления формализуют идею о том, что ситуации являются историями, имея . Они также включают другие свойства, такие как индукция второго порядка по ситуациям. ${\displaystyle do(a,s)=do(a',s')\iff a=a'\land s=s'}$

Регрессия

Регрессия ^[4] — это механизм доказательства следствий в исчислении ситуаций. ^[5] Он основан на выражении формулы, содержащей ситуацию , через формулу, содержащую действие a и ситуацию s , но не ситуацию . Повторяя эту процедуру, можно получить эквивалентную формулу, содержащую только исходную ситуацию S ₀ . Доказывать следствия из этой формулы предположительно проще, чем из исходной. ${\displaystyle do(a,s)}$ ${\displaystyle do(a,s)}$

ГОЛОГ

GOLOG — это язык логического программирования, основанный на ситуационном исчислении. ^{[6] [7]}

Первоначальная версия ситуационного исчисления

Главное отличие между первоначальным ситуационным исчислением Маккарти и Хейза и тем, что используется сегодня, заключается в интерпретации ситуаций. В современной версии ситуационного исчисления ситуация — это последовательность действий. Первоначально ситуации определялись как «полное состояние вселенной в момент времени». С самого начала было ясно, что такие ситуации не могут быть полностью описаны; идея состояла в том, чтобы просто дать некоторые утверждения о ситуациях и вывести из них следствия. Это также отличается от подхода, который используется в текучем исчислении , где состояние может быть набором известных фактов, то есть, возможно, неполным описанием вселенной.

В оригинальной версии исчисления ситуаций флюенты не овеществляются. Другими словами, условия, которые могут меняться, представлены предикатами, а не функциями. На самом деле Маккарти и Хейз определили флюент как функцию, которая зависит от ситуации, но затем они всегда использовали предикаты для представления флюентов. Например, тот факт, что в месте x в ситуации s идет дождь, представлен литералом . В версии исчисления ситуаций Маккарти 1986 года используются функциональные флюенты. Например, положение объекта x в ситуации s представлено значением , где местоположение является функцией. Утверждения о таких функциях могут быть даны с использованием равенства: означает, что положение объекта x одинаково в двух ситуациях s и . ${\displaystyle raining(x,s)}$ ${\displaystyle location(x,s)}$ ${\displaystyle location(x,s)=location(x,s')}$ ${\displaystyle s'}$

Выполнение действий представлено функцией result : выполнение действия a в ситуации s является ситуацией . Эффекты действий выражаются формулами, связывающими флюэнты в ситуации s и флюэнты в ситуациях . Например, то, что действие открытия двери приводит к тому, что дверь открывается, если она не заперта, представлено формулой: ${\displaystyle {\textit {result}}(a,s)}$ ${\displaystyle {\textit {result}}(a,s)}$

${\displaystyle \neg locked(door,s)\rightarrow open(door,{\textit {result}}(opens,s))}$

Предикаты locked и open представляют условия запирания и открывания двери соответственно. Поскольку эти условия могут различаться, они представлены предикатами с аргументом ситуации. Формула гласит, что если дверь не заперта в ситуации, то дверь открыта после выполнения действия открытия, это действие представлено константой opens .

Эти формулы недостаточны для вывода всего, что считается правдоподобным. Действительно, флюенты в разных ситуациях связаны только в том случае, если они являются предварительными условиями и эффектами действий; если флюент не затронут действием, нет способа вывести, что он не изменился. Например, приведенная выше формула не подразумевает, что следует из , чего можно было бы ожидать (дверь не запирается, когда ее открывают). Для того чтобы инерция сохранялась, необходимы формулы, называемые аксиомами фрейма . Эти формулы определяют все неэффекты действий: ${\displaystyle \neg locked(door,{\textit {result}}(opens,s))}$ ${\displaystyle \neg locked(door,s)}$

${\displaystyle \neg locked(door,s)\rightarrow \neg locked(door,{\textit {result}}(opens,s))}$

В первоначальной формулировке исчисления ситуаций начальная ситуация, позже обозначенная как ⁠ ⁠ ${\displaystyle S_{0}}$ , явно не идентифицирована. Начальная ситуация не нужна, если ситуации рассматриваются как описания мира. Например, представление сценария, в котором дверь была закрыта, но не заперта, и действие по ее открытию выполняется, формализуется путем принятия константы s для обозначения начальной ситуации и создания утверждений о ней (например, ). То, что дверь открыта после изменения, отражается формулой, которая выводится. Начальная ситуация вместо этого необходима, если, как в современном исчислении ситуаций, ситуация рассматривается как история действий, поскольку начальная ситуация представляет собой пустую последовательность действий. ${\displaystyle \neg locked(door,s)}$ ${\displaystyle open(door,{\textit {result}}(opens,s))}$

Версия исчисления ситуаций, представленная Маккарти в 1986 году, отличается от оригинальной использованием функциональных флюентов (например, является термином, представляющим положение x в ситуации s ), а также попыткой использовать ограничение для замены аксиом фрейма. ${\displaystyle location(x,s)}$

Ситуационное исчисление как логическая программа

Также возможно (например, Ковальски 1979, Апт и Безем 1990, Шанахан 1997) записать исчисление ситуаций в виде логической программы:

${\displaystyle {\textit {Holds}}(f,do(a,s))\leftarrow {\textit {Poss}}(a,s)\wedge {\textit {Initiates}}(a,f,s)}$

${\displaystyle {\textit {Holds}}(f,do(a,s))\leftarrow {\textit {Poss}}(a,s)\wedge {\textit {Holds}}(f,s)\wedge \neg {\textit {Terminates}}(a,f,s)}$

Здесь Holds — метапредикат, а переменная f ранжируется по флюентам. Предикаты Poss , Initiates и Terminates соответствуют предикатам Poss , и соответственно. Левая стрелка ← — это половина эквивалентности ↔. Другая половина подразумевается в завершении программы, в которой отрицание интерпретируется как отрицание как неудача . Аксиомы индукции также неявны и нужны только для доказательства свойств программы. Обратное рассуждение, как в разрешении SLD , которое является обычным механизмом, используемым для выполнения логических программ, неявно реализует регрессию. ${\displaystyle \gamma _{F}^{+}({\overrightarrow {x}},a,s)}$ ${\displaystyle \gamma _{F}^{-}({\overrightarrow {x}},a,s)}$

Смотрите также

• Проблема с рамкой
• Исчисление событий

Ссылки

1. Маккарти, Джон (1963). «Ситуации, действия и причинные законы» (PDF) . Технический отчет Стэнфордского университета . Архивировано из оригинала (PDF) 21 марта 2020 г.
2. «Вклад в дебаты ECSTER».
3. «Объединение повествований, Джон Маккарти и др. (1998)» (PDF) .
4. Уолдингер, Ричард. «Достижение нескольких целей одновременно». В «Чтениях по искусственному интеллекту», стр. 250-271. Морган Кауфманн, 1981.
5. Рейтер, Р., 1991. Проблема фрейма в ситуационном исчислении: простое решение (иногда) и результат полноты для целевой регрессии. Искусственная и математическая теория вычислений, 3.
6. Лейкмейер, Герхард. «Исчисление ситуаций и Голог: Учебное пособие» (PDF) . www.hybrid-reasoning.org . Получено 16 июля 2014 г. .
7. "Публикации о GOLOG" . Получено 16 июля 2014 г.

• J. McCarthy и P. Hayes (1969). Некоторые философские проблемы с точки зрения искусственного интеллекта. В B. Meltzer и D. Michie, редакторы, Machine Intelligence , 4:463–502. Edinburgh University Press, 1969.
• Р. Ковальски (1979). Логика для решения проблем - Elsevier North Holland.
• KR Apt и M. Bezem (1990). Ациклические программы. В: 7-я Международная конференция по логическому программированию. MIT Press. Иерусалим, Израиль.
• Р. Рейтер (1991). Проблема фрейма в ситуационном исчислении: простое решение (иногда) и результат полноты для целевой регрессии. В книге Владимира Лифшица, редактора, Искусственный интеллект и математическая теория вычислений: статьи в честь Джона Маккарти , страницы 359–380, Сан-Диего, Калифорния, США. Academic Press Professional, Inc. 1991.
• М. Шанахан (1997). Решение проблемы рамы: математическое исследование закона инерции здравого смысла. MIT Press.
• H. Levesque, F. Pirri и R. Reiter (1998). Основы ситуационного исчисления. Electronic Transactions on Artificial Intelligence , 2(3–4):159-178.
• Ф. Пирри и Р. Рейтер (1999). Некоторые вклады в метатеорию ситуационного исчисления. Журнал ACM , 46(3):325–361. doi :10.1145/316542.316545
• Р. Рейтер (2001). Знание в действии: логические основы для спецификации и реализации динамических систем. Издательство MIT.