Final.hs

{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ParallelListComp #-}
{-# LANGUAGE OverloadedLists #-}

module Data.Logic.Final where

import           Control.Applicative            ( Applicative(liftA2) )
import           Control.Monad                  ( replicateM )
import           Data.Biapplicative             ( (<<*>>)
                                                , bipure
                                                )
import qualified Data.Map                      as M
import qualified Data.Set                      as S

-----------------------------------------------------
-- A tagless final encoding of boolean expressions --
-----------------------------------------------------

class BoolSYM s where
  {-# MINIMAL top, neg, (conj|disj) #-}
  top :: s
  bot :: s
  bot = neg top
  neg :: s -> s
  conj :: s -> s -> s
  conj s t = neg (neg s `disj` neg t)
  disj :: s -> s -> s
  disj s t = neg (neg s `conj` neg t)

-- Duplicator boilerplate (will come in handy later).
instance (BoolSYM a,BoolSYM b) => BoolSYM (a,b) where
  top = (top, top)
  bot = (bot, bot)
  neg p = (neg, neg) <<*>> p
  conj p q = (conj, conj) <<*>> p <<*>> q
  disj p q = (disj, disj) <<*>> p <<*>> q

-- More duplicator boilerplate just in case.
instance (BoolSYM a,BoolSYM b,BoolSYM c) => BoolSYM (a,b,c) where
  top = (top, top, top)
  bot = (bot, bot, bot)
  neg (s, t, u) = (neg s, neg t, neg u)
  conj (s, t, u) (s', t', u') = (conj s s', conj t t', conj u u')
  disj (s, t, u) (s', t', u') = (disj s s', disj t t', disj u u')

-- Newtype wrappers to distinguish between ascii and unicode strings.
newtype A = A String
newtype U = U String

-- An evaluator for printing boolean formulas as ascii strings.
instance BoolSYM A where
  top = A "T"
  bot = A "F"
  neg (A s) = A $ "~" ++ s
  conj (A s) (A t) = A $ "(" ++ s ++ "&" ++ t ++ ")"
  disj (A s) (A t) = A $ "(" ++ s ++ "|" ++ t ++ ")"

viewA :: A -> String
viewA (A s) = s

-- An evaluator for printing boolean formulas as unicode strings.
instance BoolSYM U where
  top = U "⊤"
  bot = U "⊥"
  neg (U s) = U $ "¬" ++ s
  conj (U s) (U t) = U $ "(" ++ s ++ "∧" ++ t ++ ")"
  disj (U s) (U t) = U $ "(" ++ s ++ "∨" ++ t ++ ")"

viewU :: U -> String
viewU (U s) = s

-- An evaluator for computing the value of a boolean formula.
instance BoolSYM Bool where
  top  = True
  bot  = False
  neg  = not
  conj = (&&)
  disj = (||)

eval :: Bool -> Bool
eval = id


----------------------------------------------
-- Modular extension to propositional logic --
----------------------------------------------

-- Integers are used as variables.
type Var = Int

-- An assignment is a mapping from variables to boolean values.
type Assignment = M.Map Var Bool

-- 'at' maps variables to expressions of propositional logic, which compose via the boolean operators.
-- N.b., we don't need to define the boolean operators again for propositional logic - this is the beauty
-- of the tagless final approach.
class BoolSYM s => PropSYM s where
  at :: Var -> s

-- Some boilerplate duplicator instances.
instance (PropSYM a, PropSYM b) => PropSYM (a,b) where
  at n = (at n, at n)

-- More boilerplate, just in case.
instance (PropSYM a, PropSYM b,PropSYM c) => PropSYM (a,b,c) where
  at n = (at n, at n, at n)

-- Now we define an evaluator just for printing variables as ascii/unicode;
-- there's no need to redefine our evaluator for boolean formulas.

instance PropSYM A where
  at = A . show

instance PropSYM U where
  at = U . show

-- An evaluator for computing the set of variables in a formula.

instance BoolSYM (S.Set Var) where
  top  = S.empty
  neg  = id
  conj = S.union
  disj = S.union

instance PropSYM (S.Set Var) where
  at n = S.singleton n

variables :: S.Set Var -> [Var]
variables = S.toList

-- A function from a set of variables, to the set of possible assignments.
universe :: S.Set Var -> [Assignment]
universe vs =
  [ M.fromList [ (v, t) | v <- variables vs | t <- ts ]
  | ts <- replicateM (length vs) [True, False]
  ]

-- We want to use a function from 'g' to 'Maybe a', since 'Map' doesn't have an applicative instance.
type Proposition = Assignment -> Maybe Bool

-- Since the semantic value of a propositional formula is richer, we do need to say how
-- boolean formulas are evaluated.
-- This takes advantage of the fact that '(->) Assignment' and 'Maybe' are applicative functors,
-- and the composition of two applicatives is an applicative.
-- N.b. we could encode this intuition directly using 'Data.Functor'.

instance BoolSYM Proposition where
  top = (pure . pure) top
  neg p = (fmap . fmap) neg p
  conj p q = (liftA2 . liftA2) conj p q
  disj p q = (liftA2 . liftA2) disj p q

-- The need for 'Maybe' comes from the 'lookup' function, although
-- in practice we'll never get a 'Nothing' value.
instance PropSYM Proposition where
  at n g = M.lookup n g

evalProp :: Proposition -> Proposition
evalProp = id

-- Computes the set of verifying assignments for a formula.
verifiers :: (S.Set Var, Proposition) -> S.Set Assignment
verifiers (vs, p) = S.fromList [ g | g <- universe vs, p g == Just True ]

-- Computes the set of falsifying assignments for a formula.
falsifiers :: (S.Set Var, Proposition) -> S.Set Assignment
falsifiers (vs, p) = S.fromList [ g | g <- universe vs, p g == Just False ]

entails :: (S.Set Var, Proposition) -> (S.Set Var, Proposition) -> Bool
entails (vs, p) (us, q) =
  let vs' = vs `S.union` us
  in  verifiers (vs', p) `S.isSubsetOf` verifiers (vs', q)

equiv :: (S.Set Var, Proposition) -> (S.Set Var, Proposition) -> Bool
equiv (vs, p) (us, q) =
  let vs' = vs `S.union` us in verifiers (vs', p) == verifiers (vs', q)

data PropType = Tautology | Contradiction | Contingency deriving (Eq,Show)

propType :: (S.Set Var, Proposition) -> PropType
propType (vs, p) | universe vs == S.toList (verifiers (vs, p)) = Tautology
                 | universe vs == S.toList (falsifiers (vs, p)) = Contradiction
                 | otherwise = Contingency

isTautology :: (S.Set Var, Proposition) -> Bool
isTautology (vs, p) = propType (vs, p) == Tautology

isContradiction :: (S.Set Var, Proposition) -> Bool
isContradiction (vs, p) = propType (vs, p) == Contradiction

isContingency :: (S.Set Var, Proposition) -> Bool
isContingency (vs, p) = propType (vs, p) == Contingency

--------------------------------------------
-- indeterminacy and formal alternatives --
--------------------------------------------

newtype AltScalar s = AltScalar [s] deriving (Functor,Applicative,Semigroup,Monoid)

newtype AltS s = AltS [s] deriving (Functor,Applicative,Semigroup,Monoid)

instance BoolSYM s => BoolSYM (AltS s) where
  top = pure top
  bot = pure bot
  neg p = neg <$> p
  conj p q = (AltS [conj,disj] <*> p <*> q) <> p <> q
  disj p q = (AltS [conj,disj] <*> p <*> q)  <> p <> q

instance BoolSYM s => BoolSYM (AltScalar s) where
  top = pure top
  bot = pure bot
  neg p = neg <$> p
  conj p q = AltScalar [conj,disj] <*> p <*> q
  disj p q = AltScalar [conj,disj] <*> p <*> q

instance PropSYM s => PropSYM (AltScalar s) where
  at n = pure $ at n

instance PropSYM s => PropSYM (AltS s) where
  at n = pure $ at n

scalarAlts :: AltScalar s -> [s]
scalarAlts (AltScalar ss) = ss

alts :: AltS s -> [s]
alts (AltS ss) = ss

viewScalarAlts :: AltScalar A -> [String]
viewScalarAlts (AltScalar as) = viewA <$> as

viewAlts :: AltS A -> [String]
viewAlts (AltS as) = viewA <$> as

tf1 :: PropSYM s => s
tf1 = at 1 `disj` at 2

tf2 :: PropSYM s => s
tf2 = tf1 `disj` at 3

From boolean to propositional formulas in the tagless final style (http://okmij.org/ftp/tagless-final/).