Официальный язык

Эта статья о техническом термине в математике и информатике. Информацию о любом формальном типе использования языка см. в разделе «Литературный язык» . Для изучения естественных языков см. Формальную семантику (естественный язык) .

Структура синтаксически правильного, хотя и совершенно бессмысленного, английского предложения «Бесцветные зеленые идеи яростно спят» ( исторический пример из Хомского, 1957).

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

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

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

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

История

В 17 веке Готфрид Лейбниц придумал и описал «characterica Universalis» , универсальный и формальный язык, в котором использовались пиктограммы . Позже Карл Фридрих Гаусс исследовал проблему кодов Гаусса .

Готтлоб Фреге попытался реализовать идеи Лейбница с помощью системы обозначений, впервые изложенной в Wortschrift (1879) и более полно развитой в его двухтомных «Основных законах арифметики» (1893/1903). Это описывало «формальный язык чистого языка».

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

В 1907 году Леонардо Торрес Кеведо ввёл формальный язык описания механических чертежей (механических устройств) в Вене . Я опубликовал «О системе обозначений и символов, предназначенных для облегчения описания машин». Хайнц Земанек оценил его как эквивалент языка программирования для числового программного управления станками.

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

Слова над алфавитом

Алфавитом ; в контексте формальных языков может быть набор любой его элементы называются буквами . Алфавит может содержать бесконечное количество элементов; однако большинство определений в теории формального языка определяют алфавиты с конечным числом элементов, и многие результаты применимы только к ним. Часто имеет смысл использовать алфавит в обычном смысле этого слова или, в более общем смысле, любую конечную кодировку символов , такую ​​как 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 = {а} ^* = {а ^н }, где n варьируется в пределах натуральных чисел и "a ^н « означает «а», повторенное n раз (это набор слов, состоящий только из символа «а»);
• набор синтаксически правильных программ на данном языке программирования (синтаксис которых обычно определяется контекстно -свободной грамматикой );
• набор входных данных, на которых определенная машина Тьюринга останавливается ; или
• набор максимальных строк буквенно-цифровых символов ASCII в этой строке, т.е.
  набор {набор, максимальных, строк, буквенно-цифровых, ASCII, символов, на, этой, строке, i, e}.

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

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

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

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

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

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

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

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

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

• Конкатенация ​ $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}$ относительно $\Sigma$ состоит из всех строк над $\Sigma$ которых нет в $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\}$.
• Струнный гомоморфизм

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

Свойства замыкания языковых семей ( $L_{1}$ На $L_{2}$ где оба $L_{1}$ и $L_{2}$ относятся к языковой семье, указанной в столбце). После Хопкрофта и Ульмана.

Операция		Обычный	DCFL	КФЛ	В	CSL	рекурсивный	РЭ
Союз	$L_{1}\cup L_{2}=\{w\mid w\in L_{1}\lor w\in L_{2}\}$	Да	Нет	Да	Да	Да	Да	Да
Пересечение	$L_{1}\cap L_{2}=\{w\mid w\in L_{1}\land w\in L_{2}\}$	Да	Нет	Нет	Нет	Да	Да	Да
Дополнение	$\neg L_{1}=\{w\mid w\not \in L_{1}\}$	Да	Да	Нет	Нет	Да	Да	Нет
Конкатенация	$L_{1}\cdot L_{2}=\{wz\mid w\in L_{1}\land z\in L_{2}\}$	Да	Нет	Да	Да	Да	Да	Да
Клини звезда	$L_{1}^{*}=\{\varepsilon \}\cup \{wz\mid w\in L_{1}\land z\in L_{1}^{*}\}$	Да	Нет	Да	Да	Да	Да	Да
(Строковый) гомоморфизм $h$	$h(L_{1})=\{h(w)\mid w\in L_{1}\}$	Да	Нет	Да	Да	Нет	Нет	Да
ε-свободный (струнный) гомоморфизм $h$	$h(L_{1})=\{h(w)\mid w\in L_{1}\}$	Да	Нет	Да	Да	Да	Да	Да
Замена $\varphi$	$\varphi (L_{1})=\bigcup _{\sigma _{1}\cdots \sigma _{n}\in L_{1}}\varphi (\sigma _{1})\cdot \ldots \cdot \varphi (\sigma _{n})$	Да	Нет	Да	Да	Да	Нет	Да
Обратный гомоморфизм $h^{-1}$	$h^{-1}(L_{1})=\bigcup _{w\in L_{1}}h^{-1}(w)$	Да	Да	Да	Да	Да	Да	Да
Обеспечить регресс	$L^{R}=\{w^{R}\mid w\in L\}$	Да	Нет	Да	Да	Да	Да	Да
Пересечение с обычным языком $R$	$L\cap R=\{w\mid w\in L\land w\in R\}$	Да	Да	Да	Да	Да	Да	Да

Приложения

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

Основные статьи: Синтаксис (языки программирования) и Компилятор-компилятор.

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

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

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

Основные статьи: Теория (математическая логика) и Формальная система.

Эта диаграмма показывает синтаксические подразделения внутри формальной системы . Строки символов можно условно разделить на бессмысленные и правильно построенные формулы . Множество корректных формул делится на теоремы и нетеоремы.

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

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

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

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

Основные статьи: Формальная семантика (логика) , Интерпретация (логика) и Теория моделей.

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

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

См. также

• Комбинаторика по словам
• Формальный метод
• Бесплатный моноид
• Грамматическая основа
• Математические обозначения
• Строка (информатика)

Ссылки

Источники

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

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

Общие ссылки

• А.Г. Гамильтон, Логика для математиков , издательство Кембриджского университета , 1978, ISBN   0-521-21838-1 .
• Сеймур Гинзбург , Алгебраические и теоретико-автоматные свойства формальных языков , Северная Голландия, 1975, ISBN   0-7204-2506-9 .
• Майкл А. Харрисон , Введение в теорию формального языка , Аддисон-Уэсли, 1978.
• Раутенберг, Вольфганг (2010). Краткое введение в математическую логику (3-е изд.). Нью-Йорк: Springer Science + Business Media . дои : 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 г.
• Черновики некоторых глав «Справочника по теории формального языка», Vol. 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