packages feed

lattices (empty) → 1.0

raw patch · 9 files changed

+494/−0 lines, 9 filesdep +basedep +containerssetup-changed

Dependencies added: base, containers

Files

+ Algebra/Enumerable.hs view
@@ -0,0 +1,40 @@+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 view
@@ -0,0 +1,210 @@+{-# LANGUAGE FlexibleInstances #-}+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, unsafeLfp,+    gfp, unsafeGfp,+  ) where++import Algebra.Enumerable+import Algebra.PartialOrd++import qualified Data.Set as S+import qualified Data.Map as M+++-- | 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++--+-- 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++--+-- 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 = 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 f = unsafeLfpFrom bottom (\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 = 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 f = unsafeGfpFrom top (\x -> f x `meet` x)
+ Algebra/Lattice/Dropped.hs view
@@ -0,0 +1,34 @@+module Algebra.Lattice.Dropped (+    Dropped(..)+  ) where++import Algebra.Lattice++--+-- 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++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 view
@@ -0,0 +1,40 @@+module Algebra.Lattice.Levitated (+    Levitated(..)+  ) where++import Algebra.Lattice++--+-- 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++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 BoundedLattice a => BoundedLattice (Levitated a) where
+ Algebra/Lattice/Lifted.hs view
@@ -0,0 +1,34 @@+module Algebra.Lattice.Lifted (+    Lifted(..)+  ) where++import Algebra.Lattice++--+-- 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++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 view
@@ -0,0 +1,89 @@+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.Map as M+++-- | 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 (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where+    leq = M.isSubmapOf++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
+ LICENSE view
@@ -0,0 +1,22 @@+Copyright (c) 2010, Maximilian Bolingbroke+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted+provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright notice, this list of+      conditions and the following disclaimer.+    * Redistributions in binary form must reproduce the above copyright notice, this list of+      conditions and the following disclaimer in the documentation and/or other materials+      provided with the distribution.+    * Neither the name of Maximilian Bolingbroke nor the names of other contributors may be used to+      endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND+FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER+IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT+OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ lattices.cabal view
@@ -0,0 +1,21 @@+Name:               lattices+Version:            1.0+Cabal-Version:      >= 1.2+Category:           Math+Synopsis:           Fine-grained library for constructing and manipulating lattices+License:            BSD3+License-File:       LICENSE+Author:             Max Bolingbroke <batterseapower@hotmail.com>+Maintainer:         Max Bolingbroke <batterseapower@hotmail.com>+Build-Type:         Simple++Library+        Exposed-Modules: Algebra.Enumerable,+                         Algebra.Lattice,+                         Algebra.Lattice.Dropped,+                         Algebra.Lattice.Levitated,+                         Algebra.Lattice.Lifted,+                         Algebra.PartialOrd+                         +        Build-Depends:   base >= 3 && < 5,+                         containers >= 0.3 && < 0.4