Реализация имеющегося алгоритма
От: Stalker-g2  
Дата: 08.01.06 14:27
Оценка:
Всем привет!

Прошу совета по реализации на C/C++ следующего алгоритма! Какие есть идеи хранения и преобразования выражения? Алгоритм следующий:

# Транслятор формул ИППП в множество предложений

Разработать способ "машинного" представления (т.е. представления линейной последовательностью символов кодировки ASCII) языка "чистого" исчисления предикатов первого порядка (ИППП) (см. [1, с. 228]). "Чистым" называется ИППП, в конструировании формул которого не участвуют функциональные буквы и термы. При этом правила построения атомарных формул заимствовать из языка Пролог [3, 4].
Разработать программу, осуществляющую преобразование вводимых пользователем (на предложенном языке) формул ИППП в множество предложений.
Примечание. Такое преобразование имеет много общего с преобразованием произвольных логических формул в конъюктивную нормальную форму.

Алгоритм преобразования состоит из следующих шагов [7].

1. Исключение из исходной формулы символов импликации, для чего используется ~F|G вместо А->G (где F и G — любые формулы ИППП, ~ — знак отрицания, | — симол операции ИЛИ, ? — символ операции И).
2. Ограничение области действия отрицания только атомарными формулами, для чего используются правила деМоргана:
~F|~G вместо ~(F?G)
~F?~G вместо ~(F|G)
3. Разделение переменных — переименование их с тем, чтобы каждый квантор имел свою переменную.
4. Исключение кванторов существования введением сколемовских констант и функций. Здесь формула вида

Ey(...P(y)...) заменяется формулой ...P(a)...
А формула вида
Ax(Ey(...P(x,y)...)) заменяется формулой Ax(...P(x,f(x))...)
5. где A обозначает квантор всеобщности, E — квантор существования, a — сколемовская константа, f(x) — сколемовская функция. Вынесение кванторов всеобщности в начало формулы и их исключение из формулы.
6. Приведение формулы ("очищенной" от кванторов) в конъюктивную нормальную форму. Используется (F|G)?(F|H) вместо F|(G?H).
7. Исключение символа ? (И), в результате образуется множество дизъюнктов, называемых также предложениями.

Будут полезны любые идеи!!
Re: Реализация имеющегося алгоритма
От: Кодт Россия  
Дата: 09.01.06 10:41
Оценка:
Здравствуйте, Stalker-g2, Вы писали:

SG># Транслятор формул ИППП в множество предложений


При желании, можно сделать чисто строковый транслятор, но, на мой взгляд, это мучительно. Лучше — графовый.

1) Строишь орграф выражений — сперва это просто дерево (с узлами "объявление предиката", "вхождение предиката" "квантор", "двух- или одно-местная операция", "переменная", "константа")
2) Склеиваешь листья, соответствующие вхождениям одних и тех же переменных (естественно, в пределах их контекста — т.е. внутри определения предиката или внутри подвыражения с квантором)
Тем самым, избавляешься от головной боли по поводу омонимов
3) Дальше над этим графом проводишь все упомянутые выше преобразования
— замена переменной на сколемовскую функцию сводится к замене содержимого узла (при этом все вхождения этой переменной автоматически заменятся, поскольку они предварительно были склеены)
— подстановка предиката (предварительно избавленного от кванторов) в выражение сводится к копированию его графа и замене листьев-аргументов на фактические значения
— преобразования булевых операций приводят к добавлению/исчезновению некоторых узлов

Перед тем, как бросаться реализовывать эту механику, советую прочитать какую-нибудь книгу, в которой описываются нюансы редукции графов.
Например, Харрисон, Филд "Функциональное программирование". (http://lib.ru/CTOTOR/FUNCPROG/)
Перекуём баги на фичи!
Re[2]: Реализация имеющегося алгоритма
От: Stalker-g2  
Дата: 09.01.06 11:31
Оценка:
К>При желании, можно сделать чисто строковый транслятор, но, на мой взгляд, это мучительно. Лучше — графовый.

К>1) Строишь орграф выражений — сперва это просто дерево (с узлами "объявление предиката", "вхождение предиката" "квантор", "двух- или одно-местная операция", "переменная", "константа")

К>2) Склеиваешь листья, соответствующие вхождениям одних и тех же переменных (естественно, в пределах их контекста — т.е. внутри определения предиката или внутри подвыражения с квантором)

Огромное спасибо за ответ!
Книжку уже списываю,а встречный вопрос-я так понимаю, что там речь про алгоритмы на графах,с ними у меня опыта 0... А невозможно ли реализовать алгоритм на деревьях бинарного поиска?
Re[3]: Реализация имеющегося алгоритма
От: Кодт Россия  
Дата: 09.01.06 12:00
Оценка:
Здравствуйте, 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 на сколемовскую функцию) потребует корректировки ровно одной ссылки, а не всех, кто использует этот узел.
Перекуём баги на фичи!
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.