home *** CD-ROM | disk | FTP | other *** search
/ PSION CD 2 / PsionCDVol2.iso / Programs / 876 / hugs.sis / Lattice.hs < prev    next >
Encoding:
Text File  |  2000-09-21  |  4.1 KB  |  127 lines
  1. -- This file contains a Hugs implementation of the programs described in:
  2. --
  3. -- Mark P. Jones, Computing with lattices: An application of type classes,
  4. -- Journal of Functional Programming, Volume 2, Number 4, Oct 1992.
  5. --
  6.  
  7. module Lattice where
  8.  
  9. class Eq a => Lattice a where           -- A type class representing lattices
  10.     bottom, top :: a
  11.     meet, join  :: a -> a -> a
  12.     lt          :: a -> a -> Bool
  13.     x `lt` y     = (x `join` y) == y
  14.  
  15. instance Lattice Bool where             -- Simple instances of Lattice
  16.     bottom = False
  17.     top    = True
  18.     meet   = (&&)
  19.     join   = (||)
  20.  
  21. instance (Lattice a, Lattice b) => Lattice (a,b) where
  22.     bottom             = (bottom,bottom)
  23.     top                = (top,top)
  24.     (x,y) `meet` (u,v) = (x `meet` u, y `meet` v)
  25.     (x,y) `join` (u,v) = (x `join` u, y `join` v)
  26.  
  27.  
  28. -- Defining the least fixed point operator:
  29.  
  30. fix f          = firstRepeat (iterate f bottom)
  31. firstRepeat xs = head [ x | (x,y) <- zip xs (tail xs), x==y ]
  32.  
  33.  
  34. -- Maximum and minimum frontiers:
  35.  
  36. data Minf a = Minf [a]
  37. data Maxf a = Maxf [a]
  38.  
  39. instance Eq a => Eq (Minf a) where                -- Equality on Frontiers
  40.     (Minf xs) == (Minf ys)  = setEquals xs ys
  41.  
  42. instance Eq a => Eq (Maxf a) where
  43.     (Maxf xs) == (Maxf ys)  = setEquals xs ys
  44.  
  45. xs `subset` ys  = all (`elem` ys) xs
  46. setEquals xs ys =  xs `subset` ys  &&  ys `subset` xs
  47.  
  48. instance Lattice a => Lattice (Minf a) where      -- Lattice structure
  49.     bottom                     = Minf []
  50.     top                        = Minf [bottom]
  51.     (Minf xs) `meet` (Minf ys) = minimal [ x`join`y | x<-xs, y<-ys ]
  52.     (Minf xs) `join` (Minf ys) = minimal (xs++ys)
  53.  
  54. instance Lattice a => Lattice (Maxf a) where
  55.     bottom                     = Maxf []
  56.     top                        = Maxf [top]
  57.     (Maxf xs) `meet` (Maxf ys) = maximal [ x`meet`y | x<-xs, y<-ys ]
  58.     (Maxf xs) `join` (Maxf ys) = maximal (xs++ys)
  59.  
  60. -- Find maximal elements of a list xs with respect to partial order po:
  61.  
  62. maximalWrt po = loop []
  63.  where loop xs []                 = xs
  64.        loop xs (y:ys)
  65.             | any (po y) (xs++ys) = loop xs ys
  66.             | otherwise           = loop (y:xs) ys
  67.  
  68. minimal :: Lattice a => [a] -> Minf a       -- list to minimum frontier
  69. minimal  = Minf . maximalWrt (flip lt)
  70. maximal :: Lattice a => [a] -> Maxf a       -- list to maximum frontier
  71. maximal  = Maxf . maximalWrt lt
  72.  
  73. -- A representation for functions of type Lattice a => a -> Bool:
  74.  
  75. data Fn a = Fn (Minf a) (Maxf a)
  76.  
  77. instance Eq a => Eq (Fn a) where
  78.     Fn f1 f0 == Fn g1 g0  =  f1==g1 -- && f0==g0
  79.  
  80. instance Lattice a => Lattice (Fn a) where
  81.     bottom               = Fn bottom top
  82.     top                  = Fn top bottom
  83.     Fn u l `meet` Fn v m = Fn (u `meet` v) (l `join` m)
  84.     Fn u l `join` Fn v m = Fn (u `join` v) (l `meet` m)
  85.  
  86. -- Navigable lattices:
  87.  
  88. class Lattice a => Navigable a where
  89.     succs :: a -> Minf a
  90.     preds :: a -> Maxf a
  91.  
  92. maxComp :: Navigable a => [a] -> Maxf a   -- implementation of complement
  93. maxComp  = foldr meet top . map preds
  94. minComp :: Navigable a => [a] -> Minf a
  95. minComp  = foldr meet top . map succs
  96.  
  97. instance Navigable Bool where             -- instances of Navigable
  98.     succs False = Minf [True]
  99.     succs True  = Minf []
  100.     preds False = Maxf []
  101.     preds True  = Maxf [False]
  102.  
  103. minfOf (Minf xs) = xs
  104. maxfOf (Maxf xs) = xs
  105.  
  106. instance (Navigable a, Navigable b) => Navigable (a,b) where
  107.     succs (x,y) = Minf ([(sx,bottom) | sx <- minfOf (succs x)] ++
  108.                         [(bottom,sy) | sy <- minfOf (succs y)])
  109.     preds (x,y) = Maxf ([(px,top)    | px <- maxfOf (preds x)] ++
  110.                         [(top,py)    | py <- maxfOf (preds y)])
  111.  
  112. instance Navigable a => Navigable (Fn a) where
  113.     succs (Fn f1 f0) = Minf [Fn (Minf [y]) (preds y) | y <- maxfOf f0]
  114.     preds (Fn f1 f0) = Maxf [Fn (succs x) (Maxf [x]) | x <- minfOf f1]
  115.  
  116. -- Upwards and downwards closure operators:
  117.  
  118. upwards (Minf [])         = []
  119. upwards ts@(Minf (t:_))   = t : upwards (ts `meet` succs t)
  120.  
  121. downwards (Maxf [])       = []
  122. downwards ts@(Maxf (t:_)) = t : downwards (ts `meet` preds t)
  123.  
  124. elements :: Navigable a => [a]    -- enumerate all elements in lattice
  125. elements  = upwards top
  126.  
  127.