{-# LANGUAGE CPP #-} {-# LANGUAGE LambdaCase #-} {-| Module : ATP.FirstOrder.Simplification Description : Simplification of first-order expressions. Copyright : (c) Evgenii Kotelnikov, 2019-2021 License : GPL-3 Maintainer : evgeny.kotelnikov@gmail.com Stability : experimental -} module ATP.FirstOrder.Simplification ( -- * Simplification Simplify(..) ) where import ATP.FirstOrder.Core import ATP.FirstOrder.Smart -- $setup -- >>> :set -XOverloadedStrings -- >>> :load Property.Generators -- * Simplification -- | A class of first-order expressions that 'simplify' syntactically shrinks -- while preserving their evaluation. class Simplify a where simplify :: a -> a -- | Simplify the given formula by replacing each of its constructors with -- corresponding smart constructors. instance Simplify LogicalExpression where simplify :: LogicalExpression -> LogicalExpression simplify = \case Clause Clause c -> Clause -> LogicalExpression Clause (Clause -> Clause forall a. Simplify a => a -> a simplify Clause c) Formula Formula f -> Formula -> LogicalExpression Formula (Formula -> Formula forall a. Simplify a => a -> a simplify Formula f) -- | Simplify the given clause by replacing the 'Literals' constructor with -- the smart constructor 'clause'. The effects of simplification are -- the following. -- -- * @'simplify' c@ does not contain negative constant literals. -- * @'simplify' c@ does not contain falsum literals. -- * @'simplify' c@ does not contain redundant tautology literals. -- -- >>> simplify (UnitClause (Signed Negative (Propositional True))) -- Literals {getLiterals = []} -- -- >>> simplify (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])]) -- Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]} -- -- >>> simplify (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])]) -- Literals {getLiterals = [Signed {signof = Positive, unsign = Propositional True}]} -- instance Simplify Clause where simplify :: Clause -> Clause simplify = [Signed Literal] -> Clause forall (f :: * -> *). Foldable f => f (Signed Literal) -> Clause clause ([Signed Literal] -> Clause) -> (Clause -> [Signed Literal]) -> Clause -> Clause forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> [Signed Literal] getLiterals -- | Simplify the given clause set by replacing the 'Clauses' constructor with -- the smart constructor 'clauses'. The effects of simplification are -- the following. -- -- * @'simplify' c@ does not contain negative constant literals. -- * @'simplify' c@ does not contain falsum literals. -- * @'simplify' c@ does not contain tautology literals. -- * @'simplify' c@ does not contain redundant falsum literals. -- -- >>> simplify (SingleClause (UnitClause (Signed Negative (Propositional True)))) -- Clauses {getClauses = [Literals {getLiterals = []}]} -- -- >>> simplify (SingleClause (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])])) -- Clauses {getClauses = [Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}]} -- -- >>> simplify (SingleClause (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])])) -- Clauses {getClauses = []} -- instance Simplify Clauses where simplify :: Clauses -> Clauses simplify = [Clause] -> Clauses forall (f :: * -> *). Foldable f => f Clause -> Clauses clauses ([Clause] -> Clauses) -> (Clauses -> [Clause]) -> Clauses -> Clauses forall b c a. (b -> c) -> (a -> b) -> a -> c . Clauses -> [Clause] getClauses -- | Simplify the given formula by replacing each of its constructors with -- corresponding smart constructors. The effects of simplification are -- the following. -- -- * @'simplify' f@ does not contain nested negations. -- * @'simplify' f@ does not contain some of the constant atomic formulas from @f@. -- * All chained applications of any binary connective inside -- @'simplify' f@ are right-associative. -- -- Any formula built only using smart constructors is simplified by construction. -- -- >>> simplify (Connected Or tautology (Atomic (Predicate "p" []))) -- Atomic (Propositional True) -- -- >>> simplify (Negate (Negate (Atomic (Predicate "p" [])))) -- Atomic (Predicate "p" []) -- -- >>> simplify (Connected And (Connected And (Atomic (Predicate "p" [])) (Atomic (Predicate "q" []))) (Atomic (Predicate "r" []))) -- Connected And (Atomic (Predicate "p" [])) (Connected And (Atomic (Predicate "q" [])) (Atomic (Predicate "r" []))) -- instance Simplify Formula where simplify :: Formula -> Formula simplify = \case Atomic Literal l -> Literal -> Formula Atomic Literal l Negate Formula f -> Formula -> Formula neg (Formula -> Formula forall a. Simplify a => a -> a simplify Formula f) Connected Connective c Formula f Formula g -> Formula -> Formula forall a. Simplify a => a -> a simplify Formula f Formula -> Formula -> Formula # Formula -> Formula forall a. Simplify a => a -> a simplify Formula g where # :: Formula -> Formula -> Formula (#) = Connective -> Formula -> Formula -> Formula smartConnective Connective c Quantified Quantifier q Var v Formula f -> Quantifier -> (Var, Formula) -> Formula forall b. Binder b => Quantifier -> b -> Formula quantified Quantifier q (Var v, Formula -> Formula forall a. Simplify a => a -> a simplify Formula f) -- | Convert a binary connective to its corresponding smart constructor. smartConnective :: Connective -> Formula -> Formula -> Formula smartConnective :: Connective -> Formula -> Formula -> Formula smartConnective = \case Connective And -> Formula -> Formula -> Formula (/\) Connective Or -> Formula -> Formula -> Formula (\/) Connective Implies -> Formula -> Formula -> Formula (==>) Connective Equivalent -> Formula -> Formula -> Formula (<=>) Connective Xor -> Formula -> Formula -> Formula (<~>) -- | Simplify the given theorem by flattening the conjunction of its premises -- and its conjecture. instance Simplify Theorem where simplify :: Theorem -> Theorem simplify (Theorem [Formula] as Formula c) = [Formula] -> [Formula] forall (f :: * -> *). Foldable f => f Formula -> [Formula] flattenConjunction ((Formula -> Formula) -> [Formula] -> [Formula] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap Formula -> Formula forall a. Simplify a => a -> a simplify [Formula] as) [Formula] -> Formula -> Theorem forall (f :: * -> *). Foldable f => f Formula -> Formula -> Theorem |- Formula -> Formula forall a. Simplify a => a -> a simplify Formula c