Delete Ternary directory
This commit is contained in:
parent
fb6dd81f33
commit
3c9c68e54e
6 changed files with 0 additions and 154 deletions
Binary file not shown.
|
|
@ -1,30 +0,0 @@
|
||||||
module Ternary.Statement (Statement(..), st) where
|
|
||||||
import Ternary.Term (Vee, Term(..), Item(..))
|
|
||||||
data Statement a = A a a -- Affirmo (general affirmative)
|
|
||||||
| I a a -- affIrmo (private affirmative)
|
|
||||||
| E a a -- nEgo (general negative)
|
|
||||||
| O a a -- negO (private negative)
|
|
||||||
| A' a a
|
|
||||||
| I' a a
|
|
||||||
| E' a a
|
|
||||||
| O' a a
|
|
||||||
deriving (Eq, Show, Read)
|
|
||||||
|
|
||||||
inv :: (Eq a) => Term a -> Term a
|
|
||||||
inv (Term p x) = Term (not p) x
|
|
||||||
|
|
||||||
i :: (Eq a) => Bool -> Term a -> Term a -> Vee a
|
|
||||||
i v x y
|
|
||||||
| x == inv y = error "x and not x under the same Vee, refusing to calculate"
|
|
||||||
| x /= y = Term v . Item $ [x, y]
|
|
||||||
| x == y = Term v . Item $ [x]
|
|
||||||
|
|
||||||
st :: (Eq a) => Statement a -> Vee a
|
|
||||||
st (A x y) = i False (Term True x) (Term False y)
|
|
||||||
st (I x y) = i True (Term True x) (Term True y)
|
|
||||||
st (E x y) = i False (Term True x) (Term True y)
|
|
||||||
st (O x y) = i True (Term True x) (Term False y)
|
|
||||||
st (A' x y) = i False (Term False x) (Term False y)
|
|
||||||
st (I' x y) = i True (Term False x) (Term True y)
|
|
||||||
st (E' x y) = i False (Term False x) (Term True y)
|
|
||||||
st (O' x y) = i True (Term False x) (Term False y)
|
|
||||||
|
|
@ -1,34 +0,0 @@
|
||||||
module Ternary.Term (Term(..), Item(..), Vee) where
|
|
||||||
import Data.List (concatMap, null, (++), (\\))
|
|
||||||
import Prelude (Applicative, Bool (False, True), Eq, Functor,
|
|
||||||
Read, Show, String, fmap, map, pure, show,
|
|
||||||
(&&), (/=), (<*>), (==), (||))
|
|
||||||
|
|
||||||
data Term a = Term Bool a deriving (Read)
|
|
||||||
newtype Item a = Item [a] deriving (Read)
|
|
||||||
type Vee a = Term (Item (Term a))
|
|
||||||
|
|
||||||
instance Functor Item where
|
|
||||||
fmap f (Item a) = Item (map f a)
|
|
||||||
|
|
||||||
instance Applicative Item where
|
|
||||||
pure x = Item [x]
|
|
||||||
(Item fs) <*> (Item xs) = Item [f x | f <- fs, x <- xs]
|
|
||||||
|
|
||||||
instance (Eq a) => Eq (Item a) where
|
|
||||||
(Item x) == (Item y) = null dxy && null dyx
|
|
||||||
where
|
|
||||||
dxy = x \\ y
|
|
||||||
dyx = y \\ x
|
|
||||||
|
|
||||||
instance (Eq a) => Eq (Term a) where
|
|
||||||
Term v x == Term w y = (v==w) && (x==y)
|
|
||||||
Term v x /= Term w y = (v/=w) || (x/=y)
|
|
||||||
|
|
||||||
instance Show (Term String) where
|
|
||||||
show (Term False y) = y ++ "`"
|
|
||||||
show (Term True y) = y
|
|
||||||
|
|
||||||
instance Show (Term (Item (Term String))) where
|
|
||||||
show (Term x i) = show (Term x "V") ++ concatMap show (it i)
|
|
||||||
where it (Item ii) = ii
|
|
||||||
Binary file not shown.
|
|
@ -1,22 +0,0 @@
|
||||||
module Ternary.Universum (Universum(..), universum, aFromStatements) where
|
|
||||||
import Data.List (nub)
|
|
||||||
import Ternary.Term (Item (..), Term (..), Vee)
|
|
||||||
|
|
||||||
data Universum = Aristotle
|
|
||||||
| Empty
|
|
||||||
| Default
|
|
||||||
|
|
||||||
universum :: (Eq a) => Universum -> [Vee a] -> [Vee a]
|
|
||||||
universum Aristotle facts =
|
|
||||||
[Term True (Item [Term x v])
|
|
||||||
| v <- aFromStatements facts,
|
|
||||||
x <- [False, True]]
|
|
||||||
universum Empty _ = []
|
|
||||||
universum Default xs = xs
|
|
||||||
|
|
||||||
aFromStatements :: (Eq a) => [Vee a] -> [a]
|
|
||||||
aFromStatements = nub . concatMap (extract . getItem . getVee)
|
|
||||||
where
|
|
||||||
getItem (Item x) = x
|
|
||||||
getVee (Term _ i) = i
|
|
||||||
extract terms = [v | (Term _ v) <- terms]
|
|
||||||
|
|
@ -1,68 +0,0 @@
|
||||||
module Ternary.Vee (isObvious, newFact, cleared, think) where
|
|
||||||
import Data.List (head, intersect, length, nub, null, union, (\\))
|
|
||||||
import Data.Maybe (Maybe (Nothing), mapMaybe)
|
|
||||||
import Prelude (Bool (False, True), Eq, any, foldr, fst, map,
|
|
||||||
not, notElem, otherwise, return, snd, ($), (&&),
|
|
||||||
(.), (/=), (<$>), (<*>), (=<<), (==))
|
|
||||||
import Ternary.Term (Item (..), Term (..), Vee)
|
|
||||||
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
|
|
||||||
a `isSubsetOf` b = nda && not ndb
|
|
||||||
where
|
|
||||||
nda = null $ a \\ b
|
|
||||||
ndb = null $ b \\ a
|
|
||||||
|
|
||||||
isObvious :: (Eq a) => Vee a -> Vee a -> Bool
|
|
||||||
isObvious (Term x (Item a)) (Term y (Item b))
|
|
||||||
| x /= y = False
|
|
||||||
| x = a `isSubsetOf` b
|
|
||||||
| not x = b `isSubsetOf` a
|
|
||||||
|
|
||||||
newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
|
|
||||||
newFact a@(Term True _) b@(Term False _) = newFact b a
|
|
||||||
newFact (Term False (Item iF)) tT@(Term True (Item iT))
|
|
||||||
| length ldF /= 1 = ([], Nothing)
|
|
||||||
| otherwise =
|
|
||||||
if d'F `notElem` iT
|
|
||||||
then (return tT, return (Term True (Item (d'F:iT))))
|
|
||||||
else ([], Nothing)
|
|
||||||
where
|
|
||||||
ldF = iF \\ iT
|
|
||||||
d'F = notT . head $ ldF
|
|
||||||
notT (Term x v) = Term (not x) v
|
|
||||||
newFact (Term False (Item i0)) (Term False (Item i1))
|
|
||||||
| length e /= 1 = ([], Nothing)
|
|
||||||
| otherwise =
|
|
||||||
if null d0 && null d1
|
|
||||||
then (map (Term False . Item) [i0, i1], vee0)
|
|
||||||
else ([], vee0)
|
|
||||||
where
|
|
||||||
notT (Term x v) = Term (not x) v
|
|
||||||
terms = (i0 `intersect` i1) `union` d0 `union` d1
|
|
||||||
e = map notT i0 `intersect` i1
|
|
||||||
d0 = (i0 \\ i1) \\ map notT e
|
|
||||||
d1 = (i1 \\ i0) \\ e
|
|
||||||
vee0 = return (Term False (Item terms))
|
|
||||||
newFact _ _ = ([], Nothing)
|
|
||||||
|
|
||||||
pseudofix :: (Eq a) => (a -> a) -> a -> a
|
|
||||||
pseudofix f x0
|
|
||||||
| y == y' = y
|
|
||||||
| otherwise = y'
|
|
||||||
where
|
|
||||||
y = f x0
|
|
||||||
y' = f y
|
|
||||||
|
|
||||||
next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a])
|
|
||||||
next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r)
|
|
||||||
where
|
|
||||||
r = newFact <$> o <*> n
|
|
||||||
|
|
||||||
applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
|
|
||||||
applyFacts old new = fst $ pseudofix next (old, new)
|
|
||||||
|
|
||||||
cleared :: (Eq a) => [Vee a] -> [Vee a]
|
|
||||||
cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees]
|
|
||||||
|
|
||||||
think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a]
|
|
||||||
think addition = foldr (applyFacts . withUni . return) [] where
|
|
||||||
withUni vees = applyFacts (addition vees) vees
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue