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