lattices 1.3 → 2.2.1.1
raw patch · 35 files changed
Files
- Algebra/Enumerable.hs +0/−50
- Algebra/Lattice.hs +0/−301
- Algebra/Lattice/Dropped.hs +0/−90
- Algebra/Lattice/Levitated.hs +0/−99
- Algebra/Lattice/Lifted.hs +0/−89
- Algebra/PartialOrd.hs +0/−111
- CHANGELOG.md +91/−0
- README.md +0/−5
- lattices.cabal +109/−24
- m2.png binary
- m3.png binary
- n5.png binary
- src/Algebra/Heyting.hs +167/−0
- src/Algebra/Heyting/Free.hs +185/−0
- src/Algebra/Heyting/Free/Expr.hs +277/−0
- src/Algebra/Lattice.hs +583/−0
- src/Algebra/Lattice/Divisibility.hs +89/−0
- src/Algebra/Lattice/Dropped.hs +119/−0
- src/Algebra/Lattice/Free.hs +144/−0
- src/Algebra/Lattice/Free/Final.hs +103/−0
- src/Algebra/Lattice/Levitated.hs +140/−0
- src/Algebra/Lattice/Lexicographic.hs +137/−0
- src/Algebra/Lattice/Lifted.hs +118/−0
- src/Algebra/Lattice/M2.hs +121/−0
- src/Algebra/Lattice/M3.hs +86/−0
- src/Algebra/Lattice/N5.hs +91/−0
- src/Algebra/Lattice/Op.hs +88/−0
- src/Algebra/Lattice/Ordered.hs +97/−0
- src/Algebra/Lattice/Unicode.hs +29/−0
- src/Algebra/Lattice/Wide.hs +135/−0
- src/Algebra/Lattice/ZeroHalfOne.hs +77/−0
- src/Algebra/PartialOrd.hs +198/−0
- src/Algebra/PartialOrd/Instances.hs +28/−0
- test/Tests.hs +689/−0
- wide.png binary
− Algebra/Enumerable.hs
@@ -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 <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------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]
− Algebra/Lattice.hs
@@ -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 <oleg.grenrus@iki.fi>------ 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: <http://en.wikipedia.org/wiki/Semilattice>------ @--- 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: <http://en.wikipedia.org/wiki/Semilattice>------ @--- 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 <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>------ @--- 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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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)
− Algebra/Lattice/Dropped.hs
@@ -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 <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------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
− Algebra/Lattice/Levitated.hs
@@ -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 <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------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
− Algebra/Lattice/Lifted.hs
@@ -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 <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------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
− Algebra/PartialOrd.hs
@@ -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 <oleg.grenrus@iki.fi>---------------------------------------------------------------------------------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: <http://en.wikipedia.org/wiki/Partially_ordered_set>------ 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
CHANGELOG.md view
@@ -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)`
− README.md
@@ -1,5 +0,0 @@-# lattices--[](https://travis-ci.org/phadej/lattices)--Fine-grained library for constructing and manipulating lattices
lattices.cabal view
@@ -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 <batterseapower@hotmail.com>+license-file: LICENSE+author:+ Maximilian Bolingbroke <batterseapower@hotmail.com>, Oleg Grenrus <oleg.grenrus@iki.fi>+ maintainer: Oleg Grenrus <oleg.grenrus@iki.fi> 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
+ m2.png view
binary file changed (absent → 4757 bytes)
+ m3.png view
binary file changed (absent → 5473 bytes)
+ n5.png view
binary file changed (absent → 6606 bytes)
+ src/Algebra/Heyting.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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+ ]
+ src/Algebra/Heyting/Free.hs view
@@ -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))
+ src/Algebra/Heyting/Free/Expr.hs view
@@ -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)
+ src/Algebra/Lattice.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+-- 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 <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.+--+-- '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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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 <http://en.wikipedia.org/wiki/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)
+ src/Algebra/Lattice/Divisibility.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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 (<d) . map divisibility . QC.shrink . getDivisibility $ d++instance QC.CoArbitrary a => 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
+ src/Algebra/Lattice/Dropped.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/Lattice/Free.hs view
@@ -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))
+ src/Algebra/Lattice/Free/Final.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------++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
+ src/Algebra/Lattice/Levitated.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/Lattice/Lexicographic.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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)
+ src/Algebra/Lattice/Lifted.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/Lattice/M2.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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'.+--+-- <<m2.png>>+--+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
+ src/Algebra/Lattice/M3.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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.+--+-- <<m3.png>>+--+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
+ src/Algebra/Lattice/N5.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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.+--+-- <<n5.png>>+--+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
+ src/Algebra/Lattice/Op.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/Lattice/Ordered.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/Lattice/Unicode.hs view
@@ -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+(⟺) = (<=>)
+ src/Algebra/Lattice/Wide.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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.+--+-- <<wide.png>>+--+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
+ src/Algebra/Lattice/ZeroHalfOne.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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
+ src/Algebra/PartialOrd.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+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+-- (<http://en.wikipedia.org/wiki/Partially_ordered_set>) 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
+ src/Algebra/PartialOrd/Instances.hs view
@@ -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 <oleg.grenrus@iki.fi>+--+-- 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++
+ test/Tests.hs view
@@ -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 ]
+ wide.png view
binary file changed (absent → 11918 bytes)