home *** CD-ROM | disk | FTP | other *** search
/ back2roots/padua / padua.7z / padua / lang / gofer223.lha / demos / lattice < prev    next >
Encoding:
Text File  |  1991-11-19  |  4.3 KB  |  134 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. --
  10.  
  11. class Eq a => Lattice a where           -- A type class representing lattices
  12.     bottom, top :: a
  13.     meet, join  :: a -> a -> a
  14.     lt          :: a -> a -> Bool
  15.     x `lt` y     = (x `join` y) == y
  16.  
  17. instance Lattice Bool where             -- Simple instances of Lattice
  18.     bottom = False
  19.     top    = True
  20.     meet   = (&&)
  21.     join   = (||)
  22.  
  23. instance (Lattice a, Lattice b) => Lattice (a,b) where
  24.     bottom             = (bottom,bottom)
  25.     top                = (top,top)
  26.     (x,y) `meet` (u,v) = (x `meet` u, y `meet` v)
  27.     (x,y) `join` (u,v) = (x `join` u, y `join` v)
  28.  
  29.  
  30. -- Defining the least fixed point operator:
  31.  
  32. fix f          = firstRepeat (iterate f bottom)
  33. firstRepeat xs = head [ x | (x,y) <- zip xs (tail xs), x==y ]
  34.  
  35.  
  36. -- Maximum and minimum frontiers:
  37.  
  38. data Minf a = Minf [a]
  39. data Maxf a = Maxf [a]
  40.  
  41. instance Eq a => Eq (Minf a) where                -- Equality on Frontiers
  42.     (Minf xs) == (Minf ys)  = setEquals xs ys
  43.  
  44. instance Eq a => Eq (Maxf a) where
  45.     (Maxf xs) == (Maxf ys)  = setEquals xs ys
  46.  
  47. xs `subset` ys  = all (`elem` ys) xs
  48. setEquals xs ys =  xs `subset` ys  &&  ys `subset` xs
  49.  
  50. instance Lattice a => Lattice (Minf a) where      -- Lattice structure
  51.     bottom                     = Minf []
  52.     top                        = Minf [bottom]
  53.     (Minf xs) `meet` (Minf ys) = minimal [ x`join`y | x<-xs, y<-ys ]
  54.     (Minf xs) `join` (Minf ys) = minimal (xs++ys)
  55.  
  56. instance Lattice a => Lattice (Maxf a) where
  57.     bottom                     = Maxf []
  58.     top                        = Maxf [top]
  59.     (Maxf xs) `meet` (Maxf ys) = maximal [ x`meet`y | x<-xs, y<-ys ]
  60.     (Maxf xs) `join` (Maxf ys) = maximal (xs++ys)
  61.  
  62. -- Find maximal elements of a list xs with respect to partial order po:
  63.  
  64. maximalWrt po = loop []
  65.  where loop xs []                 = xs
  66.        loop xs (y:ys)
  67.             | any (po y) (xs++ys) = loop xs ys
  68.             | otherwise           = loop (y:xs) ys
  69.  
  70. minimal :: Lattice a => [a] -> Minf a       -- list to minimum frontier
  71. minimal  = Minf . maximalWrt (flip lt)
  72. maximal :: Lattice a => [a] -> Maxf a       -- list to maximum frontier
  73. maximal  = Maxf . maximalWrt lt
  74.  
  75. -- A representation for functions of type Lattice a => a -> Bool:
  76.  
  77. data Fn a = Fn (Minf a) (Maxf a)
  78.  
  79. instance (Eq (Minf a), Eq (Maxf a)) => Eq (Fn a) where
  80.     Fn f1 f0 == Fn g1 g0  =  f1==g1 -- && f0==g0
  81.  
  82. instance (Lattice (Minf a), Lattice (Maxf a)) => Lattice (Fn a) where
  83.     bottom               = Fn bottom top
  84.     top                  = Fn top bottom
  85.     Fn u l `meet` Fn v m = Fn (u `meet` v) (l `join` m)
  86.     Fn u l `join` Fn v m = Fn (u `join` v) (l `meet` m)
  87.  
  88. -- Navigable lattices:
  89.  
  90. class (Lattice (Minf a), Lattice (Maxf a)) => Navigable a where
  91.     succs :: a -> Minf a
  92.     preds :: a -> Maxf a
  93.  
  94. maxComp :: Navigable a => [a] -> Maxf a   -- implementation of complement
  95. maxComp  = foldr meet top . map preds
  96. minComp :: Navigable a => [a] -> Minf a
  97. minComp  = foldr meet top . map succs
  98.  
  99. instance Navigable Bool where             -- instances of Navigable
  100.     succs False = Minf [True]
  101.     succs True  = Minf []
  102.     preds False = Maxf []
  103.     preds True  = Maxf [False]
  104.  
  105. instance (Navigable a, Navigable b) => Navigable (a,b) where
  106.     succs (x,y) = Minf ([(sx,bottom) | Minf xs = succs x, sx<-xs] ++
  107.                         [(bottom,sy) | Minf ys = succs y, sy<-ys])
  108.     preds (x,y) = Maxf ([(px,top)    | Maxf xs = preds x, px<-xs] ++
  109.                         [(top,py)    | Maxf ys = preds y, py<-ys])
  110.  
  111. instance Navigable a => Navigable (Fn a) where
  112.     succs (Fn f1 f0) = Minf [Fn (Minf [y]) (preds y) | Maxf ys = f0, y<-ys]
  113.     preds (Fn f1 f0) = Maxf [Fn (succs x) (Maxf [x]) | Minf xs = f1, x<-xs]
  114.  
  115. -- Upwards and downwards closure operators:
  116.  
  117. upwards (Minf [])         = []
  118. upwards ts@(Minf (t:_))   = t : upwards (ts `meet` succs t)
  119.  
  120. downwards (Maxf [])       = []
  121. downwards ts@(Maxf (t:_)) = t : downwards (ts `meet` preds t)
  122.  
  123. elements :: Navigable a => [a]    -- enumerate all elements in lattice
  124. elements  = upwards top
  125.  
  126. -- Dual lattices:
  127.  
  128. class (Lattice a, Lattice b, Dual b a) => Dual a b where
  129.     comp :: a -> b
  130.  
  131. instance Dual Bool Bool where
  132.     comp = not
  133.  
  134.