О типизации рефальских выражений

Subject: О типизации рефальских выражений
From: Mikhail Kovtun (mkovtun@mindspring.com)
Date: Sun Aug 19 2001 - 18:55:10 MSD

Привет всем!

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

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

Регулярные языки деревьев (чтобы было не страшно:-) -- это ML-евские datatype.

Несколько фактов об регулярных языках деревьев:

-- Распознаются конечными автоматами.

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

-- Мощнее регулярных строковых языков; в некотором смысле, эквивалентны контекстно-свободным языкам. Именно: для любого контекстно-свободного языка L можно построить регулярный язык деревьев T такой, что множество предложений языка L -- это в точности множество строк, являющихся списками терминалов деревьев из T. (Кстати, по-английски такая строка называется yield -- а как по-русски? Я бы воздержался от транслитерации. А интересно, как этот термин переведут любители "рестрикций на перфектных деревьях"? Эх, был бы жив адмирал Шишков, я бы отправил в его журнал статью под названием "К чему могут привести попытки перевода иностранных слов путем транслитерации":-). Другими словами, множество деревьев синтаксического разбора некоторого строкового контекстно-свободного языка образует регулярный язык деревьев.

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

Phylum => Constructor(Phylum1,...,Phylumn)

Phyla (Шишков, прости!) служат нетерминалами в выводе. В сгенерированном дереве есть только конструкторы, причем 0-местные конструкторы являются терминалами. В приложении к типизации, 0-местные конструкторы естественно отождествить с примитивными типами.

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

BinTree => NonTerminal(Integer,BinTree,BinTree)
BinTree => Terminal()
Integer => int()

Нетрудно видеть, что с точностью до обозначений и естественных сокращений, это ML-евское определение datatype.

Применительно к рефалу, добавим новую форму правила:

Phylum => регулярное выражение, составленное из phyla

и разрешим только 1- и 0-местные конструкторы (многоместные конструкторы теперь выразимы как одноместные конструкторы, имеющие аргументом регулярное выражение вида "конкатенация").

(Я бы мог привести формальное определение, но на данном этапе это только запутало бы дело.)

В качестве примера рассмотрим двоичные деревья, нетерминальным вершинам которых приприсаны целые числа так, что обход "левое поддерево -- корень -- правое поддерево" выдает упорядоченную последовательность чисел. Рассмотрим также функцию, которая добавляет к дереву новое число с сохранением порядка.

На "нетипизированном рефале" эта функция выглядит так:

AddNode
{
    s.new () = (s.new () ());
    s.new (s.root t.left t.right),
        <GreaterThen s.new s.root> : {
            True  = (s.root t.left <AddNode s.new t.right>);
            False = (s.root <AddNode s.new t.left> t.right);
        };
};

(Я надеюсь, что здесь не слишком много синтаксических ошибок.)

Теперь добавим типовую информацию (я ни в коем случае не настаиваю на синтаксисе; это дело будущего):

datatype
T1 => (T2):nt | ():t;
T2 => int T1 T1;
T3 => int T1
enddatatype;

AddNode : T3 -> T1
{
    s:int.new ():T1 = (s:int.new ():t ():t):nt;
    s:int.new (s:int.root t:T1.left t:T1.right):T1,
        <GreaterThen s:int.new s:int.root>:bool : {
            True:bool  = (s:int.root t:T1.left <AddNode s:int.new t:T1.right>:T1):nt;
            False:bool = (s:int.root <AddNode s:int.new t:T1.left>:T1 t:T1.right):nt;
        };
};

Здесь:

Несколько замечаний:

1. Типами помечены все термы; при этом пометки в левой части -- это phyla, а пометки в правой части -- конструкторы. (Примитивные типы при подходящей формализации попадают в обе категории).

2. Как мне кажется, любую данную типизацию можно проверить (т.е. существует алгоритм проверки).

3. В общем случае, восстановить типы по нетипизируемой программе невозможно. Достаточно того, что любую рефальскую функцию можно доопределить до всюду определенной с помощью предложения "e.x=e.x" -- и такое предложение часто используется в реальных программах "не по делу". Однако кажется, что по достаточно богатой частичной типизации восстановить полную типизацию можно. Вопрос: можно ли разумным способом определить понятие "минимальной типизации", по которой можно однозначно восстановить полную типизацию?

4. Можно представить себе реализацию, в которой каждый терм хранит при себе тип, и программа должна быть полностью типизирована. В такой реализации отождествление будет происходить по-другому: например, образец "e.x s.1 ey" в стандартной реализации отождествляется с выражением "1'A'" (целое и литера) как e.x=пусто, s.1=1, e.y='A'; типизированный же образец "e:Any.x s:char.1 e:Any.y" как e.x=1, s.1='A', e.y=пусто. Но, может быть, это и лучше?

Другой пример (где встречаются открытые переменные) -- слегка модифицированная функция Next из примера "Paths in graph" книги по Рефалу-5:

Next
{
    s.V e.x s.V(e.N) e.y = e.N
};

Типизированный вариант:

datatype
Vx => char;    /* Vertex */
Vxs => Vx*;    /* Vertices */
T1 => (Vxs):vxs;    /* List of vertices in parentheses */
T2 => Vx T1;        /* Vertex with a list of successors */
Gr => T2*;     /* Graph */
Arg => Vx Gr   /* Argument of Next function */
enddatatype;

Next : Arg -> Vxs
{
    s:Vx.V e:Gr.x s:Vx.V(e:Vxs.N):T1 e:Gr.y = e:Vxs.N
};

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

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

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

P.S. Представление графа в последнем примере, конечно, является "ужасным" с точки зрения времени исполнения функции: имея вершину, мы каждый раз ищем связанную с ней информацию -- вместо того, чтобы связать ее один раз при построении графа. В рефале одним из разумных способов представить граф является использование ящиков. Однако образцы не могут заглядывать в ящики, что усложняет программирование. Были ли какие-нибудь интересные мысли по этому поводу?

--
Best regards,

Mikhail
 

This archive was generated by hypermail 2b25 : Mon Oct 25 2004 - 21:24:59 MSD