Файлопомойка Маздайщика

Типизация для Рефала-5

Александр Коновалов, июль 2020

Синтаксис

Переменные в Рефале бывают трёх разновидностей: s-, t- и e-переменные. Обычно, s, t и e называют типами переменных, но в данной работе термин «тип» удобнее использовать для других целей. Поэтому разновидности переменных s, t и e мы будем называть видами переменных.

Типы объектных выражений предлагается описывать при помощи грамматик, нетерминальные символы которых записываются при помощи переменных (мы их будем называть именами типов), в алфавит терминальных символов входят символы Рефала и структурные скобки.

Правила грамматики имеют вид

〈имя-типа〉 ::= 〈ти́повое-выражение〉

где 〈имя-типа〉 — переменная (вида s-, t- или e-), а 〈типовое-выражение〉 — выражение РБНФ, построенное из символов Рефала, переменных, круглых скобок, фигурных скобок {, }, знака | и знаков *, +, ?.

• Символы в правой части описывают символы, переменные — вхождения соответствующих нетерминалов, структурные скобки — структурные скобки.
• Наивысший приоритет имеют квантификаторы — знаки *, +, ?, которые обозначают итерацию, позитивную итерацию и опцию соответственно. Знаки + и ? являются синтаксическим сахаром, поэтому в теоретических выкладках использоваться, как правило, не будут.
• Следующей операцией по уровню приоритета является конкатенация, обозначаемая пробелом. Выражение 'ab'* означает строки 'a', 'ab', 'abb' и т. д.
• Наинизший приоритет имеет знак | означающий альтернативу.
• Знаки { и } используются для группировки и изменения приоритета. Обычно для задания приоритета используются круглые скобки, но здесь они уже заняты.
• Скобки (структурные Рефала и группирующие фигурные) должны быть правильно сбалансированы.
• Пустое выражение мы будем обозначать при помощи знака ε.

Операция конкатенации ассоциативна. Операция альтернативы коммутативна и ассоциативна.

Типы, описанные при помощи e-, t- и s-переменных, мы будем называть, соответственно, e-типами, t-типами и s-типами.

Правая часть в правиле должна описывать синтаксическое подмножество значений типа слева.

• У e-типов справа может быть записано произвольное выражение.
• Правило для t-типов должно иметь вид:

  t.Name ::= 〈терм〉 | 〈терм〉 …
  

  где 〈терм〉 — символ, произвольное выражение в скобках, s- или t-тип. Иначе говоря, на верхнем уровне выражения запрещены квантификаторы, конкатенация, e-типы и фигурные скобки, также выражение справа не может быть пустым. Таким образом обеспечивается, что значение t-типа может быть только одним объектным термом.

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

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

e.OneTerm ::= (A*)
e.Empty ::= ε
t.OneTerm ::= e.OneTerm | e.Empty X e.Empty

Но работать с такими типами было бы гораздо сложнее.

Множество значений типа также может быть пустым, что мы будем обозначать при помощи знака @ — множество объектных выражений, описываемых этим типом пустое (∅). В реальных программах этот тип будет использоваться редко (возможно, только для записи типа результата функции Exit), но он будет полезен в промежуточных выкладках и теоретических построениях.

Любое типовое выражение, содержащее символ @ можно либо привести к выражению, состоящему из единственного символа @, либо к выражению, этого символа не содержащему. Для этого достаточно воспользоваться следующими правилами сокращения:

E @ = @ E = @
E | @ = @ | E = E
(@) = @+ = @
@* = @? = ε

Нотация также подразумевает использование нескольких предопределённых типов: s.CHAR, s.WORD, s.NUMBER означают соответствующие категории символов Рефала-5 — множество литер, множество слов (составных символов, идентификаторов) и множество чисел (макроцифр). В Рефале-5λ к ним можно добавить s.FUNCTION — указатель на функцию или замыкание. Но здесь типы высшего порядка мы рассматривать не будем, ограничимся только первым порядком.

Также удобно ввести обозначения s.ANY, t.ANY и e.ANY — любой символ, любой терм и любое выражение. Можно считать, что они определены как

s.ANY ::= s.CHAR | s.WORD | s.NUMBER
t.ANY ::= s.ANY | (e.ANY)
e.ANY ::= t.ANY*

Типы s.ANY, t.ANY и e.ANY далее мы будем называть универсумами или универсальными типами.

Типы вида s.CHAR, s.WORD и s.NUMBER будем называть субуниверсумами.

Синглетным типом будем называть s-тип, правая часть которого содержит ровно один константный символ. Индекс синглетного типа будем записывать как символ (значение типа) в квадратных скобках. Примеры синглетных типов:

s.['A'] ::= 'A'
s.[42] ::= 42
s.[Hello] ::= Hello

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

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

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

Далее по тексту имена s-, t- и e-типов для краткости будут называться s-, t- и e-переменными, если это не приводит к недоразумениям.

Тип функции записывается следующим образом:

<〈имя-функции〉 〈типовое-выражение〉> == 〈типовое-выражение〉

Знак == символизирует, что функция может вычислять свой результат за несколько шагов рефал-машины. Типовое выражение внутри угловых скобок описывает тип аргумента, типовое выражение справа от == — тип результата (возвращаемого значения).

Если тип результата записан как альтернатива, то будем использовать следующий синтаксический сахар:

<〈имя-функции〉 〈тип-аргумента〉>
  == 〈тип-результата-1〉
  == 〈тип-результата-2〉
     …
  == 〈тип-результата-N〉

что является альтернативной записью для

<〈имя-функции〉 〈тип-аргумента〉>
  == 〈тип-результата-1〉 | … | 〈тип-результата-N〉

Язык типов как неформальная нотация

Описанный выше язык типов автор этих строк уже давно использует как полуформальную нотацию при программировании на Рефале. В частности, эта нотация используется для описания типов в Рефале-5λ, в Рефал-05, в наборе библиотек для Рефала-5 и Рефала-05, в Модульном Рефале. В документации к Рефалу-5λ есть даже приложение, посвящённое использованию этой нотации в комментариях.

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

Притягательной является идея по автоматической верификации типов программ на Рефале — имея некоторую программу на Рефале и описания типов функций для неё, проверить, что функции действительно могут принимать значения указанных типов и что они возвращают значения, входящие в тип результата, типы фактических аргументов в вызовах функций входят в их формальные типы.

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

В данной работе делается попытка описать теоретические основы для работы с описанными типами.

Регулярная грамматика типов и её нормальные формы

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

Мотивация ограничения грамматики

Нотация, описанная выше, позволяет описывать контекстно-свободные (КС) грамматики произвольного вида. Но произвольные контекстно-свободные грамматики слишком неудобны для анализа. Для них почти нет никаких хороших свойств в смысле теоретико-множественных операций. Например, операция пересечения множеств не замкнута на множестве контестно-свободных грамматик. Единственное известное мне хорошее свойство — пересечение КС-грамматики с автоматной грамматикой тоже является КС-грамматикой.

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

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

Внимание! Далее мы будем рассматривать грамматики без субуниверсумов, т.е. предопределённых типов вида s.CHAR. Под универсумом мы будем понимать набор типов вида

s.ANY ::= 〈все символы, явно заданные в грамматике типов〉
t.ANY ::= s.ANY | (e.ANY)
e.ANY ::= t.ANY*

Позже мы отдельно рассмотрим, каким образом в наш подход можно включить субуниверсумы.

Определение регулярной грамматики типов

Будем говорить, что грамматика типов регулярная, если не существует вывода из какого-либо e-типа, что

e.〈тип〉 →* 〈слева〉 e.〈тип〉 〈справа〉

при этом части сентенциальной формы 〈слева〉 и 〈справа〉 являются правильными объектными выражениями, т.е. состоят только из символов и структурных скобок, при этом скобки сбалансированы.

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

В работе Омера Эгеджиоглу со ссылкой на Хомского утверждается, что если грамматика несамовложимая (non-self-embedding), то она описывает регулярный язык. В нашем случае самовложение допустимо, но оно должно быть внутри структурных скобок.

В принципе, в языке можно ограниченно допустить и «плоскую» рекурсию для e-типов, но описание частных случаев для этого довольно громоздко, кроме того неоправданно усложнится алгоритм нормализации.

По опыту автора регулярного подмножества грамматики типов вполне достаточно для записи типов данных в подавляющем большинстве программ. Более того, автору не известны случаи, когда типы выходят за рамки регулярных грамматик типов (контекстно-зависимые инварианты в структурах данных не считаются).

Нормальная форма регулярной грамматики типов

Опишем нормальную форму (НФ) регулярной грамматики типов:

• Все типы грамматики объединены в тройки: для каждого типа, описываемого переменной с некоторым индексом, существуют связанные с ним два типа других видов с тем же индексом. Тройка типов с одинаковым индексом объединена следующим соотношением:

  t.SomeType ::= s.SomeType | (e.SomeType)
  

• Все t-типы определены так, как описано выше.
• Типовое выражение для s-типа может быть либо @, либо перечислением константных символов (не может включать s-переменные), символы в правиле не должны повторяться.
• Типовое выражение для e-типа может быть либо @, либо состоять только из t-переменных, фигурных скобок, знаков | и *.

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

Преобразование грамматики к нормальной форме

Можно показать, что любую регулярную грамматику типов можно привести к регулярной нормальной форме.

Будем считать, что в исходной грамматике индексы типов или уникальны, т.е. не существует двух типов разных видов с одинаковым индексом, или три типа с одинаковым индексом уже представляют собой тройку, т.е. t-тип выражен как

t.〈индекс〉 ::= s.〈индекс〉 | e.〈индекс〉

Примером уже готовой тройки типов является тройка с индексом .ANY.

Если это не так, переименуем типы с конфликтующими индексами.

Преобразование выполняется в несколько этапов:

1. Устранение квантификаторов ? и +.
2. Нормализация правил для s-типов и упрощение правил для t-типов.
3. Построение троек для s- и e-типов.
4. Нормализация и построение троек для t-типов.
5. Нормализация для e-типов.

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

1. Устранение квантификаторов ? и +

Квантификаторы ? и + устраняются как синтаксический сахар по правилам:

EXPR? → { ε | EXPR }
EXPR+ → EXPR EXPR*

Это самый простой и тривиальный этап.

2. Нормализация правил для s-типов и упрощение правил для t-типов

Правила для s- и t-типов по определению имеют вид

〈тип〉 → 〈терм1〉 | 〈терм2〉 | … | 〈термN〉

Т.е. фактически их можно рассматривать просто как множества, элементами которых являются термовые типовые выражения. Для s-типов элементами множества будут конкретные значения символов и имена s-типов. Для t-типов те же элементы, что и для s-типов плюс t-переменные и типовые выражения в структурных скобках.

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

• Для каждого s- и t-типа 〈T〉 введём множество SET[〈T〉].
• Для каждого правила

  〈T〉 ::= 〈T1〉 | 〈T2〉 | … | 〈Tn〉
  

  где 〈Ti〉 — типовое выражение для терма, проинициализируем множество

  SET[〈T〉] := { 〈T1〉, 〈T2〉, …, 〈Tn〉 }
  

• Следующий цикл повторяем, пока множества SET[〈T〉] не перестанут изменяться:

  Для каждого s- и t-типа 〈T〉 исходной программы:
    Для каждого 〈U〉 ∈ SET[〈T〉], такого что 〈U〉 является s- или t-переменной:
      SET[〈T〉] := SET[〈T〉] ⋃ SET[〈U〉]
  

• Из элементов SET[〈T〉] удаляем все термы-переменные на верхнем уровне (т.е. внутри скобочных термов ничего не трогаем).
• Заменяем правила для s- и t-типов на правила

  〈T〉 ::= 〈T1〉 | 〈T2〉 | … | 〈Tn〉
  

  где 〈Ti〉 — соответствующие элементы множеств SET[〈T〉]. Если множество пустое, то добавляется правило

  〈T〉 ::= @
  

3. Построение троек для s- и e-типов

Если некоторый s- или e-тип уже входит в правильную тройку, то этот этап для него не выполняется.

Для этих типов тройки строятся тривиально. Для каждого s-типа s.〈имя〉 строятся t- и e-типы

t.〈имя〉 ::= s.〈имя〉 | (e.〈имя〉)
e.〈имя〉 ::= @

Аналогично для e-типа e.〈имя〉:

s.〈имя〉 ::= @
t.〈имя〉 ::= s.〈имя〉 | (e.〈имя〉)

4. Нормализация и построение троек для t-типов

Если некоторый тип уже входит в правильную тройку, то этот этап для него не выполняется.

Для t-типов процедура чуть более интересна. После упрощения t-типы имеют вид:

t.〈имя〉 ::= 〈Sym1〉 | … | 〈SymM〉 | (〈Expr1〉) | … | (〈ExprN〉)

Все значения-символы переносим в s-тип, все содержимые скобок — в e-тип:

s.〈имя〉 ::= 〈Sym1〉 | … | 〈SymM〉
t.〈имя〉 ::= s.〈имя〉 | (e.〈имя〉)
e.〈имя〉 ::= 〈Expr1〉 | … | 〈ExprN〉

5. Нормализация для e-типов

От нормальной формы нас отделяет только вид правил для e-типов. В типовых выражениях для e-правил могут использоваться только t-переменные, фигурные скобки и знаки | и *. Т.е. из описаний e-типов нам нужно исключить константные символы, s-переменные, структурные скобки и e-переменные.

Устранять их будем поэтапно.

1. Устраняем константные символы. Для каждого вхождения символа 〈Sym〉 в правиле для e-типа создаётся тройка:

   s.[〈Sym〉] ::= 〈Sym〉
   t.[〈Sym〉] ::= s.NEW | (e.NEW)
   e.[〈Sym〉] ::= @
   

   После этого каждое символа этого 〈Sym〉 в правилах для e-типов заменяется на t.[〈Sym〉]. Т.е. фактически создаётся тройка для синглетного типа. Такие тройки мы будем называть синглетными тройками. Если синглетный тип для данного символа ранее уже был определён, повторное определение в грамматику не добавляется.

2. Каждое вхождение s-типа заменяется на одноимённый t-тип. Действительно, каждый из s-типов исходной грамматики мы достроили до тройки, t-тип которой идентичен исходному s-типу, т.к. e-тип тройки является пустым множеством.
3. Для каждого скобочного терма (〈Expr〉) в правиле для e-типа создаётся новая тройка

   s.NEW ::= @
   t.NEW ::= s.NEW | (e.NEW)
   e.NEW ::= 〈Expr〉
   

   Вхождение (〈Expr〉) заменяется на t.NEW. Этот этап повторяется до тех пор, пока скобочные термы из всех e-правил не будут исключены.

4. Поскольку грамматика типов является регулярной, «плоских» рекурсивных вхождений для e-типов не будет, а значит, все e-переменные в описаниях e-типов можно заменить на конкретные значения.

Можно заметить, что в нормальной форме для регулярной грамматики типов выражения для e-типов фактически являются регулярными выражениями поверх алфавита имён t-типов. Именно поэтому такая грамматика типов и названа регулярной.

Раз мы можем e-типы описывать при помощи регулярных выражений, возникает соблазн использовать матапарат для регулярных языков для операций над типами: проверка вложения, пересечение, объединение, разность, дополнение и т.д. Но не всё так просто. t-типы, в терминах которых описываются e-типы, могут накладываться друг на друга, а значит, проводить формальные операции над множествами над ними бессмысленно.

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

Ортогональная нормальная форма грамматики типов

Опишем форму грамматики, в которой выразимы такие операции, как пересечение и разность множеств. Если грамматику типов формально дополнить универсальным типом вида

s.ANY ::= 〈все символы, явно записанные в грамматике〉
t.ANY ::= s.ANY | (e.ANY)
e.ANY ::= t.ANY*

то дополнение некоторого типа до универсума будет выражаться как разность универсального и рассматриваемого типа.

Проверка на вложение одного типа в другое сводится к вычислению разности типов и проверке этой разности на пустоту.

Будем говорить, что два типа одного вида ортогональны, если они описывают непересекающиеся множества объектных выражений.

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

Типы из ORTHO записаны в НФ — s-типы представляют собой множества символов, e-типы — регулярные языки в алфавите t-типов из ORTHO, t-типы — как объединение s-типа и скобочного терма с e-типом внутри.

Тройки типов из ORTHO попарно ортогональны.

Типы из SRC описаны как объединения типов соответствующего вида из ORTHO.

s.〈src1〉 ::= s.〈ortho1〉 | … | s.〈orthoK〉
t.〈src2〉 ::= t.〈ortho1〉 | … | t.〈orthoM〉
e.〈src3〉 ::= e.〈ortho1〉 | … | e.〈orthoN〉

Очевидно, что для набора исходных типов операции над множествами выражаются тривиально — как операции над множествами ортогональных типов.

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

Покажем, что это возможно — опишем процедуру построения ОНФ.

Процедура ортогонализации регулярной грамматики типов

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

Процедуру построения ортогональной нормальной формы для краткости назовём процедурой ортогонализации регулярной грамматики типов.

Как и процедура нормализации, процедура ортогонализации делится на несколько этапов:

1. Построение нормальной формы и нумерация троек.
2. Построение набора имён ортогональных типов, запись ортогональных t-типов.
3. Выражение исходных t-типов через ортогональные.
4. Вычисление значений ортогональных s-типов.
5. Запись исходных e-типов в алфавите ортогональных типов.
6. Вычисление значений ортогональных e-типов.
7. Выражение исходных s- и e-типов через ортогональные.

Как и ранее, будем считать, что в исходной грамматике типов нет типов разного вида, но с одинаковыми индексами. Либо есть три типа с одним индексом и они уже образуют правильную тройку.

Также будем считать, что в исходной грамматике типов нет типов, индексы которых начинаются на 0 или 1. Если таковые есть, переименуем их.

1. Построение нормальной формы и нумерация троек

Строим нормальную форму регулярной грамматики. Множество SRC инициализируем как множество построенных типов, множество ORTHO — как пустое множество. Да, в SRC в данном случае будут находиться «лишние» типы, которых не было в исходной грамматике, но это не принципиально. «Лишними» будут типы, которые были построены в ходе процедуры нормализации — дополнения до троек, символы и скобочные термы, вынесенные из определений e-типов. Эти «лишние» типы при необходимости можно безопасно удалить после завершения построения ОНФ.

Также будем считать, что процедура нормализации не создаёт новых типов с индексами, начинающимися на 0 и 1.

Каждой тройке в НФ назначаем номер, начиная с 1. Далее будем считать, что у нас получилось N троек.

2. Построение набора имён ортогональных типов, запись ортогональных t-типов

Сгенерируем 2^N различных строк из знаков 0 и 1 длиной N. Это будут индексы типов из набора ORTHO. Набор ORTHO должен быть описан в нормальной форме, т.е. быть набором троек. Поэтому каждый из этих новых индексов будет индексом и s-, и t-, и e-типа. Ортогональные t-типы записываются как

t.〈ortho〉 ::= s.〈ortho〉 | (e.〈ortho〉)

Каждый тип из ORTHO представляет собой пересечение N множеств, каждое из этих множеств — либо множество значений типа данного вида из некоторой исходной тройки, либо дополнение типа исходной тройки до универсума. Знак 1 в i-й позиции индекса означает, что i-е множество совпадает с типом соответствующего вида исходной тройки, знак 0 — что берётся дополнение этого типа тройки до универсума соответствующего вида.

Если сопоставить два разных индекса типов из ORTHO, то найдётся как минимум одна позиция, где у одного типа будет 1, а у другого 0. Пусть это будет i-я позиция. Тогда первый тип будет подмножеством типа i-й тройки, а второй — подмножеством её дополнения. Таким образом типы из ORTHO будут попарно ортогональными.

Также по построению очевидно, что объединение всех типов некоторого вида из ORTHO образует универсум, а также объединение всех типов некоторого вида из ORTHO с 1 в i-й позиции — компонент соответствующего вида i-й тройки.

Таким образом, весь набор ORTHO есть разбиение универсума, а его подмножество с 1 в i-й позиции — разбиение i-й тройки.

3. Выражение исходных t-типов через ортогональные

Каждый t-тип из SRC записываем как объединение t-типов из ORTHO с 1 в i-й позиции, где i — номер тройки данного t-типа:

t.〈i〉 ::= … | t.〈…〉1〈…〉 | …

4. Вычисление значений ортогональных s-типов

Значения s-типов из ORTHO выражаются как пересечения N множеств исходных s-типов или их дополнений.

s.〈bitstr〉 ::= SET(s, 1, 〈bitstr〉) ⋂ … ⋂ SET(s, N, 〈bitstr〉)

где функция SET(〈вид〉, i, 〈bitstr〉) определена как

SET(mode, i, bitstr) =  mode.i, bitstr[i] == '1'
                     | ~mode.i, bitstr[i] == '0'

Здесь знаком ~ обозначено дополнение до универсума:

~〈вид〉.〈имя〉 = 〈вид〉.ANY \ 〈вид〉.〈имя〉

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

5. Запись исходных e-типов в алфавите ортогональных типов

t-типы из SRC ранее были определены как объединения t-типов из ORTHO. Для записи e-типов в SRC в терминах t-типов из ORTHO достаточно сделать соответствующую подстановку t-типов в их регулярные выражения.

Если регулярные языки e-типов были описаны при помощи конечных автоматов, то преобразование будет сложнее. Каждый переход из состояния Qi в Qj по символу t.〈i〉 заменяется на 2^(N−1) переходов по t-типам из ORTHO, в индексах которых в i-й позиции находится 1. Автомат при этом может стать недетерминированным.

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

6. Вычисление значений ортогональных e-типов

Значения e-типов из ORTHO записываются аналогично значениям для s-типов:

e.〈bitstr〉 ::= SET(e, 1, 〈bitstr〉) ⋂ … ⋂ SET(e, N, 〈bitstr〉)

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

7. Выражение исходных s- и e-типов через ортогональные

s- и e-типы из SRC выражаются аналогично t-типам ранее — как объединение типов соответствующего вида из ORTHO с 1 в i-й позиции, где i — номер тройки данного типа:

s.〈i〉 ::= … | s.〈…〉1〈…〉 | …
e.〈i〉 ::= … | e.〈…〉1〈…〉 | …

Свойства ОНФ, разряжённость множества ORTHO и его сокращение

Пересечения s- и e-типов

Если в i-й тройке s-компонент был пустым (@), а в j-й тройке e-компонент был пустым, то все типы из ORTHO, имеющие единицу и в i-й, и в j-й позициях, будут пустыми.

Свойство повторной ортогонализации

Если типы в исходной грамматике уже были ортогональными, то непустые типы из ORTHO будут иметь единственную единицу в индексе, т.е. индексы будут иметь вид 〈вид〉.0…010…0, а типы из SRC будут описываться правилами:

〈вид〉.〈src〉 ::= 〈вид〉.0…010…0

Разряжённость множества ORTHO для реальных программ

Приведённая выше процедура строит ОНФ экспоненциального размера от числа троек НФ исходной грамматики. Но на практике размер ОНФ хоть и будет большим, но, скорее всего, разумного размера.

Первое свойство показывает, что число непустых типов в грамматике будет равно не O(2^N), где N — число троек, а O(2^Ne+2^Ns), где Ne и Ns — число троек с непустым компонентом e-типа и s-типа соответственно.

Тройки с пустыми компонентами возникают двумя путями: либо они явно строятся из типов исходной грамматики, либо они возникли в процессе нормализации. Первые возникают при расширении до троек исходных s- и e-типов, либо если t-типы описывают только скобочные термы (что не редкость). Вторые — результат вынесения констант и скобочных термов из выражений для e-типов.

Второе свойство говорит о том, что если в исходной грамматике в НФ было K взаимно ортогональных троек, то число непустых троек в ORTHO будет в 2^K раз меньше.

Ортогональные типы в реальных грамматиках не редкость. Программисты обычно проектируют типы данных таким образом, чтобы альтернативы в грамматике можно было различать при помощи сопоставления с образцом, причём это сопоставление должно выполняться по возможности эффективно. Наиболее эффективно выполняется сопоставление с L-выражениями, т.е. выражениями без открытых e-переменных и повторных t- и e-переменных. Поэтому альтернативы в описании типа часто описываются жёсткими выражениями, ортогональность которых очевидна.

Например, отдельные элементы могут описываться в виде скобочных термов, где в различных альтернативах первым термом в скобках является символ-слово:

t.Token ::=
    (Number t.Pos s.NUMBER)
  | (Variable t.Pos s.CHAR+)
  | ("+" t.Pos)
  | ("(" t.Pos)
    …
  | (EOF t.Pos)

t.Expr ::=
    (Value s.NUMBER)
  | (Variable s.WORD)
  | (t.Expr s.BinOp t.Expr)
  | ('-' t.Expr)

s.BinOp ::= '+' | '-' | '*' | '/'

Процедура удаления пустых типов из множества ORTHO

Как сказано выше, во множестве ORTHO на практике часто оказывается много пустых типов. Теоретическим построениям такие типы не мешают, но на практике целесообразнее работать с более компактной ОНФ.

Поэтому опишем процедуру, которая устраняет из ORTHO все пустые тройки.

• Повторять до тех пор, пока количество типов в ORTHO не перестанет уменьшаться:
  • Найти тройку, у которой s- и e-компоненты пустые.
  • Удалить эту тройку.
  • Упростить регулярные языки для e-типов с учётом отсутствия в алфавите данного t-типа (см. далее).
• Удалить из правил в SRC все типы, которые теперь отсутствуют в ORTHO.

Алгоритм упрощения регулярного языка зависит от представления этого языка.

• Если язык описан регулярным выражением, то достаточно заменить соответствующий символ знаком @ и выполнить известные процедуры упрощения (конкатенация с @ даёт @, слагаемые @ в альтернативах отбрасываем, итерация @* равна пустой строке). В результате регулярное выражение может упроститься до @.
• Если язык описан конечным автоматом, из таблицы переходов нужно будет удалить соответствующую колонку и почистить автомат от недостижимых состояний. Одновременно с этим можно проверить достижимость финальных состояний. Если все финальные состояния стали недостижимыми, можно весь регулярный язык заменить на @.

Очевидное ускорение алгоритма чистки — одновременное удаление нескольких троек за раз

Внешний цикл в алгоритме необходим, т.к. после удаления некоторых t-типов регулярные языки для e-типов тоже могут оказаться пустыми. Тройки с опустевшими e-типами могли иметь пустые s-типы, а значит, их тоже нужно будет удалить.

Инкрементное построение ОНФ

Допустим, описанная выше процедура ортогонализации в сочетании с последующей чисткой позволяет получить итоговую ОНФ разумного размера. Но промежуточная ОНФ до чистки должна будет иметь 2^N троек в ORTHO! Если исходная НФ имела три десятка троек, то промежуточная ОНФ заведомо не влезет в 32-разрядное пространство процесса!

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

Но прежде чем рассмотреть саму процедуру, рассмотрим теоремы, лежащие в её основе.

Теорема о расширении ОНФ

Пусть нам дана грамматика в нормальной форме и пусть мы можем разбить её тройки на два множества: U и V, причём регулярные языки, описываемые e-типами из U, не содержат строк, содержащих t-типы из V.

Т.е. если регулярные языки представлены регулярными выражениями, то в их записи t-типы из V отсутствуют. Если регулярные языки представлены конечными автоматами, то по t-типам из V в них нет переходов.

Иначе говоря, грамматика U самодостаточна, типы из грамматики V могут зависеть от типов грамматики V.

Тогда построение ОНФ для грамматики U ⋃ V можно разбить на несколько этапов:

1. Построение ОНФ для U, обозначим компоненты этой ОНФ как SRC-U и ORTHO-U.
2. Выражение e-типов из V в терминах t-типов из V и ORTHO-U.
3. Построение ОНФ для U ⋃ V путём расщепления типов из ORTHO-U.

1. Построение ОНФ для U

ОНФ может строиться любым образом. Либо наивным алгоритмом, либо инкрементным.

2. Выражение e-типов из V в терминах t-типов из V и ORTHO-U

По условию, e-типы из U не выражаются в терминах t-типов из V. Однако, возможно обратное: e-типы из V могут быть выражены в терминах типов из U, теперь уже SRC-U. Их нам необходимо выразить в терминах t-типов из ORTHO-U.

Если регулярный язык для e-типа представлен регулярным выражением, просто заменяем t-тип из SRC-U на объединение соответствующих t-типов из ORTHO-U.

Если конечный автомат — заменяем каждый переход по t-терму из SRC-U на переходы по t-термам из ORTHO-U, из которых составлен исходный t-тип. Автомат при этом может стать недетерминированным.

3. Построение ОНФ для U ⋃ V путём расщепления типов из ORTHO-U

Пусть множество U содержит M троек, множество V — N троек. Строим 2^N различных строк длины N из знаков 0 и 1.

Для каждой тройки из ORHTO-U с индексом 〈u〉 и каждой вновь построенной строки 〈v〉 заготавливаем новую тройку с индексом 〈u〉〈v〉. Эти тройки будут образовывать множество ORTHO полной грамматики.

t-типы множества ORTHO-U будут выражаться как

t.〈u〉 ::= t.〈u〉0…0 | … | t.〈u〉〈v〉 | … | t.〈u〉1…1

t-типы множества V будут выражаться как объединения типов соответствующего вида с 1 в позиции M+i, где i — номер тройки в V:

t.〈i〉 ::= … | t.〈…〉1〈…〉 | …

e-типы множеств U и V нужно выразить в терминах новых t-типов из ORTHO, пользуясь упомянутыми выше подстановками.

Типы новой тройки определяются как

s.〈u〉〈v〉 ::= s.〈u〉 ⋂ SET(s, 1, 〈v〉) ⋂ … ⋂ SET(s, N, 〈v〉)
t.〈u〉〈v〉 ::= s.〈u〉〈v〉 | (e.〈u〉〈v〉)
e.〈u〉〈v〉 ::= e.〈u〉 ⋂ SET(e, 1, 〈v〉) ⋂ … ⋂ SET(e, N, 〈v〉)

где функция SET(mode, i, 〈v〉) выбирает i-й тип соответствующего вида или его дополнение из множества V.

s-типы по данной формуле вычисляются тривиально как операции над конечными множествами.

Для вычисления пересечений и дополнений e-типов из ORTHO-U и V можно использовать соответствующие алгоритмы из теории конечных автоматов, т.к. они теперь записаны в алфавите непересекающихся типов ORTHO.

s- и e-типы из множеств ORTHO-U и V выражаются аналогично t-типам:

s.〈u〉 ::= s.〈u〉0…0 | … | s.〈u〉〈v〉 | … | s.〈u〉1…1
e.〈u〉 ::= e.〈u〉0…0 | … | e.〈u〉〈v〉 | … | e.〈u〉1…1

s.〈i〉 ::= … | s.〈…〉1〈…〉 | …
e.〈i〉 ::= … | e.〈…〉1〈…〉 | …

Далее, остаётся сделать подстановку в типы SRC-U, удалить, ставшие ненужными типы ORTHO-U, и ОНФ построена.

Доказательство теоремы: по построению.

Теорема о расширении ОНФ уже позволяет нам построить более эффективный алгоритм для построения ОНФ. Для этого нужно построить НФ для исходной грамматики, множество троек разбить на подмножества U1, U2, …, Uk, таким образом, чтобы для i < j типы из Ui не зависели от типов Uj. Затем построить ОНФ для U1 и последовательно её расширять процедурой из теоремы.

Но есть и ещё одна теорема, позволяющая ускорить построение ОНФ для одного частного случая

Теорема о пересечении ОНФ

Пусть нам дана грамматика в нормальной форме и пусть мы можем разбить её тройки на два множества: U и V, причём регулярные языки, описываемые e-типами из U, не содержат строк, содержащих t-типы из V, регулярные языки, описываемые e-типами из V не содержат строк, содержащих t-типы из U.

Тогда построение ОНФ для объединённой грамматики можно свести к построению ОНФ каждого из множеств и построению их декартова произведения.

Построим ОНФ для обоих множеств U и V, их компоненты назовём, соответственно, SRC-U, ORTHO-U, SRC-V, ORTHO-V.

Пусть 〈u〉 — индексы троек из ORTHO-U, 〈v〉 — индексы троек из ORTHO-V.

Тогда индексы результирующего множества ORTHO будут иметь вид 〈u〉〈v〉.

t-типы из ORTHO-U и ORTHO-V будут выражаться как

t.〈u〉 ::= t.〈u〉0…0 | … | t.〈u〉〈v〉 | … | t.〈u〉1…1
t.〈v〉 ::= t.0…0〈v〉 | … | t.〈u〉〈v〉 | … | t.1…1〈v〉

Соответствующие подстановки нужно будет применить к языкам e-типов e.〈u〉 и e.〈v〉.

s- и e-типы троек ORTHO будут выражаться как декартовы произведения:

s.〈u〉〈v〉 ::= s.〈u〉 ⋂ s.〈v〉
e.〈u〉〈v〉 ::= s.〈u〉 ⋂ s.〈v〉

Значения s-типов вычисляются как соответствующие операции над множествами, значения e-типов — как пересечения двух регулярных языков.

Затем нужно выразить s- и e-типы из ORTHO-U и ORTHO-V в терминах типов тех же видов из ORTHO, выполнить подстановки всех типов из ORTHO-U и ORTHO-V в SRC-U и SRC-V.

Типы из ORTHO-U и ORTHO-V отбрасываем как ненужные, объединение SRC-U и SRC-V даст SRC результирующей нормальной формы.

Доказательство очевидно.

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

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

Теорема о декартовом произведении ОНФ накладывающихся грамматик

Если множество исходных троек грамматики в НФ можно разбить на три множества U, V, W, таких, что U не зависит от V и W, V не зависит от W и W не зависит от V, то ОНФ можно вычислить в четыре этапа:

1. Вычисляем ОНФ для U. Ортогональную часть обозначим как ORTHO-U.
2. Вычисляем ОНФ для U ⋃ V путём расширения ОНФ для U. Ортогональную часть обозначим как ORTHO-UV.
3. Вычисляем ОНФ для U ⋃ W путём расширения ОНФ для U. Ортогональную часть обозначим как ORTHO-UW.
4. Вычисляем ORTHO как декартово произведение ORTHO-UV и ORTHO-UW.

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

Индексы из ORTHO, ORTHO-UV и ORTHO-UW будут иметь вид 〈u〉, 〈u〉〈v〉 и 〈u〉〈w〉 соответственно. Тогда типы для ORTHO будут иметь индекс 〈u〉〈v〉〈w〉 и определяться соотношениями

s.〈u〉〈v〉〈w〉 ::= s.〈u〉〈v〉 ⋂ s.〈u〉〈w〉
e.〈u〉〈v〉〈w〉 ::= e.〈u〉〈v〉 ⋂ e.〈u〉〈w〉

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

Вот таким вот образом можно повысить на практике эффективность построения ОНФ. Кроме того, теорема о расширении ОНФ будет использоваться далее в процедуре проверки типов.

Добавление s- или e-типа к ОНФ

Рассмотрим два частных случая — имеем грамматику в ОНФ и мы хотим к ней добавить либо новый s-тип, описанный перечислением константных символов, либо e-тип, язык которого описан в алфавите t-типов из ORTHO. Случаи кажутся редкими, однако они будут возникать в процедуре проверки типов.

Добавление s-типа к ОНФ

Пусть у нас есть некий s-тип, назовём его s.ADD. Следующую процедуру будем выполнять для каждой тройки из ORTHO с индексом 〈ortho〉.

Если s-компонента в очередной тройке пустая, её индекс переименовываем в 〈ortho〉0.

Если не пустая, то заменяем тройку на две, с индексами 〈ortho〉1 и 〈ortho0〉:

s.〈ortho〉1 ::= s.〈ortho〉 ⋃ s.ADD
t.〈ortho〉1 ::= s.〈ortho〉1 | (e.〈ortho〉1)
e.〈ortho〉1 ::= @

s.〈ortho〉0 ::= s.〈ortho〉 \ s.ADD
t.〈ortho〉0 ::= s.〈ortho〉0 | (e.〈ortho〉0)
e.〈ortho〉0 ::= e.〈ortho〉

Если s.〈ortho〉 ⋃ s.ADD, то первую тройку отбрасываем и тип 〈ortho〉 переименовываем в 〈ortho〉0.

Иначе если s.〈ortho〉 \ s.ADD пусто и при этом пусто e.〈ortho〉, то отбрасываем вторую тройку и 〈ortho〉 переименовываем в 〈ortho〉1.

Иначе оставляем обе тройки, исходный тип 〈вид〉.〈ortho〉 заменяем на объединение новых типов 〈вид〉.〈ortho〉0 | 〈вид〉.〈ortho〉1.

Тип s.ADD определяется как объединение всех s-типов из ORTHO, индексы которых заканчиваются на 1.

При необходимости тип s.ADD может быть достроен до полной тройки известным образом.

Добавление e-типа к ОНФ

Оно выполняется аналогично добавлению s-типа. Точно также перебираются тройки из ORTHO, их индексы 〈ortho〉.

Если очередная тройка имеет пустую e-компоненту, то она переименовывается в 〈ortho〉0. Иначе тройка заменяется двумя

s.〈ortho〉1 ::= @
t.〈ortho〉1 ::= s.〈ortho〉1 | (e.〈ortho〉1)
e.〈ortho〉1 ::= e.〈ortho〉 ⋃ e.ADD

s.〈ortho〉0 ::= s.〈ortho〉
t.〈ortho〉0 ::= s.〈ortho〉0 | (e.〈ortho〉0)
e.〈ortho〉0 ::= e.〈ortho〉 \ e.ADD

где e.ADD — добавляемый тип. Аналогично нужно проверить каждую из троек на пустоту. Если одна из них пустая, то переименовываем исходный тип либо в 〈ortho〉〈b〉, где 〈ortho〉〈b〉 — индекс непустой тройки. Если непустые обе, то обе оставляем, а тип 〈вид〉.〈ortho〉 заменяем на объединение новых типов 〈вид〉.〈ortho〉0 | 〈вид〉.〈ortho〉1.

Тип e.ADD определяется как объединение всех e-типов из ORTHO, индексы которых заканчиваются на 1.

Также при необходимости можно достроить тип e.ADD до полной тройки.

Добавление к грамматике e-типа со структурными скобками сводится к рекурсивному определению типов для выражений в скобках, достраиванию этих типов до троек и замене скобочных термов для соответствующие t-типы.

Простая задача верификации

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

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

Поэтому теперь мы можем воспользоваться этим фундаментом для проверки типов в программах на Рефале. Но для начала нужно определиться, что же мы хотим поверять. В начале мы опишем задачу проверки типов для подмножества Рефала, приведём её решение, а затем обсудим, как рассматриваемое подмножество можно расширить.

Постановка простой задачи верификации типов

Базисным подмножеством Рефала-5 назовём множество программ на Рефале-5, в котором не используются условия и блоки. Предложения в базисном подмножестве имеют вид

〈образец〉 = 〈результат〉;

L-выражением (или L-образцом) назовём образцовое выражение, в котором отсутствуют повторные t- и e-переменные и отсутствуют подвыражения вида e.X PAT e.Y, где PAT — некоторая последовательность образцовых термов.

Ограниченным Рефалом назовём множество программ базисного подмножества Рефала-5, в котором все образцы являются L-выражениями и отсутствуют вызовы встроенных функций.

Определение ограниченного Рефала изначально было дано Турчиным в 1972 году, в его определении t-переменные в L-выражениях были вообще запрещены. Целью Турчина было определение подмножества, в котором выразима прогонка. Однако, добавление в ограниченный Рефал t-переменных на выразимость прогонки никак не влияет, кроме того, здесь мы решаем другую задачу.

Также, поскольку мы рассматриваем типизацию применительно к Рефалу-5, мы определяем ограниченный Рефал не как семантическое подмножество Рефала, а как синтаксическое подмножество Рефала-5. Так нам удобнее.

Простая задача верификации типов. Дана программа на ограниченном Рефале, дана грамматика типов и для каждой функции программы описан её тип в терминах типов грамматики. Кроме того, полагаем, что алфавит допустимых символов в поле зрения конечен и образован теми символами, которые явно представлены константами либо в программе, либо в грамматике типов, либо в типах аргументов и результатов функций.

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

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

В процессе решения задачи верификации можно делать дополнительные проверки:

1. Проверка на «мёртвый код»: для каждого предложения должно быть подмножество типа аргумента, при котором оно активируется. Предложение может быть «мёртвым кодом» либо если оно просто не соответствует типу аргумента, либо экранируется предшествующими.
2. Проверка на исчерпаемость: любое объектное выражение, входящее в тип аргумента, должно перехватываться одним из предложений.

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

Последующее изложение будет сосредоточено на решении задачи верификации типов, дополнительные проверки также будут рассматриваться, но рассматриваться «между делом».

Решение простой задачи верификации типов

Как и ранее, задачу будем решать поэтапно. Сначала мы опишем простейшее решение, затем предложим пути его улучшения.

Общий вид алгоритма верификации можно описать в следующем виде:

1. Исходные данные подвергаем предварительной нормализации:
   • Для каждого символа, присутствующего в тексте программы, добавляем к грамматике соответствующий синглетный тип.
   • Для каждого описания типов функции добавляем два типа: тип аргумента (обозначим его e.Arg[〈Func〉], где 〈Func〉 — имя функции) и тип результата (обозначим его e.Res[〈Func〉]). Соответственно, описание типа функции трансформируется в

     <〈Func〉 e.Arg[〈Func〉]> == e.Res[〈Func〉]
     

   • Строим ОНФ для получившейся грамматики типов.
2. В результате аргумент каждой функции будет представлен как объединение нескольких непересекающихся типов (по определению ОНФ).

   e.Arg[〈Func〉] ::= e.〈ortho1〉 | … | e.〈orthoN〉
   

   При этом каждый из e.〈orthoK〉 будет описан некоторым регулярным языком поверх алфавита t-типов из ORTHO. Для каждого e.〈orthoK〉 и каждого предложения выполняем верификацию предложения.

Данный алгоритм никак не учитывает экранирование предложений — это мы исправим позже. Кроме того, он содержит неопределённую процедуру верификации предложения. Определим её.

Задача верификации предложения и её решение

Задача верификации предложения. Дана функция 〈Func〉 ограниченного Рефала, номер предложения K и подмножество значений аргумента e.Arg′, представленное как регулярный язык поверх алфавита из t-типов ORTHO. Требуется проверить корректность вызовов в правой части (вложение фактических типов в формальные) и вложение фактического типа правой части в e.Res[〈Func〉].

Решение задачи сводится к сопоставлению регулярного языка e.Arg′ с образцом предложения и проверки вызовов в результатной части.

1. Выполняем сопоставление e.Arg′ с образцом k-го предложения, в результате получаем несколько решений.
2. Для каждого из решений выполняем проверку правой части.

Опишем обе процедуры — сопоставление регулярного языка поверх алфавита ортогональных t-типов с L-образцом и проверку правой части.

Сначала мы рассмотрим проверку типов в программах, где s-переменные отсутствуют, затем расширим алгоритм на случай, когда такие переменные есть.

К слову, ограничение на отсутствие повторных переменных не влияет на алгоритмическую полноту Рефала. Нормальные алгорифмы тривиально моделируются в базисном Рефале, и несколько более громоздко — в ограниченном Рефале. Моделирование машины Тьюринга в ограниченном Рефале тоже не требует наличия повторных s-переменных.

Сопоставление e-типа из ORTHO с образцом Рефала без повторных переменных

Хотя, на самом деле, это процедура сопоставления любого регулярного языка поверх алфавита t-типов из ORTHO с образцом Рефала. Сопоставление в результате даёт ноль или более решений.

Решение представляет собой отображение s- и t-переменных образца в s- и t-типы троек из ORTHO и e-переменных образца в некоторые регулярные языки поверх алфавита t-типов из ORTHO.

В процессе сопоставления мы будем рассматривать системы уравнений вида RegLang : Pat, где RegLang является регулярным языком, Pat — L-выражением.

Решение в процессе будет разветвляться. Если некоторая ветвь решений не имеет, то она отсекается. На концах ветвей мы будем иметь решения.

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

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

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

Будем считать, что конечный автомат описывается четвёркой <Q, qs, δ, F>, где Q — множество состояний, qs — стартовое состояние, δ — функция переходов и F — множество финальных состояний. Алфавит явно не представлен, поскольку для всех автоматов он одинаков и является множеством t-типов из ORTHO. Функция переходов определена как

δ : Q×t.X → Q

т.е. её первым аргументом является состояние, вторым — тип и результат — состояние. Таким образом, считаем, что автомат детерминированный. Дальнейший алгоритм можно описать и для недетерминированного автомата, а также для недетерминированного автомата с λ-переходами (переходами по пустой строке), однако изложение алгоритма в этом случае будет более громоздким.

Система уравнений инициализируется единственным уравнением

<Q, qs, δ, F> : P

где слева — автомат, а справа — L-выражение.

В дальнейшем изложении буквой P мы будем обозначать некоторый образец, буквой T — некоторый образец терма (t-переменная, s-переменная или скобочный терм), Sym — некоторый символ Рефала.

В дальнейшем система преобразуется по следующим правилам:

• Если система пустая, значит данная ветвь решения успешно завершилась.
• Если в системе есть уравнение вида

  <Q, qs, δ, F> : ε
  

  то если qs ∈ F, то исключаем уравнение из системы. Иначе отсекаем ветвь решения.

• Если в системе есть уравнение вида

  <Q, qs, δ, F> : T E
  

  то для каждого t-типа t.X, такого что δ(qs, t.X) = q′ строим новую ветку решения, где данное уравнение заменяется уравнениями

  t.X : T
  <Q, q′, δ, F> : E
  

• Если в системе есть уравнение вида

  <Q, qs, δ, F> : E T
  

  то для каждого t-типа t.X, такого, что δ(q′, t.X) = q″, q″ ∈ F строим новую ветку решения, где данное уравнение заменяется уравнениями

  <Q, qs, δ, { q″ }> : E
  t.X : T
  

• Если в системе есть уравнение вида

  t.X : t.Y
  

  то к решению данной ветки добавляем отображение t.Y → t.X, уравнение исключаем из системы.

• Если в системе есть уравнение вида

  t.X : s.Y
  

  то к решению данной ветки добавляем отображение s.Y → s.X, где s.X — s-компонента тройки с термом t.X. Уравнение исключаем из системы.

• Если в системе есть уравнение вида

  t.X : Sym
  

  то если s-компонента s.X тройки с типом t.X включает символ Sym, т.е. Sym ∈ s.X, то исключаем уравнение из системы. Иначе отсекаем данную ветку.

• Если в системе есть уравнение вида

  t.X : (E)
  

  то заменяем его уравнением

  e.X : E
  

  где e.X — e-компонента тройки с типом t.X.

• Если в системе есть уравнение вида

  <Q, qs, δ, F> : e.Y
  

  то к решению ветки добавляем отображение e.Y → <Q, qs, δ, F>, уравнение удаляем.

Проверка правой части для некоторого решения

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

Проверять вложение мы можем только для типов одной грамматики, представленной в ОНФ. Поэтому нам нужно типы аргументов и тип правой части добавить к исходной грамматике и повторно выполнить процедуру нормализации. Либо можно воспользоваться процедурой добавления нового e-типа к грамматике в ОНФ.

Рассмотрим вызов некоторой функции

<F E>

Фактический аргумент в форме типового выражения e.CallArg получается путём подстановки в E вместо переменных их конкретных значений из решения и вместо вызовов функций (например, <G …>) типов их результатов (e.Res[G]). Затем тип e.CallArg добавляется к грамматике типов (типы в ORTHO при этом могут переименоваться и расщепиться) и проверяется вложение типа e.CallArg в e.Arg[F].

Аналогичным образом проверяется корректность возвращаемого типа. Делаются те же подстановки в правую часть E, для полученного типа e.Res выполняется проверка его вложения в тип e.Res[〈Func〉].

Учёт повторных s-переменных в образце

Проверка правой части предложения при известных значениях переменных