Исторически формальные системы создавались с конкретной целью более точного обоснования методов построения математических теорий. Однако стало ясно, что на основе тех же принципов - исходного набора аксиом, правил вывода и понятия выводимости - можно описывать не только множества выражений, интерпретируемых как высказывания, но и перечислимые множества объектов произвольного вида.
Основы теории таких формальных систем были заложены Постом. Эту теорию можно назвать абстрактной или общей, так как она не рассматривает свойства формальных систем относительно их конкретных интерпретаций, а изучает лишь их внутренние, синтаксические свойства.
В отличие от логических исчисленй в формальных системах не выделяется понятие формулы, их объекты – произвольные слова в фиксированном алфавите.
Итак, формальная система FS определяется:
1. алфавитом А (множество всех слов в алфавите А обозначим А*);
2. разрешимым множеством А1А*, элементы которого называются аксиомами;
3. конечным множеством вычислимых отношений Ri(1,...n,) на множестве А*, называемых правилами вывода.
Слово называется выводимым из 1,...n по правилу Ri. Понятия вывода, выводимости и доказательства те же что и для формальных теорий.
Языки и грамматики
Общие понятия(Марышев)
Формальные системы приобретают все большее значение при проектировании, реализации и изучении языков программирования. Формальные системы используются для описания синтаксиса языка программирования. Такое описание играет важную роль как для пользователя, так и для создателя компиляторов. Пользователь нуждается в ясном описании языка. Создатель компилятора сталкивается с проблемами мобильности и сопровождения. Если один и тот же язык должен быть реализован на различных машинах, то допустимые строки языка должны быть так определены, чтобы их представление на пользовательском уровне было инвариантным (насколько это возможно).
Формальные системы используются для синтаксически-ориен-тированной компиляции (COK). СОК используют базу данных, содержащую синтаксические правила исходного языка, для проведения грамматического разбора.
Поскольку число языков программирования и вычислительных машин постоянно растет, возрастает и необходимость в автоматизации процесса создания компиляторов. Для этого требуется формальное описание как исходного языка, так и выходного. Аналогичной проблемой является проблема генерирования тестовых программ для проверки языкового процессора. Это может быть весьма полезным при проверке программного обеспечения, поскольку машина может выполнить более скурпулезную проверку, чем человек.
Формальные системы используются для изучения сложности языков программирования и компиляторов. Создатели и языка и компилятора хотят знать, какие свойства языка наиболее существенным образом увеличивают в компиляторе сложность фазы распознавания. Создатель компилятора, кроме того, хочет иметь некоторую основу для оценки производительности компилятора.
Формальные системы используются при попытках доказательства эквивалентности и правильности программ. Формальные системы создают почву для анализа и сравнения различных языков. Они помогают ответить на такие вопросы: что является базовыми элементами языка, какие конструкции допустимы в языке, как можно комбинировать элементы языка для построения новых конструкций, какие классы задач могут быть запрограммированы на этом языке, какова стоимость и трудность написания программ.
Язык можно представить как некоторое множество предложений или формул – строк символов – с корректно определенной структурой и, обычно, со значением. Правила определяющие допустимые конструкции языка, составляют его синтаксис.
Если бы все языки состояли из конечного числа допустимых предложений или формул, проблема описания синтаксиса не стояла бы: достаточно было бы просто перечислить все допустимые предложения – строка символов являлась бы предложением языка только в том случае, если бы она попадала в список допустимых.
Однако в этом нет необходимости, если любой элемент списка может быть сгенерирован, когда это необходимо, даже если генерация всех предложений является процессом бесконечным. Если существует алгоритм, который будет последовательно порождать правильные строки, любая строка будет отнесена к языку, если только она когда-либо появляется в генерируемом описании. Такой алгоритм называется порождающим описанием языка.
Для описания языка можно использовать и другой тип алгоритма: в этом случае проверяемая строка выступает в виде исходных данных в разрешающем алгоритме. После необходимых вычислений вырабатывается ответ "да, строка правильная" или "нет, строка неправильная".
Такое определение языка называется аналитическим. Язык с аналити-ческим описанием разрешим, если анализатор для каждой входной строки завершает свою работу за конечное число шагов.
Естественный язык не подходит для формального описания из-за его неопределенности. Компьютер не воспримет программу написанную на не до конца формализованном языке.
Самым элементарным объектом является символ. Символы соединяются друг с другом в строки, которые могут принадлежать языку или нет.
Алфавит Т – есть конечное множество символов. Строка – конкатенация символов. Обозначим Т* – класс всех возможных конечных строк алфавита Т. – нулевая или пустая строка. Обычно из всех возможных строк только вполне определенные являются правильными формулами языка.
Язык L есть подмножество множества конечных строк в алфавите Т
L T*.
Формальные грамматики
Терминальные символы – это символы алфавита Т. Нетерминальные символы образуют множество символов N, не входящих в Т и использующиеся на промежуточных шагах порождающего процесса.
Начальным символом называется нетерминальный символ, из которого выводятся все строки языка.
Сам по себе порождающий процесс состоит в применении на каждом шагу одного из правил преобразований или продукции. Этот процесс преобразует заданную строку в новую строку; процесс заканчивается либо когда ни одна из продукций не может быть применена, либо когда строка состоит из одних термальных символов.
Формальная грамматика G есть четверка G=(N,T,E,P), где N – множество нетерминальных символов, T – множество терминальных символов, E – начальный символ, P – множество продукций, и 
Каждая новая строка в процессе вывода должна получаться из уже выведенной строки применением продукции.
Предложение – это строка, состоящая только из терминальных символов, выводимая из начального символа.
Язык L, определяемый грамматикой G, есть множество предложений, выводимых в G из L: 
.
Иерархия языков
Продукции позволяют осуществлять самые pазные трансформации строк. Чаще всего языки делят на четыре типа, в зависимости от ограничений, налагаемых на грамматику.
В наиболее общем типе грамматике на продукции не накладывается никаких ограничений. В частности, допустимы продукции, исключающие символы. И на промежуточных шагах допустимы изменения и укорачивания строк. Грамматика без ограничений называется грамматикой типа 0.
Простейшим ограничением является требование, чтобы правая часть каждой продукции имела по крайней мере столько же символов, что и левая. Грамматика такого вида называется грамматикой типа 1 или неукорачивающей контекстно-зависимой грамматикой.
Если левая часть продукции ограничивается одним нетерминальным символом, то ее применение не зависит от контекста, в котором этот символ появляется в исходной строке. Грамматика с таким ограничением называется грамматикой типа 2 или контекстно-свободной грамматикой.
Третий тип ограничений, накладываемых на продукции, ограничивает число терминальных и нетерминальных символов на каждом шаге вывода.
Когда не более чем один нетерминальный символ используется как в правой, так и в левой части продукции, то такая продукция называется линейной. Если нетерминал находится справа от всех символов правой части, такая продукция называется праволинейной. Если нетерминал находится левее всех других символов, то продукция называется леволинейной. Грамматика называется праволинейной, если каждая из ее продукций является праволинейной.
Язык называется регулярным, если он может быть порожден праволинейной или леволинейной грамматикой.