packages feed

lawz (empty) → 0.0.1

raw patch · 21 files changed

+495/−0 lines, 21 filesdep +base

Dependencies added: base

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for properties++## 0.0.1  -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2019, Chris McKinlay++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Chris McKinlay nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ lawz.cabal view
@@ -0,0 +1,46 @@+name:                lawz+version:             0.0.1+synopsis:            Common mathematical laws.+description:         Library of predicates for property testing.+homepage:            https://github.com/cmk/lawz+license:             BSD3+license-file:        LICENSE+author:              Chris McKinlay+maintainer:          chris.mckinlay@gmail.com+category:            Testing, Math+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10++library+  exposed-modules:+     Test.Relation+     Test.Relation.Connex+     Test.Relation.Reflexive+     Test.Relation.Symmetric+     Test.Relation.Transitive+     Test.Function+     Test.Function.Equivalent+     Test.Function.Idempotent+     Test.Function.Injective+     Test.Function.Invertible+     Test.Function.Monotone+     Test.Operation+     Test.Operation.Annihilative+     Test.Operation.Associative+     Test.Operation.Commutative+     Test.Operation.Distributive+     Test.Operation.Neutral+     Test.Util++  default-extensions:+     FlexibleInstances+     RankNTypes+     ScopedTypeVariables+     TypeApplications++  build-depends:       +      base <5.0++  hs-source-dirs:      src+  default-language:    Haskell2010
+ src/Test/Function.hs view
@@ -0,0 +1,7 @@+module Test.Function (module Export) where++import Test.Function.Equivalent as Export+import Test.Function.Idempotent as Export+import Test.Function.Injective  as Export+import Test.Function.Invertible as Export+import Test.Function.Monotone   as Export
+ src/Test/Function/Equivalent.hs view
@@ -0,0 +1,16 @@+module Test.Function.Equivalent where++import Test.Util++++-- | \( \forall a: f a \equiv g a \)+--+equivalent :: Eq r => (r -> r) -> (r -> r) -> (r -> Bool)+equivalent = equivalent_on (==)+++-- | \( \forall a: f a \doteq g a \)+--+equivalent_on :: Rel r -> (r -> r) -> (r -> r) -> (r -> Bool)+equivalent_on (~~) f g a = f a ~~ g a
+ src/Test/Function/Idempotent.hs view
@@ -0,0 +1,29 @@+module Test.Function.Idempotent where++import Data.List (unfoldr)+import Numeric.Natural (Natural(..))+import Test.Util++-- | \( \forall a: g \circ f (a) = f (a) \)+--+projective :: Eq r => (r -> r) -> (r -> r) -> r -> Bool+projective = projective_on (==)++-- | \( \forall a: g \circ f (a) \sim f (a) \)+--+projective_on :: Rel s -> (r -> s) -> (s -> s) -> r -> Bool+projective_on (~~) f g r = g (f r) ~~ f r++-- | \( \forall a: f \circ f(a) = f(a) \)+--+idempotent :: Eq r => (r -> r) -> r -> Bool+idempotent f = idempotent_on (==) f++-- | \( \forall a: f \circ f(a) \sim f(a) \)+--+idempotent_on :: Rel r -> (r -> r) -> r -> Bool+idempotent_on (~~) f = projective_on (~~) f f++idempotent_k :: Eq r => Natural -> (r -> r) -> r -> Bool+idempotent_k k f r = k >= 1 ==> foldr (.) id fs r == f r+  where fs = (`unfoldr` k) $ \m -> if m==1 then Nothing else Just (f,m-1)
+ src/Test/Function/Injective.hs view
@@ -0,0 +1,14 @@+module Test.Function.Injective where++import Test.Util++-- | \( \forall a: f a \equiv f b \Rightarrow a \equiv b \)+--+injective :: Eq r => (r -> r) -> r -> r -> Bool+injective = injective_on (==)+++-- | \( \forall a: f a \doteq f b \Rightarrow a \doteq b \)+--+injective_on :: Rel r -> (r -> r) -> r -> r -> Bool+injective_on (~~) f a b = (f a ~~ f b) ==> (a ~~ b)
+ src/Test/Function/Invertible.hs view
@@ -0,0 +1,21 @@+module Test.Function.Invertible where++import Test.Util+++-- | \( \forall a: f a \# b \Leftrightarrow a \# g b \)+--+-- For example, a Galois connection is defined by @adjoint_on (<=)@.+--+adjoint_on :: Rel r -> Rel s -> (s -> r) -> (r -> s) -> (s -> r -> Bool)+adjoint_on (#) (%) f g a b = f a # b <==> a % g b++-- | \( \forall a: f (g a) \equiv a \)+--+invertible :: Eq r => (r -> s) -> (s -> r) -> (r -> Bool)+invertible = invertible_on (==)++-- | \( \forall a: f (g a) \doteq a \)+--+invertible_on :: Rel s -> (s -> r) -> (r -> s) -> (s -> Bool)+invertible_on (~~) f g a = g (f a) ~~ a
+ src/Test/Function/Monotone.hs view
@@ -0,0 +1,20 @@+module Test.Function.Monotone where++import Test.Util++monotone :: Ord r => (r -> r) -> r -> r -> Bool+monotone = monotone_on (<=) (<=)++-- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \)+--+monotone_on :: Rel r -> Rel s -> (r -> s) -> r -> r -> Bool+monotone_on (#) (%) f a b = a # b ==> f a % f b++antitone :: Ord r => (r -> r) -> r -> r -> Bool+antitone = antitone_on (<=) (<=)++-- | \( \forall a, b: a \leq b \Rightarrow f(b) \leq f(a) \)+--+antitone_on :: Rel r -> Rel s -> (r -> s) -> r -> r -> Bool+antitone_on (#) (%) f a b = a # b ==> f b % f a+
+ src/Test/Operation.hs view
@@ -0,0 +1,7 @@+module Test.Operation (module Export) where++import Test.Operation.Annihilative as Export+import Test.Operation.Associative  as Export+import Test.Operation.Commutative  as Export+import Test.Operation.Distributive as Export+import Test.Operation.Neutral      as Export
+ src/Test/Operation/Annihilative.hs view
@@ -0,0 +1,28 @@+module Test.Operation.Annihilative where++import Test.Util+++-- | \( \forall a: (u \# a) \equiv u \)+--+-- Right annihilativity of an element /u/ with respect to an operator /#/.+--+-- For example, @False@ is a right annihilative element of @||@.+--+annihilative :: Eq r => (r -> r -> r) -> r -> (r -> Bool)+annihilative = annihilative_on (==)++-- | \( \forall a: (a \# u) \equiv u \)+--+-- Left annihilativity of an element /u/ with respect to an operator /#/.+--+-- For example, @Nothing@ is a right annihilative element of @*>@.+--+annihilative' :: Eq r => (r -> r -> r) -> r -> (r -> Bool)+annihilative' = annihilative_on' (==)++annihilative_on :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)+annihilative_on (~~) (#) u a = (u # a) ~~ u++annihilative_on' :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)+annihilative_on' (~~) (#) u a = (a # u) ~~ u
+ src/Test/Operation/Associative.hs view
@@ -0,0 +1,15 @@+module Test.Operation.Associative where++import Test.Util+++-- | \( \forall a, b, c: (a \# b) \# c \equiv a \# (b \# c) \)+--+associative :: Eq r => (r -> r -> r) -> (r -> r -> r -> Bool)+associative = associative_on (==)+++-- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \)+--+associative_on :: Rel r -> (r -> r -> r) -> (r -> r -> r -> Bool)+associative_on (~~) (#) a b c = ((a # b) # c) ~~ (a # (b # c))
+ src/Test/Operation/Commutative.hs view
@@ -0,0 +1,14 @@+module Test.Operation.Commutative where++import Test.Util++-- | \( \forall a, b: a \# b \equiv b \# a \)+--+commutative :: Eq r => (r -> r -> r) -> r -> r -> Bool+commutative = commutative_on (==)++-- | \( \forall a, b: a \# b \doteq b \# a \)+--+commutative_on :: Rel r -> (r -> r -> r) -> r -> r -> Bool+commutative_on (~~) (#) a b = (a # b) ~~ (b # a)+
+ src/Test/Operation/Distributive.hs view
@@ -0,0 +1,20 @@+module Test.Operation.Distributive where++import Test.Util+++-- | \( \forall a, b, c: (a \# b) \% c \equiv (a \% c) \# (b \% c) \)+--+distributive :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)+distributive = distributive_on (==)++-- | \( \forall a, b, c: c \% (a \# b) \equiv (c \% a) \# (c \% b) \)+--+distributive' :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)+distributive' = distributive_on' (==)++distributive_on :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)+distributive_on (~~) (#) (%) a b c = ((a # b) % c) ~~ ((a % c) # (b % c))++distributive_on' :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)+distributive_on' (~~) (#) (%) a b c = (c % (a # b)) ~~ ((c % a) # (c % b))
+ src/Test/Operation/Neutral.hs view
@@ -0,0 +1,27 @@+module Test.Operation.Neutral where++import Test.Util++-- | \( \forall a: (u \# a) \equiv a \)+--+-- Right neutrality of a unit /u/ with respect to an operator /#/.+--+-- For example, an implementation of 'Monoid' must satisfy @neutral (<>) mempty@+--+neutral :: Eq r => (r -> r -> r) -> r -> (r -> Bool)+neutral = neutral_on (==)++-- | \( \forall a: (a \# u) \equiv a \)+--+-- Left neutrality of a unit /u/ with respect to an operator /#/.+--+-- For example, an implementation of 'Monoid' must satisfy @neutral (<>) mempty@+--+neutral' :: Eq r => (r -> r -> r) -> r -> (r -> Bool)+neutral' = neutral_on' (==)++neutral_on :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)+neutral_on (~~) (#) u a = (u # a) ~~ a++neutral_on' :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)+neutral_on' (~~) (#) u a = (a # u) ~~ a
+ src/Test/Relation.hs view
@@ -0,0 +1,6 @@+module Test.Relation (module Export) where++import Test.Relation.Connex     as Export+import Test.Relation.Reflexive  as Export+import Test.Relation.Symmetric  as Export+import Test.Relation.Transitive as Export
+ src/Test/Relation/Connex.hs view
@@ -0,0 +1,47 @@+-- | See <https://en.wikipedia.org/wiki/Connex_relation>.+module Test.Relation.Connex where++import Test.Util++-- | \( \forall a, b: ((a \# b) \vee (b \# a)) \)+--+-- For example, ≥ is a connex relation, while 'divides evenly' is not.+-- +-- A connex relation cannot be symmetric, except for the universal relation.+--+connex :: (r -> r -> Bool) -> r -> r -> Bool+connex (#) a b = (a # b) || (b # a)+++-- | \( \forall a, b: \neg (a \equiv b) \Rightarrow ((a \# b) \vee (b \# a)) \)+--+-- A binary relation is semiconnex if it relates all pairs of _distinct_ elements in some way.+--+-- A relation is connex if and only if it is semiconnex and reflexive.+--+semiconnex :: Eq r => (r -> r -> Bool) -> r -> r -> Bool+semiconnex = semiconnex_on (==)+++-- | \( \forall a, b: \neg (a \doteq b) \Rightarrow ((a \# b) \vee (b \# a)) \)+--+semiconnex_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool+semiconnex_on (~~) (#) a b = not (a ~~ b) ==> connex (#) a b+++-- | \( \forall a, b, c: ((a \# b) \vee (a \equiv b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \equiv b) \wedge (b \# a)) \)+--+-- Note that @ trichotomous (>) @ should hold for any 'Ord' instance.+--+trichotomous :: Eq r => (r -> r -> Bool) -> r -> r -> Bool+trichotomous = trichotomous_on (==)+++-- | \( \forall a, b, c: ((a \# b) \vee (a \doteq b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \doteq b) \wedge (b \# a)) \)+--+-- In other words, exactly one of \(a \# b\), \(a \doteq b\), or \(b \# a\) holds.+-- 	+-- For example, > is a trichotomous relation, while ≥ is not.+--+trichotomous_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool+trichotomous_on (~~) (#) a b = xor3 (a # b) (a ~~ b) (b # a)
+ src/Test/Relation/Reflexive.hs view
@@ -0,0 +1,51 @@+-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.+-- +-- Note that these properties do not exhaust all of the possibilities.+--+-- For example, the relation \( y = x^2 \) is neither irreflexive, +-- nor coreflexive, nor reflexive, since it contains the pairs+-- \( (0, 0) \) and \( (2, 4) \), but not \( (2, 2) \).+--+--  The latter two facts also rule out quasi-reflexivity.+module Test.Relation.Reflexive where++import Test.Util+++-- | \( \forall a: (a \# a) \)+--+-- For example, ≥ is a reflexive relation but > is not.+--+reflexive :: (r -> r -> Bool) -> (r ->  Bool)+reflexive (#) a = a # a +++-- | \( \forall a: \neg (a \# a) \)+--+-- For example, > is an irreflexive relation, but ≥ is not.+--+irreflexive :: (r -> r -> Bool) -> (r ->  Bool)+irreflexive (#) a = not $ a # a+++-- | \( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \equiv b) \)+--+-- For example, the relation over the integers in which each odd number is +-- related to itself is a coreflexive relation. The equality relation is the +-- only example of a relation that is both reflexive and coreflexive, and any +-- coreflexive relation is a subset of the equality relation.+--+coreflexive :: Eq r => (r -> r -> Bool) -> (r -> r -> Bool)+coreflexive = coreflexive_on (==)+++-- | \( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \doteq b) \)+--+coreflexive_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> (r -> r -> Bool)+coreflexive_on (~~) (#) a b = (a # b) && (b # a) ==> (a ~~ b)+++-- | \( \forall a, b: (a \# b) \Rightarrow ((a \# a) \wedge (b \# b)) \)+--+quasireflexive :: (r -> r -> Bool) -> (r -> r -> Bool)+quasireflexive (#) a b = (a # b) ==> (a # a) && (b # b)
+ src/Test/Relation/Symmetric.hs view
@@ -0,0 +1,43 @@+-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.+--+-- Note that these properties do not exhaust all of the possibilities.+--+-- As an example over the natural numbers, the relation \(a \# b \) defined by +-- \( a > 2 \) is neither symmetric nor antisymmetric, let alone asymmetric.+module Test.Relation.Symmetric where++import Test.Util+++-- | \( \forall a, b: (a \# b) \Leftrightarrow (b \# a) \)+--+-- For example, "is a blood relative of" is a symmetric relation, because +-- A is a blood relative of B if and only if B is a blood relative of A.+--+symmetric :: (r -> r -> Bool) -> r -> r -> Bool+symmetric (#) a b = (a # b) <==> (b # a)+++-- | \( \forall a, b: (a \# b) \Rightarrow \neg (b \# a) \)+--+-- For example, > is an asymmetric relation, but ≥ is not.+--+-- A relation is asymmetric if and only if it is both antisymmetric and irreflexive.+-- +asymmetric :: (r -> r -> Bool) -> r -> r -> Bool+asymmetric (#) a b = (a # b) ==> not (b # a)+++-- | \( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \equiv b \)+--+-- For example, ≥ is an antisymmetric relation; so is >, but vacuously +-- (the condition in the definition is always false).+-- +antisymmetric :: Eq r => (r -> r -> Bool) -> r -> r -> Bool+antisymmetric = antisymmetric_on (==)+++-- | \( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \doteq b \)+-- +antisymmetric_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool+antisymmetric_on (~~) (#) a b = (a # b) && (b # a) ==> (a ~~ b)
+ src/Test/Relation/Transitive.hs view
@@ -0,0 +1,27 @@+module Test.Relation.Transitive where++import Test.Util+++-- | \( \forall a, b, c: ((a \# b) \wedge (b \# c)) \Rightarrow (a \# c) \)+--+-- For example, "is ancestor of" is a transitive relation, while "is parent of" is not.+--+transitive :: (r -> r -> Bool) -> r -> r -> r -> Bool+transitive (#) a b c = (a # b) && (b # c) ==> a # c+++-- | \( \forall a, b, c: ((a \# b) \wedge (a \# c)) \Rightarrow (b \# c) \)+--+-- For example, /=/ is an right Euclidean relation because if /x = y/ and /x = z/ then /y = z/.+--+euclidean :: (r -> r -> Bool) -> r -> r -> r -> Bool+euclidean (#) a b c = (a # b) && (a # c) ==> b # c+++-- |  \( \forall a, b, c: ((b \# a) \wedge (c \# a)) \Rightarrow (b \# c) \)+--+-- For example, /=/ is a left Euclidean relation because if /x = y/ and /x = z/ then /y = z/.+--+euclidean' :: (r -> r -> Bool) -> r -> r -> r -> Bool+euclidean' (#) a b c = (b # a) && (c # a) ==> b # c
+ src/Test/Util.hs view
@@ -0,0 +1,22 @@+module Test.Util where++type Rel r = r -> r -> Bool++xor :: Bool -> Bool -> Bool+xor a b = (a || b) && not (a && b)++xor3 :: Bool -> Bool -> Bool -> Bool+xor3 a b c = (a `xor` (b `xor` c)) && not (a && b && c)++infixr 0 ==>++(==>) :: Bool -> Bool -> Bool+(==>) a b = not a || b++iff :: Bool -> Bool -> Bool+iff a b = a ==> b && b ==> a++infixr 1 <==>++(<==>) :: Bool -> Bool -> Bool+(<==>) = iff