diff --git a/Algebra/Enumerable.hs b/Algebra/Enumerable.hs deleted file mode 100644 --- a/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 ( - 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/Algebra/Lattice.hs b/Algebra/Lattice.hs deleted file mode 100644 --- a/Algebra/Lattice.hs +++ /dev/null @@ -1,301 +0,0 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- --- In mathematics, a lattice is a partially ordered set in which every --- two elements have a unique supremum (also called a least upper bound --- or @join@) and a unique infimum (also called a greatest lower bound or --- @meet@). --- --- In this module lattices are defined using `meet` and `join` operators, --- as it's constructive one. --- ----------------------------------------------------------------------------- -module Algebra.Lattice ( - -- * Unbounded lattices - JoinSemiLattice(..), MeetSemiLattice(..), Lattice, - joinLeq, joins1, meetLeq, meets1, - - -- * Bounded lattices - BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice, - joins, meets, - - -- * Fixed points of chains in lattices - lfp, lfpFrom, unsafeLfp, - gfp, gfpFrom, unsafeGfp, - ) where - -import Algebra.Enumerable -import qualified Algebra.PartialOrd as PO - -import qualified Data.Set as S -import qualified Data.IntSet as IS -import qualified Data.Map as M -import qualified Data.IntMap as IM - -import Data.Hashable -import qualified Data.HashSet as HS -import qualified Data.HashMap.Lazy as HM - --- | A algebraic structure with element joins: --- --- @ --- Associativity: x `join` (y `join` z) == (x `join` y) `join` z --- Commutativity: x `join` y == y `join` x --- Idempotency: x `join` x == x --- @ -class JoinSemiLattice a where - join :: a -> a -> a - --- | The partial ordering induced by the join-semilattice structure -joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool -joinLeq x y = x `join` y == y - --- | The join of at a list of join-semilattice elements (of length at least one) -joins1 :: JoinSemiLattice a => [a] -> a -joins1 = foldr1 join - --- | A algebraic structure with element meets: --- --- @ --- Associativity: x `meet` (y `meet` z) == (x `meet` y) `meet` z --- Commutativity: x `meet` y == y `meet` x --- Idempotency: x `meet` x == x --- @ -class MeetSemiLattice a where - meet :: a -> a -> a - --- | The partial ordering induced by the meet-semilattice structure -meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool -meetLeq x y = x `meet` y == x - --- | The meet of at a list of meet-semilattice elements (of length at least one) -meets1 :: MeetSemiLattice a => [a] -> a -meets1 = foldr1 meet - --- | The combination of two semi lattices makes a lattice if the absorption law holds: --- see and --- --- @ --- Absorption: a `join` (a `meet` b) == a `meet` (a `join` b) == a --- @ -class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where - --- | A join-semilattice with some element |bottom| that `join` approaches. --- --- @ --- Identity: x `join` bottom == x --- @ -class JoinSemiLattice a => BoundedJoinSemiLattice a where - bottom :: a - --- | The join of a list of join-semilattice elements -joins :: BoundedJoinSemiLattice a => [a] -> a -joins = foldr join bottom - --- | A meet-semilattice with some element |top| that `meet` approaches. --- --- @ --- Identity: x `meet` top == x --- @ -class MeetSemiLattice a => BoundedMeetSemiLattice a where - top :: a - --- | The meet of a list of meet-semilattice elements -meets :: BoundedMeetSemiLattice a => [a] -> a -meets = foldr meet top - - --- | Lattices with both bounds -class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where - - --- --- Sets --- - -instance Ord a => JoinSemiLattice (S.Set a) where - join = S.union - -instance (Ord a, Enumerable a) => MeetSemiLattice (S.Set (Enumerated a)) where - meet = S.intersection - -instance (Ord a, Enumerable a) => Lattice (S.Set (Enumerated a)) where - -instance Ord a => BoundedJoinSemiLattice (S.Set a) where - bottom = S.empty - -instance (Ord a, Enumerable a) => BoundedMeetSemiLattice (S.Set (Enumerated a)) where - top = S.fromList universe - -instance (Ord a, Enumerable a) => BoundedLattice (S.Set (Enumerated a)) where - --- --- IntSets --- - -instance JoinSemiLattice IS.IntSet where - join = IS.union - -instance BoundedJoinSemiLattice IS.IntSet where - bottom = IS.empty - --- --- HashSet --- - -instance (Eq a, Hashable a) => JoinSemiLattice (HS.HashSet a) where - join = HS.union - -instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where - meet = HS.intersection - -instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where - bottom = HS.empty - --- --- Maps --- - -instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where - join = M.unionWith join - -instance (Ord k, Enumerable k, MeetSemiLattice v) => MeetSemiLattice (M.Map (Enumerated k) v) where - meet = M.intersectionWith meet - -instance (Ord k, Enumerable k, Lattice v) => Lattice (M.Map (Enumerated k) v) where - -instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where - bottom = M.empty - -instance (Ord k, Enumerable k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map (Enumerated k) v) where - top = M.fromList (universe `zip` repeat top) - -instance (Ord k, Enumerable k, BoundedLattice v) => BoundedLattice (M.Map (Enumerated k) v) where - --- --- IntMaps --- - -instance JoinSemiLattice v => JoinSemiLattice (IM.IntMap v) where - join = IM.unionWith join - -instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where - bottom = IM.empty - --- --- HashMaps --- - -instance (Eq k, Hashable k) => JoinSemiLattice (HM.HashMap k v) where - join = HM.union - -instance (Eq k, Hashable k) => MeetSemiLattice (HM.HashMap k v) where - meet = HM.intersection - -instance (Eq k, Hashable k) => BoundedJoinSemiLattice (HM.HashMap k v) where - bottom = HM.empty - --- --- Functions --- - -instance JoinSemiLattice v => JoinSemiLattice (k -> v) where - f `join` g = \x -> f x `join` g x - -instance MeetSemiLattice v => MeetSemiLattice (k -> v) where - f `meet` g = \x -> f x `meet` 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 - --- --- Tuples --- - -instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where - (x1, y1) `join` (x2, y2) = (x1 `join` x2, y1 `join` y2) - -instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where - (x1, y1) `meet` (x2, y2) = (x1 `meet` x2, y1 `meet` 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 - join = (||) - -instance MeetSemiLattice Bool where - meet = (&&) - -instance Lattice Bool where - -instance BoundedJoinSemiLattice Bool where - bottom = False - -instance BoundedMeetSemiLattice Bool where - top = True - -instance BoundedLattice Bool where - - --- | Implementation of Kleene fixed-point theorem . --- Assumes that the function is monotone and does not check if that is correct. -{-# INLINE unsafeLfp #-} -unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a -unsafeLfp = PO.unsafeLfpFrom bottom - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be monotone. -{-# INLINE lfp #-} -lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a -lfp = lfpFrom bottom - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be monotone. -{-# INLINE lfpFrom #-} -lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a -lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x `join` x) - - --- | Implementation of Kleene fixed-point theorem . --- Assumes that the function is antinone and does not check if that is correct. -{-# INLINE unsafeGfp #-} -unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a -unsafeGfp = PO.unsafeGfpFrom top - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be antinone. -{-# INLINE gfp #-} -gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a -gfp = gfpFrom top - --- | Implementation of Kleene fixed-point theorem . --- Forces the function to be antinone. -{-# INLINE gfpFrom #-} -gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a -gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x `meet` x) diff --git a/Algebra/Lattice/Dropped.hs b/Algebra/Lattice/Dropped.hs deleted file mode 100644 --- a/Algebra/Lattice/Dropped.hs +++ /dev/null @@ -1,90 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Dropped --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Dropped ( - Dropped(..) - ) where - -#ifndef MIN_VERSION_base -#define MIN_VERSION_base(x,y,z) 1 -#endif - -import Algebra.Lattice - -#if MIN_VERSION_base(4,8,0) -#else -import Data.Monoid (Monoid(..)) -import Data.Foldable -import Data.Traversable -#endif - -import Control.Applicative -import Control.DeepSeq -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- 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 - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Functor Dropped where - fmap _ Top = Top - fmap f (Drop a) = Drop (f a) - -instance Foldable Dropped where - foldMap _ Top = mempty - foldMap f (Drop a) = f a - -instance Traversable Dropped where - traverse _ Top = pure Top - traverse f (Drop a) = Drop <$> f a - -instance NFData a => NFData (Dropped a) where - rnf Top = () - rnf (Drop a) = rnf a - -instance Hashable a => Hashable (Dropped a) - -instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where - Top `join` _ = Top - _ `join` Top = Top - Drop x `join` Drop y = Drop (x `join` y) - -instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where - Top `meet` drop_y = drop_y - drop_x `meet` Top = drop_x - Drop x `meet` Drop y = Drop (x `meet` 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 - top = Top - -instance BoundedLattice a => BoundedLattice (Dropped a) where diff --git a/Algebra/Lattice/Levitated.hs b/Algebra/Lattice/Levitated.hs deleted file mode 100644 --- a/Algebra/Lattice/Levitated.hs +++ /dev/null @@ -1,99 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Levitated --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Levitated ( - Levitated(..) - ) where - -#ifndef MIN_VERSION_base -#define MIN_VERSION_base(x,y,z) 1 -#endif - -import Algebra.Lattice - -#if MIN_VERSION_base(4,8,0) -#else -import Data.Monoid (Monoid(..)) -import Data.Foldable -import Data.Traversable -#endif - -import Control.Applicative -import Control.DeepSeq -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- Levitated --- - --- | 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 - | Levitate a - | Bottom - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) -instance Functor Levitated where - fmap _ Bottom = Bottom - fmap _ Top = Top - fmap f (Levitate a) = Levitate (f a) - -instance Foldable Levitated where - foldMap _ Bottom = mempty - foldMap _ Top = mempty - foldMap f (Levitate a) = f a - -instance Traversable Levitated where - traverse _ Bottom = pure Bottom - traverse _ Top = pure Top - traverse f (Levitate a) = Levitate <$> f a - -instance NFData a => NFData (Levitated a) where - rnf Top = () - rnf Bottom = () - rnf (Levitate a) = rnf a - -instance Hashable a => Hashable (Levitated a) - -instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where - Top `join` _ = Top - _ `join` Top = Top - Levitate x `join` Levitate y = Levitate (x `join` y) - Bottom `join` lev_y = lev_y - lev_x `join` Bottom = lev_x - -instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where - Top `meet` lev_y = lev_y - lev_x `meet` Top = lev_x - Levitate x `meet` Levitate y = Levitate (x `meet` y) - Bottom `meet` _ = Bottom - _ `meet` Bottom = Bottom - -instance Lattice a => Lattice (Levitated a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where - bottom = Bottom - -instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where - top = Top - -instance Lattice a => BoundedLattice (Levitated a) where diff --git a/Algebra/Lattice/Lifted.hs b/Algebra/Lattice/Lifted.hs deleted file mode 100644 --- a/Algebra/Lattice/Lifted.hs +++ /dev/null @@ -1,89 +0,0 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.Lattice.Lifted --- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.Lattice.Lifted ( - Lifted(..) - ) where - -#ifndef MIN_VERSION_base -#define MIN_VERSION_base(x,y,z) 1 -#endif - -import Algebra.Lattice - -#if MIN_VERSION_base(4,8,0) -#else -import Data.Monoid (Monoid(..)) -import Data.Foldable -import Data.Traversable -#endif - -import Control.Applicative -import Control.DeepSeq -import Data.Data -import Data.Hashable -import GHC.Generics - --- --- 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 - deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic -#if __GLASGOW_HASKELL__ >= 706 - , Generic1 -#endif - ) - -instance Functor Lifted where - fmap _ Bottom = Bottom - fmap f (Lift a) = Lift (f a) - -instance Foldable Lifted where - foldMap _ Bottom = mempty - foldMap f (Lift a) = f a - -instance Traversable Lifted where - traverse _ Bottom = pure Bottom - traverse f (Lift a) = Lift <$> f a - -instance NFData a => NFData (Lifted a) where - rnf Bottom = () - rnf (Lift a) = rnf a - -instance Hashable a => Hashable (Lifted a) - -instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where - Lift x `join` Lift y = Lift (x `join` y) - Bottom `join` lift_y = lift_y - lift_x `join` Bottom = lift_x - -instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where - Lift x `meet` Lift y = Lift (x `meet` y) - Bottom `meet` _ = Bottom - _ `meet` Bottom = Bottom - -instance Lattice a => Lattice (Lifted a) where - -instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where - bottom = Bottom - -instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where - top = Lift top - -instance BoundedLattice a => BoundedLattice (Lifted a) where diff --git a/Algebra/PartialOrd.hs b/Algebra/PartialOrd.hs deleted file mode 100644 --- a/Algebra/PartialOrd.hs +++ /dev/null @@ -1,111 +0,0 @@ -{-# LANGUAGE Safe #-} ----------------------------------------------------------------------------- --- | --- Module : Algebra.PartialOrd --- Copyright : (C) 2010-2015 Maximilian Bolingbroke --- License : BSD-3-Clause (see the file LICENSE) --- --- Maintainer : Oleg Grenrus --- ----------------------------------------------------------------------------- -module Algebra.PartialOrd ( - -- * Partial orderings - PartialOrd(..), - partialOrdEq, - - -- * Fixed points of chains in partial orders - lfpFrom, unsafeLfpFrom, - gfpFrom, unsafeGfpFrom - ) where - -import Algebra.Enumerable - -import qualified Data.Set as S -import qualified Data.IntSet as IS -import qualified Data.Map as M -import qualified Data.IntMap as IM - - --- | A partial ordering on sets: --- --- This can be defined using either |joinLeq| or |meetLeq|, or a more efficient definition --- can be derived directly. --- --- @ --- Reflexive: a `leq` a --- Antisymmetric: a `leq` b && b `leq` a ==> a == b --- Transitive: a `leq` b && b `leq` c ==> a `leq` c --- @ --- --- The superclass equality (which can be defined using |partialOrdEq|) must obey these laws: --- --- @ --- Reflexive: a == a --- Transitive: a == b && b == c ==> a == b --- @ -class Eq a => PartialOrd a where - leq :: a -> a -> Bool - --- | The equality relation induced by the partial-order structure -partialOrdEq :: PartialOrd a => a -> a -> Bool -partialOrdEq x y = leq x y && leq y x - - -instance Ord a => PartialOrd (S.Set a) where - leq = S.isSubsetOf - -instance PartialOrd IS.IntSet where - leq = IS.isSubsetOf - -instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where - m1 `leq` m2 = m1 `M.isSubmapOf` m2 && M.fold (\(x1, x2) b -> b && x1 `leq` x2) True (M.intersectionWith (,) m1 m2) - -instance PartialOrd v => PartialOrd (IM.IntMap v) where - im1 `leq` im2 = im1 `IM.isSubmapOf` im2 && IM.fold (\(x1, x2) b -> b && x1 `leq` x2) True (IM.intersectionWith (,) im1 im2) - -instance (Eq v, Enumerable k) => Eq (k -> v) where - f == g = all (\k -> f k == g k) universe - -instance (PartialOrd v, Enumerable k) => PartialOrd (k -> v) where - f `leq` g = all (\k -> f k `leq` g k) universe - -instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where - -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical - -- ordering is incompatible with the transitivity axiom we require for the derived partial order - (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2 - - --- | Least point of a partially ordered monotone function. Checks that the function is monotone. -lfpFrom :: PartialOrd a => a -> (a -> a) -> a -lfpFrom = lfpFrom' leq - --- | Least point of a partially ordered monotone function. Does not checks that the function is monotone. -unsafeLfpFrom :: Eq a => a -> (a -> a) -> a -unsafeLfpFrom = lfpFrom' (\_ _ -> True) - -{-# INLINE lfpFrom' #-} -lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a -lfpFrom' check init_x f = go init_x - where go x | x' == x = x - | x `check` x' = go x' - | otherwise = error "lfpFrom: non-monotone function" - where x' = f x - - --- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone. -{-# INLINE gfpFrom #-} -gfpFrom :: PartialOrd a => a -> (a -> a) -> a -gfpFrom = gfpFrom' leq - --- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone. -{-# INLINE unsafeGfpFrom #-} -unsafeGfpFrom :: Eq a => a -> (a -> a) -> a -unsafeGfpFrom = gfpFrom' (\_ _ -> True) - -{-# INLINE gfpFrom' #-} -gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a -gfpFrom' check init_x f = go init_x - where go x | x' == x = x - | x' `check` x = go x' - | otherwise = error "gfpFrom: non-antinone function" - where x' = f x diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,94 @@ +# 2.2.1 (2024-05-16) + +- Support GHC-8.6.5..GHC-9.10.1 + +# 2.2 (2022-03-15) + +- Drop `semigroupoids` dependency in favour of `foldable1-classes-compat`. + Be careful with which `Foldable1` class you end up using. + +# 2.1 (2022-12-27) + +- Fix `comprable` for `PartialOrd (a,b)` instance +- Remove `Stacked`, use `Either` instead for ordinal sum. + There is no type for disjoint union / parallel composition. + Open an issue if you need one. + Terminology is from https://en.wikipedia.org/wiki/Partially_ordered_set#Sums_of_partially_ordered_sets + +# 2.0.3 (2021-10-30) + +- Add instances for `Solo` + +# 2.0.2 (2020-02-18) + +- Add `Algebra.Lattice.Stacked` + [#99](https://github.com/phadej/lattices/pull/99) + +# 2.0.1 (2019-07-22) + +- Add `(PartialOrd a, PartialOrd b) => PartialOrd (Either a b)` instance + +# 2 (2019-04-17) + +- Reduce to three classes (from six): `Lattice`, `BoundedMeetSemiLattice`, + `BoundedJoinSemiLattice`. + 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 + +# 1.7.1 (2018-01-29) + +- Correct *Safe Haskell* annotations. See https://github.com/ekmett/semigroupoids/issues/69 +- Bump lower bounds + +# 1.7 (2017-10-01) + +- `HashMap` instances changed +- `PartialOrd Meet` and `Join` +- `PartialOrd ()` and `Void` +- `BoundedLattice (HashSet a)` +- `PartialOrd [a]` (`leq = isInfixOf`) + +# 1.6.0 (2017-06-26) + +- Correct PartialOrd Map and IntMap instances +- Add Lattice instance for `containers` types. +- Change `meets1` and `joins1` to use `Foldable1` +- Add `comparable` to `PartialOrd` +- Add `Algebra.Lattice.Free` module +- Add `Divisibility` lattice. +- Fix `Lexicographic`. + +# 1.5.0 (2015-12-18) + +- Move `PartialOrd (k -> v)` instance into own module +- `Const` and `Identity` instances +- added `fromBool` +- Add `Lexicographic`, `Ordered` and `Op` newtypes + +# 1.4.1 (2015-10-26) + +- `MINIMAL` pragma in with GHC 7.8 +- Add `DEPREACTED` pragma for `meet` and `join`, + use infix version `\/` and `/\` + +# 1.4 (2015-09-19) + +- Infix operators +- `meets` and `joins` generalised to work on any `Foldable` +- Deprecate `Algebra.Enumerable`, use [universe package](http://hackage.haskell.org/package/universe) +- Add `Applicative` and `Monad` typeclasses to `Dropped`, `Lifted` and `Levitated` +- Add `Semigroup` instance to `Join` and `Meet` +- Add instances for `()`, `Proxy`, `Tagged` and `Void` + # 1.3 (2015-05-18) - relaxed constraint for `BoundedLattice (Levitated a)` diff --git a/README.md b/README.md deleted file mode 100644 --- a/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# lattices - -[![Build Status](https://travis-ci.org/phadej/lattices.svg?branch=master)](https://travis-ci.org/phadej/lattices) - -Fine-grained library for constructing and manipulating lattices diff --git a/lattices.cabal b/lattices.cabal --- a/lattices.cabal +++ b/lattices.cabal @@ -1,39 +1,124 @@ +cabal-version: 1.18 name: lattices -version: 1.3 -cabal-version: >= 1.10 +version: 2.2.1.1 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.git/issues -copyright: (C) 2010-2015 Maximilian Bolingbroke +bug-reports: http://github.com/phadej/lattices/issues +copyright: + (C) 2010-2015 Maximilian Bolingbroke, 2016-2019 Oleg Grenrus + build-type: Simple -extra-source-files: README.md CHANGELOG.md -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 ==8.6.5 + || ==8.8.3 + || ==8.10.4 + || ==9.0.2 + || ==9.2.8 + || ==9.4.8 + || ==9.6.7 + || ==9.8.4 + || ==9.10.2 + || ==9.12.4 + || ==9.14.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 have a unique supremum (also called a least upper bound or @join@) and a unique infimum (also called a greatest lower bound or @meet@). + 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@) + and a unique infimum (also called a greatest lower bound, meet, or @x /\\ y@). + . + This package provide type-classes for different lattice types, as well + as a class for the partial order. source-repository head - type: git - location: git://github.com/phadej/lattices.git + type: git + location: https://github.com/phadej/lattices.git library - exposed-modules: Algebra.Enumerable, - Algebra.Lattice, - Algebra.Lattice.Dropped, - Algebra.Lattice.Levitated, - Algebra.Lattice.Lifted, - Algebra.PartialOrd + default-language: Haskell2010 + hs-source-dirs: src + ghc-options: -Wall + 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 - build-depends: base >= 3 && < 5, - containers >= 0.3 && < 0.6, - deepseq >= 1.1 && < 1.5, - hashable >= 1.2 && < 1.3, - unordered-containers >= 0.2 && < 0.3 + exposed-modules: + Algebra.Heyting + Algebra.Heyting.Free + Algebra.Heyting.Free.Expr + + exposed-modules: + Algebra.PartialOrd + Algebra.PartialOrd.Instances + + build-depends: + base >=4.12 && <4.23 + , containers >=0.5.0.0 && <0.9 + , deepseq >=1.3.0.0 && <1.6 + , hashable >=1.2.7.0 && <1.6 + , integer-logarithms >=1.0.3 && <1.1 + , QuickCheck >=2.12.6.1 && <2.19 + , tagged >=0.8.6 && <0.9 + , transformers >=0.3.0.0 && <0.7 + , universe-base >=1.1 && <1.2 + , universe-reverse-instances >=1.1 && <1.2 + , unordered-containers >=0.2.8.0 && <0.3 + + if !impl(ghc >=9.6) + build-depends: foldable1-classes-compat >=0.1 && <0.2 + + if !impl(ghc >=9.2) + if impl(ghc >=9.0) + build-depends: ghc-prim + else + build-depends: OneTuple >=0.4 && <0.5 + +test-suite test-lattices + type: exitcode-stdio-1.0 + main-is: Tests.hs + hs-source-dirs: test ghc-options: -Wall default-language: Haskell2010 + build-depends: + base + , containers + , lattices + , QuickCheck + , quickcheck-instances >=0.3.19 && <0.5 + , tasty >=1.2.1 && <1.6 + , tasty-quickcheck >=0.10 && <0.12 + , universe-base + , universe-reverse-instances + , unordered-containers - if impl(ghc >= 7.4 && < 7.5) - build-depends: ghc-prim + if !impl(ghc >=8.0) + build-depends: semigroups 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/Heyting.hs b/src/Algebra/Heyting.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Heyting.hs @@ -0,0 +1,167 @@ +{-# LANGUAGE CPP #-} +{-# 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 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 Set + +#if MIN_VERSION_base(4,18,0) +import Data.Tuple (Solo (MkSolo)) +#elif MIN_VERSION_base(4,16,0) +import Data.Tuple (Solo (Solo)) +#define MkSolo Solo +#elif MIN_VERSION_base(4,15,0) +import GHC.Tuple (Solo (Solo)) +#define MkSolo Solo +#else +import Data.Tuple.Solo (Solo (MkSolo)) +#endif + +-- | 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, Solo +------------------------------------------------------------------------------- + +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) + +-- | @since 2.0.3 +instance Heyting a => Heyting (Solo a) where + MkSolo a ==> MkSolo b = MkSolo (a ==> b) + neg (MkSolo a) = MkSolo (neg a) + MkSolo a <=> MkSolo b = MkSolo (a <=> b) + +------------------------------------------------------------------------------- +-- Sets +------------------------------------------------------------------------------- + +instance (Ord a, Finite a) => Heyting (Set.Set a) where + x ==> y = Set.union (neg x) y + + neg xs = Set.fromList [ x | x <- universeF, Set.notMember x xs] + + x <=> y = Set.fromList + [ z + | z <- universeF + , Set.member z x <=> Set.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,185 @@ +{-# 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 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 + +-- $setup +-- >>> import Algebra.Lattice +-- >>> import Algebra.PartialOrd +-- >>> import Algebra.Heyting + +------------------------------------------------------------------------------- +-- 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,277 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Algebra.Heyting.Free.Expr ( + Expr (..), + proofSearch, + ) where + +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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice.hs @@ -0,0 +1,583 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +-- In mathematics, a lattice is a partially ordered set in which every +-- two elements have a unique supremum (also called a least upper bound +-- or @join@) and a unique infimum (also called a greatest lower bound or +-- @meet@). +-- +-- In this module lattices are defined using 'meet' and 'join' operators, +-- as it's constructive one. +-- +---------------------------------------------------------------------------- +module Algebra.Lattice ( + -- * Unbounded lattices + Lattice (..), + joinLeq, joins1, meetLeq, meets1, + + -- * Bounded lattices + BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), + joins, meets, + fromBool, + BoundedLattice, + + -- * Monoid wrappers + Meet(..), Join(..), + + -- * Fixed points of chains in lattices + lfp, lfpFrom, unsafeLfp, + gfp, gfpFrom, unsafeGfp, + ) where + +import qualified Algebra.PartialOrd as PO + +import Control.Applicative (Const (..)) +import Control.Monad.Zip (MonadZip (..)) +import Data.Data (Data, Typeable) +import Data.Foldable1 (Foldable1 (..)) +import Data.Functor.Identity (Identity (..)) +import Data.Hashable (Hashable (..)) +import Data.Proxy (Proxy (..)) +import Data.Semigroup (All (..), Any (..), Endo (..), Semigroup (..)) +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 Map +import qualified Data.Set as Set +import qualified Test.QuickCheck as QC + +#if MIN_VERSION_base(4,18,0) +import Data.Tuple (Solo (MkSolo)) +#elif MIN_VERSION_base(4,16,0) +import Data.Tuple (Solo (Solo)) +#define MkSolo Solo +#elif MIN_VERSION_base(4,15,0) +import GHC.Tuple (Solo (Solo)) +#define MkSolo Solo +#else +import Data.Tuple.Solo (Solo (MkSolo)) +#endif + +infixr 6 /\ -- This comment needed because of CPP +infixr 5 \/ + +-- | An algebraic structure with joins and meets. +-- +-- 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 +-- @ +-- +-- /Commutativity/ +-- +-- @ +-- 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 + + -- | meet + (/\) :: a -> a -> a + +-- | The partial ordering induced by the join-semilattice structure +joinLeq :: (Eq a, Lattice a) => a -> a -> Bool +joinLeq x y = (x \/ y) == y + +meetLeq :: (Eq a, Lattice a) => a -> a -> Bool +meetLeq x y = (x /\ y) == x + +-- | A join-semilattice with an identity element 'bottom' for '\/'. +-- +-- /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 +joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a +joins = getJoin . foldMap Join + +-- | The join of at a list of join-semilattice elements (of length at least one) +joins1 :: (Lattice a, Foldable1 f) => f a -> a +joins1 = getJoin . foldMap1 Join + +-- | A meet-semilattice with an identity element 'top' for '/\'. +-- +-- /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 +meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a +meets = getMeet . foldMap Meet +-- +-- | The meet of at a list of meet-semilattice elements (of length at least one) +meets1 :: (Lattice a, Foldable1 f) => f a -> a +meets1 = getMeet . foldMap1 Meet + +type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a) + +-- | 'True' to 'top' and 'False' to 'bottom' +fromBool :: BoundedLattice a => Bool -> a +fromBool True = top +fromBool False = bottom + +-- +-- Sets +-- + +instance Ord a => Lattice (Set.Set a) where + (\/) = Set.union + (/\) = Set.intersection + +instance Ord a => BoundedJoinSemiLattice (Set.Set a) where + bottom = Set.empty + +instance (Ord a, Finite a) => BoundedMeetSemiLattice (Set.Set a) where + top = Set.fromList universeF + +-- +-- IntSets +-- + +instance Lattice IS.IntSet where + (\/) = IS.union + (/\) = IS.intersection + +instance BoundedJoinSemiLattice IS.IntSet where + bottom = IS.empty + +-- +-- HashSet +-- + + +instance (Eq a, Hashable a) => Lattice (HS.HashSet a) where + (\/) = HS.union + (/\) = HS.intersection + +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 + +-- +-- Maps +-- + +instance (Ord k, Lattice v) => Lattice (Map.Map k v) where + (\/) = Map.unionWith (\/) + (/\) = Map.intersectionWith (/\) + +instance (Ord k, Lattice v) => BoundedJoinSemiLattice (Map.Map k v) where + bottom = Map.empty + +instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Map.Map k v) where + top = Map.fromList (universeF `zip` repeat top) + +-- +-- IntMaps +-- + +instance Lattice v => Lattice (IM.IntMap v) where + (\/) = IM.unionWith (\/) + (/\) = IM.intersectionWith (/\) + +instance Lattice v => BoundedJoinSemiLattice (IM.IntMap v) where + bottom = IM.empty + +-- +-- HashMaps +-- + +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) + +-- +-- Functions +-- + +instance Lattice v => Lattice (k -> v) where + f \/ g = \x -> f x \/ g x + f /\ g = \x -> f x /\ g x + +instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where + bottom = const bottom + +instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where + top = const top + +-- +-- Unit +-- + + +instance Lattice () where + _ \/ _ = () + _ /\ _ = () + +instance BoundedJoinSemiLattice () where + bottom = () + +instance BoundedMeetSemiLattice () where + top = () + +-- +-- Tuples +-- + +instance (Lattice a, Lattice b) => Lattice (a, b) where + (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2) + (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2) + +instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where + bottom = (bottom, bottom) + +instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where + top = (top, top) + +-- +-- Either +-- + +-- | Ordinal sum. +-- +-- @since 2.1 +instance (Lattice a, Lattice b) => Lattice (Either a b) where + Right x \/ Right y = Right (x \/ y) + u@(Right _) \/ _ = u + _ \/ u@(Right _) = u + Left x \/ Left y = Left (x \/ y) + + Left x /\ Left y = Left (x /\ y) + l@(Left _) /\ _ = l + _ /\ l@(Left _) = l + Right x /\ Right y = Right (x /\ y) + +-- | @since 2.1 +instance (BoundedJoinSemiLattice a, Lattice b) => BoundedJoinSemiLattice (Either a b) where + bottom = Left bottom + +-- | @since 2.1 +instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Either a b) where + top = Right top + +-- +-- Bools +-- + +instance Lattice Bool where + (\/) = (||) + (/\) = (&&) + +instance BoundedJoinSemiLattice Bool where + bottom = False + +instance BoundedMeetSemiLattice Bool where + top = True + +--- Monoids + +-- | Monoid wrapper for join-'Lattice' +newtype Join a = Join { getJoin :: a } + deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) + +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, Lattice a) => PO.PartialOrd (Join a) where + leq (Join a) (Join b) = joinLeq a b + +instance Functor Join where + fmap f (Join x) = Join (f x) + +instance Applicative Join where + pure = Join + Join f <*> Join x = Join (f x) + _ *> x = x + +instance Monad Join where + return = pure + Join m >>= f = f m + (>>) = (*>) + +instance MonadZip Join where + mzip (Join x) (Join y) = Join (x, y) + +instance Universe a => Universe (Join a) where + universe = fmap Join universe + +instance Finite a => Finite (Join a) where + universeF = fmap Join universeF + +-- | Monoid wrapper for meet-'Lattice' +newtype Meet a = Meet { getMeet :: a } + deriving (Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic) + +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, Lattice a) => PO.PartialOrd (Meet a) where + leq (Meet a) (Meet b) = meetLeq a b + +instance Functor Meet where + fmap f (Meet x) = Meet (f x) + +instance Applicative Meet where + pure = Meet + Meet f <*> Meet x = Meet (f x) + _ *> x = x + +instance Monad Meet where + return = pure + Meet m >>= f = f m + (>>) = (*>) + +instance MonadZip Meet where + mzip (Meet x) (Meet y) = Meet (x, y) + +instance Universe a => Universe (Meet a) where + universe = fmap Meet universe + +instance Finite a => Finite (Meet a) where + universeF = fmap Meet universeF + +-- All + +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 BoundedMeetSemiLattice All where + top = All True + +-- Any +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 BoundedMeetSemiLattice Any where + top = Any True + +-- Endo +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 BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where + top = Endo top + +-- Tagged + +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 BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where + top = Tagged top + +-- Proxy +instance Lattice (Proxy a) where + _ \/ _ = Proxy + _ /\ _ = Proxy + +instance BoundedJoinSemiLattice (Proxy a) where + bottom = Proxy + +instance BoundedMeetSemiLattice (Proxy a) where + top = Proxy + +-- Identity + +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 BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where + bottom = Identity bottom + +-- Const +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 BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where + top = Const top + +------------------------------------------------------------------------------- +-- Void +------------------------------------------------------------------------------- + +instance Lattice Void where + a \/ _ = a + a /\ _ = a + +------------------------------------------------------------------------------- +-- 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 + +------------------------------------------------------------------------------- +-- OneTuple +------------------------------------------------------------------------------- + +-- | @since 2.0.3 +instance Lattice a => Lattice (Solo a) where + MkSolo a \/ MkSolo b = MkSolo (a \/ b) + MkSolo a /\ MkSolo b = MkSolo (a /\ b) + +-- | @since 2.0.3 +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Solo a) where + top = MkSolo top + +-- | @since 2.0.3 +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Solo a) where + bottom = MkSolo bottom + +------------------------------------------------------------------------------- +-- Theorems +------------------------------------------------------------------------------- + +-- | Implementation of Kleene fixed-point theorem . +-- Assumes that the function is monotone and does not check if that is correct. +{-# INLINE unsafeLfp #-} +unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a +unsafeLfp = PO.unsafeLfpFrom bottom + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be monotone. +{-# INLINE lfp #-} +lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a +lfp = lfpFrom bottom + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be monotone. +{-# INLINE lfpFrom #-} +lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a +lfpFrom init_x f = PO.unsafeLfpFrom init_x (\x -> f x \/ x) + + +-- | Implementation of Kleene fixed-point theorem . +-- Assumes that the function is antinone and does not check if that is correct. +{-# INLINE unsafeGfp #-} +unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a +unsafeGfp = PO.unsafeGfpFrom top + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be antinone. +{-# INLINE gfp #-} +gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a +gfp = gfpFrom top + +-- | Implementation of Kleene fixed-point theorem . +-- Forces the function to be antinone. +{-# INLINE gfpFrom #-} +gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a +gfpFrom init_x f = PO.unsafeGfpFrom init_x (\x -> f x /\ x) diff --git a/src/Algebra/Lattice/Divisibility.hs b/src/Algebra/Lattice/Divisibility.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Divisibility.hs @@ -0,0 +1,89 @@ +{-# 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-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Divisibility ( + Divisibility(..) + ) where + +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 + +-- +-- Divisibility +-- + +-- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. +newtype Divisibility a = Divisibility { getDivisibility :: a } + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Divisibility where + pure = return + (<*>) = ap + +instance Monad Divisibility where + return = Divisibility + Divisibility x >>= f = f x + +instance NFData a => NFData (Divisibility a) where + rnf (Divisibility a) = rnf a + +instance Hashable a => Hashable (Divisibility a) + +instance Integral a => Lattice (Divisibility a) where + Divisibility x \/ Divisibility y = Divisibility (lcm x y) + + Divisibility x /\ Divisibility y = Divisibility (gcd x y) + +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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Dropped.hs @@ -0,0 +1,119 @@ +{-# 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-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Dropped ( + Dropped(..) + , retractDropped + , foldDropped + ) where + +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 + +-- +-- 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 = Drop a + | Top + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Dropped where + pure = return + (<*>) = ap + +instance Monad Dropped where + return = Drop + Top >>= _ = Top + Drop x >>= f = f x + +instance NFData a => NFData (Dropped a) where + rnf Top = () + rnf (Drop a) = rnf a + +instance Hashable a => Hashable (Dropped a) + +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) + + Top /\ drop_y = drop_y + drop_x /\ Top = drop_x + Drop x /\ Drop y = Drop (x /\ y) + +instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where + bottom = Drop bottom + +instance Lattice a => BoundedMeetSemiLattice (Dropped a) where + top = Top + +-- | Interpret @'Dropped' a@ using the 'BoundedMeetSemiLattice' of @a@. +retractDropped :: BoundedMeetSemiLattice a => Dropped a -> a +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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Free.hs @@ -0,0 +1,144 @@ +{-# 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 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 + +-- $setup +-- >>> import Algebra.Lattice + +------------------------------------------------------------------------------- +-- Free +------------------------------------------------------------------------------- + +-- | Free distributive lattice. +-- +-- `Eq` and `PartialOrd` instances aren't structural. +-- +-- >>> (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) + +infixr 6 :/\: +infixr 5 :\/: + +liftFree :: a -> Free a +liftFree = Var + +retractFree :: Lattice a => Free a -> a +retractFree = lowerFree id + +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 + +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 + +------------------------------------------------------------------------------- +-- Monad +------------------------------------------------------------------------------- + +instance Applicative Free where + pure = liftFree + (<*>) = ap + +instance Monad Free where + return = pure + (>>=) = substFree + +------------------------------------------------------------------------------- +-- Instances +------------------------------------------------------------------------------- + +instance Lattice (Free a) where + x /\ y = x :/\: y + x \/ y = x :\/: y + +instance Ord a => Eq (Free a) where + (==) = partialOrdEq + +instance Ord a => PartialOrd (Free a) where + leq x y = E.proofSearch (toExpr x E.:=>: toExpr 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 (intLog2 (max 1 n)) + + compound = + [ liftA2 (:/\:) arb' arb' + , liftA2 (:\/:) arb' arb' + ] + + prim = Var <$> QC.arbitrary + + 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,103 @@ +{-# 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 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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Levitated.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Levitated +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Levitated ( + Levitated(..) + , retractLevitated + , foldLevitated + ) where + +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 + +-- +-- Levitated +-- + +-- | 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 = Bottom + | Levitate a + | Top + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Levitated where + pure = return + (<*>) = ap + +instance Monad Levitated where + return = Levitate + Top >>= _ = Top + Bottom >>= _ = Bottom + Levitate x >>= f = f x + +instance NFData a => NFData (Levitated a) where + rnf Top = () + rnf Bottom = () + rnf (Levitate a) = rnf a + +instance Hashable a => Hashable (Levitated a) + +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 + + Top /\ lev_y = lev_y + lev_x /\ Top = lev_x + Levitate x /\ Levitate y = Levitate (x /\ y) + Bottom /\ _ = Bottom + _ /\ Bottom = Bottom + +instance Lattice a => BoundedJoinSemiLattice (Levitated a) where + bottom = Bottom + +instance Lattice a => BoundedMeetSemiLattice (Levitated a) where + top = Top + +-- | Interpret @'Levitated' a@ using the 'BoundedLattice' of @a@. +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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Lexicographic.hs @@ -0,0 +1,137 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Lexicographic +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Lexicographic ( + Lexicographic(..) + ) where + +import Algebra.Lattice +import Algebra.PartialOrd + +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 +-- + +-- | A pair lattice with a lexicographic ordering. This means in +-- a join the second component of the resulting pair is the second +-- component of the pair with the larger first component. If the +-- first components are equal, then the second components will be +-- joined. The meet is similar only it prefers the smaller first +-- component. +-- +-- An application of this type is versioning. For example, a +-- Last-Writer-Wins register would look like +-- @'Lexicographic' ('Algebra.Lattice.Ordered.Ordered' Timestamp) v@ where the lattice +-- structure handles the, presumably rare, case of matching +-- @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 + , Generic1 + ) + +instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where + pure = return + (<*>) = ap + +-- Essentially the Writer monad. +instance BoundedJoinSemiLattice k => Monad (Lexicographic k) where + return = Lexicographic bottom + Lexicographic k v >>= f = + case f v of + Lexicographic k' v' -> Lexicographic (k \/ k') v' + +instance (NFData k, NFData v) => NFData (Lexicographic k v) where + rnf (Lexicographic k v) = rnf k `seq` rnf v + +instance (Hashable k, Hashable v) => Hashable (Lexicographic k v) + +-- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause? +-- +-- For example what is the join of @(2, 1)@ and @(3, 2)@ +-- in lexicographic divisibility divisibility lattice. +-- +-- With @v1 \\/ v2@, we get the upper bound, but not least! +-- +-- @ +-- (2, 1) `leq` (6, 2) +-- (3, 2) `leq` (6, 2) +-- @ +-- +-- But @(6, 1) `leq` (6, 2)@, and +-- +-- @ +-- (2, 1) `leq` (6, 1) +-- (3, 2) `leq` (6, 1) +-- @ +-- +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 + + 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, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where + bottom = Lexicographic bottom bottom + +instance (PartialOrd k, BoundedMeetSemiLattice k, BoundedJoinSemiLattice v, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Lexicographic k v) where + top = Lexicographic top top + +instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where + Lexicographic k1 v1 `leq` Lexicographic k2 v2 + | k1 == k2 = v1 `leq` v2 + | k1 `leq` k2 = True + | otherwise = False -- Incomparable or k2 `leq` k1 + 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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Lifted.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Lifted +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Lifted ( + Lifted(..) + , retractLifted + , foldLifted + ) where + +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 + +-- +-- 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 = Bottom + | Lift a + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Lifted where + pure = return + (<*>) = ap + +instance Monad Lifted where + return = Lift + Bottom >>= _ = Bottom + Lift x >>= f = f x + +instance NFData a => NFData (Lifted a) where + rnf Bottom = () + rnf (Lift a) = rnf a + +instance Hashable a => Hashable (Lifted a) + +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 + + Lift x /\ Lift y = Lift (x /\ y) + Bottom /\ _ = Bottom + _ /\ Bottom = Bottom + +instance Lattice a => BoundedJoinSemiLattice (Lifted a) where + bottom = Bottom + +instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where + top = Lift top + +-- | Interpret @'Lifted' a@ using the 'BoundedJoinSemiLattice' of @a@. +retractLifted :: BoundedJoinSemiLattice a => Lifted a -> a +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,121 @@ +{-# 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 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,86 @@ +{-# 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 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,91 @@ +{-# 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 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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Op.hs @@ -0,0 +1,88 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE TypeOperators #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.Lattice.Op +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Op ( + Op(..) + ) where + +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 GHC.Generics (Generic, Generic1) + +import qualified Test.QuickCheck as QC + +-- +-- Op +-- + +-- | The opposite lattice of a given lattice. That is, switch +-- meets and joins. +newtype Op a = Op { getOp :: a } + deriving ( Eq, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Ord a => Ord (Op a) where + compare (Op a) (Op b) = compare b a + +instance Applicative Op where + pure = return + (<*>) = ap + +instance Monad Op where + return = Op + Op x >>= f = f x + +instance NFData a => NFData (Op a) where + rnf (Op a) = rnf a + +instance Hashable a => Hashable (Op a) + +instance Lattice a => Lattice (Op a) where + Op x \/ Op y = Op (x /\ y) + Op x /\ Op y = Op (x \/ y) + +instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where + bottom = Op top + +instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where + top = Op bottom + +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 new file mode 100644 --- /dev/null +++ b/src/Algebra/Lattice/Ordered.hs @@ -0,0 +1,97 @@ +{-# 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-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.Lattice.Ordered ( + Ordered(..) + ) where + +import Algebra.Heyting +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 + +-- +-- Ordered +-- + +-- | A total order gives rise to a lattice. Join is +-- 'max', meet is 'min'. +newtype Ordered a = Ordered { getOrdered :: a } + deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable + , Generic1 + ) + +instance Applicative Ordered where + pure = return + (<*>) = ap + +instance Monad Ordered where + return = Ordered + Ordered x >>= f = f x + +instance NFData a => NFData (Ordered a) where + rnf (Ordered a) = rnf a + +instance Hashable a => Hashable (Ordered a) + +instance Ord a => Lattice (Ordered a) where + Ordered x \/ Ordered y = Ordered (max x y) + Ordered x /\ Ordered y = Ordered (min x y) + +instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where + bottom = Ordered minBound + +instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where + top = Ordered maxBound + +-- | 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,135 @@ +{-# 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 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,77 @@ +{-# 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 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 new file mode 100644 --- /dev/null +++ b/src/Algebra/PartialOrd.hs @@ -0,0 +1,198 @@ +{-# LANGUAGE Safe #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.PartialOrd +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +---------------------------------------------------------------------------- +module Algebra.PartialOrd ( + -- * Partial orderings + PartialOrd(..), + partialOrdEq, + + -- * Fixed points of chains in partial orders + lfpFrom, unsafeLfpFrom, + gfpFrom, unsafeGfpFrom + ) where + +import Data.Foldable (Foldable (..)) +import Data.Hashable (Hashable (..)) +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.List as L +import qualified Data.Map as Map +import Data.Monoid (All (..), Any (..)) +import qualified Data.Set as Set +import Data.Void (Void) + +-- | A partial ordering on sets +-- () is a set equipped +-- with a binary relation, `leq`, that obeys the following laws +-- +-- @ +-- Reflexive: a ``leq`` a +-- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b +-- Transitive: a ``leq`` b && b ``leq`` c ==> a ``leq`` c +-- @ +-- +-- Two elements of the set are said to be `comparable` when they are are +-- ordered with respect to the `leq` relation. So +-- +-- @ +-- `comparable` a b ==> a ``leq`` b || b ``leq`` a +-- @ +-- +-- If `comparable` always returns true then the relation `leq` defines a +-- total ordering (and an `Ord` instance may be defined). Any `Ord` instance is +-- trivially an instance of `PartialOrd`. 'Algebra.Lattice.Ordered' provides a +-- convenient wrapper to satisfy 'PartialOrd' given 'Ord'. +-- +-- As an example consider the partial ordering on sets induced by set +-- inclusion. Then for sets `a` and `b`, +-- +-- @ +-- a ``leq`` b +-- @ +-- +-- is true when `a` is a subset of `b`. Two sets are `comparable` if one is a +-- subset of the other. Concretely +-- +-- @ +-- a = {1, 2, 3} +-- b = {1, 3, 4} +-- c = {1, 2} +-- +-- a ``leq`` a = `True` +-- a ``leq`` b = `False` +-- a ``leq`` c = `False` +-- b ``leq`` a = `False` +-- b ``leq`` b = `True` +-- b ``leq`` c = `False` +-- c ``leq`` a = `True` +-- c ``leq`` b = `False` +-- c ``leq`` c = `True` +-- +-- `comparable` a b = `False` +-- `comparable` a c = `True` +-- `comparable` b c = `False` +-- @ +class Eq a => PartialOrd a where + -- | The relation that induces the partial ordering + leq :: a -> a -> Bool + + -- | 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 :: a -> a -> Bool + comparable x y = leq x y || leq y x + +-- | 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 +partialOrdEq x y = leq x y && leq y x + +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.isSequenceOf'@. +instance Eq a => PartialOrd [a] where + leq = L.isSubsequenceOf + +instance Ord a => PartialOrd (Set.Set a) where + leq = Set.isSubsetOf + +instance PartialOrd IS.IntSet where + leq = IS.isSubsetOf + +instance (Eq k, Hashable k) => PartialOrd (HS.HashSet k) where + leq a b = HS.null (HS.difference a b) + +instance (Ord k, PartialOrd v) => PartialOrd (Map.Map k v) where + leq = Map.isSubmapOfBy leq + +instance PartialOrd v => PartialOrd (IM.IntMap v) where + leq = IM.isSubmapOfBy leq + +instance (Eq k, Hashable k, PartialOrd v) => PartialOrd (HM.HashMap k v) where + x `leq` y = {- wish: HM.isSubmapOfBy leq -} + HM.null (HM.difference x y) && getAll (fold $ HM.intersectionWith (\vx vy -> All (vx `leq` vy)) x y) + +instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where + -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical + -- ordering is incompatible with the transitivity axiom we require for the derived partial order + (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2 + +-- | Ordinal sum. +-- +-- @since 2.1 +instance (PartialOrd a, PartialOrd b) => PartialOrd (Either a b) where + leq (Right x) (Right y) = leq x y + leq (Right _) _ = False + leq _ (Right _) = True + leq (Left x) (Left y) = leq x y + + comparable (Right x) (Right y) = comparable x y + comparable (Right _) _ = True + comparable _ (Right _) = True + comparable (Left x) (Left y) = comparable x y + +-- | Least point of a partially ordered monotone function. Checks that the function is monotone. +lfpFrom :: PartialOrd a => a -> (a -> a) -> a +lfpFrom = lfpFrom' leq + +-- | Least point of a partially ordered monotone function. Does not checks that the function is monotone. +unsafeLfpFrom :: Eq a => a -> (a -> a) -> a +unsafeLfpFrom = lfpFrom' (\_ _ -> True) + +{-# INLINE lfpFrom' #-} +lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a +lfpFrom' check init_x f = go init_x + where go x | x' == x = x + | x `check` x' = go x' + | otherwise = error "lfpFrom: non-monotone function" + where x' = f x + + +-- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone. +{-# INLINE gfpFrom #-} +gfpFrom :: PartialOrd a => a -> (a -> a) -> a +gfpFrom = gfpFrom' leq + +-- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone. +{-# INLINE unsafeGfpFrom #-} +unsafeGfpFrom :: Eq a => a -> (a -> a) -> a +unsafeGfpFrom = gfpFrom' (\_ _ -> True) + +{-# INLINE gfpFrom' #-} +gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a +gfpFrom' check init_x f = go init_x + where go x | x' == x = x + | x' `check` x = go x' + | otherwise = error "gfpFrom: non-antinone function" + where x' = f x diff --git a/src/Algebra/PartialOrd/Instances.hs b/src/Algebra/PartialOrd/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/PartialOrd/Instances.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE Safe #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +---------------------------------------------------------------------------- +-- | +-- Module : Algebra.PartialOrd.Instances +-- Copyright : (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus +-- License : BSD-3-Clause (see the file LICENSE) +-- +-- Maintainer : Oleg Grenrus +-- +-- This module re-exports orphan instances from 'Data.Universe.Instances.Eq' +-- module, and @(PartialOrd v, Finite k) => PartialOrd (k -> v)@ instance. +---------------------------------------------------------------------------- +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 new file mode 100644 --- /dev/null +++ b/test/Tests.hs @@ -0,0 +1,689 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Main (main) where + +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 (testProperty) + +import qualified Test.QuickCheck as QC + +import Algebra.Heyting +import Algebra.Lattice +import Algebra.PartialOrd + +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.Wide as W + +import Data.HashMap.Lazy (HashMap) +import Data.HashSet (HashSet) +import Data.IntMap (IntMap) +import Data.IntSet (IntSet) +import Data.Map (Map) +import Data.Set (Set) + +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 +data Proxy (a :: *) = Proxy +data Proxy1 (a :: * -> *) = Proxy1 + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "Tests" + [ 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 (LBounded Partial Modular) (Proxy :: Proxy (M2, M2)) + , allLatticeLaws (LBounded Partial Distributive) (Proxy :: Proxy (Either M2 M2)) + , allLatticeLaws (LBounded Partial NonModular) (Proxy :: Proxy (Either M3 N5)) -- non modular, though it takes QC time to find + + , 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 + , Arbitrary (m Int) + , Eq (m Int) + , Show (m Int) + , Arbitrary (m (Fun Int Int)) + , Show (m (Fun Int Int))) + => String + -> Proxy1 m + -> TestTree +monadLaws name _ = testGroup ("Monad laws: " <> name) + [ 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 + + rightIdentityProp :: m Int -> Property + rightIdentityProp m = (m >>= return) === m + + compositionProp :: m Int -> Fun Int (m Int) -> Fun Int (m Int) -> Property + compositionProp m (Fun _ k) (Fun _ h) = (m >>= (\x -> k x >>= h)) === ((m >>= k) >>= h) + + pureProp :: Int -> Property + pureProp x = pure x === (return x :: m Int) + + apProp :: m (Fun Int Int) -> m Int -> Property + apProp f x = (f' <*> x) === ap f' x + where f' = apply <$> f +{-# NOINLINE monadLaws #-} + +------------------------------------------------------------------------------- +-- Partial ord laws +------------------------------------------------------------------------------- + +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 +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 +{-# NOINLINE partialOrdLaws #-} + +------------------------------------------------------------------------------- +-- 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)) +{-# NOINLINE allLatticeLaws #-} + +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 + joinLeqProp x y = leq x y === joinLeq x y + + meetLeqProp :: a -> a -> Property + meetLeqProp x y = leq x y === meetLeq x y + + meetLower :: a -> a -> Property + meetLower x y = (m `leq` x) QC..&&. (m `leq` y) + where + m = x /\ y + + joinUpper :: a -> a -> Property + joinUpper x y = (x `leq` j) QC..&&. (y `leq` j) + where + j = x \/ y + + meetComm :: a -> a -> Property + meetComm x y = x /\ y === y /\ x + + joinComm :: a -> a -> Property + joinComm x y = x \/ y === y \/ x + + meetAssoc :: a -> a -> a -> Property + meetAssoc x y z = x /\ (y /\ z) === (x /\ y) /\ z + + joinAssoc :: a -> a -> a -> Property + joinAssoc x y z = x \/ (y \/ z) === (x \/ y) \/ z + + meetAbsorb :: a -> a -> Property + meetAbsorb x y = x /\ (x \/ y) === x + + joinAbsorb :: a -> a -> Property + joinAbsorb x y = x \/ (x /\ y) === x + + meetIdemp :: a -> Property + meetIdemp x = x /\ x === x + + joinIdemp :: a -> Property + joinIdemp x = x \/ x === x + + comparableDef :: a -> a -> Property + comparableDef x y = (leq x y || leq y x) === comparable x y +{-# NOINLINE latticeLaws #-} + +------------------------------------------------------------------------------- +-- 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) +{-# NOINLINE modularLaws #-} + +------------------------------------------------------------------------------- +-- 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 + lhs = x /\ (y \/ z) + rhs = (x /\ y) \/ (x /\ z) + + distr2Prop :: a -> a -> a -> Property + distr2Prop x y z = lhs === rhs where + lhs = x \/ (y /\ z) + rhs = (x \/ y) /\ (x \/ z) +{-# NOINLINE distributiveLaws #-} + +------------------------------------------------------------------------------- +-- Bounded lattice laws +------------------------------------------------------------------------------- + +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 + + identityRightProp :: a -> Property + identityRightProp x = lhs === rhs where + lhs = x /\ top + rhs = x + + annihilationLeftProp :: a -> Property + annihilationLeftProp x = lhs === rhs where + lhs = top \/ x + rhs = top + + annihilationRightProp :: a -> Property + annihilationRightProp x = lhs === rhs where + lhs = x \/ top + rhs = top +{-# NOINLINE boundedMeetLaws #-} + +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 + + annihilationLeftProp :: a -> Property + annihilationLeftProp x = lhs === rhs where + lhs = bottom /\ x + rhs = bottom + + annihilationRightProp :: a -> Property + annihilationRightProp x = lhs === rhs where + lhs = x /\ bottom + rhs = bottom +{-# NOINLINE boundedJoinLaws #-} + +------------------------------------------------------------------------------- +-- Heyting laws +------------------------------------------------------------------------------- + +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 + + equivDefaultProp :: a -> a -> Property + equivDefaultProp x y = lhs === rhs where + lhs = x <=> y + rhs = (x ==> y) /\ (y ==> x) + + idIsTopProp :: a -> Property + idIsTopProp x = lhs === rhs where + lhs = x ==> x + rhs = top + + andDomainProp :: a -> a -> Property + andDomainProp x y = lhs === rhs where + lhs = x /\ (x ==> y) + rhs = x /\ y + + andCodomainProp :: a -> a -> Property + andCodomainProp x y = lhs === rhs where + lhs = y /\ (x ==> y) + rhs = y + + 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 + + implDistrProp' :: a -> a -> a -> Property + implDistrProp' x y z = lhs === rhs where + lhs = x ==> (y /\ z) + rhs = (x ==> y) /\ (x ==> z) + + deMorganProp1 :: a -> a -> Property + deMorganProp1 x y = lhs === rhs where + lhs = neg (x \/ y) + rhs = neg x /\ neg y + + deMorganProp2weak :: a -> a -> Property + deMorganProp2weak x y = lhs === rhs where + lhs = neg (x /\ y) + rhs = neg (neg (neg x \/ neg y)) +{-# NOINLINE heytingLaws #-} + +------------------------------------------------------------------------------- +-- De morgan +------------------------------------------------------------------------------- + +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 +{-# NOINLINE deMorganLaws #-} + +------------------------------------------------------------------------------- +-- Boolean laws +------------------------------------------------------------------------------- + +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 + + -- 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 +{-# NOINLINE booleanLaws #-} + +------------------------------------------------------------------------------- +-- 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) +{-# NOINLINE finiteLaws #-} + +------------------------------------------------------------------------------- +-- Lexicographic M2 search +------------------------------------------------------------------------------- + +searchM3 :: (Eq a, PartialOrd a, Lattice a) => [a] -> Maybe (a,a,a,a,a) +searchM3 xs = listToMaybe $ do + x0 <- xs + xa <- xs + guard (xa `notElem` [x0]) + guard (x0 `leq` xa) + xb <- xs + guard (xb `notElem` [x0,xa]) + guard (x0 `leq` xb) + guard (not $ comparable xa xb) + xc <- xs + guard (xc `notElem` [x0,xa,xb]) + guard (x0 `leq` xc) + guard (not $ comparable xa xc) + guard (not $ comparable xb xc) + x1 <- xs + guard (x1 `notElem` [x0,xa,xb,xc]) + guard (x0 `leq` x1) + guard (xa `leq` x1) + guard (xb `leq` x1) + guard (xc `leq` x1) + + -- homomorphism + let f M3o = x1 + f M3a = xa + f M3b = xb + f M3c = xc + f M3i = x1 + + ma <- [minBound .. maxBound] + mb <- [minBound .. maxBound] + guard (f (ma /\ mb) == f ma /\ f mb) + guard (f (ma \/ mb) == f ma \/ f mb) + + return (x0,xa,xb,xc,x1) + +type L2 = LO.Lexicographic M2 M2 + +searchM3LexM2 :: Maybe (L2,L2,L2,L2,L2) +searchM3LexM2 = searchM3 xs + 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