Определение правил и фактов (циклическое?) в механизме вывода
Я работаю над двигателем обратной цепи в качестве школьного проекта. До сих пор я в основном делал проекты на C, поэтому я решил попробовать Haskell для этого проекта. Я прочитал LYAH, чтобы начать работу, и приступил к реализации представления правил и фактов в моей машине вывода. Пока вот что у меня получилось
module Inference () where
type Op = Bool -> Bool -> Bool
type Label = String
type Fact = (Label, [Rule])
data Rule = Operation Rule Op Rule
| Fact Fact
eval_fact:: [Label] -> Fact -> Bool
eval_fact proved (label,rules) = label `elem` proved || any (eval_rule proved) rules
eval_rule:: [Label] -> Rule -> Bool
eval_rule proved (Fact x) = eval_fact proved x
eval_rule proved (Operation r op r') = eval_rule proved r `op` eval_rule proved r'
Идея состоит в том, чтобы иметь некий граф, в котором узлы фактов указывают на узлы правил, если факт уже не находится в списке известных фактов.
Однако здесь я сталкиваюсь с проблемой определения моих действительных фактов и правил.
Делать что-то вроде
let fact_e = ("E", [Fact ("C", [(Operation (Fact ("A", [])) (||) (Fact ("B", [])))])])
в ghci для представления правил
C => E
A || B => C
Это работает. Но я действительно не вижу, в каком направлении двигаться, чтобы создавать эти правила программно. Кроме того, я не понимаю, как я могу обрабатывать циклические правила с помощью этой схемы (например, добавляя правило E => A).
Я видел, что есть способы определить самоссылающиеся структуры данных в Haskell с помощью трюка под названием «Завязывание узла» в вики Haskell, но я не вижу, как (и даже если) я должен применить это в данном случае.
Мой вопрос, по сути, в том, иду ли я в правильном направлении, или у меня все наоборот с таким подходом?
PS: Мне тоже кажется, что мой код не такой лаконичный, как должен быть (проходя по списку [Label], повторяя eVal_rule proved много раз...), но я тоже толком не знаю, как это сделать в другом способ.
Я имею в виду, что не вижу, как это сделать динамически (например, путем анализа файла), а не статически записывать их в коде. Что касается let, это то, что я пытался, спасибо :).
Для динамического создания списка Fact вы должны иметь возможность сделать это, как и любую другую структуру данных. Например, если у вас есть C => E, вы можете разделить его на ["C", "=>", "E"], затем написать функции для преобразования отдельных элементов списка в Operation и другие Fact, а затем объединить их вместе с помощью соответствующих конструкторов. Трудно сказать что-либо помимо этого, не зная точно, на чем вы застряли; вы боретесь с разбором String или преобразованием проанализированного String в Fact?
Моя проблема больше связана с возможным самоотнесением правил. Разобрать мой источник в моем представлении несложно, но перевести в самореферентное выражение немного сложнее. Я думаю, что ответ от @K. А. Бур — это именно то, что я пытался сделать.
Ответы 1
Идея состоит в том, чтобы сначала проанализировать правила в промежуточном представлении, которое является самореферентным нет. Например, учитывая представление:
type Program = [(Label, [Rule_P])]
data Rule_P = Operation_P Rule_P Op Rule_P | Fact_P Label
тогда набор правил:
C => E
A || B => C
E => A
F => E
будет проанализирован, собран по импликативной цели и представлен как:
prog1 :: Program
prog1 = [ ("E", [ Fact_P "C" -- C => E
, Fact_P "F" ]) -- F => E
, ("C", [ Operation_P (Fact_P "A") (||) (Fact_P "B") ]) -- A || B => C
, ("A", [ Fact_P "E" ]) ] -- E => A
Затем, чтобы преобразовать это в циклически самореферентную базу знаний (используя исходный тип Fact):
type Knowledge = [Fact]
вы завязываете узел так:
learn :: Program -> Knowledge
learn program = knowledge
where
knowledge :: [Fact]
knowledge = [ (target, map learn1 rules_p) | (target, rules_p) <- program ]
remember lbl = fromJust (find ((==lbl) . fst) knowledge)
learn1 :: Rule_P -> Rule
learn1 (Fact_P lbl) = Fact (remember lbl)
learn1 (Operation_P rule1 op rule2) = Operation (learn1 rule1) op (learn1 rule2)
Это, пожалуй, заслуживает некоторого пояснения. Мы создаем knowledge, просто применяя learn1 для преобразования каждого вхождения несамореферентного Rule_P в исходной программе в самореферентный Rule в базе знаний. Функция learn1 делает это очевидным рекурсивным способом и «завязывает узел» на каждом Fact_P, просматривая (rememberинг) метку в теле knowledge, определение которой мы находимся в процессе определения.
В любом случае, чтобы доказать себе, что это самореференциально, вы можете поиграть с ним в GHCi:
> know1 = learn prog1
> Just [Operation factA _ _] = lookup "C" know1
> Fact ("A", [factE]) = factA
> Fact ("E", [factC, _]) = factE
> Fact ("C", [Operation factA' _ _]) = factC
> Fact ("A", [factE']) = factA'
Конечно, пытаясь:
> eval_fact [] $ fromJust $ find ((= = "E").fst) (learn prog1)
будет зацикливаться до тех пор, пока не закончится память, поскольку он пытается (безуспешно) доказать E из C из A из E и т. д., поэтому вам нужно будет добавить некоторую логику, чтобы прервать циклические доказательства.
Разве вы уже не создаете правила программно? То есть вы уже указываете правила, такие как
fact_e, используя программирование. Для циклических правил вы должны иметь возможность просто поместить их все в один блокlet(например,let x1 = val1 <newline> x2 = val2 <newline> x3 = val3 in _), и ленивость автоматически определит цикличность. Что касается твоего P.S.: для прохождения[Label]попробуй узнать о «Readerмонаде». Повторениеeval_rule provedтакже должно стать немного лучше, если вы используетеReader.