Формальный язык

В логике , математике , информатике и лингвистике формальный язык состоит из слов , буквы которых взяты из алфавита и правильно сформированы в соответствии с определенным набором правил, называемым формальной грамматикой .

Алфавит формального языка состоит из символов, букв или токенов , которые объединяются в строки, называемые словами. ^[1] Слова, принадлежащие определенному формальному языку, иногда называются правильно сформированными словами или правильно сформированными формулами . Формальный язык часто определяется посредством формальной грамматики, такой как регулярная грамматика или контекстно-свободная грамматика , которая состоит из правил ее формирования .

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

Область формальной теории языка изучает в первую очередь чисто синтаксические аспекты таких языков, то есть их внутренние структурные модели. Формальная теория языка возникла из лингвистики как способ понимания синтаксических закономерностей естественных языков .

История

В 17 веке Готфрид Лейбниц придумал и описал characteristicsa universalis , универсальный и формальный язык, который использовал пиктограммы . Позже Карл Фридрих Гаусс исследовал проблему кодов Гаусса . ^[2]

Готтлоб Фреге попытался реализовать идеи Лейбница с помощью системы обозначений, впервые изложенной в Begriffsschrift (1879) и более полно разработанной в его двухтомном труде Grundgesetze der Arithmetik (1893/1903). ^[3] В нем описывался «формальный язык чистого языка». ^[4]

В первой половине 20-го века было сделано несколько разработок, имеющих отношение к формальным языкам. Аксель Туэ опубликовал четыре статьи, касающиеся слов и языка, между 1906 и 1914 годами. Последняя из них представила то, что Эмиль Пост позже назвал «Системами Туэ», и привела ранний пример неразрешимой проблемы . ^[5] Позже Пост использовал эту статью в качестве основы для доказательства 1947 года, «что проблема слов для полугрупп была рекурсивно неразрешима», ^[6] и позже разработал каноническую систему для создания формальных языков.

В 1907 году Леонардо Торрес Кеведо ввел формальный язык для описания механических чертежей (механических устройств) в Вене . Он опубликовал "Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las máquinas" ("О системе обозначений и символов, предназначенных для облегчения описания машин"). ^[7] Хайнц Земанек оценил его как эквивалент языка программирования для числового управления станками. ^[8]

Ноам Хомский разработал абстрактное представление формальных и естественных языков, известное как иерархия Хомского . ^[9] В 1959 году Джон Бэкус разработал форму Бэкуса-Наура для описания синтаксиса языка программирования высокого уровня, следуя своей работе по созданию FORTRAN . ^[10] Питер Наур был секретарем/редактором отчета ALGOL60, в котором он использовал форму Бэкуса-Наура для описания формальной части ALGOL60.

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

Алфавитом в контексте формальных языков может быть любой набор ; его элементы называются буквами . Алфавит может содержать бесконечное число элементов; ^{[примечание 1] однако большинство определений в теории формального языка указывают алфавиты с конечным числом элементов, и многие}результаты применимы только к ним. Часто имеет смысл использовать алфавит в обычном смысле этого слова или, в более общем смысле, любую конечную кодировку символов , такую как ASCII или Unicode .

Слово в алфавите может быть любой конечной последовательностью (т. е. строкой ) букв. Множество всех слов в алфавите Σ обычно обозначается как Σ ^* (используя звезду Клини ). Длина слова — это количество букв, из которых оно состоит. Для любого алфавита существует только одно слово длины 0, пустое слово , которое часто обозначается как e, ε, λ или даже Λ. С помощью конкатенации можно объединить два слова, чтобы сформировать новое слово, длина которого равна сумме длин исходных слов. Результатом конкатенации слова с пустым словом является исходное слово.

В некоторых приложениях, особенно в логике , алфавит также известен как словарь , а слова известны как формулы или предложения ; это разрушает метафору буква/слово и заменяет ее метафорой слово/предложение.

Определение

Формальный язык L над алфавитом Σ является подмножеством Σ ^* , то есть набором слов над этим алфавитом. Иногда наборы слов группируются в выражения, тогда как правила и ограничения могут быть сформулированы для создания «правильно сформированных выражений».

В информатике и математике, которые обычно не имеют дела с естественными языками , прилагательное «формальный» часто опускается как избыточное.

В то время как формальная теория языка обычно занимается формальными языками, которые описываются некоторыми синтаксическими правилами, фактическое определение понятия «формальный язык» только как указано выше: (возможно, бесконечное) множество строк конечной длины, составленных из заданного алфавита, не больше и не меньше. На практике существует множество языков, которые можно описать правилами, например, регулярные языки или контекстно-свободные языки . Понятие формальной грамматики может быть ближе к интуитивному понятию «языка», описываемого синтаксическими правилами. Из-за злоупотребления определением часто считается, что конкретный формальный язык сопровождается формальной грамматикой, которая его описывает.

Примеры

Следующие правила описывают формальный язык $L$ над алфавитом Σ = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, +, =}:

Каждая непустая строка, не содержащая «+» или «=» и не начинающаяся с «0», содержится в $L$ .
Строка «0» находится в $L.$
Строка, содержащая «=», содержится в $L$ тогда и только тогда , когда существует ровно один «=», и он разделяет две допустимые строки $L.$
Строка, содержащая «+», но не содержащая «=», содержится в $L$ тогда и только тогда, когда каждый «+» в строке разделяет две допустимые строки $L$ .
$В языке L$ нет других строк, кроме тех, которые подразумеваются предыдущими правилами.

Согласно этим правилам, строка "23+4=555" находится в $L$ , а строка "=234=+" - нет. Этот формальный язык выражает натуральные числа , правильно сформированные сложения и правильно сформированные равенства сложения, но он выражает только то, как они выглядят (их синтаксис ), а не то, что они означают ( семантика ). Например, нигде в этих правилах нет никаких указаний на то, что "0" означает число ноль, "+" означает сложение, "23+4=555" ложно и т. д.

Конструкции

Для конечных языков можно явно перечислить все правильно сформированные слова. Например, мы можем описать язык $L$ как $L$ = {a, b, ab, cba}. Вырожденный случай этой конструкции — пустой язык , который вообще не содержит слов ( $L$ = ∅ ).

Однако даже над конечным (непустым) алфавитом, таким как Σ = {a, b}, существует бесконечное число слов конечной длины, которые потенциально могут быть выражены: "a", "abb", "ababba", "aaababbbbaab", .... Поэтому формальные языки, как правило, бесконечны, и описание бесконечного формального языка не так просто, как написание L = {a, b, ab, cba}. Вот несколько примеров формальных языков:

$L$ = Σ ^* , множество всех слов над Σ;
$L$ = {a} ^* = {a ⁿ }, где n принимает значения в диапазоне натуральных чисел, а «a ⁿ » означает «a», повторенное n раз (это набор слов, состоящий только из символа «a»);
набор синтаксически правильных программ на данном языке программирования (синтаксис которого обычно определяется контекстно -свободной грамматикой );
набор входных данных, на которых останавливается определенная машина Тьюринга ; или
набор максимальных строк буквенно-цифровых символов ASCII в этой строке, т. е.
набор {набор, максимальных, строк, буквенно-цифровых, символов ASCII, на, этой, строке, i, e}.

Формализмы спецификации языка

Формальные языки используются в качестве инструментов во многих дисциплинах. Однако формальная теория языка редко занимается конкретными языками (за исключением примеров), а в основном занимается изучением различных типов формализмов для описания языков. Например, язык может быть задан как

эти строки генерируются некоторой формальной грамматикой ;
те строки, которые описаны или сопоставлены с определенным регулярным выражением ;
те строки, которые принимаются некоторым автоматом , например, машиной Тьюринга или конечным автоматом ;
те строки, для которых некоторая процедура принятия решения ( алгоритм , который задает последовательность связанных вопросов ДА/НЕТ) дает ответ ДА.

Типичные вопросы, задаваемые о подобных формализмах, включают в себя:

Какова их выразительная сила? (Может ли формализм X описать каждый язык, который может описать формализм Y ? Может ли он описать другие языки?)
Какова их узнаваемость? (Насколько сложно решить, принадлежит ли данное слово языку, описываемому формализмом X ?)
Какова их сопоставимость? (Насколько сложно решить, являются ли два языка, один из которых описан в формализме X , а другой — в формализме Y , или снова в X , на самом деле одним и тем же языком?).

Удивительно часто ответом на эти проблемы принятия решений является «это вообще невозможно сделать» или «это чрезвычайно дорого» (с характеристикой того, насколько дорого). Таким образом, формальная теория языка является основной областью применения теории вычислимости и теории сложности . Формальные языки могут быть классифицированы в иерархии Хомского на основе выразительной силы их порождающей грамматики, а также сложности их распознающего автомата . Контекстно-свободные грамматики и регулярные грамматики обеспечивают хороший компромисс между выразительностью и простотой синтаксического анализа и широко используются в практических приложениях.

Операции над языками

Некоторые операции над языками являются общими. Сюда входят стандартные операции над множествами, такие как объединение, пересечение и дополнение. Другой класс операций — поэлементное применение строковых операций.

Примеры: предположим, что и — это языки с некоторым общим алфавитом . $L_{1}$ $L_{2}$ $\Сигма$

Конкатенация состоит из всех строк вида , где — строка из , а — строка из . $L_{1}\cdot L_{2}$ $vw$ $v$ $L_{1}$ $w$ $L_{2}$
Пересечение и состоит из всех строк, которые содержатся в обоих языках . $L_{1}\cap L_{2}$ $L_{1}$ $L_{2}$
Дополнение относительно состоит из всех строк свыше , которые не входят в . $\neg L_{1}$ $L_{1}$ $\Сигма$ $\Сигма$ $L_{1}$
Звезда Клини : язык, состоящий из всех слов, которые являются конкатенациями нуля или более слов исходного языка;
Обратное :
- Пусть ε — пустое слово, тогда и $\varepsilon ^{R}=\varepsilon$
- для каждого непустого слова (где — элементы некоторого алфавита), пусть , $w=\sigma _{1}\cdots \sigma _{n}$ $\sigma _{1},\ldots ,\sigma _{n}$ $w^{R}=\sigma _{n}\cdots \sigma _{1}$
- тогда для формального языка , . $L$ $L^{R}=\{w^{R}\mid w\in L\}$
Гомоморфизм строк

Такие строковые операции используются для исследования свойств замыкания классов языков. Класс языков замкнут относительно определенной операции, когда операция, примененная к языкам в классе, всегда снова производит язык в том же классе. Например, известно, что контекстно-свободные языки замкнуты относительно объединения, конкатенации и пересечения с обычными языками , но не замкнуты относительно пересечения или дополнения. Теория трио и абстрактных семейств языков изучает наиболее общие свойства замыкания языковых семейств по их собственному праву. ^[11]

Приложения

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

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

Конечно, компиляторы делают больше, чем просто анализируют исходный код — они обычно переводят его в некий исполняемый формат. Из-за этого синтаксический анализатор обычно выводит больше, чем ответ «да/нет», обычно абстрактное синтаксическое дерево . Это используется последующими этапами компилятора, чтобы в конечном итоге сгенерировать исполняемый файл, содержащий машинный код , который выполняется непосредственно на оборудовании, или некоторый промежуточный код , который требует виртуальной машины для выполнения.

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

В математической логике формальная теория — это набор предложений, выраженных на формальном языке.

Формальная система (также называемая логическим исчислением или логической системой ) состоит из формального языка вместе с дедуктивным аппаратом (также называемым дедуктивной системой ). Дедуктивный аппарат может состоять из набора правил преобразования , которые могут интерпретироваться как допустимые правила вывода, или набора аксиом , или иметь и то, и другое. Формальная система используется для вывода одного выражения из одного или нескольких других выражений. Хотя формальный язык можно идентифицировать по его формулам, формальная система не может быть также идентифицирована по ее теоремам. Две формальные системы и могут иметь все те же теоремы и все же отличаться некоторым существенным теоретическим способом доказательства (например, формула A может быть синтаксическим следствием формулы B в одном, но не в другом). ${\mathcal {FS}}$ ${\mathcal {FS'}}$

Формальное доказательство или вывод — это конечная последовательность правильно сформированных формул (которые могут быть интерпретированы как предложения или суждения ), каждое из которых является аксиомой или следует из предыдущих формул в последовательности по правилу вывода . Последнее предложение в последовательности — теорема формальной системы. Формальные доказательства полезны, потому что их теоремы могут быть интерпретированы как истинные суждения.

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

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

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

Смотрите также

Примечания

^ Например, логика первого порядка часто выражается с помощью алфавита, который, помимо таких символов, как ∧, ¬, ∀ и скобок, содержит бесконечно много элементов x ₀ , x ₁ , x ₂ , …, которые играют роль переменных.

Ссылки

Цитаты

^ См. например, Reghizzi, Stefano Crespi (2009). Формальные языки и компиляция. Тексты по информатике. Springer. стр. 8. Bibcode :2009flc..book.....C. ISBN 9781848820500. Алфавит — это конечное множество
^ «В предыстории формальной теории языка: языки Гаусса». Январь 1992 г. Получено 30 апреля 2021 г.
^ "Готтлоб Фреге". 5 декабря 2019 года . Проверено 30 апреля 2021 г.
^ Мартин Дэвис (1995). «Влияние математической логики на информатику». В Рольфе Херкене (ред.). Универсальная машина Тьюринга: обзор за полвека . Springer. стр. 290. ISBN 978-3-211-82637-9.
^ "Работа Туэ 1914 года: перевод" (PDF) . 28 августа 2013 г. Архивировано (PDF) из оригинала 30 апреля 2021 г. . Получено 30 апреля 2021 г. .
^ "Emil Leon Post". Сентябрь 2001 г. Получено 30 апреля 2021 г.
^ Торрес Кеведо, Леонардо. Sobre un sistema de notaciones y símbolos destinados a facilitar la descripción de las maquinas, (pdf), стр. 25–30, Revista de Obras Públicas, 17 января 1907 г.
^ Брудерер, Герберт (2021). «Глобальная эволюция компьютерных технологий». Вехи в аналоговых и цифровых вычислениях . Springer. стр. 1212. ISBN 978-3030409739.
^ Ягер, Герхард; Роджерс, Джеймс (19 июля 2012 г.). «Формальная теория языка: уточнение иерархии Хомского». Philosophical Transactions of the Royal Society B . 367 (1598): 1956–1970. doi :10.1098/rstb.2012.0077. PMC 3367686 . PMID 22688632.
^ "Джон Уорнер Бэкус". Февраль 2016 г. Получено 30 апреля 2021 г.
^ Хопкрофт и Ульман (1979), Глава 11: Замкнутые свойства семейств языков.

Источники

Цитируемые работы

Хопкрофт, Джон Э .; Ульман, Джеффри Д. (1979). Введение в теорию автоматов, языки и вычисления . Рединг, Массачусетс: Addison-Wesley Publishing. ISBN 81-7808-347-7.

Общие ссылки

А. Гамильтон, Логика для математиков , Cambridge University Press , 1978, ISBN 0-521-21838-1 .
Сеймур Гинзбург , Алгебраические и автоматные теоретические свойства формальных языков , Северная Голландия, 1975, ISBN 0-7204-2506-9 .
Майкл А. Харрисон , Введение в формальную теорию языка , Эддисон-Уэсли, 1978.
Раутенберг, Вольфганг (2010). Краткое введение в математическую логику (3-е изд.). Нью-Йорк: Springer Science+Business Media . doi :10.1007/978-1-4419-1221-3. ISBN 978-1-4419-1220-6.
Гжегож Розенберг , Арто Саломаа , Справочник по формальным языкам: Том I–III , Springer, 1997, ISBN 3-540-61486-9 .
Патрик Суппес, Введение в логику , Д. Ван Ностранд, 1957, ISBN 0-442-08072-7 .

Внешние ссылки

«Формальный язык», Энциклопедия математики , EMS Press , 2001 [1994]
Университет Мэриленда , Формальные определения языка
Джеймс Пауэр, «Заметки о формальной теории языка и синтаксическом анализе». Архивировано 21 ноября 2007 г. на Wayback Machine , 29 ноября 2002 г.
Черновики некоторых глав в «Справочнике по формальной теории языка», том 1–3, Г. Розенберг и А. Саломаа (ред.), Springer Verlag , (1997):
- Александру Матееску и Арто Саломаа, «Предисловие» в томе 1, стр. v – viii, и «Формальные языки: введение и краткий обзор», глава 1 в томе. 1, стр. 1–39.
- Шэн Юй, «Регулярные языки», Глава 2 в томе 1
- Жан-Мишель Отебер, Жан Берстель, Люк Боассон, «Контекстно-свободные языки и автоматы с магазинной памятью», Глава 3 в томе 1
- Кристиан Чоффрут и Юхани Кархумяки, «Комбинаторика слов», глава 6 в томе. 1
- Теро Харью и Юхани Кархумяки, «Морфизмы», глава 7 в томе. 1, стр. 439–510.
- Жан-Эрик Пэн, «Синтаксические полугруппы», Глава 10 в томе 1, стр. 679–746
- М. Крохмор и К. Ханкарт, «Автоматы для сопоставления шаблонов», Глава 9 в томе 2
- Дора Джаммаррези, Антонио Рестиво, «Двумерные языки», глава 4 в томе. 3, стр. 215–267.