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