Subject: Re: О типизации рефальских выражени
From: Arkady Klimov (klark@bagirra.net)
Date: Sun Aug 19 2001 - 23:41:30 MSD
Привет всем
Некоторые вопросы и комментарии см. ниже по тексту.
Прошу прощения за то, что цитирую все без сокращений.
АРКадий.
----- Original Message -----
From: Mikhail Kovtun
To: refal@botik.ru
Sent: Sunday, August 19, 2001 5:55 PM
Subject: О типизации рефальских выражений
Привет всем!
Мне пришла в голову одна мысль, которой я бы хотел поделиться -- может быть, здесь есть что-то стоящее.
В качестве типов рефальских выражений предлагается использовать регулярные выражения, построенные из регулярных языков деревьев.
Регулярные языки деревьев (чтобы было не страшно:-) -- это 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-местные конструкторы (многоместные конструкторы теперь выразимы как одноместные конструкторы, имеющие аргументом регулярное выражение вида "конкатенация").
АРК:
Одно интересное замечание: похоже, это получается в точности то, как определяется тип xml-документа посредством DTD (если отвлечься от некоторых деталей, например атрибутов).
(Я бы мог привести формальное определение, но на данном этапе это только запутало бы дело.)
В качестве примера рассмотрим двоичные деревья, нетерминальным вершинам которых приприсаны целые числа так, что обход "левое поддерево -- корень -- правое поддерево" выдает упорядоченную последовательность чисел. Рассмотрим также функцию, которая добавляет к дереву новое число с сохранением порядка.
На "нетипизированном рефале" эта функция выглядит так:
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;
};
};
Здесь:
a.. Вся типовая информация выделена курсивом и цветом.
b.. В определении типов имена конструкторов записаны через двоеточие после аргументов.
Несколько замечаний:
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
};
Кстати, последний пример показывает, что для проверки правильности типизации требуется распознавать эквивалентность регулярных выражений (что является разрешимой задачей, но сложной).
Оба примера не очень хороши, поскольку в первом нет открытых переменных, а во втором -- не рекурсивная структура данных. Не знает ли кто-нибудь хорошего примера, в котором есть все?
Очень хотелось бы услышать ваше мнение. Если это кажется интересным, можно было бы рассмотреть формализацию этого подхода.
АРК:
С учетом замечания выше об XML это может иметь практический смысл (нужно еще добавить в такой язык средства обработки атрибутов).
А в более широком контексте (развитие рефала?) это тоже очень интересно. В принципе это направлено на то же, что обсуждается в моем письме в группу refal двухгодичной давности (от 11 августа 1999 года, Subj="Refal weak typing"). Только решение здесь предлагается несколько иное. Кажется, более общее (то есть система типов помощнее). Если она по-прежнему столь же "разрешима", то наверно, она предпочтительнее. У меня система более ограничена: допускаются не любые регулярные выражения, а непересекающиеся объединения выражений, составленных из конкатенаций и не более одного итератора - L-выражений. (Впрочем, может быть с учетом композиций, соотношение между нашими системами и более сложное. Надо изучить все это внимательнее.) Я исходил из действующей практики: "разумные" программисты строят только такие структуры. Твое "обобщение" выглядит очень симпатично, и если не слишком зарубается разрешимость разных задач, то я готов за него голосовать.
P.S. Представление графа в последнем примере, конечно, является "ужасным" с точки зрения времени исполнения функции: имея вершину, мы каждый раз ищем связанную с ней информацию -- вместо того, чтобы связать ее один раз при построении графа. В рефале одним из разумных способов представить граф является использование ящиков. Однако образцы не могут заглядывать в ящики, что усложняет программирование.
АРК:
Но можно "заглядывать" с помощью условий рефала-5/6/+. Это может показаться громоздким, так как должно быть вынесено из выражения, но на практике вполне удобоваримо.
Были ли какие-нибудь интересные мысли по этому поводу? --
Best regards,
Mikhail
This archive was generated by hypermail 2b25 : Mon Oct 25 2004 - 21:24:59 MSD