From 6bebdddd649020c7e91b8fcec84aaff503666525 Mon Sep 17 00:00:00 2001 From: Michael Hanus Date: Thu, 4 Oct 2018 11:57:09 +0200 Subject: [PATCH] Adss example for non-equivalence of two non-deterministic insert operations --- examples/equivalent_operations/NDInsert.curry | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 examples/equivalent_operations/NDInsert.curry diff --git a/examples/equivalent_operations/NDInsert.curry b/examples/equivalent_operations/NDInsert.curry new file mode 100644 index 0000000..55adb61 --- /dev/null +++ b/examples/equivalent_operations/NDInsert.curry @@ -0,0 +1,25 @@ +--- Example to show the non-equivalence of two versions of a +--- non-deterministic insert operation. + +import Test.Prop + +-- Non-deterministic defined by overlapping rules: +ndinsert1 :: a -> [a] -> [a] +ndinsert1 x ys = x : ys +ndinsert1 x (y:ys) = y : ndinsert1 x ys + +-- Non-deterministic defined by non-overlapping rules: +ndinsert2 :: a -> [a] -> [a] +ndinsert2 x [] = [x] +ndinsert2 x (y:ys) = x : y : ys ? y : ndinsert2 x ys + +-- The equality of both ndinsert operations on ground values always succeeds: +ndinsert_groundequiv x xs = ndinsert1 x xs <~> ndinsert2 x xs + +-- Actually, ndinsert1 and ndinsert2 are not equivalent, as can be seen +-- by evaluating `head (ndinsert 1 failed)`. +-- Thus, we check the equivalence with CurryCheck: + +-- In PAKCS, the counter example is reported by the 7th test: +ndinsert_equiv = ndinsert1 <=> ndinsert2 + -- GitLab