Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Add new ways of computing fixed points of lattices, fix bugs in the P…

…artialOrd instances for maps
  • Loading branch information...
commit bed09ab599c1c460e2b34a3e57ec613e9d17a8a9 1 parent de8aba1
@batterseapower authored
Showing with 29 additions and 9 deletions.
  1. +19 −7 Algebra/Lattice.hs
  2. +9 −1 Algebra/PartialOrd.hs
  3. +1 −1  lattices.cabal
View
26 Algebra/Lattice.hs
@@ -9,12 +9,12 @@ module Algebra.Lattice (
joins, meets,
-- * Fixed points of chains in lattices
- lfp, unsafeLfp,
- gfp, unsafeGfp,
+ lfp, lfpFrom, unsafeLfp,
+ gfp, gfpFrom, unsafeGfp,
) where
import Algebra.Enumerable
-import Algebra.PartialOrd
+import qualified Algebra.PartialOrd as PO
import qualified Data.Set as S
import qualified Data.IntSet as IS
@@ -210,23 +210,35 @@ instance BoundedLattice Bool where
-- 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
+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 f = unsafeLfpFrom bottom (\x -> f x `join` x)
+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 = unsafeGfpFrom top
+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 f = unsafeGfpFrom top (\x -> f x `meet` x)
+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)
View
10 Algebra/PartialOrd.hs
@@ -11,7 +11,9 @@ module Algebra.PartialOrd (
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>
@@ -38,8 +40,14 @@ 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
- leq = M.isSubmapOf
+ 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
View
2  lattices.cabal
@@ -1,5 +1,5 @@
Name: lattices
-Version: 1.1
+Version: 1.2
Cabal-Version: >= 1.2
Category: Math
Synopsis: Fine-grained library for constructing and manipulating lattices
Please sign in to comment.
Something went wrong with that request. Please try again.