Commit 36780534 authored by Sven Keidel's avatar Sven Keidel

add test to show unsoundness of fixpoint algorithm

parent d7dbe4c2
......@@ -4,11 +4,13 @@
{-# LANGUAGE StandaloneDeriving #-}
module Control.Arrow.Transformer.Fix where
import Prelude hiding ((.))
import Control.Arrow
import Control.Arrow.Class.Fix
import Control.Category
import Data.Order
import Data.Order
newtype Fix a b x y = Fix { runFix :: x -> y }
deriving (Arrow,ArrowChoice,ArrowApply)
......
......@@ -8,7 +8,7 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -DTRACE #-}
-- {-# OPTIONS_GHC -DTRACE #-}
module Control.Arrow.Transformer.FixpointCache(CacheArrow,runCacheArrow,runCacheArrow',liftCache) where
import Prelude hiding (id,(.),lookup)
......
......@@ -3,6 +3,7 @@
module Data.Boolean where
import qualified Prelude as P
import Data.Order
class Logic b where
true :: b
......@@ -25,22 +26,55 @@ instance Logic P.Bool where
not P.False = true
not P.True = false
data AbsBool = True | False | Top
data AbsBool = Bot | True | False | Top deriving (P.Eq)
instance P.Show AbsBool where
show Bot = "⊥"
show True = "True"
show False = "False"
show Top = "⊤"
instance Logic AbsBool where
true = True
false = False
and b1 b2 = case (b1,b2) of
(Bot,_) -> Bot
(_,Bot) -> Bot
(True,True) -> true
(False,_) -> false
(_,False) -> false
(_,_) -> Top
or b1 b2 = case (b1,b2) of
(Bot,_) -> Bot
(_,Bot) -> Bot
(True,_) -> true
(_,True) -> true
(False,False) -> false
(_,_) -> Top
not b = case b of
Bot -> Bot
True -> false
False -> true
Top -> Top
instance PreOrd AbsBool where
Bot _ = P.True
_ Top = P.True
True True = P.True
False False = P.True
_ _ = P.False
instance Complete AbsBool where
Bot b = b
b Bot = b
Top _ = Top
_ Top = Top
True True = True
False False = False
_ _ = Top
instance LowerBounded AbsBool where
bottom = Bot
instance UpperBounded AbsBool where
top = Top
......@@ -30,7 +30,10 @@ instance (Num n, Complete n, LowerBounded n, CoComplete n, UpperBounded n) => Nu
(*) = withBounds2 (*)
negate Bot = Bot
negate (Interval i1 i2) = Interval (negate i2) (negate i1)
abs = withBounds1 abs
abs Bot = Bot
abs (Interval i j)
| 0 i = Interval i j
| otherwise = Interval 0 (i j)
signum = withBounds1 signum
fromInteger = constant . fromInteger
......
......@@ -75,6 +75,7 @@ test-suite specs
build-depends: base,
hspec,
sturdy-lib,
hashable,
unordered-containers,
text
default-language: Haskell2010
......
......@@ -4,6 +4,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveGeneric #-}
module FixpointCacheSpec where
import Prelude hiding (lookup)
......@@ -16,10 +17,14 @@ import Control.Arrow.State
import Data.Interval (Interval)
import qualified Data.Interval as I
import Data.Sign (Sign)
import qualified Data.Sign as S
import Data.Order
import Data.Error
import Data.InfiniteNumbers
import qualified Data.Store as S
import Data.Boolean(AbsBool,Logic(..))
import Data.Hashable
import GHC.Generics
import Test.Hspec
......@@ -37,11 +42,11 @@ spec = do
let fib f =
ifLowerThan 0
(proc _ -> returnA -< 0)
(ifEq 1 (proc _ -> returnA -< 1)
(proc n -> do
x <- f -< n-1
y <- f -< n-2
returnA -< x + y))
(ifLowerThan 1 (proc _ -> returnA -< 1)
(proc n -> do
x <- f -< n-1
y <- f -< n-2
returnA -< x + y))
in it "should memoize numbers that have been computed before already" $ do
runCacheArrow (fixA fib :: Cache IV IV) (I.Interval 5 10) `shouldBe` I.Interval 5 55
......@@ -49,11 +54,46 @@ spec = do
describe "the analysis of the factorial function" $
let fact f = proc n -> do
ifLowerThan 0 (proc _ -> returnA -< 1)
ifLowerThan 1 (proc _ -> returnA -< 1)
(proc n -> do {x <- f -< (n-1); returnA -< n * x}) -< n
in it "fact [-∞,∞] should produce [1,∞]" $
runCacheArrow (fixA fact :: Cache IV IV) (I.Interval NegInfinity Infinity) `shouldBe` I.Interval 1 Infinity
describe "the analysis of foo" $
let foo :: Cache Sign Sign -> Cache Sign Sign
foo f = proc s -> case s of
S.Positive -> f -< S.Negative
S.Negative -> do
x <- f -< S.Positive
returnA -< S.Negative x
_ -> error "undefined" -< ()
in it "foo positive should produce top" $ do
pendingWith "Our optimization is unsound"
runCacheArrow (fixA foo :: Cache Sign Sign) S.Positive `shouldBe` S.Top
describe "the even and odd functions" $
let evenOdd :: Cache (EvenOdd,IV) AbsBool -> Cache (EvenOdd,IV) AbsBool
evenOdd f = proc (e,x) -> case e of
Even -> ifLowerThan 0 (proc _ -> returnA -< true)
(ifLowerThan 1 (proc _ -> returnA -< false)
(proc x -> f -< (Odd,x-1))) -< x
Odd -> ifLowerThan 0 (proc _ -> returnA -< false)
(ifLowerThan 1 (proc _ -> returnA -< true)
(proc x -> f -< (Even,x-1))) -< x
in it "even([-∞,∞]) should produce top" $
runCacheArrow (fixA evenOdd) (Even,I.Interval 0 Infinity) `shouldBe` top
describe "the ackermann function" $
let ackermann :: Cache (IV,IV) IV -> Cache (IV,IV) IV
ackermann f = proc (m,n) ->
ifLowerThan 0 (proc _ -> returnA -< n+1)
(proc m' -> ifLowerThan 0 (proc _ -> f -< (m'-1,1))
(proc n' -> do { x <- f -< (m,n'-1); f -< (m'-1,x)}) -<< n) -<< m
in it "ackerman ([0,∞], [0,∞]) should be [0,∞] " $
runCacheArrow (fixA ackermann) (I.Interval 0 Infinity,I.Interval 0 Infinity)
`shouldBe` I.Interval 1 Infinity
describe "the analyis of a diverging program" $
let diverge :: Cache Int Sign -> Cache Int Sign
diverge f = proc n -> case n of
......@@ -88,25 +128,19 @@ spec = do
`shouldBe` (S.fromList [((Number n,5- Number n),(10-Number n,())) | n <- [0..5]],(10,()))
where
ifEq :: (Num n, Ord n, ArrowChoice c, Complete (c (Interval n, Interval n) (Interval n)), Complete (c (Interval n,(Interval n, Interval n)) (Interval n))) => n -> c (Interval n) (Interval n) -> c (Interval n) (Interval n) -> c (Interval n) (Interval n)
ifEq l f g = proc b -> case b of
I.Bot -> returnA -< I.Bot
I.Interval m n
| m == l && n == l -> f -< b
| n < l || l < m -> g -< b
| otherwise -> joined f (joined g g) -< (I.Interval l l,(toBot $ I.Interval m (l-1), toBot $ I.Interval (l+1) n))
where
toBot :: Ord n => Interval n -> Interval n
toBot I.Bot = I.Bot
toBot x@(I.Interval m n)
| n < m = I.Bot
| otherwise = x
ifLowerThan :: (Num n, Ord n, ArrowChoice c, Complete (c (Interval n,Interval n) (Interval n))) => n -> c (Interval n) (Interval n) -> c (Interval n) (Interval n) -> c (Interval n) (Interval n)
ifLowerThan :: (Num n, Ord n, LowerBounded x, ArrowChoice c, Complete (c (Interval n,Interval n) x)) => n -> c (Interval n) x -> c (Interval n) x -> c (Interval n) x
ifLowerThan l f g = proc b -> case b of
I.Bot -> returnA -< I.Bot
I.Bot -> returnA -< bottom
I.Interval m n
| n <= l -> f -< b
| l < m -> g -< b
| otherwise -> joined f g -< (I.Interval m l, I.Interval (l+1) n)
| otherwise -> joined f g -< (toBot $ I.Interval m l, toBot $ I.Interval (l+1) n)
toBot :: Ord n => Interval n -> Interval n
toBot I.Bot = I.Bot
toBot x@(I.Interval m n)
| n < m = I.Bot
| otherwise = x
data EvenOdd = Even | Odd deriving (Eq,Generic,Show)
instance Hashable EvenOdd
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment