Определение правил и фактов (циклическое?) В механизме вывода

Я работаю над движком с обратной цепочкой как школьный проект. До сих пор я в основном работал над проектами на 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 много раз ...), но я действительно не знаю, как это сделать в другом способ.


inference-engine haskell recursive-datastructures cyclic-reference
person VannTen    schedule 20.06.2019    source источник
comment
Разве вы еще не конструируете правила программно? То есть вы уже задаете такие правила, как fact_e, используя программирование. Для циклических правил вы должны иметь возможность просто поместить их все в один let блок (например, let x1 = val1 <newline> x2 = val2 <newline> x3 = val3 in _), а лень автоматически отсортирует цикличность. Что касается вашего P.S .: для передачи [Label], попробуйте узнать о монаде Reader. Повторение eval_rule proved также должно стать немного лучше, если вы используете Reader.   -  person bradrn    schedule 21.06.2019
comment
Я имею в виду, что я не вижу, как это делать динамически (например, путем синтаксического анализа из файла), а не статически записывать их в код. Насчет let, вот что я пробовал, спасибо :).   -  person VannTen    schedule 21.06.2019
comment
Для динамического создания списка Fact вы должны иметь возможность делать это, как и любую другую структуру данных. Например, если у вас есть C => E, вы можете разделить его на ["C", "=>", "E"], затем написать функции для преобразования отдельных элементов списка в Operation и другие Fact, а затем объединить их вместе с помощью соответствующих конструкторов. Трудно сказать что-то еще, не зная точно, на чем вы застряли; вы боретесь с синтаксическим анализом String или преобразованием проанализированного String в Fact?   -  person bradrn    schedule 22.06.2019
comment
Моя проблема больше в том, что правила могут быть указаны сами собой. Разобрать мой источник в моем представлении несложно, но перевод на самореференциальное выражение немного сложнее. Я знаю ответ от @K. А. Бур - это именно то, что я пытался сделать.   -  person VannTen    schedule 24.06.2019

Ответы (1)


arrow_upward
2
arrow_downward

Идея состоит в том, чтобы сначала разобрать правила в промежуточное представление, которое не самореферентно. Например, учитывая представление:

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, просматривая (remembering) метку в теле 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 и т. д., поэтому вам нужно добавить некоторую логику для прерывания циклических доказательств.

person K. A. Buhr    schedule 22.06.2019