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

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

2 голосов
/ 20 июня 2019

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

1 Ответ

2 голосов
/ 22 июня 2019

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

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

...