Введение

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

Элементы

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

Действия

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

Ситуации

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

Ситуация – это конечная последовательность действий. И точка. Это не состояние, не снимок, а история. Ситуация, предшествующая выполнению каких-либо действий, обычно обозначается как S₀ и называется начальной ситуацией. Новая ситуация, возникающая в результате выполнения действия, обозначается с помощью символа функции do (в некоторых других источниках также используется result). Эта функция принимает ситуацию и действие в качестве аргументов и возвращает ситуацию, которая возникает в результате выполнения данного действия в данной ситуации. Тот факт, что ситуации являются последовательностями действий, а не состояниями, обеспечивается аксиомой, утверждающей, что равно тогда и только тогда, если и . Это условие лишено смысла, если бы ситуации были состояниями, поскольку два различных действия, выполненных в двух различных состояниях, могут привести к одному и тому же состоянию. Например, в мире робота, если первое действие робота – перемещение в местоположение , то первое действие – , а результирующая ситуация – . Если следующим действием робота будет поднять мяч, то результирующая ситуация будет . Термины ситуаций, такие как и , обозначают последовательность выполненных действий, а не описание состояния, которое является результатом их выполнения.

Текущие

Заявления, истинность которых может изменяться, моделируются реляционными флюентами – предикатами, принимающими ситуацию в качестве последнего аргумента. Также возможны функциональные флюенты – функции, принимающие ситуацию в качестве последнего аргумента и возвращающие значение, зависящее от ситуации. Флюенты можно рассматривать как "свойства мира". В примере флюент может быть использован для указания, что робот несет определенный объект в конкретной ситуации. Если робот изначально ничего не несет, то ложно, а верно. Расположение робота можно смоделировать с помощью функционального флюента, который возвращает местоположение робота в конкретной ситуации.

Формулы

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

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

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

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

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

Проблема с рамкой

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

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

Основные аксиомы

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

Регрессия

Регрессия — это механизм доказательства следствий в ситуационном исчислении. Он основан на выражении формулы, содержащей ситуацию, через формулу, содержащую действие *a* и ситуацию *s*, но не содержащую саму ситуацию. Повторяя эту процедуру, можно получить эквивалентную формулу, содержащую только начальную ситуацию S0. Предполагается, что доказывать следствия из этой формулы проще, чем из исходной.

ГОЛОГ

GOLOG - это язык логического программирования, основанный на ситуационном исчислении.

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

Основное различие между исходным ситуационным исчислением Маккарти и Хейса и используемым сегодня заключается в интерпретации ситуаций. В современной версии ситуационного исчисления ситуация — это последовательность действий. Первоначально ситуация определялась как «полное состояние вселенной в определенный момент времени». С самого начала было ясно, что такие ситуации нельзя описать полностью; идея заключалась лишь в том, чтобы делать некоторые утверждения о ситуациях и выводить из них следствия. Это также отличается от подхода, используемого в текущем исчислении, где состояние может быть набором известных фактов, то есть, возможно, неполным описанием вселенной. В первоначальной версии ситуационного исчисления флюенты не реифицируются. Другими словами, условия, которые могут изменяться, представляются предикатами, а не функциями. Фактически, Маккарти и Хейс определили флюент как функцию, зависящую от ситуации, но затем всегда использовали предикаты для представления флюентов. Например, факт, что в месте x идет дождь в ситуации s, представляется литералом В версии ситуационного исчисления Маккарти 1986 года используются функциональные флюенты. Например, положение объекта x в ситуации s представлено значением , где location — функция. Утверждения о таких функциях можно делать с помощью равенства: означает, что положение объекта x одинаково в двух ситуациях s и . Исполнение действий представлено функцией result: выполнение действия a в ситуации s является ситуацией . Эффекты действий выражаются формулами, связывающими флюенты в ситуации s и флюенты в ситуациях . Например, действие открытия двери, приводящее к тому, что дверь открыта, если она не заперта, представляется следующим образом: Предикаты locked и open представляют условия запертой и открытой двери соответственно. Поскольку эти условия могут меняться, они представлены предикатами с аргументом ситуации. Формула говорит, что если дверь не заперта в ситуации, то после выполнения действия открытия дверь открыта, а это действие представлено константой opens. Эти формулы недостаточны для вывода всего, что считается правдоподобным. Действительно, флюенты в разных ситуациях связаны только в том случае, если они являются предпосылками и эффектами действий; если на флюент не влияет какое-либо действие, невозможно сделать вывод о том, что он не изменился. Например, приведенная выше формула не подразумевает, что следует из , что и следовало ожидать (открытие двери не приводит к ее запиранию). Для поддержания инерции необходимы формулы, называемые аксиомами рамки. Эти формулы указывают все неэффекты действий: В первоначальной формулировке ситуационного исчисления начальная ситуация, позже обозначенная как S0, не определяется явно. Начальная ситуация не нужна, если ситуации рассматриваются как описания мира. Например, для представления сценария, в котором дверь была закрыта, но не заперта, и выполняется действие по ее открытию, используется константа s, обозначающая начальную ситуацию, и делаются утверждения о ней (например, ). Тот факт, что дверь открыта после изменения, отражается тем, что формула является следствием. Начальная ситуация необходима, если, как в современном ситуационном исчислении, ситуация рассматривается как история действий, поскольку начальная ситуация представляет собой пустую последовательность действий. Версия ситуационного исчисления, представленная Маккарти в 1986 году, отличается от исходной использованием функциональных флюентов (например, является термом, представляющим положение x в ситуации s) и попыткой использовать обход для замены аксиом рамки.

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

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

Здесь Holds является метапредикатом, а переменная f изменяется в пределах флюентов. Предикаты Poss, Initiates и Terminates соответствуют предикатам Poss, и соответственно. Левая стрелка ← представляет собой половину эквивалентности ↔. Другая половина подразумевается в завершении программы, где отрицание интерпретируется как отрицание при неудаче. Аксиомы индукции также неявны и необходимы только для доказательства свойств программы. Обратное рассуждение, как в разрешении SLD, обычно используемом механизме выполнения логических программ, неявно реализует регрессию.