Здравствуйте, Stalker-g2, Вы писали:
SG># Транслятор формул ИППП в множество предложений
При желании, можно сделать чисто строковый транслятор, но, на мой взгляд, это мучительно. Лучше — графовый.
1) Строишь орграф выражений — сперва это просто дерево (с узлами "объявление предиката", "вхождение предиката" "квантор", "двух- или одно-местная операция", "переменная", "константа")
2) Склеиваешь листья, соответствующие вхождениям одних и тех же переменных (естественно, в пределах их контекста — т.е. внутри определения предиката или внутри подвыражения с квантором)
Тем самым, избавляешься от головной боли по поводу омонимов
3) Дальше над этим графом проводишь все упомянутые выше преобразования
— замена переменной на сколемовскую функцию сводится к
замене содержимого узла (при этом все вхождения этой переменной автоматически заменятся, поскольку они предварительно были склеены)
— подстановка предиката (предварительно избавленного от кванторов) в выражение сводится к
копированию его графа и замене листьев-аргументов на фактические значения
— преобразования булевых операций приводят к добавлению/исчезновению некоторых узлов
Перед тем, как бросаться реализовывать эту механику, советую прочитать какую-нибудь книгу, в которой описываются нюансы редукции графов.
Например, Харрисон, Филд "Функциональное программирование". (
http://lib.ru/CTOTOR/FUNCPROG/)
К>При желании, можно сделать чисто строковый транслятор, но, на мой взгляд, это мучительно. Лучше — графовый.
К>1) Строишь орграф выражений — сперва это просто дерево (с узлами "объявление предиката", "вхождение предиката" "квантор", "двух- или одно-местная операция", "переменная", "константа")
К>2) Склеиваешь листья, соответствующие вхождениям одних и тех же переменных (естественно, в пределах их контекста — т.е. внутри определения предиката или внутри подвыражения с квантором)
Огромное спасибо за ответ!
Книжку уже списываю,а встречный вопрос-я так понимаю, что там речь про алгоритмы на графах,с ними у меня опыта 0...
А невозможно ли реализовать алгоритм на деревьях бинарного поиска?
Здравствуйте, Stalker-g2, Вы писали:
SG>Книжку уже списываю,а встречный вопрос-я так понимаю, что там речь про алгоритмы на графах,с ними у меня опыта 0... А невозможно ли реализовать алгоритм на деревьях бинарного поиска?
А при чём здесь поиск?
Деревья — ну, наверное, проще всего работать с бинарными. Только это будут не деревья поиска, а cons-пары.
Можно не использовать графы — но тогда сложнее будет вносить поправки во все вхождения одной переменной. Нужно же учитывать, что могут встречаться тёзки — разные переменные с одним и тем же именем. Для этого в лямбда-исчислении был разработан довольно заморочистый аппарат, как чисто на строках избавляться от неоднозначностей.
С графами особой сложности нет. Используются не "графы вообще", а обобщение деревьев (заключающееся в том, что некоторые дочерние узлы разделяются между несколькими родительскими).
Например, x & (!x | y) представляется
| |
AND AND
/ \ | \
x OR | OR
/ \ | | \
NOT y | NOT y
| |/
x x
Только удобнее расщепить каждый узел на два:
|
*
|
AND
| \
* *
| |
| OR
| | \
| * *
| | |
| NOT y
|/
*
|
x
Тогда замена содержимого (скажем, переменной x на сколемовскую функцию) потребует корректировки ровно одной ссылки, а не всех, кто использует этот узел.