3. Абстрактные формальные системы

Абстрактная формальная система – это

Алфавит А ( множество слов в этом алфавите –А*).

Разрешимое множество А₁  А*, элементы множестваА₁называют аксиомами.

Конечное множество вычислимых отношений R_i (₁, …, _n, ) на множествеA*, называемых правилами вывода. Говорят, что слово выводимо из слов₁, …, _nпо правилуR_i.

Аксиомы тоже могут быть заданы как унарные отношения, но это не всегда удобно.

Выводимость.Вывод формулы В из формулA₁,A₂, … ,A_n- последовательность формулF₁,F₂, … ,F_m=B, такая, чтоF_i(i=1,…m) либо аксиома, либо одна из формулA₁,A₂, … ,A_n, либо непосредственно выводима изF₁,F₂, … ,F_i-1 по одному из правил вывода. Если существует вывод формулы В из формулA₁,A₂, … ,A_n, то В выводима изA₁,A₂, … ,A_n . Множество формул, выводимых из аксиом, называется теоремами теории.

Теорема.Для любой формальной теории множество выводимых в ней слов перечислимо.

Док-во:

А** -множество всех конечных последовательностей₁, …, _n, где_i - слова в алфавите А. А** - перечислимо. Из-за разрешимости множества аксиом и вычислимости правил вывода по любой последовательности можно эффективно узнать, является ли она выводом в данной формальной системе (FS).

Если в процессе перечисления А** отбрасывать все последовательности, не являющиеся выводами, то получаем перечисление множества выводов последних слов выводов.

 множество слов (формул), выводимых в произвольной формальной системе, перечислимо.

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

Каноническая система <A,X,M,R>

A= {a₁,a₂,…,a_n} – алфавит констант,

X= {x₁,x₂,…,x_m} – алфавит переменных,

M= {M₁,M₂, …,M_k} – множество аксиом,M_i(AX)*,

R= {R₁,R₂, …,R_l} – множество продукций, имеющих вид

₁,₂,…,_j,_i,(AX)*,₁,₂,…,_jназываются посылками,- следствием.

Слова в (AX)* называются термами, слова в А* - просто словами.

Слово называется применением аксиомы, еслиполучается изподстановкой слов вместо переменных.

Слово непосредственно выводимо из₁, …,_nприменением продукцииR, если существует подстановка слов вместо переменных в продукциюR, которая посылки превратит в₁, …,_n, а заключение – в.

Например, из acb , cabbприменением продукцииa x₁ b, x₁ b x₂  b x₂(подстановкаx₁=ca, x₂=b) непосредственно выводимоbb.

Выводимость – транзитивное и рефлексивное замыкание непосредственной выводимости.

Доказуемо (теорема формальной системы ) - выводимо из множества аксиом.

Например, <{I}, {x}, {I}, {xxII}> позволяет построить множество нечетных чисел в унарном представлении.

Теорема. Для любого перечислимого множества М слов в алфавите А существует каконическая система над А, множество теорем которой совпадает с М.

(доказательство, с использованием МТ, приводится в [3])

4. Формальные порождающие грамматики

Порождающей грамматикой называется упорядоченная четверка G=< V_T,V_N, S, R>, гдеV_T -алфавит терминальных или основных символов;V_N — алфавит нетерминальных или вспомогательных символов(V_TV_N =  ); S - начальный символ или аксиома,S V_N, R -конечное множество правил или продукций вида, где(V_TV_N )* V_N (V_TV_N )*, (V_TV_N )* - различные цепочки, аспециальный символ, не принадлежащий V_TV_N и служащий для отделения левой части правилаот правой. Такие символы, которые служат для описания языка, но не принадлежат самому языку, будем называть метасимволами. Го­ворят, что цепочка ₁непосредственно выводима из цепочки₀ (обозначается₀₁), если существуют такие₁, ₂, , , что ₀₁  ₂, ₁₁  ₂ и существует правило ( R). Иными словами ₀₁ , если в₀найдется вхождение левой части какого-либо пра­вила грамматики, а цепочка₁получена заменой этого вхож­дения на правую часть правила. Существенно, что при опреде­лении отношения непосредственной выводимости обозначаемого(разумеется, также метасимвол) мы не указываем, какое правило нужно применять и к какому именно вхождению (если их несколько). Здесь проявляются характерные черты ис­числений, к классу которых относятся и порождающие грамма­тики. Исчисления представляют собой "разрешения" в отличие от алгоритмов, являющихся "предписаниями".

Говорят, что цепочка _nвыводима из цепочки ₀ за один или несколько шагов или просто выводима (обозначается₀⁺_n),если существует последовательность цепочек₁, ₂,…, _n(n>0), такая, что _i_i+1, i{0,…n}. Эта последовательность называется выводом _nиз ₀, аn– длиной вывода. Выводимость заnшагов иногда обозначается₀ⁿ _nНа­конец, если ₀⁺_nили ₀=_n, то пишут ₀*_n.

Нетрудно видеть, что ⁺есть транзитивное, а* - транзитивно-рефлексивное замыкание отношения .

Цепочка  называется сентенциальной формой, если она совпадает или выводима из начального символа грамматики, т.е. если S   ,

Множество цепочек в основном алфавите грамматики, вы­водимых из начального символа, иначе множество сентенциаль­ных форм, состоящих из терминальных символов, называется языком, порождаемым грамматикой G, и обозначаетсяL(G).

L(G) = {x / S * x & xV_T }.

Для любого перечислимого множества слов М существует грамматика G, такая, что М=L(G).

Говорят, что грамматики G₁ иG₂эквивалентны, еслиL(G₁ )=L(G₂).

Например,

G₁ = < {S}, {a}, S, { Sa, S a a S}>

L(G₁)= {a ²ⁿ⁺¹, n 0}

G₂ = < {S, A}, {0, 1}, S, R>

R = {S  1 A, A  1 A, A  0 A, A 0 }

L(G₂) – множество четных двоичных чисел, больших нуля.

G₃ = < {S, A}, {0, 1}, S, R>

R = {S  1 A 0, A  1 A, A  0 A, A  }

L(G₂) = L(G₃)

Для сокращения записи грамматик и выводов будем изо­бражать нетерминальные символы прописными буквами латин­ского алфавита А , В , С , … , Sтерминальные -строчными буквами a, b, c,…и цифрами. Прописными буквамиU, V, Z будем обозначать символы, которые могут быть как терминальными, так и нетерминальными; строчными буквами u, v, z cиндексами или без них - цепочки, составленные из терминальных сим­волов, а буквами …- из любых символов. Кроме того, для обозначения правил

₁

₂

_………..

_n

будем пользоваться записью ₁₂…_n .

Правила вида , где V_T, называются заключительными.