diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,15 @@ +# 2 (2019-04-17) + +- Reduce to three classes (from six): `Lattice`, `BoundedMeetSemiLattice` + `BoundeJoinSemiLattice`. + The latter two names are kept to help migration. +- Remove `Algebra.Enumerable` module. Use `universe` package. +- Drop GHC-7.4.3 support (broken `ConstraintKinds`) +- Move `Algebra.Lattice.Free` to `Algebra.Lattice.Free.Final` +- Add concrete syntax `Algebra.Lattice.Free` and `Algebra.Heyting.Free` using + LJT-proof search for `Eq` and `PartialOrd` +- Change `PartialOrd [a]` to be `leq = isSubsequenceOf` + # 1.7.1.1 (2019-07-05) - Allow newer dependencies, update cabal file diff --git a/README.md b/README.md deleted file mode 100644 --- a/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# lattices - -[![Build Status](https://travis-ci.org/phadej/lattices.svg?branch=master)](https://travis-ci.org/phadej/lattices) -[![Hackage](https://img.shields.io/hackage/v/lattices.svg)](http://hackage.haskell.org/package/lattices) -[![Stackage LTS 2](http://stackage.org/package/lattices/badge/lts-2)](http://stackage.org/lts-2/package/lattices) -[![Stackage LTS 3](http://stackage.org/package/lattices/badge/lts-3)](http://stackage.org/lts-3/package/lattices) -[![Stackage Nightly](http://stackage.org/package/lattices/badge/nightly)](http://stackage.org/nightly/package/lattices) - -Fine-grained library for constructing and manipulating lattices diff --git a/lattices.cabal b/lattices.cabal --- a/lattices.cabal +++ b/lattices.cabal @@ -1,18 +1,32 @@ +cabal-version: 1.18 name: lattices -version: 1.7.1.1 -cabal-version: >= 1.10 +version: 2 category: Math license: BSD3 -license-File: LICENSE -author: Maximilian Bolingbroke +license-file: LICENSE +author: + Maximilian Bolingbroke , Oleg Grenrus + maintainer: Oleg Grenrus homepage: http://github.com/phadej/lattices/ bug-reports: http://github.com/phadej/lattices/issues -copyright: (C) 2010-2015 Maximilian Bolingbroke +copyright: + (C) 2010-2015 Maximilian Bolingbroke, 2016-2019 Oleg Grenrus + build-type: Simple -extra-source-files: README.md CHANGELOG.md -tested-with: GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.3, GHC==8.0.2, GHC==8.2.2, GHC==8.4.3 -synopsis: Fine-grained library for constructing and manipulating lattices +extra-source-files: CHANGELOG.md +extra-doc-files: + m2.png + m3.png + n5.png + wide.png + +tested-with: + GHC ==7.6.3 || ==7.8.4 || ==7.10.3 || ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1 + +synopsis: + Fine-grained library for constructing and manipulating lattices + description: In mathematics, a lattice is a partially ordered set in which every two elements @x@ and @y@ have a unique supremum (also called a least upper bound, join, or @x /\\ y@) @@ -22,64 +36,83 @@ as a class for the partial order. source-repository head - type: git + type: git location: git://github.com/phadej/lattices.git library - exposed-modules: Algebra.Enumerable, - Algebra.Lattice, - Algebra.Lattice.Divisibility, - Algebra.Lattice.Dropped, - Algebra.Lattice.Free, - Algebra.Lattice.Levitated, - Algebra.Lattice.Lexicographic, - Algebra.Lattice.Lifted, - Algebra.Lattice.Op, - Algebra.Lattice.Ordered, - Algebra.PartialOrd, - Algebra.PartialOrd.Instances - - build-depends: base >= 4.5 && < 4.12, - base-compat >= 0.9.3 && < 0.11, - containers >= 0.4.2.1 && < 0.6, - deepseq >= 1.3.0.0 && < 1.5, - hashable >= 1.2.6.1 && < 1.3, - tagged >= 0.8.5 && < 0.9, - unordered-containers >= 0.2.6.0 && < 0.3, - semigroupoids >= 5.2.2 && < 5.4, - universe-base >= 1.0 && < 1.1, - universe-reverse-instances >= 1.0 && < 1.1 + default-language: Haskell2010 hs-source-dirs: src ghc-options: -Wall - default-language: Haskell2010 + exposed-modules: + Algebra.Lattice + Algebra.Lattice.Divisibility + Algebra.Lattice.Dropped + Algebra.Lattice.Free + Algebra.Lattice.Free.Final + Algebra.Lattice.Levitated + Algebra.Lattice.Lexicographic + Algebra.Lattice.Lifted + Algebra.Lattice.M2 + Algebra.Lattice.M3 + Algebra.Lattice.N5 + Algebra.Lattice.Op + Algebra.Lattice.Ordered + Algebra.Lattice.Unicode + Algebra.Lattice.Wide + Algebra.Lattice.ZeroHalfOne - if !impl(ghc >= 8.0) - build-depends: semigroups >= 0.18.3 && < 0.19 + exposed-modules: + Algebra.Heyting + Algebra.Heyting.Free + Algebra.Heyting.Free.Expr - if !impl(ghc >= 7.10) - build-depends: void >= 0.7 && < 0.8, - transformers >= 0.3 && < 0.6 + exposed-modules: + Algebra.PartialOrd + Algebra.PartialOrd.Instances - if impl(ghc >= 7.4 && < 7.5) - build-depends: ghc-prim + build-depends: + base >=4.6 && <4.13 + , base-compat >=0.10.5 && <0.11 + , containers >=0.5.0.0 && <0.7 + , deepseq >=1.3.0.0 && <1.5 + , hashable >=1.2.7.0 && <1.3 + , integer-logarithms >=1.0.3 && <1.1 + , QuickCheck >=2.12.6.1 && <2.14 + , semigroupoids >=5.3.2 && <5.4 + , tagged >=0.8.6 && <0.9 + , transformers >=0.3.0.0 && <0.6 + , universe-base >=1.1 && <1.2 + , universe-reverse-instances >=1.1 && <1.2 + , unordered-containers >=0.2.8.0 && <0.3 + if !impl(ghc >=8.0) + build-depends: semigroups >=0.18.5 && <0.19 + + if !impl(ghc >=7.10) + build-depends: void >=0.7.2 && <0.8 + + if impl(ghc >=7.4 && <7.5) + build-depends: ghc-prim + test-suite test - type: exitcode-stdio-1.0 - main-is: Tests.hs - hs-source-dirs: test - ghc-options: -Wall - default-language: Haskell2010 - build-depends: base, - base-compat, - tasty >= 0.10 && < 1.2, - tasty-quickcheck >= 0.8 && < 0.11, - QuickCheck >= 2.10 && <2.12, - quickcheck-instances >=0.3.16 && <0.4, - universe-instances-base >= 1.0 && <1.1, - lattices, - containers, - transformers, - unordered-containers + type: exitcode-stdio-1.0 + main-is: Tests.hs + hs-source-dirs: test + ghc-options: -Wall + default-language: Haskell2010 + build-depends: + base + , base-compat + , containers + , lattices + , QuickCheck + , quickcheck-instances >=0.3.19 && <0.4 + , tasty >=1.2.1 && <1.3 + , tasty-quickcheck >=0.10 && <0.11 + , transformers + , universe-base + , universe-reverse-instances + , unordered-containers - if !impl(ghc >= 8.0) - build-depends: semigroups >= 0.18.3 && < 0.19 + if !impl(ghc >=8.0) + build-depends: semigroups >=0.18.3 && <0.19 diff --git a/m2.png b/m2.png new file mode 100644 Binary files /dev/null and b/m2.png differ diff --git a/m3.png b/m3.png new file mode 100644 Binary files /dev/null and b/m3.png differ diff --git a/n5.png b/n5.png new file mode 100644 Binary files /dev/null and b/n5.png differ diff --git a/src/Algebra/Enumerable.hs b/src/Algebra/Enumerable.hs deleted file mode 100644 --- a/src/Algebra/Enumerable.hs +++ /dev/null @@ -1,50 +0,0 @@ -{-# LANGUAGE Safe #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Enumerable --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Enumerable {-# DEPRECATED "Use Data.Universe.Class" #-} ( - Enumerable(..), universeBounded, - Enumerated(..) - ) where - --- | Finitely enumerable things -class Enumerable a where - universe :: [a] - -universeBounded :: (Enum a, Bounded a) => [a] -universeBounded = enumFromTo minBound maxBound - - --- | Wrapper used to mark where we expect to use the fact that something is Enumerable -newtype Enumerated a = Enumerated { unEnumerated :: a } - deriving (Eq, Ord) - -instance Enumerable a => Enumerable (Enumerated a) where - universe = map Enumerated universe - - --- TODO: add to this rather sorry little set of instances. Can we exploit commonality with lazy-smallcheck? - -instance Enumerable Bool where - universe = universeBounded - -instance Enumerable Int where - universe = universeBounded - -instance Enumerable a => Enumerable (Maybe a) where - universe = Nothing : map Just universe - -instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where - universe = map Left universe ++ map Right universe - -instance Enumerable () where - universe = [()] - -instance (Enumerable a, Enumerable b) => Enumerable (a, b) where - universe = [(a, b) | a <- universe, b <- universe] diff --git a/src/Algebra/Heyting.hs b/src/Algebra/Heyting.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Heyting.hs @@ -0,0 +1,151 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Heyting +-- Copyright : (C) 2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Heyting where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Control.Applicative (Const (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Hashable (Hashable (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (All (..), Any (..), Endo (..)) +import Data.Tagged (Tagged (..)) +import Data.Universe.Class (Finite (..)) + +import qualified Data.HashSet as HS +import qualified Data.Set as S + +-- | A Heyting algebra is a bounded lattice equipped with a +-- binary operation \(a \to b\) of implication. +-- +-- /Laws/ +-- +-- @ +-- x '==>' x ≡ 'top' +-- x '/\' (x '==>' y) ≡ x '/\' y +-- y '/\' (x '==>' y) ≡ y +-- x '==>' (y '/\' z) ≡ (x '==>' y) '/\' (x '==>' z) +-- @ +-- +class BoundedLattice a => Heyting a where + -- | Implication. + (==>) :: a -> a -> a + + -- | Negation. + -- + -- @ + -- 'neg' x = x '==>' 'bottom' + -- @ + neg :: a -> a + neg x = x ==> bottom + + -- | Equivalence. + -- + -- @ + -- x '<=>' y = (x '==>' y) '/\' (y '==>' x) + -- @ + (<=>) :: a -> a -> a + x <=> y = (x ==> y) /\ (y ==> x) + +infixr 5 ==>, <=> + +------------------------------------------------------------------------------- +-- base +------------------------------------------------------------------------------- + +instance Heyting () where + _ ==> _ = () + neg _ = () + _ <=> _ = () + +instance Heyting Bool where + False ==> _ = True + True ==> y = y + + neg = not + (<=>) = (==) + +instance Heyting a => Heyting (b -> a) where + f ==> g = \x -> f x ==> g x + f <=> g = \x -> f x <=> g x + neg f = neg . f + +------------------------------------------------------------------------------- +-- All, Any, Endo +------------------------------------------------------------------------------- + +instance Heyting All where + All a ==> All b = All (a ==> b) + neg (All a) = All (neg a) + All a <=> All b = All (a <=> b) + +instance Heyting Any where + Any a ==> Any b = Any (a ==> b) + neg (Any a) = Any (neg a) + Any a <=> Any b = Any (a <=> b) + +instance Heyting a => Heyting (Endo a) where + Endo a ==> Endo b = Endo (a ==> b) + neg (Endo a) = Endo (neg a) + Endo a <=> Endo b = Endo (a <=> b) + +------------------------------------------------------------------------------- +-- Proxy, Tagged, Const, Identity +------------------------------------------------------------------------------- + +instance Heyting (Proxy a) where + _ ==> _ = Proxy + neg _ = Proxy + _ <=> _ = Proxy + +instance Heyting a => Heyting (Identity a) where + Identity a ==> Identity b = Identity (a ==> b) + neg (Identity a) = Identity (neg a) + Identity a <=> Identity b = Identity (a <=> b) + +instance Heyting a => Heyting (Tagged b a) where + Tagged a ==> Tagged b = Tagged (a ==> b) + neg (Tagged a) = Tagged (neg a) + Tagged a <=> Tagged b = Tagged (a <=> b) + +instance Heyting a => Heyting (Const a b) where + Const a ==> Const b = Const (a ==> b) + neg (Const a) = Const (neg a) + Const a <=> Const b = Const (a <=> b) + +------------------------------------------------------------------------------- +-- Sets +------------------------------------------------------------------------------- + +instance (Ord a, Finite a) => Heyting (S.Set a) where + x ==> y = S.union (neg x) y + + neg xs = S.fromList [ x | x <- universeF, S.notMember x xs] + + x <=> y = S.fromList + [ z + | z <- universeF + , S.member z x <=> S.member z y + ] + +instance (Eq a, Hashable a, Finite a) => Heyting (HS.HashSet a) where + x ==> y = HS.union (neg x) y + + neg xs = HS.fromList [ x | x <- universeF, not $ HS.member x xs] + + x <=> y = HS.fromList + [ z + | z <- universeF + , HS.member z x <=> HS.member z y + ] diff --git a/src/Algebra/Heyting/Free.hs b/src/Algebra/Heyting/Free.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Heyting/Free.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Algebra.Heyting.Free ( + Free (..), + liftFree, + lowerFree, + retractFree, + substFree, + toExpr, + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Heyting +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.Applicative (liftA2) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import GHC.Generics (Generic, Generic1) +import Math.NumberTheory.Logarithms (intLog2) + +import qualified Algebra.Heyting.Free.Expr as E +import qualified Test.QuickCheck as QC + +------------------------------------------------------------------------------- +-- Free +------------------------------------------------------------------------------- + +-- | Free Heyting algebra. +-- +-- Note: `Eq` and `PartialOrd` instances aren't structural. +-- +-- >>> Top == (Var 'x' ==> Var 'x') +-- True +-- +-- >>> Var 'x' == Var 'y' +-- False +-- +-- You can test for taulogogies: +-- +-- >>> leq Top $ (Var 'A' /\ Var 'B' ==> Var 'C') <=> (Var 'A' ==> Var 'B' ==> Var 'C') +-- True +-- +-- >>> leq Top $ (Var 'A' /\ neg (Var 'A')) <=> Bottom +-- True +-- +-- >>> leq Top $ (Var 'A' \/ neg (Var 'A')) <=> Top +-- False +-- +data Free a + = Var a + | Bottom + | Top + | Free a :/\: Free a + | Free a :\/: Free a + | Free a :=>: Free a + deriving (Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable) + +infixr 6 :/\: +infixr 5 :\/: +infixr 4 :=>: + +liftFree :: a -> Free a +liftFree = Var + +substFree :: Free a -> (a -> Free b) -> Free b +substFree z k = go z where + go (Var x) = k x + go Bottom = Bottom + go Top = Top + go (x :/\: y) = go x /\ go y + go (x :\/: y) = go x \/ go y + go (x :=>: y) = go x ==> go y + +retractFree :: Heyting a => Free a -> a +retractFree = lowerFree id + +lowerFree :: Heyting b => (a -> b) -> Free a -> b +lowerFree f = go where + go (Var x) = f x + go Bottom = bottom + go Top = top + go (x :/\: y) = go x /\ go y + go (x :\/: y) = go x \/ go y + go (x :=>: y) = go x ==> go y + +toExpr :: Free a -> E.Expr a +toExpr (Var a) = E.Var a +toExpr Bottom = E.Bottom +toExpr Top = E.Top +toExpr (x :/\: y) = toExpr x E.:/\: toExpr y +toExpr (x :\/: y) = toExpr x E.:\/: toExpr y +toExpr (x :=>: y) = toExpr x E.:=>: toExpr y + +------------------------------------------------------------------------------- +-- Monad +------------------------------------------------------------------------------- + +instance Applicative Free where + pure = liftFree + (<*>) = ap + +instance Monad Free where + return = pure + (>>=) = substFree + +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +-- instances do small local optimisations. + +instance Lattice (Free a) where + Top /\ y = y + Bottom /\ _ = Bottom + x /\ Top = x + _ /\ Bottom = Bottom + x /\ y = x :/\: y + + Top \/ _ = Top + Bottom \/ y = y + _ \/ Top = Top + x \/ Bottom = x + x \/ y = x :\/: y + +instance BoundedJoinSemiLattice (Free a) where + bottom = Bottom + +instance BoundedMeetSemiLattice (Free a) where + top = Top + +instance Heyting (Free a) where + Bottom ==> _ = Top + Top ==> y = y + _ ==> Top = Top + x ==> y = x :=>: y + +instance Ord a => Eq (Free a) where + x == y = E.proofSearch (toExpr (x <=> y)) + +instance Ord a => PartialOrd (Free a) where + leq x y = E.proofSearch (toExpr (x ==> y)) + +------------------------------------------------------------------------------- +-- Other instances +------------------------------------------------------------------------------- + +instance QC.Arbitrary a => QC.Arbitrary (Free a) where + arbitrary = QC.sized arb where + arb n | n <= 0 = prim + | otherwise = QC.oneof (prim : compound) + where + arb' = arb (sc n) + arb'' = arb (sc (sc n)) -- make domains be smaller. + + sc = intLog2 . max 1 + + compound = + [ liftA2 (:/\:) arb' arb' + , liftA2 (:\/:) arb' arb' + , liftA2 (:=>:) arb'' arb' + ] + + prim = QC.frequency + [ (20, Var <$> QC.arbitrary) + , (1, pure Bottom) + , (2, pure Top) + ] + + shrink (Var c) = Top : map Var (QC.shrink c) + shrink Bottom = [] + shrink Top = [Bottom] + shrink (x :/\: y) = x : y : map (uncurry (:/\:)) (QC.shrink (x, y)) + shrink (x :\/: y) = x : y : map (uncurry (:\/:)) (QC.shrink (x, y)) + shrink (x :=>: y) = x : y : map (uncurry (:=>:)) (QC.shrink (x, y)) diff --git a/src/Algebra/Heyting/Free/Expr.hs b/src/Algebra/Heyting/Free/Expr.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Heyting/Free/Expr.hs @@ -0,0 +1,280 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Algebra.Heyting.Free.Expr ( + Expr (..), + proofSearch, + ) where + +import Prelude () +import Prelude.Compat + +import Control.Monad (ap) +import Control.Monad.Trans.State (State, evalState, get, put) +import Data.Data (Data, Typeable) +import Data.Set (Set) +import GHC.Generics (Generic, Generic1) + +import qualified Data.Set as Set + +------------------------------------------------------------------------------- +-- Expr +------------------------------------------------------------------------------- + +-- | Heyting algebra expression. +-- +-- /Note:/ this type doesn't have 'Algebra.Heyting.Heyting' instance, +-- as its 'Eq' and 'Ord' are structural. +-- +data Expr a + = Var a + | Bottom + | Top + | Expr a :/\: Expr a + | Expr a :\/: Expr a + | Expr a :=>: Expr a + deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable) + +infixr 6 :/\: +infixr 5 :\/: +infixr 4 :=>: + +instance Applicative Expr where + pure = Var + (<*>) = ap + +instance Monad Expr where + return = pure + + Var x >>= k = k x + Bottom >>= _ = Bottom + Top >>= _ = Top + (x :/\: y) >>= k = (x >>= k) :/\: (y >>= k) + (x :\/: y) >>= k = (x >>= k) :\/: (y >>= k) + (x :=>: y) >>= k = (x >>= k) :=>: (y >>= k) + +------------------------------------------------------------------------------- +-- LJT proof search +------------------------------------------------------------------------------- + +-- | Decide whether @x :: 'Expr' a@ is provable. +-- +-- /Note:/ this doesn't construct a proof term, but merely returns a 'Bool'. +-- +proofSearch :: forall a. Ord a => Expr a -> Bool +proofSearch tyGoal = evalState (emptyCtx |- fmap R tyGoal) 0 + where + freshVar = do + n <- get + put (n + 1) + return (L n) + + infix 4 |- + infixr 3 .&& + + (.&&) :: Monad m => m Bool -> m Bool -> m Bool + x .&& y = do + x' <- x + if x' + then y + else return False + + (|-) :: Ctx a -> Expr (Am a) -> State Int Bool + + -- Ctx ats ai ii xs |- _ + -- | traceShow (length ats, length ai, length ii, length xs) False + -- = return False + + -- T-R + _ctx |- Top + = return True + + -- T-L + Ctx ats ai ii (Top : ctx) |- ty + = Ctx ats ai ii ctx |- ty + + -- F-L + Ctx _ _ _ (Bottom : _ctx) |- _ty + = return True + + -- Id-atoms + Ctx ats _ai _ii [] |- Var a + | Set.member a ats + = return True + + -- Id + Ctx _ats _ai _ii (x : _ctx) |- ty + | x == ty + = return True + + -- Move atoms to atoms part of context + Ctx ats ai ii (Var a : ctx) |- ty + = Ctx (Set.insert a ats) ai ii ctx |- ty + + -- =>-R + Ctx ats ai ii ctx |- (a :=>: b) + = Ctx ats ai ii (a : ctx) |- b + + -- /\-L + Ctx ats ai ii ((x :/\: y) : ctx) |- ty + = Ctx ats ai ii (x : y : ctx) |- ty + + -- =>-L-extra (Top) + -- + -- \Gamma, C |- G + -- -------------------------- + -- \Gamma, 1 -> C |- G + -- + Ctx ats ai ii ((Top :=>: c) : ctx) |- ty + = Ctx ats ai ii (c : ctx) |- ty + + -- =>-L-extra (Bottom) + -- + -- \Gamma |- G + -- -------------------------- + -- \Gamma, 0 -> C |- G + -- + Ctx ats ai ii ((Bottom :=>: _) : ctx) |- ty + = Ctx ats ai ii ctx |- ty + + -- =>-L2 (Conj) + -- + -- \Gamma, A -> (B -> C) |- G + -- -------------------------- + -- \Gamma, (A /\ B) -> C |- G + -- + Ctx ats ai ii ((a :/\: b :=>: c) : ctx) |- ty + = Ctx ats ai ii ((a :=>: b :=>: c) : ctx) |- ty + + -- =>-L3 (Disj) + -- + -- \Gamma, A -> C, B -> C |- G + -- --------------------------- + -- \Gamma, (A \/ B) -> C |- G + -- + -- or with fresh var: (P = A \/ B, but an atom) + -- + -- \Gamma, A -> P, B -> P, P -> C |- G + -- ----------------------------------- + -- \Gamma, (A \/ B) -> C |- G + -- + Ctx ats ai ii ((a :\/: b :=>: c) : ctx) |- ty = do + p <- Var <$> freshVar + Ctx ats ai ii ((p :=>: c) : (a :=>: p) : (b :=>: p) : ctx) |- ty + + -- =>-L4 preparation + -- + -- \Gamma, B -> C, A |- B \Gamma, C |- G + -- ------------------------------------------ + -- \Gamma, (A -> B) -> C |- G + -- + Ctx ats ai ii (((a :=>: b) :=>: c) : ctx) |- ty + = Ctx ats ai (Set.insert (ImplImpl a b c) ii) ctx |- ty + + -- =>-L1 preparation + -- + -- \Gamma, X, B |- G + -- ---------------------- + -- \Gamma, X, X -> B |- G + -- + Ctx ats ai ii ((Var x :=>: b) : ctx) |- ty + = Ctx ats (Set.insert (AtomImpl x b) ai) ii ctx |- ty + + -- These two rules, (\/-L) and (/\-R), are pushed to the last, as they branch. + + -- \/-L + Ctx ats ai ii ((x :\/: y) : ctx) |- ty + = Ctx ats ai ii (x : ctx) |- ty + .&& Ctx ats ai ii (y : ctx) |- ty + + -- /\-R + ctx |- (a :/\: b) + = ctx |- a + .&& ctx |- b + + -- Last rules + Ctx ats ai ii [] |- ty + -- L1 completion + | ((y, ai') : _) <- match + = Ctx ats ai' ii [y] |- ty + + -- \/-R and =>-L4 + | not (null rest) = iter rest + where + match = + [ (y, Set.delete ai' ai) + | ai'@(AtomImpl x y) <- Set.toList ai + , x `Set.member` ats + ] + + -- try in order + iter [] = return False + iter (Right (ctx', ty') : rest') = do + res <- ctx' |- ty' + if res + then return True + else iter rest' + + iter (Left (ctxa, a, ctxb, b) : rest') = do + res <- ctxa |- a .&& ctxb |- b + if res + then return True + else iter rest' + + rest = disj ++ implImpl + + -- =>-L4 + implImpl = + [ Left (Ctx ats ai ii' [x, y :=>: z], y, Ctx ats ai ii' [z], ty) + | entry@(ImplImpl x y z) <- Set.toList ii + , let ii' = Set.delete entry ii + ] + + -- \/-R + disj = case ty of + a :\/: b -> + [ Right (Ctx ats ai ii [], a) + , Right (Ctx ats ai ii [], b) + ] + _ -> [] + + Ctx _ _ _ [] |- (_ :\/: _) + = error "panic! @proofSearch should be matched before" + + Ctx _ _ _ [] |- Var _ + = return False + + Ctx _ _ _ [] |- Bottom + = return False + +------------------------------------------------------------------------------- +-- Context +------------------------------------------------------------------------------- + +data Am a + = L !Int + | R a + deriving (Eq, Ord, Show) + +data Ctx a = Ctx + { ctxAtoms :: Set (Am a) + , ctxAtomImpl :: Set (AtomImpl a) + , ctxImplImpl :: Set (ImplImpl a) + , ctxHypothesis :: [Expr (Am a)] + } + deriving Show + +emptyCtx :: Ctx l +emptyCtx = Ctx Set.empty Set.empty Set.empty [] + +-- [[ AtomImpl a b ]] = a => b +data AtomImpl a = AtomImpl (Am a) (Expr (Am a)) + deriving (Eq, Ord, Show) + +-- [[ ImplImpl a b c ]] = (a ==> b) ==> c +data ImplImpl a = ImplImpl !(Expr (Am a)) !(Expr (Am a)) !(Expr (Am a)) + deriving (Eq, Ord, Show) diff --git a/src/Algebra/Lattice.hs b/src/Algebra/Lattice.hs --- a/src/Algebra/Lattice.hs +++ b/src/Algebra/Lattice.hs @@ -1,23 +1,12 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} -#if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709 -{-# OPTIONS_GHC -fno-warn-amp #-} -#endif - -#define unordered_containers_SAFE MIN_VERSION_unordered_containers(0,2,6) -#define semigroupoids_SAFE (!MIN_VERSION_semigroupoids(5,2,2) || __GLASGOW_HASKELL__ >= 802) - -#if __GLASGOW_HASKELL__ >= 710 && unordered_containers_SAFE && semigroupoids_SAFE +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE Safe #-} -#else -{-# LANGUAGE Trustworthy #-} -#endif ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice --- Copyright : (C) 2010-2015 Maximilian Bolingbroke +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -33,13 +22,14 @@ ---------------------------------------------------------------------------- module Algebra.Lattice ( -- * Unbounded lattices - JoinSemiLattice(..), MeetSemiLattice(..), Lattice, + Lattice (..), joinLeq, joins1, meetLeq, meets1, -- * Bounded lattices - BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice, + BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), joins, meets, fromBool, + BoundedLattice, -- * Monoid wrappers Meet(..), Join(..), @@ -54,86 +44,95 @@ import qualified Algebra.PartialOrd as PO -import Data.Universe.Class (Finite (..), Universe (..)) - -import Control.Monad.Zip (MonadZip (..)) -import Data.Data (Data, Typeable) -import Data.Hashable (Hashable (..)) -import Data.Proxy (Proxy (..)) -import Data.Semigroup (All (..), Any (..), Endo (..), Semigroup (..)) -import Data.Tagged (Tagged (..)) -import Data.Void (Void) -import GHC.Generics (Generic) - -import qualified Data.IntMap as IM -import qualified Data.IntSet as IS -import qualified Data.Map as M -import qualified Data.Set as S - -import qualified Data.HashMap.Lazy as HM -import qualified Data.HashSet as HS - import Control.Applicative (Const (..)) +import Control.Monad.Zip (MonadZip (..)) +import Data.Data (Data, Typeable) import Data.Functor.Identity (Identity (..)) +import Data.Hashable (Hashable (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (All (..), Any (..), Endo (..), Semigroup (..)) import Data.Semigroup.Foldable (Foldable1 (..)) +import Data.Tagged (Tagged (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Void (Void) +import GHC.Generics (Generic) +import qualified Data.HashMap.Lazy as HM +import qualified Data.HashSet as HS +import qualified Data.IntMap as IM +import qualified Data.IntSet as IS +import qualified Data.Map as M +import qualified Data.Set as S +import qualified Test.QuickCheck as QC + infixr 6 /\ -- This comment needed because of CPP infixr 5 \/ --- | A algebraic structure with element joins: +-- | An algebraic structure with joins and meets. -- --- > Associativity: x \/ (y \/ z) == (x \/ y) \/ z --- > Commutativity: x \/ y == y \/ x --- > Idempotency: x \/ x == x -class JoinSemiLattice a where +-- See and . +-- +-- 'Lattice' is very symmetric, which is seen from the laws: +-- +-- /Associativity/ +-- +-- @ +-- x '\/' (y '\/' z) ≡ (x '\/' y) '\/' z +-- x '/\' (y '/\' z) ≡ (x '/\' y) '/\' z +-- @ +-- +-- /Commputativity/ +-- +-- @ +-- x '\/' y ≡ y '\/' x +-- x '/\' y ≡ y '/\' x +-- @ +-- +-- /Idempotency/ +-- +-- @ +-- x '\/' x ≡ x +-- x '/\' x ≡ x +-- @ +-- +-- /Absorption/ +-- +-- @ +-- a '\/' (a '/\' b) ≡ a +-- a '/\' (a '\/' b) ≡ a +-- @ +class Lattice a where + -- | join (\/) :: a -> a -> a - (\/) = join - join :: a -> a -> a - join = (\/) - -#if __GLASGOW_HASKELL__ >= 707 - {-# MINIMAL (\/) | join #-} -#endif -{-# DEPRECATED join "Use '\\/' infix operator" #-} + -- | meet + (/\) :: a -> a -> a -- | The partial ordering induced by the join-semilattice structure -joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool +joinLeq :: (Eq a, Lattice a) => a -> a -> Bool joinLeq x y = (x \/ y) == y --- | A algebraic structure with element meets: --- --- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z --- > Commutativity: x /\ y == y /\ x --- > Idempotency: x /\ x == x -class MeetSemiLattice a where - (/\) :: a -> a -> a - (/\) = meet - - meet :: a -> a -> a - meet = (/\) - -#if __GLASGOW_HASKELL__ >= 707 - {-# MINIMAL (/\) | meet #-} -#endif -{-# DEPRECATED meet "Use '/\\' infix operator" #-} - --- | The partial ordering induced by the meet-semilattice structure -meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool +meetLeq :: (Eq a, Lattice a) => a -> a -> Bool meetLeq x y = (x /\ y) == x - - --- | The combination of two semi lattices makes a lattice if the absorption law holds: --- see and --- --- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a -class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where - -- | A join-semilattice with an identity element 'bottom' for '\/'. -- --- > Identity: x \/ bottom == x -class JoinSemiLattice a => BoundedJoinSemiLattice a where +-- /Laws/ +-- +-- @ +-- x '\/' 'bottom' ≡ x +-- @ +-- +-- /Corollary/ +-- +-- @ +-- x '/\' 'bottom' +-- ≡⟨ identity ⟩ +-- (x '/\' 'bottom') '\/' 'bottom' +-- ≡⟨ absorption ⟩ +-- 'bottom' +-- @ +class Lattice a => BoundedJoinSemiLattice a where bottom :: a -- | The join of a list of join-semilattice elements @@ -141,13 +140,28 @@ joins = getJoin . foldMap Join -- | The join of at a list of join-semilattice elements (of length at least one) -joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a +joins1 :: (Lattice a, Foldable1 f) => f a -> a joins1 = getJoin . foldMap1 Join -- | A meet-semilattice with an identity element 'top' for '/\'. -- --- > Identity: x /\ top == x -class MeetSemiLattice a => BoundedMeetSemiLattice a where +-- /Laws/ +-- +-- @ +-- x '/\' 'top' ≡ x +-- @ +-- +-- /Corollary/ +-- +-- @ +-- x '\/' 'top' +-- ≡⟨ identity ⟩ +-- (x '\/' 'top') '/\' 'top' +-- ≡⟨ absorption ⟩ +-- 'top' +-- @ +-- +class Lattice a => BoundedMeetSemiLattice a where top :: a -- | The meet of a list of meet-semilattice elements @@ -155,11 +169,10 @@ meets = getMeet . foldMap Meet -- -- | The meet of at a list of meet-semilattice elements (of length at least one) -meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a +meets1 :: (Lattice a, Foldable1 f) => f a -> a meets1 = getMeet . foldMap1 Meet --- | Lattices with both bounds -class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where +type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) -- | 'True' to 'top' and 'False' to 'bottom' fromBool :: BoundedLattice a => Bool -> a @@ -170,34 +183,24 @@ -- Sets -- -instance Ord a => JoinSemiLattice (S.Set a) where +instance Ord a => Lattice (S.Set a) where (\/) = S.union - -instance Ord a => MeetSemiLattice (S.Set a) where (/\) = S.intersection -instance Ord a => Lattice (S.Set a) - instance Ord a => BoundedJoinSemiLattice (S.Set a) where bottom = S.empty instance (Ord a, Finite a) => BoundedMeetSemiLattice (S.Set a) where top = S.fromList universeF -instance (Ord a, Finite a) => BoundedLattice (S.Set a) - -- -- IntSets -- -instance JoinSemiLattice IS.IntSet where +instance Lattice IS.IntSet where (\/) = IS.union - -instance MeetSemiLattice IS.IntSet where (/\) = IS.intersection -instance Lattice IS.IntSet - instance BoundedJoinSemiLattice IS.IntSet where bottom = IS.empty @@ -205,168 +208,127 @@ -- HashSet -- -instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where - (\/) = HS.union -instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where +instance (Eq a, Hashable a) => Lattice (HS.HashSet a) where + (\/) = HS.union (/\) = HS.intersection -instance (Eq a, Hashable a) => Lattice (HS.HashSet a) - instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where bottom = HS.empty instance (Eq a, Hashable a, Finite a) => BoundedMeetSemiLattice (HS.HashSet a) where top = HS.fromList universeF -instance (Eq a, Hashable a, Finite a) => BoundedLattice (HS.HashSet a) - -- -- Maps -- -instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where +instance (Ord k, Lattice v) => Lattice (M.Map k v) where (\/) = M.unionWith (\/) - -instance (Ord k, MeetSemiLattice v) => MeetSemiLattice (M.Map k v) where (/\) = M.intersectionWith (/\) -instance (Ord k, Lattice v) => Lattice (M.Map k v) where - -instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where +instance (Ord k, Lattice v) => BoundedJoinSemiLattice (M.Map k v) where bottom = M.empty instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map k v) where top = M.fromList (universeF `zip` repeat top) -instance (Ord k, Finite k, BoundedLattice v) => BoundedLattice (M.Map k v) where - -- -- IntMaps -- -instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where +instance Lattice v => Lattice (IM.IntMap v) where (\/) = IM.unionWith (\/) - -instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where - bottom = IM.empty - -instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where (/\) = IM.intersectionWith (/\) -instance Lattice v => Lattice (IM.IntMap v) - +instance Lattice v => BoundedJoinSemiLattice (IM.IntMap v) where + bottom = IM.empty -- -- HashMaps -- -instance (Eq k, Hashable k, JoinSemiLattice v) => JoinSemiLattice (HM.HashMap k v) where - (\/) = HM.unionWith (\/) - -instance (Eq k, Hashable k, MeetSemiLattice v) => MeetSemiLattice (HM.HashMap k v) where - (/\) = HM.intersectionWith (/\) - -instance (Eq k, Hashable k, JoinSemiLattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where +instance (Eq k, Hashable k, Lattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where bottom = HM.empty instance (Eq k, Hashable k, Lattice v) => Lattice (HM.HashMap k v) where + (\/) = HM.unionWith (\/) + (/\) = HM.intersectionWith (/\) instance (Eq k, Hashable k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (HM.HashMap k v) where top = HM.fromList (universeF `zip` repeat top) -instance (Eq k, Hashable k, Finite k, BoundedLattice v) => BoundedLattice (HM.HashMap k v) where - -- -- Functions -- -instance JoinSemiLattice v => JoinSemiLattice (k -> v) where +instance Lattice v => Lattice (k -> v) where f \/ g = \x -> f x \/ g x - -instance MeetSemiLattice v => MeetSemiLattice (k -> v) where f /\ g = \x -> f x /\ g x -instance Lattice v => Lattice (k -> v) where - instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where bottom = const bottom instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where top = const top -instance BoundedLattice v => BoundedLattice (k -> v) where - +-- -- Unit -instance JoinSemiLattice () where - _ \/ _ = () +-- + +instance Lattice () where + _ \/ _ = () + _ /\ _ = () + instance BoundedJoinSemiLattice () where bottom = () -instance MeetSemiLattice () where - _ /\ _ = () - instance BoundedMeetSemiLattice () where top = () -instance Lattice () where -instance BoundedLattice () where - -- -- Tuples -- -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where +instance (Lattice a, Lattice b) => Lattice (a, b) where (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2) - -instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) -instance (Lattice a, Lattice b) => Lattice (a, b) where - instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where bottom = (bottom, bottom) instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where top = (top, top) -instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where - -- -- Bools -- -instance JoinSemiLattice Bool where +instance Lattice Bool where (\/) = (||) - -instance MeetSemiLattice Bool where (/\) = (&&) -instance Lattice Bool where - instance BoundedJoinSemiLattice Bool where bottom = False instance BoundedMeetSemiLattice Bool where top = True -instance BoundedLattice Bool where - --- Monoids --- | Monoid wrapper for JoinSemiLattice +-- | Monoid wrapper for join-'Lattice' newtype Join a = Join { getJoin :: a } deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) -instance JoinSemiLattice a => Semigroup (Join a) where +instance Lattice a => Semigroup (Join a) where Join a <> Join b = Join (a \/ b) instance BoundedJoinSemiLattice a => Monoid (Join a) where mempty = Join bottom Join a `mappend` Join b = Join (a \/ b) -instance (Eq a, JoinSemiLattice a) => PO.PartialOrd (Join a) where +instance (Eq a, Lattice a) => PO.PartialOrd (Join a) where leq (Join a) (Join b) = joinLeq a b instance Functor Join where @@ -391,18 +353,18 @@ instance Finite a => Finite (Join a) where universeF = fmap Join universeF --- | Monoid wrapper for MeetSemiLattice +-- | Monoid wrapper for meet-'Lattice' newtype Meet a = Meet { getMeet :: a } deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) -instance MeetSemiLattice a => Semigroup (Meet a) where +instance Lattice a => Semigroup (Meet a) where Meet a <> Meet b = Meet (a /\ b) instance BoundedMeetSemiLattice a => Monoid (Meet a) where mempty = Meet top Meet a `mappend` Meet b = Meet (a /\ b) -instance (Eq a, MeetSemiLattice a) => PO.PartialOrd (Meet a) where +instance (Eq a, Lattice a) => PO.PartialOrd (Meet a) where leq (Meet a) (Meet b) = meetLeq a b instance Functor Meet where @@ -428,127 +390,107 @@ universeF = fmap Meet universeF -- All -instance JoinSemiLattice All where + +instance Lattice All where All a \/ All b = All $ a \/ b + All a /\ All b = All $ a /\ b instance BoundedJoinSemiLattice All where bottom = All False -instance MeetSemiLattice All where - All a /\ All b = All $ a /\ b - instance BoundedMeetSemiLattice All where top = All True -instance Lattice All where -instance BoundedLattice All where - -- Any -instance JoinSemiLattice Any where +instance Lattice Any where Any a \/ Any b = Any $ a \/ b + Any a /\ Any b = Any $ a /\ b instance BoundedJoinSemiLattice Any where bottom = Any False -instance MeetSemiLattice Any where - Any a /\ Any b = Any $ a /\ b - instance BoundedMeetSemiLattice Any where top = Any True -instance Lattice Any where -instance BoundedLattice Any where - -- Endo -instance JoinSemiLattice a => JoinSemiLattice (Endo a) where +instance Lattice a => Lattice (Endo a) where Endo a \/ Endo b = Endo $ a \/ b + Endo a /\ Endo b = Endo $ a /\ b instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where bottom = Endo bottom -instance MeetSemiLattice a => MeetSemiLattice (Endo a) where - Endo a /\ Endo b = Endo $ a /\ b - instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where top = Endo top -instance Lattice a => Lattice (Endo a) where -instance BoundedLattice a => BoundedLattice (Endo a) where - -- Tagged -instance JoinSemiLattice a => JoinSemiLattice (Tagged t a) where + +instance Lattice a => Lattice (Tagged t a) where Tagged a \/ Tagged b = Tagged $ a \/ b + Tagged a /\ Tagged b = Tagged $ a /\ b instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where bottom = Tagged bottom -instance MeetSemiLattice a => MeetSemiLattice (Tagged t a) where - Tagged a /\ Tagged b = Tagged $ a /\ b - instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where top = Tagged top -instance Lattice a => Lattice (Tagged t a) where -instance BoundedLattice a => BoundedLattice (Tagged t a) where - -- Proxy -instance JoinSemiLattice (Proxy a) where +instance Lattice (Proxy a) where _ \/ _ = Proxy + _ /\ _ = Proxy instance BoundedJoinSemiLattice (Proxy a) where bottom = Proxy -instance MeetSemiLattice (Proxy a) where - _ /\ _ = Proxy - instance BoundedMeetSemiLattice (Proxy a) where top = Proxy -instance Lattice (Proxy a) where -instance BoundedLattice (Proxy a) where - -#if MIN_VERSION_base(4,8,0) -- Identity -instance JoinSemiLattice a => JoinSemiLattice (Identity a) where - Identity a \/ Identity b = Identity (a \/ b) -instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where - bottom = Identity bottom - -instance MeetSemiLattice a => MeetSemiLattice (Identity a) where +instance Lattice a => Lattice (Identity a) where + Identity a \/ Identity b = Identity (a \/ b) Identity a /\ Identity b = Identity (a /\ b) instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where top = Identity top -instance Lattice a => Lattice (Identity a) where -instance BoundedLattice a => BoundedLattice (Identity a) where -#endif +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where + bottom = Identity bottom -- Const -instance JoinSemiLattice a => JoinSemiLattice (Const a b) where +instance Lattice a => Lattice (Const a b) where Const a \/ Const b = Const (a \/ b) + Const a /\ Const b = Const (a /\ b) instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where bottom = Const bottom -instance MeetSemiLattice a => MeetSemiLattice (Const a b) where - Const a /\ Const b = Const (a /\ b) - instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where top = Const top -instance Lattice a => Lattice (Const a b) where -instance BoundedLattice a => BoundedLattice (Const a b) where - +------------------------------------------------------------------------------- -- Void -instance JoinSemiLattice Void where - a \/ _ = a +------------------------------------------------------------------------------- -instance MeetSemiLattice Void where +instance Lattice Void where + a \/ _ = a a /\ _ = a -instance Lattice Void where +------------------------------------------------------------------------------- +-- QuickCheck +------------------------------------------------------------------------------- + +instance Lattice QC.Property where + (\/) = (QC..||.) + (/\) = (QC..&&.) + +instance BoundedJoinSemiLattice QC.Property where bottom = QC.property False +instance BoundedMeetSemiLattice QC.Property where top = QC.property True + +------------------------------------------------------------------------------- +-- Theorems +------------------------------------------------------------------------------- -- | Implementation of Kleene fixed-point theorem . -- Assumes that the function is monotone and does not check if that is correct. diff --git a/src/Algebra/Lattice/Divisibility.hs b/src/Algebra/Lattice/Divisibility.hs --- a/src/Algebra/Lattice/Divisibility.hs +++ b/src/Algebra/Lattice/Divisibility.hs @@ -1,20 +1,16 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Divisibility --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -30,12 +26,16 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Divisibility -- @@ -43,9 +43,7 @@ -- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. newtype Divisibility a = Divisibility { getDivisibility :: a } deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance Applicative Divisibility where @@ -61,16 +59,34 @@ instance Hashable a => Hashable (Divisibility a) -instance Integral a => JoinSemiLattice (Divisibility a) where +instance Integral a => Lattice (Divisibility a) where Divisibility x \/ Divisibility y = Divisibility (lcm x y) -instance Integral a => MeetSemiLattice (Divisibility a) where Divisibility x /\ Divisibility y = Divisibility (gcd x y) -instance Integral a => Lattice (Divisibility a) where - instance Integral a => BoundedJoinSemiLattice (Divisibility a) where bottom = Divisibility 1 instance (Eq a, Integral a) => PartialOrd (Divisibility a) where leq (Divisibility a) (Divisibility b) = b `mod` a == 0 + +instance Universe a => Universe (Divisibility a) where + universe = map Divisibility universe +instance Finite a => Finite (Divisibility a) where + universeF = map Divisibility universeF + cardinality = retag (cardinality :: Tagged a Natural) + +instance (QC.Arbitrary a, Num a, Ord a) => QC.Arbitrary (Divisibility a) where + arbitrary = divisibility <$> QC.arbitrary + shrink d = filter ( QC.CoArbitrary (Divisibility a) where + coarbitrary = QC.coarbitrary . getDivisibility + +instance QC.Function a => QC.Function (Divisibility a) where + function = QC.functionMap getDivisibility Divisibility + +divisibility :: (Ord a, Num a) => a -> Divisibility a +divisibility x | x < (-1) = Divisibility (abs x) + | x < 1 = Divisibility 1 + | otherwise = Divisibility x diff --git a/src/Algebra/Lattice/Dropped.hs b/src/Algebra/Lattice/Dropped.hs --- a/src/Algebra/Lattice/Dropped.hs +++ b/src/Algebra/Lattice/Dropped.hs @@ -1,20 +1,16 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Dropped --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -23,31 +19,35 @@ module Algebra.Lattice.Dropped ( Dropped(..) , retractDropped + , foldDropped ) where import Prelude () import Prelude.Compat import Algebra.Lattice +import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Dropped -- -- | Graft a distinct top onto an otherwise unbounded lattice. -- As a bonus, the top will be an absorbing element for the join. -data Dropped a = Top - | Drop a +data Dropped a = Drop a + | Top deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance Applicative Dropped where @@ -65,27 +65,58 @@ instance Hashable a => Hashable (Dropped a) -instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where +instance PartialOrd a => PartialOrd (Dropped a) where + leq _ Top = True + leq Top _ = False + leq (Drop x) (Drop y) = leq x y + comparable Top _ = True + comparable _ Top = True + comparable (Drop x) (Drop y) = comparable x y + +instance Lattice a => Lattice (Dropped a) where Top \/ _ = Top _ \/ Top = Top Drop x \/ Drop y = Drop (x \/ y) -instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where Top /\ drop_y = drop_y drop_x /\ Top = drop_x Drop x /\ Drop y = Drop (x /\ y) -instance Lattice a => Lattice (Dropped a) where - instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where bottom = Drop bottom -instance MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a) where +instance Lattice a => BoundedMeetSemiLattice (Dropped a) where top = Top -instance BoundedLattice a => BoundedLattice (Dropped a) where - -- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a -retractDropped Top = top -retractDropped (Drop x) = x +retractDropped = foldDropped top id + +-- | Similar to @'maybe'@, but for @'Dropped'@ type. +foldDropped :: b -> (a -> b) -> Dropped a -> b +foldDropped _ f (Drop x) = f x +foldDropped y _ Top = y + +instance Universe a => Universe (Dropped a) where + universe = Top : map Drop universe +instance Finite a => Finite (Dropped a) where + universeF = Top : map Drop universeF + cardinality = fmap succ (retag (cardinality :: Tagged a Natural)) + +instance QC.Arbitrary a => QC.Arbitrary (Dropped a) where + arbitrary = QC.frequency + [ (1, pure Top) + , (9, Drop <$> QC.arbitrary) + ] + + shrink Top = [] + shrink (Drop x) = Top : map Drop (QC.shrink x) + +instance QC.CoArbitrary a => QC.CoArbitrary (Dropped a) where + coarbitrary Top = QC.variant (0 :: Int) + coarbitrary (Drop x) = QC.variant (1 :: Int) . QC.coarbitrary x + +instance QC.Function a => QC.Function (Dropped a) where + function = QC.functionMap fromDropped toDropped where + fromDropped = foldDropped Nothing Just + toDropped = maybe Top Drop diff --git a/src/Algebra/Lattice/Free.hs b/src/Algebra/Lattice/Free.hs --- a/src/Algebra/Lattice/Free.hs +++ b/src/Algebra/Lattice/Free.hs @@ -1,148 +1,144 @@ -{-# LANGUAGE RankNTypes #-} - ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Free --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- - -module Algebra.Lattice.Free - ( -- * Free join-semilattices - FreeJoinSemiLattice - , liftFreeJoinSemiLattice - , lowerFreeJoinSemiLattice - , retractFreeJoinSemiLattice - - -- * Free meet-semilattices - , FreeMeetSemiLattice - , liftFreeMeetSemiLattice - , lowerFreeMeetSemiLattice - , retractFreeMeetSemiLattice - - -- * Free lattices - , FreeLattice - , liftFreeLattice - , lowerFreeLattice - , retractFreeLattice - ) where +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Algebra.Lattice.Free ( + Free (..), + liftFree, + lowerFree, + substFree, + retractFree, + toExpr, + ) where import Prelude () import Prelude.Compat import Algebra.Lattice -import Data.Universe.Class - --- --- Free join-semilattices --- - -newtype FreeJoinSemiLattice a = FreeJoinSemiLattice - { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b => - (a -> b) -> b - } - -liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a -liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a) - -retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a -retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id - -instance Functor FreeJoinSemiLattice where - fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f)) - a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a))) - -instance JoinSemiLattice (FreeJoinSemiLattice a) where - FreeJoinSemiLattice f \/ FreeJoinSemiLattice g = - FreeJoinSemiLattice (\inj -> f inj \/ g inj) - -instance BoundedJoinSemiLattice a => - BoundedJoinSemiLattice (FreeJoinSemiLattice a) where - bottom = FreeJoinSemiLattice (\inj -> inj bottom) +import Algebra.PartialOrd -instance Universe a => Universe (FreeJoinSemiLattice a) where - universe = fmap liftFreeJoinSemiLattice universe +import Control.Applicative (liftA2) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import GHC.Generics (Generic, Generic1) +import Math.NumberTheory.Logarithms (intLog2) -instance Finite a => Finite (FreeJoinSemiLattice a) where - universeF = fmap liftFreeJoinSemiLattice universeF +import qualified Algebra.Heyting.Free.Expr as E +import qualified Test.QuickCheck as QC +------------------------------------------------------------------------------- +-- Free +------------------------------------------------------------------------------- +-- | Free distributive lattice. -- --- Free meet-semilattices +-- `Eq` and `PartialOrd` instances aren't structural. -- - -newtype FreeMeetSemiLattice a = FreeMeetSemiLattice - { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b => - (a -> b) -> b - } - -instance Functor FreeMeetSemiLattice where - fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f)) - a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a))) - -liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a -liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a) - -retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a -retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id +-- >>> (Var 'x' /\ Var 'y') == (Var 'y' /\ Var 'x' /\ Var 'x') +-- True +-- +-- >>> Var 'x' == Var 'y' +-- False +-- +-- This is /distributive/ lattice. +-- +-- >>> import Algebra.Lattice.M3 -- non distributive lattice +-- >>> let x = M3a; y = M3b; z = M3c +-- >>> let lhs = Var x \/ (Var y /\ Var z) +-- >>> let rhs = (Var x \/ Var y) /\ (Var x \/ Var z) +-- +-- 'Free' is distributive so +-- +-- >>> lhs == rhs +-- True +-- +-- but when retracted, values are inequal +-- +-- >>> retractFree lhs == retractFree rhs +-- False +-- +-- >>> (retractFree lhs, retractFree rhs) +-- (M3a,M3i) +-- +data Free a + = Var a + | Free a :/\: Free a + | Free a :\/: Free a + deriving (Show, Functor, Foldable, Traversable, Generic, Generic1, Data, Typeable) -instance MeetSemiLattice (FreeMeetSemiLattice a) where - FreeMeetSemiLattice f /\ FreeMeetSemiLattice g = - FreeMeetSemiLattice (\inj -> f inj /\ g inj) +infixr 6 :/\: +infixr 5 :\/: -instance BoundedMeetSemiLattice a => - BoundedMeetSemiLattice (FreeMeetSemiLattice a) where - top = FreeMeetSemiLattice (\inj -> inj top) +liftFree :: a -> Free a +liftFree = Var -instance Universe a => Universe (FreeMeetSemiLattice a) where - universe = fmap liftFreeMeetSemiLattice universe +retractFree :: Lattice a => Free a -> a +retractFree = lowerFree id -instance Finite a => Finite (FreeMeetSemiLattice a) where - universeF = fmap liftFreeMeetSemiLattice universeF +substFree :: Free a -> (a -> Free b) -> Free b +substFree z k = go z where + go (Var x) = k x + go (x :/\: y) = go x /\ go y + go (x :\/: y) = go x \/ go y +lowerFree :: Lattice b => (a -> b) -> Free a -> b +lowerFree f = go where + go (Var x) = f x + go (x :/\: y) = go x /\ go y + go (x :\/: y) = go x \/ go y --- --- Free lattices --- +toExpr :: Free a -> E.Expr a +toExpr (Var a) = E.Var a +toExpr (x :/\: y) = toExpr x E.:/\: toExpr y +toExpr (x :\/: y) = toExpr x E.:\/: toExpr y -newtype FreeLattice a = FreeLattice - { lowerFreeLattice :: forall b. Lattice b => - (a -> b) -> b - } +------------------------------------------------------------------------------- +-- Monad +------------------------------------------------------------------------------- -instance Functor FreeLattice where - fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f)) - a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a))) +instance Applicative Free where + pure = liftFree + (<*>) = ap -liftFreeLattice :: a -> FreeLattice a -liftFreeLattice a = FreeLattice (\inj -> inj a) +instance Monad Free where + return = pure + (>>=) = substFree -retractFreeLattice :: Lattice a => FreeLattice a -> a -retractFreeLattice a = lowerFreeLattice a id +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- -instance JoinSemiLattice (FreeLattice a) where - FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj) +instance Lattice (Free a) where + x /\ y = x :/\: y + x \/ y = x :\/: y -instance MeetSemiLattice (FreeLattice a) where - FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj) +instance Ord a => Eq (Free a) where + (==) = partialOrdEq -instance Lattice (FreeLattice a) +instance Ord a => PartialOrd (Free a) where + leq x y = E.proofSearch (toExpr x E.:=>: toExpr y) -instance BoundedJoinSemiLattice a => - BoundedJoinSemiLattice (FreeLattice a) where - bottom = FreeLattice (\inj -> inj bottom) +------------------------------------------------------------------------------- +-- Other instances +------------------------------------------------------------------------------- -instance BoundedMeetSemiLattice a => - BoundedMeetSemiLattice (FreeLattice a) where - top = FreeLattice (\inj -> inj top) +instance QC.Arbitrary a => QC.Arbitrary (Free a) where + arbitrary = QC.sized arb where + arb n | n <= 0 = prim + | otherwise = QC.oneof (prim : compound) + where + arb' = arb (intLog2 (max 1 n)) -instance BoundedLattice a => - BoundedLattice (FreeLattice a) + compound = + [ liftA2 (:/\:) arb' arb' + , liftA2 (:\/:) arb' arb' + ] -instance Universe a => Universe (FreeLattice a) where - universe = fmap liftFreeLattice universe + prim = Var <$> QC.arbitrary -instance Finite a => Finite (FreeLattice a) where - universeF = fmap liftFreeLattice universeF + shrink (Var c) = map Var (QC.shrink c) + shrink (x :/\: y) = x : y : map (uncurry (:/\:)) (QC.shrink (x, y)) + shrink (x :\/: y) = x : y : map (uncurry (:\/:)) (QC.shrink (x, y)) diff --git a/src/Algebra/Lattice/Free/Final.hs b/src/Algebra/Lattice/Free/Final.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Free/Final.hs @@ -0,0 +1,106 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} + +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Free +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- + +module Algebra.Lattice.Free.Final ( + -- * Free Lattice + FLattice, + liftFLattice, + lowerFLattice, + retractFLattice, + -- * Free BoundedLattice + FBoundedLattice, + liftFBoundedLattice, + lowerFBoundedLattice, + retractFBoundedLattice, + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice + +import Data.Universe.Class (Finite (..), Universe (..)) + +------------------------------------------------------------------------------- +-- Lattice +------------------------------------------------------------------------------- + +newtype FLattice a = FLattice + { lowerFLattice :: forall b. Lattice b => + (a -> b) -> b + } + +instance Functor FLattice where + fmap f (FLattice g) = FLattice (\inj -> g (inj . f)) + a <$ FLattice f = FLattice (\inj -> f (const (inj a))) + +liftFLattice :: a -> FLattice a +liftFLattice a = FLattice (\inj -> inj a) + +retractFLattice :: Lattice a => FLattice a -> a +retractFLattice a = lowerFLattice a id + +instance Lattice (FLattice a) where + FLattice f \/ FLattice g = FLattice (\inj -> f inj \/ g inj) + FLattice f /\ FLattice g = FLattice (\inj -> f inj /\ g inj) + + +instance BoundedJoinSemiLattice a => + BoundedJoinSemiLattice (FLattice a) where + bottom = FLattice (\inj -> inj bottom) + +instance BoundedMeetSemiLattice a => + BoundedMeetSemiLattice (FLattice a) where + top = FLattice (\inj -> inj top) + +instance Universe a => Universe (FLattice a) where + universe = fmap liftFLattice universe + +instance Finite a => Finite (FLattice a) where + universeF = fmap liftFLattice universeF + +------------------------------------------------------------------------------- +-- BoundedLattice +------------------------------------------------------------------------------- + +newtype FBoundedLattice a = FBoundedLattice + { lowerFBoundedLattice :: forall b. BoundedLattice b => + (a -> b) -> b + } + +instance Functor FBoundedLattice where + fmap f (FBoundedLattice g) = FBoundedLattice (\inj -> g (inj . f)) + a <$ FBoundedLattice f = FBoundedLattice (\inj -> f (const (inj a))) + +liftFBoundedLattice :: a -> FBoundedLattice a +liftFBoundedLattice a = FBoundedLattice (\inj -> inj a) + +retractFBoundedLattice :: BoundedLattice a => FBoundedLattice a -> a +retractFBoundedLattice a = lowerFBoundedLattice a id + +instance Lattice (FBoundedLattice a) where + FBoundedLattice f \/ FBoundedLattice g = FBoundedLattice (\inj -> f inj \/ g inj) + FBoundedLattice f /\ FBoundedLattice g = FBoundedLattice (\inj -> f inj /\ g inj) + + +instance BoundedJoinSemiLattice (FBoundedLattice a) where + bottom = FBoundedLattice (\_ -> bottom) + +instance BoundedMeetSemiLattice (FBoundedLattice a) where + top = FBoundedLattice (\_ -> top) + +instance Universe a => Universe (FBoundedLattice a) where + universe = fmap liftFBoundedLattice universe + +instance Finite a => Finite (FBoundedLattice a) where + universeF = fmap liftFBoundedLattice universeF diff --git a/src/Algebra/Lattice/Levitated.hs b/src/Algebra/Lattice/Levitated.hs --- a/src/Algebra/Lattice/Levitated.hs +++ b/src/Algebra/Lattice/Levitated.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} @@ -6,15 +5,12 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE Safe #-} -#endif ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Levitated --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -23,19 +19,25 @@ module Algebra.Lattice.Levitated ( Levitated(..) , retractLevitated + , foldLevitated ) where import Prelude () import Prelude.Compat import Algebra.Lattice +import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Levitated -- @@ -43,13 +45,11 @@ -- | Graft a distinct top and bottom onto an otherwise unbounded lattice. -- The top is the absorbing element for the join, and the bottom is the absorbing -- element for the meet. -data Levitated a = Top +data Levitated a = Bottom | Levitate a - | Bottom + | Top deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance Applicative Levitated where @@ -69,32 +69,75 @@ instance Hashable a => Hashable (Levitated a) -instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where +instance PartialOrd a => PartialOrd (Levitated a) where + leq _ Top = True + leq Top _ = False + leq Bottom _ = True + leq _ Bottom = False + leq (Levitate x) (Levitate y) = leq x y + comparable Top _ = True + comparable _ Top = True + comparable Bottom _ = True + comparable _ Bottom = True + comparable (Levitate x) (Levitate y) = comparable x y + +instance Lattice a => Lattice (Levitated a) where Top \/ _ = Top _ \/ Top = Top Levitate x \/ Levitate y = Levitate (x \/ y) Bottom \/ lev_y = lev_y lev_x \/ Bottom = lev_x -instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where Top /\ lev_y = lev_y lev_x /\ Top = lev_x Levitate x /\ Levitate y = Levitate (x /\ y) Bottom /\ _ = Bottom _ /\ Bottom = Bottom -instance Lattice a => Lattice (Levitated a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where +instance Lattice a => BoundedJoinSemiLattice (Levitated a) where bottom = Bottom -instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where +instance Lattice a => BoundedMeetSemiLattice (Levitated a) where top = Top -instance Lattice a => BoundedLattice (Levitated a) where - -- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@. -retractLevitated :: BoundedLattice a => Levitated a -> a -retractLevitated Top = top -retractLevitated Bottom = bottom -retractLevitated (Levitate x) = x +retractLevitated :: (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) => Levitated a -> a +retractLevitated = foldLevitated bottom id top + +-- | Fold 'Levitated'. +foldLevitated :: b -> (a -> b) -> b -> Levitated a -> b +foldLevitated b _ _ Bottom = b +foldLevitated _ f _ (Levitate x) = f x +foldLevitated _ _ t Top = t + +instance Universe a => Universe (Levitated a) where + universe = Top : Bottom : map Levitate universe +instance Finite a => Finite (Levitated a) where + universeF = Top : Bottom : map Levitate universeF + cardinality = fmap (2 +) (retag (cardinality :: Tagged a Natural)) + +instance QC.Arbitrary a => QC.Arbitrary (Levitated a) where + arbitrary = QC.frequency + [ (1, pure Top) + , (1, pure Bottom) + , (9, Levitate <$> QC.arbitrary) + ] + + shrink Top = [] + shrink Bottom = [] + shrink (Levitate x) = Top : Bottom : map Levitate (QC.shrink x) + +instance QC.CoArbitrary a => QC.CoArbitrary (Levitated a) where + coarbitrary Top = QC.variant (0 :: Int) + coarbitrary Bottom = QC.variant (0 :: Int) + coarbitrary (Levitate x) = QC.variant (0 :: Int) . QC.coarbitrary x + +instance QC.Function a => QC.Function (Levitated a) where + function = QC.functionMap fromLevitated toLevitated where + fromLevitated Top = Left True + fromLevitated Bottom = Left False + fromLevitated (Levitate x) = Right x + + toLevitated (Left True) = Top + toLevitated (Left False) = Bottom + toLevitated (Right x) = Levitate x diff --git a/src/Algebra/Lattice/Lexicographic.hs b/src/Algebra/Lattice/Lexicographic.hs --- a/src/Algebra/Lattice/Lexicographic.hs +++ b/src/Algebra/Lattice/Lexicographic.hs @@ -1,20 +1,16 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else {-# LANGUAGE Safe #-} -#endif +{-# LANGUAGE TypeOperators #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Lexicographic --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -30,12 +26,16 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap, liftM2) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Lexicographic -- @@ -49,15 +49,13 @@ -- -- An application of this type is versioning. For example, a -- Last-Writer-Wins register would look like --- 'Lexicographc (Ordered Timestamp) v' where the lattice +-- @'Lexicographic' ('Algebra.Lattice.Ordered.Ordered' Timestamp) v@ where the lattice -- structure handles the, presumably rare, case of matching --- 'Timestamps'. Typically this is done in an arbitary, but +-- @Timestamp@s. Typically this is done in an arbitary, but -- deterministic manner. data Lexicographic k v = Lexicographic !k !v deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where @@ -95,30 +93,25 @@ -- (3, 2) `leq` (6, 1) -- @ -- -instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where +instance (PartialOrd k, Lattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => Lattice (Lexicographic k v) where l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2) | k1 == k2 = Lexicographic k1 (v1 \/ v2) | k1 `leq` k2 = r | k2 `leq` k1 = l | otherwise = Lexicographic (k1 \/ k2) bottom -instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2) | k1 == k2 = Lexicographic k1 (v1 /\ v2) | k1 `leq` k2 = l | k2 `leq` k1 = r | otherwise = Lexicographic (k1 /\ k2) top -instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where - -instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where +instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where bottom = Lexicographic bottom bottom -instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where +instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where top = Lexicographic top top -instance (PartialOrd k, BoundedLattice k, BoundedLattice v) => BoundedLattice (Lexicographic k v) where - instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where Lexicographic k1 v1 `leq` Lexicographic k2 v2 | k1 == k2 = v1 `leq` v2 @@ -127,3 +120,21 @@ comparable (Lexicographic k1 v1) (Lexicographic k2 v2) | k1 == k2 = comparable v1 v2 | otherwise = comparable k1 k2 + +instance (Universe k, Universe v) => Universe (Lexicographic k v) where + universe = map (uncurry Lexicographic) universe +instance (Finite k, Finite v) => Finite (Lexicographic k v) where + universeF = map (uncurry Lexicographic) universeF + cardinality = liftM2 (*) + (retag (cardinality :: Tagged k Natural)) + (retag (cardinality :: Tagged v Natural)) + +instance (QC.Arbitrary k, QC.Arbitrary v) => QC.Arbitrary (Lexicographic k v) where + arbitrary = uncurry Lexicographic <$> QC.arbitrary + shrink (Lexicographic k v) = uncurry Lexicographic <$> QC.shrink (k, v) + +instance (QC.CoArbitrary k, QC.CoArbitrary v) => QC.CoArbitrary (Lexicographic k v) where + coarbitrary (Lexicographic k v) = QC.coarbitrary (k, v) + +instance (QC.Function k, QC.Function v) => QC.Function (Lexicographic k v) where + function = QC.functionMap (\(Lexicographic k v) -> (k,v)) (uncurry Lexicographic) diff --git a/src/Algebra/Lattice/Lifted.hs b/src/Algebra/Lattice/Lifted.hs --- a/src/Algebra/Lattice/Lifted.hs +++ b/src/Algebra/Lattice/Lifted.hs @@ -1,20 +1,16 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else {-# LANGUAGE Safe #-} -#endif +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Lifted --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -23,31 +19,35 @@ module Algebra.Lattice.Lifted ( Lifted(..) , retractLifted + , foldLifted ) where import Prelude () import Prelude.Compat import Algebra.Lattice +import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Lifted -- -- | Graft a distinct bottom onto an otherwise unbounded lattice. -- As a bonus, the bottom will be an absorbing element for the meet. -data Lifted a = Lift a - | Bottom +data Lifted a = Bottom + | Lift a deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance Applicative Lifted where @@ -65,27 +65,57 @@ instance Hashable a => Hashable (Lifted a) -instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where +instance PartialOrd a => PartialOrd (Lifted a) where + leq Bottom _ = True + leq _ Bottom = False + leq (Lift x) (Lift y) = leq x y + comparable Bottom _ = True + comparable _ Bottom = True + comparable (Lift x) (Lift y) = comparable x y + +instance Lattice a => Lattice (Lifted a) where Lift x \/ Lift y = Lift (x \/ y) Bottom \/ lift_y = lift_y lift_x \/ Bottom = lift_x -instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where Lift x /\ Lift y = Lift (x /\ y) Bottom /\ _ = Bottom _ /\ Bottom = Bottom -instance Lattice a => Lattice (Lifted a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where +instance Lattice a => BoundedJoinSemiLattice (Lifted a) where bottom = Bottom instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where top = Lift top -instance BoundedLattice a => BoundedLattice (Lifted a) where - -- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a -retractLifted Bottom = bottom -retractLifted (Lift x) = x +retractLifted = foldLifted bottom id + +-- | Similar to @'maybe'@, but for @'Lifted'@ type. +foldLifted :: b -> (a -> b) -> Lifted a -> b +foldLifted _ f (Lift x) = f x +foldLifted y _ Bottom = y + +instance Universe a => Universe (Lifted a) where + universe = Bottom : map Lift universe +instance Finite a => Finite (Lifted a) where + universeF = Bottom : map Lift universeF + cardinality = fmap succ (retag (cardinality :: Tagged a Natural)) + +instance QC.Arbitrary a => QC.Arbitrary (Lifted a) where + arbitrary = QC.frequency + [ (1, pure Bottom) + , (9, Lift <$> QC.arbitrary) + ] + shrink Bottom = [] + shrink (Lift x) = Bottom : map Lift (QC.shrink x) + +instance QC.CoArbitrary a => QC.CoArbitrary (Lifted a) where + coarbitrary Bottom = QC.variant (0 :: Int) + coarbitrary (Lift x) = QC.variant (1 :: Int) . QC.coarbitrary x + +instance QC.Function a => QC.Function (Lifted a) where + function = QC.functionMap fromLifted toLifted where + fromLifted = foldLifted Nothing Just + toLifted = maybe Bottom Lift diff --git a/src/Algebra/Lattice/M2.hs b/src/Algebra/Lattice/M2.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/M2.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.M2 +-- Copyright : (C) 2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.M2 ( + M2 (..), + toSetBool, + fromSetBool, + ) where + +import Prelude () +import Prelude.Compat + +import Control.DeepSeq (NFData (..)) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic) + +import qualified Test.QuickCheck as QC + +import Algebra.Heyting +import Algebra.Lattice +import Algebra.PartialOrd + +import Data.Set (Set) +import qualified Data.Set as Set + +-- | \(M_2\) is isomorphic to \(\mathcal{P}\{\mathbb{B}\}\), i.e. powerset of 'Bool'. +-- +-- <> +-- +data M2 = M2o | M2a | M2b | M2i + deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic) + +instance PartialOrd M2 where + M2o `leq` _ = True + _ `leq` M2i = True + M2a `leq` M2a = True + M2b `leq` M2b = True + _ `leq` _ = False + +instance Lattice M2 where + M2o \/ y = y + M2i \/ _ = M2i + x \/ M2o = x + _ \/ M2i = M2i + M2a \/ M2a = M2a + M2b \/ M2b = M2b + _ \/ _ = M2i + + M2o /\ _ = M2o + M2i /\ y = y + _ /\ M2o = M2o + x /\ M2i = x + M2a /\ M2a = M2a + M2b /\ M2b = M2b + _ /\ _ = M2o + +instance BoundedJoinSemiLattice M2 where + bottom = M2o + +instance BoundedMeetSemiLattice M2 where + top = M2i + +instance Heyting M2 where + M2o ==> _ = M2i + M2i ==> x = x + + M2a ==> M2o = M2b + M2a ==> M2a = M2i + M2a ==> M2b = M2b + M2a ==> M2i = M2i + + M2b ==> M2o = M2a + M2b ==> M2a = M2a + M2b ==> M2b = M2i + M2b ==> M2i = M2i + + neg M2o = M2i + neg M2a = M2b + neg M2b = M2a + neg M2i = M2o + +toSetBool :: M2 -> Set Bool +toSetBool M2o = mempty +toSetBool M2a = Set.singleton False +toSetBool M2b = Set.singleton True +toSetBool M2i = Set.fromList [True, False] + +fromSetBool :: Set Bool -> M2 +fromSetBool x = case Set.toList x of + [False,True] -> M2i + [False] -> M2a + [True] -> M2b + _ -> M2o + +instance QC.Arbitrary M2 where + arbitrary = QC.arbitraryBoundedEnum + shrink x | x == minBound = [] + | otherwise = [minBound .. pred x] + +instance QC.CoArbitrary M2 where + coarbitrary = QC.coarbitraryEnum + +instance QC.Function M2 where + function = QC.functionBoundedEnum + +instance Universe M2 where universe = [minBound .. maxBound] +instance Finite M2 where cardinality = 4 + +instance NFData M2 where + rnf x = x `seq` () + +instance Hashable M2 where + hashWithSalt salt = hashWithSalt salt . fromEnum diff --git a/src/Algebra/Lattice/M3.hs b/src/Algebra/Lattice/M3.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/M3.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.M3 +-- Copyright : (C) 2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.M3 ( + M3 (..), + ) where + +import Prelude () +import Prelude.Compat + +import Control.DeepSeq (NFData (..)) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic) + +import qualified Test.QuickCheck as QC + +import Algebra.Lattice +import Algebra.PartialOrd + +-- | \(M_3\), is smallest non-distributive, yet modular lattice. +-- +-- <> +-- +data M3 = M3o | M3a | M3b | M3c | M3i + deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic) + +instance PartialOrd M3 where + M3o `leq` _ = True + _ `leq` M3i = True + M3a `leq` M3a = True + M3b `leq` M3b = True + M3c `leq` M3c = True + _ `leq` _ = False + +instance Lattice M3 where + M3o \/ y = y + M3i \/ _ = M3i + x \/ M3o = x + _ \/ M3i = M3i + M3a \/ M3a = M3a + M3b \/ M3b = M3b + M3c \/ M3c = M3c + _ \/ _ = M3i + + M3o /\ _ = M3o + M3i /\ y = y + _ /\ M3o = M3o + x /\ M3i = x + M3a /\ M3a = M3a + M3b /\ M3b = M3b + M3c /\ M3c = M3c + _ /\ _ = M3o + +instance BoundedJoinSemiLattice M3 where + bottom = M3o + +instance BoundedMeetSemiLattice M3 where + top = M3i + +instance QC.Arbitrary M3 where + arbitrary = QC.arbitraryBoundedEnum + shrink x | x == minBound = [] + | otherwise = [minBound .. pred x] + +instance QC.CoArbitrary M3 where + coarbitrary = QC.coarbitraryEnum + +instance QC.Function M3 where + function = QC.functionBoundedEnum + +instance Universe M3 where universe = [minBound .. maxBound] +instance Finite M3 where cardinality = 5 + +instance NFData M3 where + rnf x = x `seq` () + +instance Hashable M3 where + hashWithSalt salt = hashWithSalt salt . fromEnum diff --git a/src/Algebra/Lattice/N5.hs b/src/Algebra/Lattice/N5.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/N5.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.N5 +-- Copyright : (C) 2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.N5 ( + N5 (..), + ) where + +import Prelude () +import Prelude.Compat + +import Control.DeepSeq (NFData (..)) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic) + +import qualified Test.QuickCheck as QC + +import Algebra.Lattice +import Algebra.PartialOrd + +-- | \(N_5\), is smallest non-modular (and non-distributive) lattice. +-- +-- <> +-- +data N5 = N5o | N5a | N5b | N5c | N5i + deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic) + +instance PartialOrd N5 where + N5o `leq` _ = True + _ `leq` N5i = True + N5a `leq` N5a = True + N5b `leq` N5a = True + N5b `leq` N5b = True + N5c `leq` N5c = True + _ `leq` _ = False + +instance Lattice N5 where + N5o \/ y = y + N5i \/ _ = N5i + x \/ N5o = x + _ \/ N5i = N5i + N5a \/ N5a = N5a + N5a \/ N5b = N5a + N5b \/ N5a = N5a + N5b \/ N5b = N5b + N5c \/ N5c = N5c + _ \/ _ = N5i + + N5o /\ _ = N5o + N5i /\ y = y + _ /\ N5o = N5o + x /\ N5i = x + N5a /\ N5a = N5a + N5b /\ N5b = N5b + N5a /\ N5b = N5b + N5b /\ N5a = N5b + N5c /\ N5c = N5c + _ /\ _ = N5o + +instance BoundedJoinSemiLattice N5 where + bottom = N5o + +instance BoundedMeetSemiLattice N5 where + top = N5i + +instance QC.Arbitrary N5 where + arbitrary = QC.arbitraryBoundedEnum + shrink x | x == minBound = [] + | otherwise = [minBound .. pred x] + +instance QC.CoArbitrary N5 where + coarbitrary = QC.coarbitraryEnum + +instance QC.Function N5 where + function = QC.functionBoundedEnum + +instance Universe N5 where universe = [minBound .. maxBound] +instance Finite N5 where cardinality = 5 + +instance NFData N5 where + rnf x = x `seq` () + +instance Hashable N5 where + hashWithSalt salt = hashWithSalt salt . fromEnum diff --git a/src/Algebra/Lattice/Op.hs b/src/Algebra/Lattice/Op.hs --- a/src/Algebra/Lattice/Op.hs +++ b/src/Algebra/Lattice/Op.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} @@ -6,15 +5,11 @@ {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else {-# LANGUAGE Safe #-} -#endif ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Op --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -30,12 +25,15 @@ import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Op -- @@ -43,12 +41,13 @@ -- | The opposite lattice of a given lattice. That is, switch -- meets and joins. newtype Op a = Op { getOp :: a } - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 + deriving ( Eq, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable , Generic1 -#endif ) +instance Ord a => Ord (Op a) where + compare (Op a) (Op b) = compare b a + instance Applicative Op where pure = return (<*>) = ap @@ -62,22 +61,31 @@ instance Hashable a => Hashable (Op a) -instance MeetSemiLattice a => JoinSemiLattice (Op a) where +instance Lattice a => Lattice (Op a) where Op x \/ Op y = Op (x /\ y) - -instance JoinSemiLattice a => MeetSemiLattice (Op a) where Op x /\ Op y = Op (x \/ y) -instance Lattice a => Lattice (Op a) where - instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where bottom = Op top instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where top = Op bottom -instance BoundedLattice a => BoundedLattice (Op a) where - instance PartialOrd a => PartialOrd (Op a) where Op a `leq` Op b = b `leq` a -- Note swap. comparable (Op a) (Op b) = comparable a b + +instance Universe a => Universe (Op a) where + universe = map Op universe +instance Finite a => Finite (Op a) where + universeF = map Op universeF + +instance QC.Arbitrary a => QC.Arbitrary (Op a) where + arbitrary = Op <$> QC.arbitrary + shrink = QC.shrinkMap getOp Op + +instance QC.CoArbitrary a => QC.CoArbitrary (Op a) where + coarbitrary = QC.coarbitrary . getOp + +instance QC.Function a => QC.Function (Op a) where + function = QC.functionMap getOp Op diff --git a/src/Algebra/Lattice/Ordered.hs b/src/Algebra/Lattice/Ordered.hs --- a/src/Algebra/Lattice/Ordered.hs +++ b/src/Algebra/Lattice/Ordered.hs @@ -1,20 +1,16 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ < 709 -{-# LANGUAGE Trustworthy #-} -#else -{-# LANGUAGE Safe #-} -#endif +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} ---------------------------------------------------------------------------- -- | -- Module : Algebra.Lattice.Ordered --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -27,26 +23,29 @@ import Prelude () import Prelude.Compat +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd -import Control.DeepSeq -import Control.Monad -import Data.Data -import Data.Hashable -import GHC.Generics +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) +import qualified Test.QuickCheck as QC + -- -- Ordered -- -- | A total order gives rise to a lattice. Join is --- max, meet is min. +-- 'max', meet is 'min'. newtype Ordered a = Ordered { getOrdered :: a } deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable -#if __GLASGOW_HASKELL__ >= 706 , Generic1 -#endif ) instance Applicative Ordered where @@ -62,22 +61,40 @@ instance Hashable a => Hashable (Ordered a) -instance Ord a => JoinSemiLattice (Ordered a) where +instance Ord a => Lattice (Ordered a) where Ordered x \/ Ordered y = Ordered (max x y) - -instance Ord a => MeetSemiLattice (Ordered a) where Ordered x /\ Ordered y = Ordered (min x y) -instance Ord a => Lattice (Ordered a) where - instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where bottom = Ordered minBound instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where top = Ordered maxBound -instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where +-- | This is interesting logic, as it satisfies both de Morgan laws; +-- but isn't Boolean: i.e. law of exluded middle doesn't hold. +-- +-- Negation "smashes" value into 'minBound' or 'maxBound'. +instance (Ord a, Bounded a) => Heyting (Ordered a) where + x ==> y | x > y = y + | otherwise = top instance Ord a => PartialOrd (Ordered a) where leq = (<=) comparable _ _ = True + +instance Universe a => Universe (Ordered a) where + universe = map Ordered universe +instance Finite a => Finite (Ordered a) where + universeF = map Ordered universeF + cardinality = retag (cardinality :: Tagged a Natural) + +instance QC.Arbitrary a => QC.Arbitrary (Ordered a) where + arbitrary = Ordered <$> QC.arbitrary + shrink = QC.shrinkMap Ordered getOrdered + +instance QC.CoArbitrary a => QC.CoArbitrary (Ordered a) where + coarbitrary = QC.coarbitrary . getOrdered + +instance QC.Function a => QC.Function (Ordered a) where + function = QC.functionMap getOrdered Ordered diff --git a/src/Algebra/Lattice/Unicode.hs b/src/Algebra/Lattice/Unicode.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Unicode.hs @@ -0,0 +1,29 @@ +-- | This module provides Unicode variants of the operators. +-- +-- Unfortunately, ⊤, ⊥, and ¬ don't fit into Haskell lexical structure well. +-- +module Algebra.Lattice.Unicode where + +import Algebra.Heyting +import Algebra.Lattice + +infixr 6 ∧ +infixr 5 ∨ +infixr 4 ⟹ +infix 4 ⟺ + +-- | Meet, alias for '/\'. +(∧) :: Lattice a => a -> a -> a +(∧) = (/\) + +-- | Join, alias for '\/'. +(∨) :: Lattice a => a -> a -> a +(∨) = (\/) + +-- | Implication, alias for '==>'. +(⟹) :: Heyting a => a -> a -> a +(⟹) = (==>) + +-- | Equivalence, alias for '<=>'. +(⟺) :: Heyting a => a -> a -> a +(⟺) = (<=>) diff --git a/src/Algebra/Lattice/Wide.hs b/src/Algebra/Lattice/Wide.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Wide.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Wide +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Wide ( + Wide(..) + ) where + +import Prelude () +import Prelude.Compat + +import Algebra.Lattice +import Algebra.PartialOrd + +import Control.DeepSeq (NFData (..)) +import Control.Monad (ap) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged, retag) +import GHC.Generics (Generic, Generic1) + +import qualified Test.QuickCheck as QC + +-- +-- Wide +-- + +-- | Graft a distinct top and bottom onto any type. +-- The 'Top' is identity for '/\' and the absorbing element for '\/'. +-- The 'Bottom' is the identity for '\/' and and the absorbing element for '/\'. +-- Two 'Middle' values join to top, unless they are equal. +-- +-- <> +-- +data Wide a + = Top + | Middle a + | Bottom + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Wide where + pure = return + (<*>) = ap + +instance Monad Wide where + return = Middle + Top >>= _ = Top + Bottom >>= _ = Bottom + Middle x >>= f = f x + +instance NFData a => NFData (Wide a) where + rnf Top = () + rnf Bottom = () + rnf (Middle a) = rnf a + +instance Hashable a => Hashable (Wide a) + +instance Eq a => Lattice (Wide a) where + Top \/ _ = Top + Bottom \/ x = x + Middle _ \/ Top = Top + Middle x \/ Bottom = Middle x + Middle x \/ Middle y = if x == y then Middle x else Top + + Bottom /\ _ = Bottom + Top /\ x = x + Middle _ /\ Bottom = Bottom + Middle x /\ Top = Middle x + Middle x /\ Middle y = if x == y then Middle x else Bottom + +instance Eq a => BoundedJoinSemiLattice (Wide a) where + bottom = Bottom + +instance Eq a => BoundedMeetSemiLattice (Wide a) where + top = Top + +instance Eq a => PartialOrd (Wide a) where + leq Bottom _ = True + leq Top Bottom = False + leq Top (Middle _) = False + leq Top Top = True + leq (Middle _) Bottom = False + leq (Middle _) Top = True + leq (Middle x) (Middle y) = x == y + + comparable Bottom _ = True + comparable Top _ = True + comparable (Middle _) Bottom = True + comparable (Middle _) Top = True + comparable (Middle x) (Middle y) = x == y + +instance Universe a => Universe (Wide a) where + universe = Top : Bottom : map Middle universe +instance Finite a => Finite (Wide a) where + universeF = Top : Bottom : map Middle universeF + cardinality = fmap (2 +) (retag (cardinality :: Tagged a Natural)) + +instance QC.Arbitrary a => QC.Arbitrary (Wide a) where + arbitrary = QC.frequency + [ (1, pure Top) + , (1, pure Bottom) + , (9, Middle <$> QC.arbitrary) + ] + + shrink Top = [] + shrink Bottom = [] + shrink (Middle x) = Top : Bottom : map Middle (QC.shrink x) + +instance QC.CoArbitrary a => QC.CoArbitrary (Wide a) where + coarbitrary Top = QC.variant (0 :: Int) + coarbitrary Bottom = QC.variant (0 :: Int) + coarbitrary (Middle x) = QC.variant (0 :: Int) . QC.coarbitrary x + +instance QC.Function a => QC.Function (Wide a) where + function = QC.functionMap fromWide toWide where + fromWide Top = Left True + fromWide Bottom = Left False + fromWide (Middle x) = Right x + + toWide (Left True) = Top + toWide (Left False) = Bottom + toWide (Right x) = Middle x diff --git a/src/Algebra/Lattice/ZeroHalfOne.hs b/src/Algebra/Lattice/ZeroHalfOne.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/ZeroHalfOne.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.ZeroHalfOne +-- Copyright : (C) 2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.ZeroHalfOne ( + ZeroHalfOne (..), + ) where + +import Prelude () +import Prelude.Compat + +import Control.DeepSeq (NFData (..)) +import Data.Data (Data, Typeable) +import Data.Hashable (Hashable (..)) +import Data.Universe.Class (Finite (..), Universe (..)) +import GHC.Generics (Generic) + +import qualified Test.QuickCheck as QC + +import Algebra.Heyting +import Algebra.Lattice +import Algebra.PartialOrd + +-- | The simplest Heyting algebra that is not already a Boolean algebra is the +-- totally ordered set \(\{ 0, \frac{1}{2}, 1 \}\). +-- +data ZeroHalfOne = Zero | Half | One + deriving (Eq, Ord, Read, Show, Enum, Bounded, Typeable, Data, Generic) + +instance PartialOrd ZeroHalfOne where + leq = (<=) + +instance Lattice ZeroHalfOne where + (\/) = max + (/\) = min + +instance BoundedJoinSemiLattice ZeroHalfOne where + bottom = Zero + +instance BoundedMeetSemiLattice ZeroHalfOne where + top = One + +-- | Not boolean: @'neg' 'Half' '\/' 'Half' = 'Half' /= 'One'@ +instance Heyting ZeroHalfOne where + Zero ==> _ = One + One ==> x = x + Half ==> Zero = Zero + Half ==> _ = One + + neg Zero = One + neg One = Zero + neg Half = Zero + +instance QC.Arbitrary ZeroHalfOne where + arbitrary = QC.arbitraryBoundedEnum + shrink x | x == minBound = [] + | otherwise = [minBound .. pred x] + +instance QC.CoArbitrary ZeroHalfOne where + coarbitrary = QC.coarbitraryEnum + +instance QC.Function ZeroHalfOne where + function = QC.functionBoundedEnum + +instance Universe ZeroHalfOne where universe = [minBound .. maxBound] +instance Finite ZeroHalfOne where cardinality = 3 + +instance NFData ZeroHalfOne where + rnf x = x `seq` () + +instance Hashable ZeroHalfOne where + hashWithSalt salt = hashWithSalt salt . fromEnum diff --git a/src/Algebra/PartialOrd.hs b/src/Algebra/PartialOrd.hs --- a/src/Algebra/PartialOrd.hs +++ b/src/Algebra/PartialOrd.hs @@ -2,7 +2,7 @@ ---------------------------------------------------------------------------- -- | -- Module : Algebra.PartialOrd --- Copyright : (C) 2010-2015 Maximilian Bolingbroke +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus -- License : BSD-3-Clause (see the file LICENSE) -- -- Maintainer : Oleg Grenrus @@ -24,9 +24,9 @@ import qualified Data.HashSet as HS import qualified Data.IntMap as IM import qualified Data.IntSet as IS -import qualified Data.List as L +import qualified Data.List.Compat as L import qualified Data.Map as M -import Data.Monoid (All (..)) +import Data.Monoid (All (..), Any (..)) import qualified Data.Set as S import Data.Void (Void) @@ -88,14 +88,17 @@ -- | Whether two elements are ordered with respect to the relation. A -- default implementation is given by -- - -- > comparable x y = leq x y || leq y x + -- @ + -- 'comparable' x y = 'leq' x y '||' 'leq' y x + -- @ comparable :: a -> a -> Bool comparable x y = leq x y || leq y x --- | The equality relation induced by the partial-order structure. It must obey --- the laws +-- | The equality relation induced by the partial-order structure. It satisfies +-- the laws of an equivalence relation: -- @ -- Reflexive: a == a +-- Symmetric: a == b ==> b == a -- Transitive: a == b && b == c ==> a == c -- @ partialOrdEq :: PartialOrd a => a -> a -> Bool @@ -104,12 +107,22 @@ instance PartialOrd () where leq _ _ = True +-- | @since 2 +instance PartialOrd Bool where + leq = (<=) + +instance PartialOrd Any where + leq = (<=) + +instance PartialOrd All where + leq = (<=) + instance PartialOrd Void where leq _ _ = True --- | @'leq' = 'Data.List.isInfixOf'@. +-- | @'leq' = 'Data.List.isSequenceOf'@. instance Eq a => PartialOrd [a] where - leq = L.isInfixOf + leq = L.isSubsequenceOf instance Ord a => PartialOrd (S.Set a) where leq = S.isSubsetOf diff --git a/src/Algebra/PartialOrd/Instances.hs b/src/Algebra/PartialOrd/Instances.hs --- a/src/Algebra/PartialOrd/Instances.hs +++ b/src/Algebra/PartialOrd/Instances.hs @@ -14,9 +14,15 @@ module Algebra.PartialOrd.Instances () where import Algebra.PartialOrd (PartialOrd (..)) +import Data.Monoid (Endo (..)) import Data.Universe.Class (Finite (..)) import Data.Universe.Instances.Eq () -- | @Eq (k -> v)@ is from 'Data.Universe.Instances.Eq' instance (PartialOrd v, Finite k) => PartialOrd (k -> v) where f `leq` g = all (\k -> f k `leq` g k) universeF + +instance (PartialOrd v, Finite v) => PartialOrd (Endo v) where + Endo f `leq` Endo g = f `leq` g + + diff --git a/test/Tests.hs b/test/Tests.hs --- a/test/Tests.hs +++ b/test/Tests.hs @@ -1,39 +1,62 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE KindSignatures #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} module Main (main) where import Prelude () import Prelude.Compat -import Data.Maybe (listToMaybe, isJust) -import Data.Semigroup ((<>)) -import Control.Monad (ap, guard) +import Control.Monad (ap, guard) +import Data.Int (Int8) +import Data.List (genericLength, nub) +import Data.Maybe (isJust, listToMaybe) +import Data.Semigroup (All, Any, Endo (..), (<>)) +import Data.Typeable (Typeable, typeOf) +import Data.Universe.Class (Finite (..), Universe (..)) +import Data.Universe.Helpers (Natural, Tagged (..)) +import Test.QuickCheck + (Arbitrary (..), Property, discard, label, (=/=), (===)) import Test.QuickCheck.Function import Test.Tasty -import Test.Tasty.QuickCheck as QC +import Test.Tasty.QuickCheck (testProperty) +import qualified Test.QuickCheck as QC + +import Algebra.Heyting import Algebra.Lattice import Algebra.PartialOrd -import qualified Algebra.Lattice.Divisibility as Div -import qualified Algebra.Lattice.Dropped as D -import qualified Algebra.Lattice.Levitated as L +import Algebra.Lattice.M2 (M2 (..)) +import Algebra.Lattice.M3 (M3 (..)) +import Algebra.Lattice.N5 (N5 (..)) +import Algebra.Lattice.ZeroHalfOne (ZeroHalfOne (..)) + +import qualified Algebra.Heyting.Free as HF +import qualified Algebra.Lattice.Divisibility as Div +import qualified Algebra.Lattice.Dropped as D +import qualified Algebra.Lattice.Free as F +import qualified Algebra.Lattice.Levitated as L import qualified Algebra.Lattice.Lexicographic as LO -import qualified Algebra.Lattice.Lifted as U -import qualified Algebra.Lattice.Op as Op -import qualified Algebra.Lattice.Ordered as O +import qualified Algebra.Lattice.Lifted as U +import qualified Algebra.Lattice.Op as Op +import qualified Algebra.Lattice.Ordered as O +import qualified Algebra.Lattice.Wide as W -import Data.IntMap (IntMap) -import Data.IntSet (IntSet) -import Data.Map (Map) -import Data.Set (Set) import Data.HashMap.Lazy (HashMap) -import Data.HashSet (HashSet) +import Data.HashSet (HashSet) +import Data.IntMap (IntMap) +import Data.IntSet (IntSet) +import Data.Map (Map) +import Data.Set (Set) -import Data.Universe.Instances.Base () +import Algebra.PartialOrd.Instances () +import Data.Universe.Instances.Eq () +import Data.Universe.Instances.Ord () +import Data.Universe.Instances.Show () import Test.QuickCheck.Instances () -- For old GHC to work @@ -45,29 +68,79 @@ tests :: TestTree tests = testGroup "Tests" - [ latticeLaws "M3" False (Proxy :: Proxy M3) -- non distributive lattice! - , latticeLaws "M2" True (Proxy :: Proxy M2) -- M2 - , latticeLaws "Map" True (Proxy :: Proxy (Map Int (O.Ordered Int))) - , latticeLaws "IntMap" True (Proxy :: Proxy (IntMap (O.Ordered Int))) - , latticeLaws "HashMap" True (Proxy :: Proxy (HashMap Int (O.Ordered Int))) - , latticeLaws "Set" True (Proxy :: Proxy (Set Int)) - , latticeLaws "IntSet" True (Proxy :: Proxy IntSet) - , latticeLaws "HashSet" True (Proxy :: Proxy (HashSet Int)) - , latticeLaws "Ordered" True (Proxy :: Proxy (O.Ordered Int)) - , latticeLaws "Divisibility" True (Proxy :: Proxy (Div.Divisibility Int)) - , latticeLaws "LexOrdered" True (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int))) - , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool))) - , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive! - , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $ - isJust searchM3LexM2 - , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped) - , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated) - , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool)) - , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted) - , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op) - , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered) - ] + [ allLatticeLaws (LBounded Partial Modular) (Proxy :: Proxy M3) -- non distributive lattice! + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy M2) -- M2 + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (Set Bool)) -- isomorphic to M2 + , allLatticeLaws (LBounded Partial NonModular) (Proxy :: Proxy N5) + , allLatticeLaws (LHeyting Total IsBoolean) (Proxy :: Proxy ()) + , allLatticeLaws (LHeyting Total IsBoolean) (Proxy :: Proxy Bool) + , allLatticeLaws (LHeyting Total DeMorgan) (Proxy :: Proxy ZeroHalfOne) + , allLatticeLaws (LNormal Partial Distributive) (Proxy :: Proxy (Map Int (O.Ordered Int))) + , allLatticeLaws (LNormal Partial Distributive) (Proxy :: Proxy (IntMap (O.Ordered Int))) + , allLatticeLaws (LNormal Partial Distributive) (Proxy :: Proxy (HashMap Int (O.Ordered Int))) + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (Set Int8)) + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (HashSet Int8)) + , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (Set Int)) + , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy IntSet) + , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (HashSet Int)) + , allLatticeLaws (LHeyting Total DeMorgan) (Proxy :: Proxy (O.Ordered Int8)) + , allLatticeLaws (LBoundedJoin Partial Distributive) (Proxy :: Proxy (Div.Divisibility Int)) + , allLatticeLaws (LNormal Total Distributive) (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int))) + , allLatticeLaws (LBounded Partial Modular) (Proxy :: Proxy (W.Wide Int)) + , allLatticeLaws (LBounded Partial NonModular) (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool))) + , allLatticeLaws (LBounded Partial NonModular) (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive! + , allLatticeLaws LNotLattice (Proxy :: Proxy String) + + , allLatticeLaws (LHeyting Total IsBoolean) (Proxy :: Proxy All) + , allLatticeLaws (LHeyting Total IsBoolean) (Proxy :: Proxy Any) + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (Endo Bool)) -- note: it's partial! + , allLatticeLaws (LBounded Partial Modular) (Proxy :: Proxy (Endo M3)) + + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (Int8 -> Bool)) + , allLatticeLaws (LHeyting Partial IsBoolean) (Proxy :: Proxy (Int8 -> M2)) + , allLatticeLaws (LBounded Partial Modular) (Proxy :: Proxy (Int8 -> M3)) + + , allLatticeLaws (LNormal Partial Distributive) (Proxy :: Proxy (F.Free Int8)) + , allLatticeLaws (LHeyting Partial NonBoolean) (Proxy :: Proxy (HF.Free Var)) + + , allLatticeLaws (LBoundedMeet Total Distributive) (Proxy :: Proxy (D.Dropped (O.Ordered Int))) + , allLatticeLaws (LBounded Total Distributive) (Proxy :: Proxy (L.Levitated (O.Ordered Int))) + , allLatticeLaws (LBoundedJoin Total Distributive) (Proxy :: Proxy (U.Lifted (O.Ordered Int))) + , allLatticeLaws (LNormal Total Distributive ) (Proxy :: Proxy (Op.Op (O.Ordered Int))) + + , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $ + isJust searchM3LexM2 + + , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped) + , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated) + , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool)) + , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted) + , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op) + , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered) + , monadLaws "Wide" (Proxy1 :: Proxy1 W.Wide) + , monadLaws "Heyting.Free" (Proxy1 :: Proxy1 HF.Free) + + , finiteLaws (Proxy :: Proxy M2) + , finiteLaws (Proxy :: Proxy M3) + , finiteLaws (Proxy :: Proxy N5) + , finiteLaws (Proxy :: Proxy ZeroHalfOne) + + , finiteLaws (Proxy :: Proxy OInt8) + , finiteLaws (Proxy :: Proxy (Div.Divisibility Int8)) + , finiteLaws (Proxy :: Proxy (W.Wide Int8)) + , finiteLaws (Proxy :: Proxy (D.Dropped OInt8)) + , finiteLaws (Proxy :: Proxy (L.Levitated OInt8)) + , finiteLaws (Proxy :: Proxy (U.Lifted OInt8)) + , finiteLaws (Proxy :: Proxy (LO.Lexicographic OInt8 OInt8)) + ] + +type OInt8 = O.Ordered Int8 + +------------------------------------------------------------------------------- +-- Monad laws +------------------------------------------------------------------------------- + monadLaws :: forall (m :: * -> *). ( Monad m #if !MIN_VERSION_base(4, 8, 0) , Applicative m @@ -81,12 +154,12 @@ -> Proxy1 m -> TestTree monadLaws name _ = testGroup ("Monad laws: " <> name) - [ QC.testProperty "left identity" leftIdentityProp - , QC.testProperty "right identity" rightIdentityProp - , QC.testProperty "composition" compositionProp - , QC.testProperty "Applicative pure" pureProp - , QC.testProperty "Applicative ap" apProp - ] + [ testProperty "left identity" leftIdentityProp + , testProperty "right identity" rightIdentityProp + , testProperty "composition" compositionProp + , testProperty "Applicative pure" pureProp + , testProperty "Applicative ap" apProp + ] where leftIdentityProp :: Int -> Fun Int (m Int) -> Property leftIdentityProp x (Fun _ k) = (return x >>= k) === k x @@ -105,33 +178,148 @@ where f' = apply <$> f ------------------------------------------------------------------------------- --- Lattice distributive +-- Partial ord laws ------------------------------------------------------------------------------- -latticeLaws - :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a) - => String - -> Bool -- ^ distributive +data IsTotal a where + Total :: Ord a => IsTotal a + Partial :: PartialOrd a => IsTotal a + +partialOrdLaws + :: forall a. (Eq a, Show a, Arbitrary a, PartialOrd a) + => IsTotal a -> Proxy a -> TestTree -latticeLaws name distr _ = testGroup ("Lattice laws: " <> name) $ - [ QC.testProperty "leq = joinLeq" joinLeqProp - , QC.testProperty "leq = meetLeq" meetLeqProp - , QC.testProperty "meet is lower bound" meetLower - , QC.testProperty "join is upper bound" joinUpper - , QC.testProperty "meet commutes" meetComm - , QC.testProperty "join commute" joinComm - , QC.testProperty "meet associative" meetAssoc - , QC.testProperty "join associative" joinAssoc - , QC.testProperty "absorbtion 1" meetAbsorb - , QC.testProperty "absorbtion 2" joinAbsorb - , QC.testProperty "meet idempontent" meetIdemp - , QC.testProperty "join idempontent" joinIdemp - , QC.testProperty "comparableDef" comparableDef - ] ++ if not distr then [] else - -- Not all lattices are distributive! - [ QC.testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp - , QC.testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop +partialOrdLaws total _ = testGroup "PartialOrd" $ + [ testProperty "reflexive" reflProp + , testProperty "anti-symmetric" antiSymProp + , testProperty "transitive" transitiveProp + ] ++ case total of + Partial -> [] + Total -> + [ testProperty "total" totalProp + , testProperty "leq/compare agree" leqCompareProp + ] + where + reflProp :: a -> Property + reflProp x = QC.property $ leq x x + + antiSymProp :: a -> a -> Property + antiSymProp x y + | leq x y && leq y x = label "same" $ x === y + | otherwise = label "diff" $ x =/= y + + transitiveProp :: a -> a -> a -> Property + transitiveProp x y z = case p of + [] -> label "non-related" $ QC.property True + ((x', _, z') : _) -> label "related" $ QC.property $ leq x' z' + where + p = [ (x', y', z') + | (x', y', z') <- [(x,y,z),(y,x,z),(z,y,x),(y,z,x),(z,x,y),(x,z,y)] + , leq x' y' + , leq y' z' + ] + + totalProp :: a -> a -> Property + totalProp x y = QC.property $ leq x y || leq y x + + leqCompareProp :: Ord a => a -> a -> Property + leqCompareProp x y = agree (leq x y) (leq y x) (compare x y) + where + agree True True = (=== EQ) + agree True False = (=== LT) + agree False True = (=== GT) + agree False False = discard + +------------------------------------------------------------------------------- +-- Lattice +------------------------------------------------------------------------------- + +-- | Lattice Kind +data LKind a where + LNotLattice :: LKind a + LNormal :: Lattice a => IsTotal a -> Distr -> LKind a + LBoundedMeet :: BoundedMeetSemiLattice a => IsTotal a -> Distr -> LKind a + LBoundedJoin :: BoundedJoinSemiLattice a => IsTotal a -> Distr -> LKind a + LBounded :: BoundedLattice a => IsTotal a -> Distr -> LKind a + LHeyting :: Heyting a => IsTotal a -> IsBoolean -> LKind a + +data Distr + = NonModular + | Modular + | Distributive + deriving (Eq, Ord) + +data IsBoolean + = NonBoolean + | DeMorgan + | IsBoolean + deriving (Eq, Ord) + +allLatticeLaws + :: forall a. (Eq a, Show a, Arbitrary a, Typeable a, PartialOrd a) + => LKind a + -> Proxy a + -> TestTree +allLatticeLaws ki pr = case ki of + LNotLattice -> testGroup name $ + [partialOrdLaws Partial pr] + LNormal t d -> testGroup name $ + partialOrdLaws t pr : allLatticeLaws' d pr + LBoundedMeet t d -> testGroup name $ + partialOrdLaws t pr : allLatticeLaws' d pr ++ + [ boundedMeetLaws pr ] + LBoundedJoin t d -> testGroup name $ + partialOrdLaws t pr : allLatticeLaws' d pr ++ + [ boundedJoinLaws pr ] + LBounded t d -> testGroup name $ + partialOrdLaws t pr : allLatticeLaws' d pr ++ + [ boundedMeetLaws pr + , boundedJoinLaws pr + ] + LHeyting t b -> testGroup name $ + partialOrdLaws t pr : allLatticeLaws' Distributive pr ++ + [ boundedMeetLaws pr + , boundedJoinLaws pr + , heytingLaws pr + ] ++ + [ deMorganLaws pr | b >= DeMorgan ] ++ + [ booleanLaws pr | b >= IsBoolean ] + where + name = show (typeOf (undefined :: a)) + +allLatticeLaws' + :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a) + => Distr + -> Proxy a + -> [TestTree] +allLatticeLaws' distr pr = + [ latticeLaws pr ] ++ + [ modularLaws pr | distr >= Modular ] ++ + [ distributiveLaws pr | distr >= Distributive ] + +------------------------------------------------------------------------------- +-- Lattice laws +------------------------------------------------------------------------------- + +latticeLaws + :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a) + => Proxy a + -> TestTree +latticeLaws _ = testGroup "Lattice" + [ testProperty "leq = joinLeq" joinLeqProp + , testProperty "leq = meetLeq" meetLeqProp + , testProperty "meet is lower bound" meetLower + , testProperty "join is upper bound" joinUpper + , testProperty "meet commutes" meetComm + , testProperty "join commute" joinComm + , testProperty "meet associative" meetAssoc + , testProperty "join associative" joinAssoc + , testProperty "absorbtion 1" meetAbsorb + , testProperty "absorbtion 2" joinAbsorb + , testProperty "meet idempontent" meetIdemp + , testProperty "join idempontent" joinIdemp + , testProperty "comparableDef" comparableDef ] where joinLeqProp :: a -> a -> Property @@ -177,133 +365,257 @@ comparableDef :: a -> a -> Property comparableDef x y = (leq x y || leq y x) === comparable x y +------------------------------------------------------------------------------- +-- Modular +------------------------------------------------------------------------------- + +modularLaws + :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a) + => Proxy a + -> TestTree +modularLaws _ = testGroup "Modular" + [ testProperty "(y ∧ (x ∨ z)) ∨ z = (y ∨ z) ∧ (x ∨ z)" modularProp + ] + where + modularProp :: a -> a -> a -> Property + modularProp x y z = lhs === rhs where + lhs = (y /\ (x \/ z)) \/ z + rhs = (y \/ z) /\ (x \/ z) + +------------------------------------------------------------------------------- +-- Distributive +------------------------------------------------------------------------------- + +distributiveLaws + :: forall a. (Eq a, Show a, Arbitrary a, Lattice a, PartialOrd a) + => Proxy a + -> TestTree +distributiveLaws _ = testGroup "Distributive" + [ testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp + , testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop + ] + where distrProp :: a -> a -> a -> Property - distrProp x y z = lhs === rhs - where + distrProp x y z = lhs === rhs where lhs = x /\ (y \/ z) rhs = (x /\ y) \/ (x /\ z) distr2Prop :: a -> a -> a -> Property - distr2Prop x y z = lhs === rhs - where + distr2Prop x y z = lhs === rhs where lhs = x \/ (y /\ z) rhs = (x \/ y) /\ (x \/ z) ------------------------------------------------------------------------------- --- Orphans +-- Bounded lattice laws ------------------------------------------------------------------------------- -instance Arbitrary a => Arbitrary (D.Dropped a) where - arbitrary = frequency [ (1, pure D.Top) - , (9, D.Drop <$> arbitrary) - ] - -instance Arbitrary a => Arbitrary (U.Lifted a) where - arbitrary = frequency [ (1, pure U.Bottom) - , (9, U.Lift <$> arbitrary) - ] +boundedMeetLaws + :: forall a. (Eq a, Show a, Arbitrary a, BoundedMeetSemiLattice a) + => Proxy a + -> TestTree +boundedMeetLaws _ = testGroup "BoundedMeetSemiLattice" + [ testProperty "top /\\ x = x" identityLeftProp + , testProperty "x /\\ top = x" identityRightProp + , testProperty "top \\/ x = top" annihilationLeftProp + , testProperty "x \\/ top = top" annihilationRightProp + ] + where + identityLeftProp :: a -> Property + identityLeftProp x = lhs === rhs where + lhs = top /\ x + rhs = x -instance Arbitrary a => Arbitrary (L.Levitated a) where - arbitrary = frequency [ (1, pure L.Top) - , (1, pure L.Bottom) - , (9, L.Levitate <$> arbitrary) - ] + identityRightProp :: a -> Property + identityRightProp x = lhs === rhs where + lhs = x /\ top + rhs = x -instance Arbitrary a => Arbitrary (O.Ordered a) where - arbitrary = O.Ordered <$> arbitrary - shrink = map O.Ordered . shrink . O.getOrdered + annihilationLeftProp :: a -> Property + annihilationLeftProp x = lhs === rhs where + lhs = top \/ x + rhs = top -instance (Arbitrary a, Num a, Ord a) => Arbitrary (Div.Divisibility a) where - arbitrary = divisibility <$> arbitrary - shrink d = filter ( Property + annihilationRightProp x = lhs === rhs where + lhs = x \/ top + rhs = top -divisibility :: (Ord a, Num a) => a -> Div.Divisibility a -divisibility x | x < (-1) = Div.Divisibility (abs x) - | x < 1 = Div.Divisibility 1 - | otherwise = Div.Divisibility x +boundedJoinLaws + :: forall a. (Eq a, Show a, Arbitrary a, BoundedJoinSemiLattice a) + => Proxy a + -> TestTree +boundedJoinLaws _ = testGroup "BoundedJoinSemiLattice" + [ testProperty "bottom \\/ x = x" identityLeftProp + , testProperty "x \\/ bottom = x" identityRightProp + , testProperty "bottom /\\ x = bottom" annihilationLeftProp + , testProperty "x /\\ bottom = bottom" annihilationRightProp + ] + where + identityLeftProp :: a -> Property + identityLeftProp x = lhs === rhs where + lhs = bottom \/ x + rhs = x + identityRightProp :: a -> Property + identityRightProp x = lhs === rhs where + lhs = x \/ bottom + rhs = x -instance Arbitrary a => Arbitrary (Op.Op a) where - arbitrary = Op.Op <$> arbitrary + annihilationLeftProp :: a -> Property + annihilationLeftProp x = lhs === rhs where + lhs = bottom /\ x + rhs = bottom -instance (Arbitrary k, Arbitrary v) => Arbitrary (LO.Lexicographic k v) where - arbitrary = uncurry LO.Lexicographic <$> arbitrary - shrink (LO.Lexicographic k v) = uncurry LO.Lexicographic <$> shrink (k, v) + annihilationRightProp :: a -> Property + annihilationRightProp x = lhs === rhs where + lhs = x /\ bottom + rhs = bottom ------------------------------------------------------------------------------- --- Examples +-- Heyting laws ------------------------------------------------------------------------------- --- | Non-distributive lattice -data M3 = M3_0 | M3_a | M3_b | M3_c | M3_1 - deriving (Eq, Ord, Show, Enum, Bounded) +heytingLaws + :: forall a. (Eq a, Show a, Arbitrary a, Heyting a, Typeable a) + => Proxy a + -> TestTree +heytingLaws _ = testGroup "Heyting" + [ testProperty "neg default" negDefaultProp + , testProperty "<=> default" equivDefaultProp + , testProperty "x ==> x = top" idIsTopProp + , testProperty "a /\\ (a ==> b) = a /\\ b" andDomainProp + , testProperty "b /\\ (a ==> b) = b" andCodomainProp + , testProperty "a ==> (b /\\ c) = (a ==> b) /\\ (a ==> c)" implDistrProp + , testProperty "de Morgan 1" deMorganProp1 + , testProperty "weak de Morgan 2" deMorganProp2weak + ] + where + negDefaultProp :: a -> Property + negDefaultProp x = lhs === rhs where + lhs = neg x + rhs = x ==> bottom -instance Arbitrary M3 where - arbitrary = QC.arbitraryBoundedEnum + equivDefaultProp :: a -> a -> Property + equivDefaultProp x y = lhs === rhs where + lhs = x <=> y + rhs = (x ==> y) /\ (y ==> x) -instance PartialOrd M3 where - x `leq` y | x == y = True - M3_0 `leq` _ = True - _ `leq` M3_1 = True - _ `leq` _ = False + idIsTopProp :: a -> Property + idIsTopProp x = lhs === rhs where + lhs = x ==> x + rhs = top -instance JoinSemiLattice M3 where - x \/ M3_0 = x - M3_0 \/ y = y - _ \/ M3_1 = M3_1 - M3_1 \/ _ = M3_1 - x \/ y | x == y = x - | otherwise = M3_1 + andDomainProp :: a -> a -> Property + andDomainProp x y = lhs === rhs where + lhs = x /\ (x ==> y) + rhs = x /\ y -instance MeetSemiLattice M3 where - x /\ M3_1 = x - M3_1 /\ y = y - _ /\ M3_0 = M3_0 - M3_0 /\ _ = M3_0 - x /\ y | x == y = x - | otherwise = M3_0 + andCodomainProp :: a -> a -> Property + andCodomainProp x y = lhs === rhs where + lhs = y /\ (x ==> y) + rhs = y -instance Lattice M3 where + implDistrProp :: a -> a -> a -> Property + implDistrProp x y z + | typeOf (undefined :: a) == typeOf (undefined :: HF.Free Var) + = QC.mapSize (min 16) $ implDistrProp' x y z + | otherwise + = implDistrProp' x y z --- | Set Bool, M2 -data M2 = M2_0 | M2_T | M2_F | M2_1 - deriving (Eq, Ord, Show, Enum, Bounded) + implDistrProp' :: a -> a -> a -> Property + implDistrProp' x y z = lhs === rhs where + lhs = x ==> (y /\ z) + rhs = (x ==> y) /\ (x ==> z) -instance Arbitrary M2 where - arbitrary = QC.arbitraryBoundedEnum + deMorganProp1 :: a -> a -> Property + deMorganProp1 x y = lhs === rhs where + lhs = neg (x \/ y) + rhs = neg x /\ neg y -instance PartialOrd M2 where - x `leq` y | x == y = True - M2_0 `leq` _ = True - _ `leq` M2_1 = True - _ `leq` _ = False + deMorganProp2weak :: a -> a -> Property + deMorganProp2weak x y = lhs === rhs where + lhs = neg (x /\ y) + rhs = neg (neg (neg x \/ neg y)) -instance JoinSemiLattice M2 where - x \/ M2_0 = x - M2_0 \/ y = y - _ \/ M2_1 = M2_1 - M2_1 \/ _ = M2_1 - x \/ y | x == y = x - | otherwise = M2_1 +------------------------------------------------------------------------------- +-- De morgan +------------------------------------------------------------------------------- -instance MeetSemiLattice M2 where - x /\ M2_1 = x - M2_1 /\ y = y - _ /\ M2_0 = M2_0 - M2_0 /\ _ = M2_0 - x /\ y | x == y = x - | otherwise = M2_0 +deMorganLaws + :: forall a. (Eq a, Show a, Arbitrary a, Heyting a) + => Proxy a + -> TestTree +deMorganLaws _ = testGroup "de Morgan" + [ testProperty "de Morgan 2" deMorganProp2 + ] + where + deMorganProp2 :: a -> a -> Property + deMorganProp2 x y = lhs === rhs where + lhs = neg (x /\ y) + rhs = neg x \/ neg y -instance Lattice M2 where +------------------------------------------------------------------------------- +-- Boolean laws +------------------------------------------------------------------------------- -instance BoundedJoinSemiLattice M2 where - bottom = M2_0 +booleanLaws + :: forall a. (Eq a, Show a, Arbitrary a, Heyting a) + => Proxy a + -> TestTree +booleanLaws _ = testGroup "Boolean" + [ testProperty "LEM: neg x \\/ x = top" lemProp + , testProperty "DN: neg (neg x) = x" dnProp + ] + where + lemProp :: a -> Property + lemProp x = lhs === rhs where + lhs = neg x \/ x + rhs = top -instance BoundedMeetSemiLattice M2 where - top = M2_1 + -- every element is regular, i.e. either of following equivalend conditions hold: + -- * neg (neg x) = x + -- * x = neg y, for some y in H -- I don't know example of this + dnProp :: a -> Property + dnProp x = lhs === rhs where + lhs = neg (neg x) + rhs = x -instance BoundedLattice M2 where +------------------------------------------------------------------------------- +-- Universe / Finite laws +------------------------------------------------------------------------------- +finiteLaws + :: forall a. (Eq a, Show a, Arbitrary a, Typeable a, Finite a) + => Proxy a + -> TestTree +finiteLaws _ = testGroup name + [ testProperty "elem x universe" elemProp + , testProperty "length pfx = length (nub pfx)" prefixProp + + , testProperty "elem x universeF" elemFProp + , testProperty "length (filter (== x) universeF) = 1" singleProp + , testProperty "cardinality = Tagged (genericLength universeF)" cardinalityProp + ] + where + name = show (typeOf (undefined :: a)) + + elemProp :: a -> Property + elemProp x = QC.property $ elem x universe + + elemFProp :: a -> Property + elemFProp x = QC.property $ elem x universeF + + prefixProp :: Int -> Property + prefixProp n = + let pfx = take n (universe :: [a]) + in QC.counterexample (show pfx) $ length pfx === length (nub pfx) + + singleProp :: a -> Property + singleProp x = length (filter (== x) universeF) === 1 + + cardinalityProp :: Property + cardinalityProp = cardinality === (Tagged (genericLength (universeF :: [a])) :: Tagged a Natural) + ------------------------------------------------------------------------------- -- Lexicographic M2 search ------------------------------------------------------------------------------- @@ -331,11 +643,11 @@ guard (xc `leq` x1) -- homomorphism - let f M3_0 = x1 - f M3_a = xa - f M3_b = xb - f M3_c = xc - f M3_1 = x1 + let f M3o = x1 + f M3a = xa + f M3b = xb + f M3c = xc + f M3i = x1 ma <- [minBound .. maxBound] mb <- [minBound .. maxBound] @@ -351,3 +663,17 @@ where xs = [ LO.Lexicographic x y | x <- ys, y <- ys ] ys = [minBound .. maxBound] + +------------------------------------------------------------------------------- +-- Variable (for Free) +------------------------------------------------------------------------------- + +-- | The less variables we have, the quicker tests will be :) +data Var = A | B | C | D + deriving (Eq, Ord, Show, Enum, Bounded, Typeable) + +instance Arbitrary Var where + arbitrary = QC.arbitraryBoundedEnum + + shrink A = [] + shrink x = [ minBound .. pred x ] diff --git a/wide.png b/wide.png new file mode 100644 Binary files /dev/null and b/wide.png differ