From 0678899f5c50949b4bdbb89b05895f9ebf0e1239 Mon Sep 17 00:00:00 2001
From: Michael Hanus
Date: Wed, 7 Nov 2018 11:30:32 +0100
Subject: [PATCH] Example added
---
.../equivalent_operations/Intersperse.curry | 26 +++++++++++++++++++
examples/equivalent_operations/README.md | 4 ++-
examples/equivalent_operations/Take.curry | 6 ++++-
3 files changed, 34 insertions(+), 2 deletions(-)
create mode 100644 examples/equivalent_operations/Intersperse.curry
diff --git a/examples/equivalent_operations/Intersperse.curry b/examples/equivalent_operations/Intersperse.curry
new file mode 100644
index 0000000..1d93da8
--- /dev/null
+++ b/examples/equivalent_operations/Intersperse.curry
@@ -0,0 +1,26 @@
+--- Example from:
+---
+--- Christiansen, J. and Seidel, D.: Minimally strict polymorphic functions
+--- Proc. of the 13th International Symposium on Principle and Practice
+--- of Declarative Programming (PPDP'11), pp. 53-64
+--- DOI: 10.1145/2003476.2003487
+
+import Test.Prop
+
+--- Definition of `intersperse` from module `List`.
+intersperse1 :: a -> [a] -> [a]
+intersperse1 _ [] = []
+intersperse1 _ [x] = [x]
+intersperse1 sep (x:xs@(_:_)) = x : sep : intersperse1 sep xs
+
+--- Less strict definition.
+intersperse2 :: a -> [a] -> [a]
+intersperse2 _ [] = []
+intersperse2 sep (x:xs) = x : go xs
+ where
+ go [] = []
+ go (y:ys) = sep : y : go ys
+
+
+-- These operations are not equivalent:
+intersperseEquiv = intersperse1 <=> intersperse2
diff --git a/examples/equivalent_operations/README.md b/examples/equivalent_operations/README.md
index b77bc3b..cc8957d 100644
--- a/examples/equivalent_operations/README.md
+++ b/examples/equivalent_operations/README.md
@@ -4,12 +4,14 @@ of CurryCheck to check the equivalence of operations.
Since most of these are examples to test whether CurryCheck
is able to report counter-examples, their test fails intentionally.
These are the programs
+- Intersperse (inserting separators in a list [Christiansen/Seidel'11])
- Ints12 (generators for infinite lists)
- NDInsert (non-deterministic list insertion)
- RevRev (double reverse)
- SimpleExample
- SortEquiv (two variants of permutation sort)
-- Take (two variants of take)
+- Take (two variants of take [Foner/Zhang/Lampropoulos'18])
+- Unzip (two variants of unzip [Chitil'11])
The following programs contain successful equivalence tests:
- Fac (recursive specification of factorial vs. iterative implementation)
diff --git a/examples/equivalent_operations/Take.curry b/examples/equivalent_operations/Take.curry
index a42731b..b13abfb 100644
--- a/examples/equivalent_operations/Take.curry
+++ b/examples/equivalent_operations/Take.curry
@@ -1,5 +1,9 @@
--- Example to show the non-equivalence of two versions of the
---- `take` operation.
+--- `take` operation, taken from
+---
+--- Foner, K. and Zhang, H. and Lampropoulos, L.: {Keep Your Laziness in Check
+--- ICFP 2018,
+--- DOI: 10.1145/3236797
import Test.Prop
--
GitLab