Проверьте формула верна в Haskell

Question

---- обновление 2 ----

В конце концов, он сказал мне, что это Exists ...

спасибо всем.

---- обновление ----

Хорошо, мы называем это Forsome

ex3: forsome x0::[False,True]. forsome x1::[0,1,2]. (x0 || (0 < x1))

(которого сказал мне "что FORALL" добавлено):

the constructor says "forall x in blah" but it really means "for some x in blah". 

the formula is satisfied for some assignment of variables so it is satisfiable. 

Как я могу это сделать? Благодаря

---- оригинал ----

Предположим, мы имеем формулу EX3

ex3: forall x0::[False,True]. forall x1::[0,1,2]. (x0 || (0 < x1)).

Сначала я думаю, что это EX3 False, потому что когда x0 = False и x1 = 0 формула (False || (0 < 0)) так EX3 абсолютно неверно. Но я бы сказал, что EX3 является True,

"satisfiable ex3 is true because there is at least one combination from sets x0 and x1 which returns true. So as long as there is 1 valid solution in Forall, it is true."

Предположим, что правильно ...

Я думаю, что нужно проверять группы комбинации с таким же уровнем, но я не понять, как это сделать. Определить «Есть ли они в той же группе», кажется, сложно.

Вот мои коды:

Файл: Formula.hs

{-# LANGUAGE GADTs #-} 

module Formula where 

-- Datatype of formulas 
-- -------------------- 

data Formula ts where 
    Body :: Term Bool      -> Formula() 
    Forall :: Show a 
     => [a] -> (Term a -> Formula as) -> Formula (a, as) 

data Term t where 
    Con  :: t   -> Term t 
    And  :: Term Bool -> Term Bool -> Term Bool 
    Or  :: Term Bool -> Term Bool -> Term Bool 
    Smaller :: Term Int -> Term Int -> Term Bool 
    Plus :: Term Int -> Term Int -> Term Int 
    Name :: String -> Term t -- to facilitate pretty printing 

-- Pretty printing formulas 
-- ------------------------ 

instance Show t => Show (Term t) where 
    show (Con v)  = show v 
    show (And p q)  = "(" ++ show p ++ " && " ++ show q ++ ")" 
    show (Or p q)  = "(" ++ show p ++ " || " ++ show q ++ ")" 
    show (Smaller n m) = "(" ++ show n ++ " < " ++ show m ++ ")" 
    show (Plus n m) = "(" ++ show n ++ " + " ++ show m ++ ")" 
    show (Name name) = name 

instance Show (Formula ts) where 
    show = show' ['x' : show i | i <- [0..]] 
    where 
     show' :: [String] -> Formula ts' -> String 
     show' ns  (Body body) = show body 
     show' (n:ns) (Forall vs p) = "forall " ++ n ++ "::" ++ show vs ++ ". " ++ show' ns (p (Name n)) 


-- Example formulas 
-- ---------------- 

ex1 :: Formula() 
ex1 = Body (Con True) 

ex2 :: Formula (Int,()) 
ex2 = Forall [1..10] $ \n -> 
     Body $ n `Smaller` (n `Plus` Con 1) 

ex3 :: Formula (Bool, (Int,())) 
ex3 = Forall [False, True] $ \p -> 
     Forall [0..2] $ \n -> 
     Body $ p `Or` (Con 0 `Smaller` n) 

wrongFormula :: Formula (Int,()) 
wrongFormula = Forall [0..4] $ \n -> 
       Body $ n `Smaller` (Con 0) 

Файл: Solver.hs

{-# LANGUAGE GADTs #-} 

module Solver where 

import Formula 


-- Evaluating terms 
-- ---------------- 

eval :: Term t -> t 
eval (Con  v) = v 
eval (And  p q) = eval p && eval q 
eval (Or  p q) = eval p || eval q 
eval (Smaller n m) = eval n < eval m 
eval (Plus n m) = eval n + eval m 
eval (Name _) = error "eval: Name" 


-- Checking formulas 
-- ----------------- 

satisfiable :: Formula ts -> Bool 
satisfiable (Body body) = eval body 
-- FIXME wrong implement 
--satisfiable (Forall xs f) = helper f xs 
-- where helper :: (Term a -> Formula t) -> [a] -> Bool 
--  helper fn (a:as) = (satisfiable $ (fn . Con) a) && (helper fn as) 
--  helper _ []  = True 

Любое предложение будет оценено.

Answer 1

Я согласен с Даниилом, что это описывает Exists, не Forall, но если вы хотите, чтобы интерпретировать это таким образом, вы просто должны изменить && к || и True к False.

Или, еще лучше, используя функции Prelude

all :: (a -> Bool) -> [a] -> Bool -- is predicate true for all elements? 
any :: (a -> Bool) -> [a] -> Bool -- is predicate true for any element? 

Вы можете написать существующую реализацию, как

satisfiable (Forall xs f) = all (satisfiable . f . Con) xs 

так, чтобы изменить его, вы просто изменить all к any.