Представление типов данных с переменными переменными - PullRequest
Новая
       16

Представление типов данных с переменными переменными

4 голосов
/ 03 октября 2011

Я пытаюсь представить формулы с переменными, например, между формулами или переменными и константами: 

R(a,b) -> Q   [Q takes formulae as substitutions]
R(x,b) v P(b) [x takes constants or variables as substitutions]

Функции над формулами имеют ограничения класса, указывающие, какой тип переменной рассматривается.Например, классы терминов, переменных и подстановок могут иметь следующую структуру: 

class Var b where ...
class (Var b) => Term b a | b -> a where ...
class (Term b a) => Subst s b a | b a -> s where ...

Существует много алгоритмов, имеющих дело с синтаксической манипуляцией терминами, для которых параметризация типов терминов в типах переменных была бы полезной.Например, рассмотрим универсальный алгоритм объединения по формулам некоторых типов терминов, имеющих разные типы переменных: 

unify :: (Subst s b a) => a -> a -> s b a
unify (P -> F(a,b)) ((Q v R) -> F(a,b)) = {P\(Q v R)}  -- formulae
unify (P(x,f(a,b))) (P(g(c),f(y,b)))    = {x\g(c),y\a} -- variables and constants

Каков способ представления таких переменных best ?Я экспериментировал с различными методами, но не остановился на удовлетворительном решении.

1 Ответ

4 голосов
/ 03 октября 2011

Может быть, ваш вопрос был бы более понятным, если бы вы сказали, что не так со следующим простым представлением терминов и формул? Есть миллион способов сделать это (возможности значительно расширены на {-LANGUAGE GADTs-}) 

  {-#LANGUAGE TypeOperators#-}

  data Term v c = Var v 
                | Const c deriving (Show, Eq, Ord)

  data Formula p v c = Atom p 
                     | Term v c := Term v c 
                     | Formula p v c :-> Formula p v c 
                     | Not (Formula p v c)
                     | Subst v (Term v c) (Formula p v c) 
                     | Inst p (Formula p v c) (Formula p v c) 
                     deriving (Show, Eq, Ord)


  update f v c v' = case v == v' of True -> c; False -> f v'

  one = Const (1:: Int)
  zero = Const (0 :: Int)
  x = Var 'x'
  y = Var 'y'
  p = Atom 'p'
  q = Atom 'q'
  absurd = one := zero
  brouwer p = (((p :-> absurd) :-> absurd) :-> absurd) :-> (p :-> absurd)

  ref ::  (v -> c) -> Term v c -> c
  ref i (Var v)  = i v
  ref i (Const c) = c

  eval :: (Eq c , Eq v , Eq p) => (v -> c) -> (p -> Bool) -> Formula p v c -> Bool
  eval i j (Atom p) = j p
  eval i j (p := q) = ref i p == ref i q
  eval i j (p :-> q) = not ( eval i j p) ||  eval i j q
  eval i j (Not p) = not (eval i j p)
  eval i j q@(Subst v t p) =  eval (update i v (ref i t)) j q
  eval i j q@(Inst p r s) = eval i (update j p (eval i j r)) s
...