2015-03-22 3 views
4

Я пытаюсь написать пропозициональный логический решатель в Haskell. Я представляю логические выражения с рекурсивным типом данных, называемым «Sentence», который имеет несколько подтипов для разных операций - «AndSentence», «OrSentence» и т. Д. Поэтому я думаю, что это дерево с несколькими типами узлов, каждый из которых имеет 0, 1, или 2 детей.«Поведение по умолчанию» для рекурсивных типов данных Haskell

Кажется, что это работает, но некоторые из кода являются повторяющимися, и я думаю, что должен быть лучший способ выразить это. В основном у меня есть несколько функций, в которых «поведение по умолчанию» состоит в том, чтобы функция просто рекурсивно действовала на дочерних узлах узла, опустившись на определенные типы узлов (обычно это «AtomicSentences», которые являются листьями). Итак, я пишу функцию, как:

imply_remove :: Sentence Symbol -> Sentence Symbol 
imply_remove (ImplySentence s1 s2) = OrSentence (NotSentence (imply_remove s1)) (imply_remove s2) 
imply_remove (AndSentence s1 s2) = AndSentence (imply_remove s1) (imply_remove s2) 
imply_remove (OrSentence s1 s2) = OrSentence (imply_remove s1) (imply_remove s2) 
imply_remove (NotSentence s1) = NotSentence (imply_remove s1) 
imply_remove (AtomicSentence s1) = AtomicSentence s1 

и я хочу более лаконичный способ, чтобы написать строки для «AndSentence», «OrSentence» и «NotSentence».

Кажется, что функторы похожи на то, что я хочу, но это не сработало ... Я хочу воздействовать на поддеревья, а не на некоторые значения, содержащиеся в каждом узле поддеревьев.

Есть ли правильный способ сделать это? Или более естественный способ структурирования моих данных?

+1

Я бы предложил библиотеку [синтаксис] (https://hackage.haskell.org/package/syntactic). – crockeea

ответ

3

Вы могли бы написать функцию по умолчанию, который определяет, как символ должен быть обработан, если никакого преобразования не относится к нему:

default_transformation :: (Sentence Symbol -> Sentence Symbol) -> Sentence Symbol -> Sentence Symbol 
default_transformation f (ImplySentence s1 s2) = ImplySentence (f s1) (f s2) 
default_transformation f (AndSentence s1 s2) = AndSentence (f s1) (f s2) 
default_transformation f (OrSentence s1 s2) = OrSentence (f s1) (f s2) 
default_transformation f (NotSentence s1) = NotSentence (f s1) 
default_transformation f (AtomicSentence s1) = AtomicSentence s1 

Функция принимает конкретное преобразование в качестве параметра.

Если вы пишете ваши конкретные преобразования вам нужно только написать случаи, что отличаются от значений по умолчанию и добавить по умолчанию в качестве последнего случая:

imply_remove :: Sentence Symbol -> Sentence Symbol 
imply_remove (ImplySentence s1 s2) = OrSentence (NotSentence (imply_remove s1)) (imply_remove s2) 
imply_remove s = default_transformation imply_remove s 

Преимущество этого подхода заключается в том, что оно может быть проще для реализации, потому что он не нуждается в каких-либо зависимостях.

5

Это выглядит как прекрасный случай для recursion-schemes.

Во-первых, мы описываем ваш тип Sentence sym как фиксированную точку уровня подходящего функтора.

{-# LANGUAGE DeriveFunctor, LambdaCase #-} 

import Data.Functor.Foldable -- from the recursion-schemes package 

-- The functor describing the recursive data type 
data SentenceF sym r 
    = AtomicSentence sym 
    | ImplySentence r r 
    | AndSentence r r 
    | OrSentence r r 
    | NotSentence r 
    deriving (Functor, Show) 

-- The original type recovered via a fixed point 
type Sentence sym = Fix (SentenceF sym) 

выше Sentence sym типа почти идентичен исходному, за исключением того что все должно быть обернуто внутри Fix. Адаптация оригинального кода для использования этого типа полностью механическая: где мы использовали (Constructor ...), теперь мы используем Fix (Constructor ...). Например

type Symbol = String 

-- A simple formula: not (p -> (p || q)) 
testSentence :: Sentence Symbol 
testSentence = 
    Fix $ NotSentence $ 
     Fix $ ImplySentence 
     (Fix $ AtomicSentence "p") 
     (Fix $ OrSentence 
      (Fix $ AtomicSentence "p") 
      (Fix $ AtomicSentence "q")) 

Вот исходный код, с его увольнениями (усугубляются дополнительных Fix х годов).

-- The original code, adapted 
imply_remove :: Sentence Symbol -> Sentence Symbol 
imply_remove (Fix (ImplySentence s1 s2)) = 
    Fix $ OrSentence (Fix $ NotSentence (imply_remove s1)) (imply_remove s2) 
imply_remove (Fix (AndSentence s1 s2)) = 
    Fix $ AndSentence (imply_remove s1) (imply_remove s2) 
imply_remove (Fix (OrSentence s1 s2)) = 
    Fix $ OrSentence (imply_remove s1) (imply_remove s2) 
imply_remove (Fix (NotSentence s1)) = 
    Fix $ NotSentence (imply_remove s1) 
imply_remove (Fix (AtomicSentence s1)) = 
    Fix $ AtomicSentence s1 

Давайте выполнить тест по оценке imply_remove testSentence: результат чего мы ожидаем:

-- Output: not ((not p) || (p || q)) 
Fix (NotSentence 
    (Fix (OrSentence 
     (Fix (NotSentence (Fix (AtomicSentence "p")))) 
     (Fix (OrSentence 
     (Fix (AtomicSentence "p")) 
     (Fix (AtomicSentence "q"))))))) 

А теперь, давайте использовать ядерное оружие, заимствованные из рекурсии-схем:

imply_remove2 :: Sentence Symbol -> Sentence Symbol 
imply_remove2 = cata $ \case 
    -- Rewrite ImplySentence as follows 
    ImplySentence s1 s2 -> Fix $ OrSentence (Fix $ NotSentence s1) s2 
    -- Keep everything else as it is (after it had been recursively processed) 
    s -> Fix s 

Если мы проведем тест imply_remove2 testSentence, мы получим тот же результат, что и исходный код.

Что делает cata? Очень грубо, когда применяется к такой функции, как в cata f, он создает катамарфит , т.е.функция, которая

  1. принимает формулу друг от друга в его подкомпонентов
  2. рекурсивно применить cata f к найденным подкомпонентов
  3. собирает преобразованные компоненты в формулу
  4. проходит эта последняя формула (с обработанной подформулах) до f так что может быть затронуто самое верхнее соединение.

Последний шаг - тот, который выполняет фактическую работу. \case выше выполняет только требуемое преобразование. Все остальное обрабатывается cata (и экземпляр Functor, который был автоматически сгенерирован).

Все сказанное выше, я бы не рекомендовал кому-либо слегка перейти на recursion-schemes. Использование cata может привести к очень изящному коду, но для этого требуется понять, какое задействованное оборудование, которое не может быть сразу понято (это наверняка не для меня).

3

То, что вы ищете, называется «универсальным программированием» в Haskell: https://wiki.haskell.org/Generics; ранняя форма называлась «Scrap Your Boilerplate», которую вы также можете захотеть в Google. Я не проверял, но я думаю, что если вы используете Data.Generics.Uniplate и Data.Generics.Uniplate.Data модули Uniplate «s можно определить imply_remove, как

imply_remove = transform w where 
    w (ImplySentence s1 s2) = OrSentence (NotSentence s1) s2 
    w s = s 

transform делает рекурсию для вас.