Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32



страница3/22
Дата07.11.2012
Размер1.2 Mb.
ТипКонспект
1   2   3   4   5   6   7   8   9   ...   22

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


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

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

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

  3. Конечное множество вычислимых отношений Ri (1, …, n, ) на множестве A*, называемых правилами вывода. В этом случае слово непосредственно выводимо из слов 1, …, n по правилу Ri.

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

Выводимость. Вывод формулы В из формул A1, A2, … , An – последовательность формул F1, F2, … , Fm = B, такая, что Fi (i=1,…, m) – либо аксиома, либо одна из формул A1, A2, … , An, либо непосредственно выводима из некоторого подмножества множества {F1, F2, … , Fi-1}по одному из правил вывода. Если существует вывод формулы В из формул A1, A2, … , An, то В выводима из A1, A2, … , An . Множество формул, выводимых из аксиом, называется теоремами теории.

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

Доказательство.

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

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

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

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


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

A= {a1,a2,…, an} – алфавит констант,

X= {x1, x2,…,xm} – алфавит переменных,

M= {M1, M2, …, Mk} – множество аксиом, Mi(AX)*,

R = {R1, R2, …, Rl} – множество продукций, имеющих вид 1, 2,…, j, где i, (AX)*, 1, 2,…,j называются посылками, – следствием (заключением).

Слова в (AX)* называются термами, слова в А* – просто словами.

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

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

Например, из acab , cabb применением продукции a x1 b, x1 b x2 b x2 (подстановка x1=ca, x2=b) непосредственно выводимо bb.

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

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

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

Теорема 2. Для любого перечислимого множества М слов в алфавите А существует каноническая система над А, множество теорем которой совпадает с М (доказательство с использованием машин Тьюринга приводится в [3]).
1   2   3   4   5   6   7   8   9   ...   22

Похожие:

Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconМетодические указания к практическим занятиям Рязань 2004 удк 519. 713 (075)
Теория автоматов в задачах. Ч1: Методические указания к практическим занятиям/ Рязан гос радиотехн акад. Сост.: Н. И. Иопа. Рязань,...
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconУчебное пособие для студентов всех специальностей Москва 2003 ббк 22. 17я7 удк 519. 22 (075. 8) 6Н1 к 60
Калинина В. Н., Соловьев В. И. Введение в многомерный статистический анализ: Учебное пособие / гуу. – М., 2003. – 92 с
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКонспект лекций москва 2003 ббк вкб / 075 : 378 я 14
История экономики России XX века (1900 – 1917 гг.) : Конспект лекций. – М.: Мгту "Станкин", 2003. – 45 с
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКонспект лекций санкт-петербург 2009 удк 532. 6(075. 8) Ббк в334я73 а 65 Рецензент И. П. Арешев
Охватывает ток (рис. 16), то
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКонспект лекций м осква 2000 ббк ВКП / 075 : 378 я 14
История экономики России XIX века: Конспект лекций. М.: Мгту "Станкин", 2000. 68 с
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКонспект лекций по философии Часть 1 Античная философия Новосибирск 2007 удк 101. 8 (075) ббк ю3я73-1
Савостьянов А. Н. Конспект лекций по философии / Новосиб гос ун-т. Новосибирск, 2007. Ч. Античная философия. 68 с
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconУчебное пособие для студентов всех специальностей Саратов 2009 удк 519. 17 Ббк 22. 174 С 32 Рецензенты
С32 Ведение в теорию графов: учеб пособие. Саратов: Сарат гос техн ун-т, 2009. 36с
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКонспект лекций Таганрог 2001 удк 621. 382. 019. 3 (075. 8) Механцев Е. Б
Обеспечение надежности электронных средств: конспект лекций. Таганрог: Изд-во трту, 2001
Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconКурс лекций Для студентов вузов Кемерово 2006 удк 113/119(075) ббк 87я7 М42 Рецензенты

Конспект лекций москва 2004 удк 519. 713(075)+519. 76(075) ббк 22. 18я7 С32 iconУчебное пособие Москва 2006 удк 341. 645: 347. 922(075) ббк 67. 412. 2 О 23

Разместите кнопку на своём сайте:
ru.convdocs.org


База данных защищена авторским правом ©ru.convdocs.org 2016
обратиться к администрации
ru.convdocs.org