Commit 4637c6ad authored by Michael Hanus 's avatar Michael Hanus

Examples for non-equivalences added

parent 264273cf
--- Example from:
---
--- Christiansen, J.: Sloth - A Tool for Checking Minimal-Strictness
--- Proc. of the 13th International Symposium on Practical Aspects of
--- Declarative Languages (PADL 2011), pp. 160-174
--- DOI: 10.1007/978-3-642-18378-2_14
import Test.Prop
-- from package BinInt:
--- Algebraic data type to represent natural numbers.
--- @cons IHi - most significant bit
--- @cons O - multiply with 2
--- @cons I - multiply with 2 and add 1
data Nat = IHi | O Nat | I Nat
deriving (Eq,Show)
--- Successor, O(n)
succ :: Nat -> Nat
succ IHi = O IHi -- 1 + 1 = 2
succ (O bs) = I bs -- 2*n + 1 = 2*n + 1
succ (I bs) = O (succ bs) -- 2*n + 1 + 1 = 2*(n+1)
--- Addition, O(max (m, n))
(+^) :: Nat -> Nat -> Nat
IHi +^ y = succ y -- 1 + n = n + 1
O x +^ IHi = I x -- 2*n + 1 = 2*n + 1
O x +^ O y = O (x +^ y) -- 2*m + 2*n = 2*(m+n)
O x +^ I y = I (x +^ y)
I x +^ IHi = O (succ x)
I x +^ O y = I (x +^ y)
I x +^ I y = O (succ x +^ y)
--- Multiplication, O(m*n)
mult :: Nat -> Nat -> Nat
mult IHi y = y
mult (O x) y = O (mult x y)
mult (I x) y = y +^ (O (mult x y))
--- Multiplication, O(m*n)
mult' :: Nat -> Nat -> Nat
mult' IHi y = y
mult' (O x) y = O (mult' x y)
mult' (I x) y = (O (mult' y x)) +^ y
-- These operations are not equivalent (falsified at 1041th test):
multEquiv = mult <=> mult'
-- These operations are not equivalent (falsified at 42th test):
multEquiv'TERMINATE = mult <=> mult'
-- Ground equivalence testing is successful:
multEquiv'GROUND x y = mult x y <~> mult' x y
--- Example from:
---
--- Christiansen, J.: Sloth - A Tool for Checking Minimal-Strictness
--- Proc. of the 13th International Symposium on Practical Aspects of
--- Declarative Languages (PADL 2011), pp. 160-174
--- DOI: 10.1007/978-3-642-18378-2_14
import Test.Prop
-- Peano numbers
data Nat = Z | S Nat
deriving (Eq, Show)
--- Addition
add :: Nat -> Nat -> Nat
add Z y = y
add (S x ) y = S (add x y)
--- "Standard" definition of multiplication.
mult :: Nat -> Nat -> Nat
mult Z _ = Z
mult (S x) y = add y (mult x y)
-- An infinite Peano number.
infinity :: Nat
infinity = S infinity
-- mult Z infinity --> Z
-- mult infinity Z --> does not terminate
-- Less strict definition of multiplication.
mult' :: Nat -> Nat -> Nat
mult' Z _ = Z
mult' (S _) Z = Z
mult' (S x) y@(S _) = add y (mult' x y)
-- These operations are not equivalent (falsified at 24th test):
multEquiv = mult <=> mult'
-- These operations are not equivalent (falsified at 9th test):
multEquiv'TERMINATE = mult <=> mult'
-- Ground equivalence testing is successful:
multEquiv'GROUND x y = mult x y <~> mult' x y
-- Testing the equivalence of non-terminating operations:
import Test.Prop
-- Two different infinite lists:
primes :: [Int]
primes = sieve [2..]
where sieve (x:xs) = x : sieve (filter (\y -> y `mod` x > 0) xs)
dummy_primes :: [Int]
dummy_primes = 2 : [3,5..]
-- This property will be falsified by the 38th test:
primes_equiv'PRODUCTIVE = primes <=> dummy_primes
......@@ -10,8 +10,11 @@ These are the programs
- BacciEtAl12 (simple example from Bacci et al PPDP'12)
- Intersperse (inserting separators in a list [Christiansen/Seidel'11])
- Ints12 (generators for infinite lists)
- MultBin (multiplication on a binary representation of natural numbers)
- MultPeano (multiplication on Peano numbers)
- NDInsert (non-deterministic list insertion)
- Perm (permutation from library Combinatorial vs. less strict version)
- Primes (computing an infinite list of all prime numbers)
- RevRev (double reverse)
- SortEquiv (two variants of permutation sort)
- SortPermute (two variants of permutation sort with a stricter permutation)
......
......@@ -31,8 +31,8 @@ isort xs = idSorted (perm xs)
-- to avoid error message w.r.t. polymorphic types with unspecifed type class
-- contexts):
-- In PAKCS, the counter example is reported by the 274th test:
psort_equiv_isort'PRODUCTIVE = psort <=> (isort :: [Int] -> [Int])
-- In PAKCS, the counter example is reported by the 89th test:
psort_equiv_isort'PRODUCTIVE = psort <=> (isort :: [Ordering] -> [Ordering])
-- In PAKCS, the counter example is reported by the 21th test:
psort_equiv_isort'TERMINATE = psort <=> (isort :: [Int] -> [Int])
-- In PAKCS, the counter example is reported by the 11th test:
psort_equiv_isort'TERMINATE = psort <=> (isort :: [Ordering] -> [Ordering])
......@@ -18,7 +18,7 @@ permute (x:xs) = ndinsert (permute xs)
sorted :: Ord a => [a] -> Bool
sorted [] = True
sorted [_] = True
sorted (x:y:zs) = x<=y && sorted (y:zs)
sorted (x:xs@(y:_)) = x<=y && sorted xs
psort :: Ord a => [a] -> [a]
psort xs | sorted ys = ys where ys = permute xs
......@@ -28,7 +28,7 @@ psort xs | sorted ys = ys where ys = permute xs
idSorted :: Ord a => [a] -> [a]
idSorted [] = []
idSorted [x] = [x]
idSorted (x:y:zs) | x<=y = x : idSorted (y:zs)
idSorted (x:xs@(y:_)) | x<=y = x : idSorted xs
isort :: Ord a => [a] -> [a]
isort xs = idSorted (permute xs)
......
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