Обзор формальных моделей вычислений

Описанная выше алгебраическая модель СП является обобщением ря­да известных моделей, среди которых отметим реляционную модель А.С. Клещева, К-системы В.Е. Кузнецова, реляционную модель S.Vere, и модель управляемой СП V.Georgeff.

Реляционная модель вычислений, предложенная А. С. Клещевым, в ка­честве языка описания использует язык исчисления предикатов первого порядка. Элементами множества состояний являются конституанты, которые представляют собой атомные формулы вида:

P(c₁,…, c_k),

где р — некоторый k-арный предикатный символ, a c_i, с_2, ..., с_k — кон­станты. Множество переходов между элементами множества состояний задаетсяс помощью теории Т в языке исчисления предикатов первого порядка L, каждое предложение которой содержит в точности один знак импликации.

Для каждого множества конституант S определим связанную с ним структуру M_s языка L с помощью следующих условий

- все m_s имеют один и тот же счетный универсум;

- в M_s истинны те и только те конституанты, которые входят в S.

Через M_q будем обозначать структуру, соответствующую пустому множеству конституант. Пусть Т — множество предложений языка L вида

f®ψ,

где ф и ψ — конъюнкции конституант, S₀ — конечное множество конституант такое, что , не является моделью Т. Тогда процесс вычислений по программе Т над исходными данными S₀ определяется следующим образом.

Для каждого ее a Î Т обозначим: n_a, w_a — множества конституант, входящих в условие и в следствие а соответственно. Пусть на i-м шаге вычислено множество конституант S_i такое, что S₀ Í S_i. Если некоторое a Î Т ложно в структуре , то

.

Выбор на i-ом шаге предложений a Î Т, ложных в структуре соот­ветствует различному порядку выполнения действий при вычислениях.

Процесс вычислений заканчивается, если для некоторого t структура , — модель Т; S_t будем называть результатом вычисления.

Аналогично определяется вывод в случае, когда в правилах язы­ка используются переменные и кванторы, т.е. правила имеют вид "n₁, …, n_n(f®$u₁, …, u_my).

А..С. Клещевым исследована корректность вычислений в реляционной модели и доказано, что результат вычислений не зависит от порядка применения продукций. Эти исследования послужили теоретической основой для технологического комплекса СИНАП, успешно реализованного в ИАПУ ДВНЦ СССР.

Другой интересной формальной моделью СП являются К-системы, предложенные Кузнецовым В.Е.

Как уже было отмечено, одна из основных проблем при выводе в СП — это выбор соответствующих правил для применения. Замечено, что база продукций, представленная в виде сотен локальных правил, не описывает в явном виде отношение "общее-частное" над правилами. В К-системах введено отношение "общее-частное" над продукциями следующим образом: если q = {x_i/t_i} — подстановка, а р, q — продукции, и

p = qq,

где qq — это продукция, получаемая из q заменой всех вхождений переменных x_i на t­_i то продукция р является частным случаем продукции q, а q — обобщение продукции р.

В К-системах введено несколько типов обобщений: подстановочное, категориальный синтез, отбрасывание посылок, исследованы свойства этих обобщений. На основании этих понятий вводится понятие исключение из правила.

Правило р является исключением из q (a q — общее правило по отношению к р), если область определения правила р является строго частным случаем области определения правила q. В К-системах реализована (встроена) следующая стратегия выбора правил: исключения всегда имеют больший приоритет чем общие правила. Данная стратегия близка к стратегии, реализованной в языке РЕФАЛ [З].

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

Формальная модель СП, предложенная S.Vere [128], называется реляционной СП и определяется как пятерка

(C, V, L,s₀ , P).

Здесь С — множество констант (обозначаемых строчными буквами); V - конечное множество символов переменных, принимающих значения в области констант (обозначаются заглавными буквами); L — множество литералов вида (е₁ e₂ ... е_n) или Ø(e₁ e₂ . . . е_n), п ³ 1, е_i Î С È V; s₀

— начальная ситуация, определяемая как конъюнкция литералов; Р — конечное множество правил вида

,

где a — условие применимости (антецедент), b — следствие (консеквент), m — аспект (грань), a, b, m — конъюнкции литералов. Для того чтобы отделить аспект от антецедента, будем его подчеркивать в пра­вилах.

Продукции предназначены для описания всевозможных преобразова­ний исходной ситуации к некоторой ситуации s.

Продукция применима к ситуации s тогда и только тогда, когда aq Í s, где q — подходящая подстановка вида

{t₁/n₁, …, t_n/n_n},

где t_i — термы, u_i — переменные.

Например, пусть s = (асе)(bес). Продукция (асХ)( ) —> (саХ) при­менима к этой ситуации, так как

(асе) = (acX){e/X},(ace) Î s.

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