Введение

Последовательность слов, сформированных по определенным правилам, – технический термин в математике и информатике.

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

История

В 17 веке Готфрид Лейбниц представил и описал *characteristica universalis* – универсальный и формальный язык, который использовал пиктограммы. Позже Карл Фридрих Гаус исследовал проблему гаусовских кодов. Готтлоб Фреге попытался реализовать идеи Лейбница посредством нотационной системы, впервые представленной в "Begriffsschrift" (1879) и более полно разработанной в его двухтомном труде "Grundgesetze der Arithmetik" (1893/1903). В этом труде описывался «формальный язык чистого мышления». В первой половине 20-го века было сделано несколько разработок, имеющих отношение к формальным языкам. Аксель Тью опубликовал четыре статьи, касающиеся слов и языка, в период с 1906 по 1914 год. Последняя из них представила то, что Эмиль Пост позже назвал «Системами Тью», и привела ранний пример неразрешимой задачи. Позже Пост использовал эту статью в качестве основы для доказательства 1947 года о том, что «проблема слов для полугрупп рекурсивно неразрешима», и впоследствии разработал каноническую систему для создания формальных языков. В 1907 году Леонардо Торрес Кеведо представил в Вене формальный язык для описания механических чертежей (механизмов). Он опубликовал работу «Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas» («О системе обозначений и символов, предназначенных для облегчения описания машин»). Хайнц Земанек оценил её как эквивалент языка программирования для числового программного управления станками. Ноам Хомский разработал абстрактное представление формальных и естественных языков, известное как иерархия Хомского. В 1959 году Джон Бэкус разработал форму Бэкуса — Наура для описания синтаксиса языка программирования высокого уровня, опираясь на свой опыт создания FORTRAN. Питер Наур был секретарем/редактором отчета ALGOL60, в котором он использовал форму Бэкуса — Наура для описания формальной части ALGOL60.

Слова по алфавиту

Алфавит, в контексте формальных языков, может быть любым множеством; его элементы называются буквами. Алфавит может содержать бесконечное число элементов; например, логика первого порядка часто выражается с помощью алфавита, который, помимо символов, таких как ∧, ¬, ∀ и скобок, содержит бесконечно много элементов x0, x1, x2, которые выполняют роль переменных. Однако большинство определений в теории формальных языков оперируют алфавитами с конечным числом элементов, и многие результаты применимы только к ним. Часто целесообразно использовать алфавит в обычном смысле этого слова, или, в более общем случае, любое конечное кодирование символов, такое как ASCII или Unicode. Словом над алфавитом называется любая конечная последовательность (то есть строка) букв. Множество всех слов над алфавитом Σ обычно обозначается Σ* (с использованием звезды Клине). Длина слова – это количество букв, из которых оно состоит. Для любого алфавита существует только одно слово нулевой длины, пустое слово, которое часто обозначается e, ε, λ или даже Λ. С помощью конкатенации можно объединить два слова, чтобы сформировать новое слово, длина которого равна сумме длин исходных слов. Результат конкатенации слова с пустым словом – это исходное слово. В некоторых приложениях, особенно в логике, алфавит также известен как словарь, а слова – как формулы или предложения; это нарушает метафору буква/слово и заменяет её метафорой слово/предложение.

Определение

Формальный язык L над алфавитом Σ является подмножеством Σ*, то есть множеством слов, составленных из символов этого алфавита. Иногда эти слова объединяются в выражения, при этом могут быть сформулированы правила и ограничения для создания "корректных выражений". В информатике и математике, где обычно не рассматриваются естественные языки, прилагательное "формальный" часто опускается как избыточное. Хотя теория формальных языков обычно изучает языки, описываемые синтаксическими правилами, само определение понятия "формальный язык" заключается лишь в следующем: (возможно, бесконечное) множество строк конечной длины, составленных из заданного алфавита, и ничего больше. На практике существует множество языков, которые можно описать с помощью правил, например, регулярные или контекстно-свободные языки. Понятие формальной грамматики может быть ближе к интуитивному представлению о "языке", определяемому синтаксическими правилами. В силу некоторой вольности в определении, конкретный формальный язык часто рассматривается вместе с формальной грамматикой, которая его описывает.

Языки программирования

Компилятор обычно состоит из двух отдельных компонентов. Лексический анализатор, иногда генерируемый инструментом вроде lex, определяет лексемы (токены) грамматики языка программирования, например, идентификаторы или ключевые слова, числовые и строковые литералы, знаки препинания и символы операторов, которые сами определяются более простым формальным языком, обычно с помощью регулярных выражений. На самом базовом концептуальном уровне, парсер, иногда генерируемый генератором парсеров вроде yacc, пытается определить, является ли исходная программа синтаксически корректной, то есть соответствует ли она грамматике языка программирования, для которого был разработан компилятор. Разумеется, компиляторы выполняют больше, чем просто разбор исходного кода – они обычно преобразуют его в исполняемый формат. В связи с этим, парсер обычно выдает не просто ответ "да/нет", а, как правило, абстрактное синтаксическое дерево. Оно используется последующими этапами компиляции для генерации исполняемого файла, содержащего машинный код, который выполняется непосредственно на аппаратном обеспечении, или промежуточного кода, требующего виртуальную машину для исполнения.

Формальные теории, системы и доказательства

В математической логике формальная теория — это множество предложений, выраженных на формальном языке. Формальная система (также называемая логическим исчислением или логической системой) состоит из формального языка вместе с дедуктивным аппаратом (также называемым дедуктивной системой). Дедуктивный аппарат может состоять из набора правил преобразования, которые могут интерпретироваться как корректные правила вывода, или набора аксиом, или включать и то, и другое. Формальная система используется для вывода одного выражения из одного или нескольких других выражений. Хотя формальный язык можно отождествлять с его формулами, формальную систему нельзя отождествлять с её теоремами. Две формальные системы могут иметь один и тот же набор теорем, но при этом различаться в каком-либо существенном теоретико-доказательном отношении (например, формула A может быть синтаксическим следствием формулы B в одной системе, но не в другой). Формальное доказательство или вывод — это конечная последовательность правильно сформированных формул (которые могут интерпретироваться как предложения или высказывания), каждая из которых является аксиомой или следует из предшествующих формул в последовательности по правилу вывода. Последняя формула в последовательности является теоремой формальной системы. Формальные доказательства полезны, поскольку их теоремы могут интерпретироваться как истинные утверждения.

Интерпретации и модели

Формальные языки по своей природе полностью синтаксичны, но им может быть придана семантика, наделяющая элементы языка смыслом. Например, в математической логике множество возможных формул конкретной логики является формальным языком, а интерпретация присваивает значение каждой из этих формул — как правило, значение истинности. Изучение интерпретаций формальных языков называется формальной семантикой. В математической логике это часто осуществляется в рамках теории моделей. В теории моделей термины, встречающиеся в формуле, интерпретируются как объекты в математических структурах, а фиксированные композиционные правила интерпретации определяют, каким образом значение истинности формулы может быть выведено из интерпретации её терминов; модель для формулы — это интерпретация терминов, при которой формула становится истинной.