Синтаксис

Формальная система представляет собой правила, манипулирующие математическими формулами. Что представляет собой формула?

Мы могли бы рассматривать формулы как последовательности символов. Так, например, выражение \(\sin(\pi\cdot x) + 1\) представляет собой последовательность следующих символов: \(sin\) (мы считаем имя функции одним символом, хотя оно состоит из трёх букв), \((\), \(\pi\), \(\cdot\), \(x\), \()\), \(+\) и \(1\).

Такое представление, однако, плохо подходит для преобразований, так как включает в себя несущественные синтаксические детали. Например, \((3\cdot 2) + 1\) и \(3\cdot 2 + 1\) представляют собой различные последовательности символов, хотя являются фактически одним и тем же выражением. Кроме того, наивная подстановка одних последовательностей символов на другие редко даёт желаемый результат: так, заменив в выражении \(3\cdot 5\) символ \(3\) на последовательность символов \(1+2\), мы получаем \(1 + 2\cdot 5\) — выражение с совсем иным смыслом, чем \((1+2)\cdot 3\).

Нам требуется представление, учитывающее вложенную природу математических формул.

Чтобы вывести такое представление, разберём формулу на части. Рассмотрим снова выражение \(\sin(\pi\cdot x) + 1\). Оно представляет собой сумму значений \(\sin(\pi\cdot x)\) и \(1\). Вынесем части этого выражения отдельно от знака суммы, и нарисуем стрелки, соединяющие сумму с подвыражениями:

Квадраты вокруг знака суммы означают места соответствующих подвыражений. Порядок стрелок имеет значение: мы считаем \(\sin(\pi\cdot x) + 1\) и \(1 + \sin(\pi\cdot x)\) синтаксически различными выражениями.

Продолжим разбирать наше выражение. \(\sin(\pi\cdot x)\) это применение функции \(\sin\) к значению \(\pi\cdot x\):

И, наконец, \(\pi\cdot x\) это произведение \(\pi\) и \(x\):

Построенная диаграмма называется синтаксическим деревом выражения \(\sin(\pi\cdot x) + 1\).

Поскольку в синтаксическом дереве выражение явно разложено на его части, синтаксическое дерево не включает в себя группирующие скобки. Например, синтаксическое дерево выражения \((1+2) \cdot 5\) имеет вид:

Будем называть термом математическую формулу, рассматриваемую как синтаксическое дерево.

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

Грамматика описывает построение термов из их частей. Опишем для примера грамматику простых арифметических выражений:

• Числа (например, \(1\), \(-3\), \(42\)) это выражения

• Переменные вроде \(x\), \(y\) это выражения

• Если \({\color{red} a}\) и \({\color{red} b}\) это выражения, то и \({\color{red} a} + {\color{red} b}\) это выражение

• Если \({\color{red} a}\) и \({\color{red} b}\) это выражения, то и \({\color{red} a} - {\color{red} b}\) это выражение

• Если \({\color{red} a}\) и \({\color{red} b}\) это выражения, то и \({\color{red} a} \cdot {\color{red} b}\) это выражение

• Если \({\color{red} a}\) и \({\color{red} b}\) это выражения, то и \({\color{red} a} \mathbin/ {\color{red} b}\) это выражение

Символы \({\color{red} a}\) и \({\color{red} b}\) в этом описании являются метапеременными, и означают некоторые термы. Всюду, где метапеременные можно было бы спутать с обычными переменными (которые являются термами языка, а не обозначают их), мы выделяем метапеременные красным цветом.

Описанную нами грамматику можно также записать более кратко:

\[\begin{split}\begin{aligned} {\color{red}expr} ::=\ &\textcolor{red}{num} & &\text{(число)} \\ \mid\quad &{\color{red}var} & &\text{(переменная)} \\ \mid\quad &{\color{red}expr}\ {+}\ {\color{red}expr} & &\text{(сложение)} \\ \mid\quad &{\color{red}expr}\ {-}\ {\color{red}expr} & &\text{(вычитание)} \\ \mid\quad &{\color{red}expr}\ {\cdot}\ {\color{red}expr} & &\text{(умножение)} \\ \mid\quad &{\color{red}expr}\ { / }\ {\color{red}expr} & &\text{(деление)} \\ \end{aligned}\end{split}\]

Эта запись означает, что каждый терм типа \({\color{red}expr}\) (то есть выражение) являются одной из альтернатив, перечисленных справа от знака \(::=\). Имена, выделенные в этой записи красным, называются нетерминалами и обозначают множества термов соответствующего типа.

Терм принадлежит языку, если его можно построить следуя правилам, перечисленным в грамматике. Построение терма данного типа осуществляется следующим образом. Мы пишем соответствующий типу нетерминал, и заменяем его на одну из соответствующих ему альтернатив. Затем раскрываем подобным способом оставшиеся в терме нетерминалы до тех пор, пока все нетерминалы в терме не будут заменены на соответствующие им термы.

Например, терм \(3\mathbin/2 + 1\) строится следующим образом:

• \({\color{red}expr}\)

• \({\color{red}expr} - {\color{red}expr}\)

• \({\color{red}expr} \mathbin/ {\color{red}expr} - {\color{red}num}\)

• \({\color{red}num} \mathbin/ {\color{red}num} - 1\)

• \(3 \mathbin/ 2 - 1\)

Синтаксическое дерево полученного выражения выглядит так:

Многие действия с термами сводятся с сопоставлению с образцом и построению новых термов, состоящих из сопоставленных частей.

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

Например, если мы сопоставим терм \(2\cdot(y-1) + x\) с образцом \({\color{red}x} \cdot {\color{red}y} + {\color{red}z}\), то получим, что метапеременная \({\color{red}x}\) означает терм \(2\), \({\color{red}y}\) означает терм \(y-1\), а \({\color{red}z}\) означает терм \(x\).

После того, как мы связали метапеременные с некоторыми термами, термы с метапеременными начинают означать конкретные термы. Например, если мы связали \({\color{red}x}\) с термом \(31 - 12\), то тогда запись \(2\cdot {\color{red}x}\) означает терм \(2 \cdot (31-12)\).

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

Правила могут включать в себя метавыражения и метаотношения. Метавыражение это выражение, описывающее определённое преобразование терма. Метаотношение же это отношение между двумя термами.

В отличие от метапеременных, метавыражения и метаотношения цветом не выделяются.