Example added

examples/equivalent_operations/Intersperse.curry

+--- 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

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)

examples/equivalent_operations/Take.curry

 --- 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