interval-algebra-1.0.0: src/IntervalAlgebra/Axioms.hs
{-|
Module : Interval Algebra Axioms
Description : Properties of Intervals
Copyright : (c) NoviSci, Inc 2020
License : BSD3
Maintainer : bsaul@novisci.com
This module exports a single typeclass @IntervalAxioms@ which contains
property-based tests for the axioms in section 1 of [Allen and Hayes (1987)](https://doi.org/10.1111/j.1467-8640.1989.tb00329.x).
The notation below is that of the original paper.
This module is useful if creating a new instance of interval types that you want to test.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module IntervalAlgebra.Axioms (
IntervalAxioms(..)
, M1set(..)
, M2set(..)
, M5set(..)
) where
import Test.QuickCheck ( (===)
, (==>)
, Property
, Arbitrary (arbitrary) )
import Data.Either ( isRight )
import Data.Maybe ( fromJust, isJust, isNothing )
import Data.Time as DT ( Day(..)
, UTCTime(..)
, DiffTime
, NominalDiffTime
)
import Data.Set ( Set
, member
, disjointUnion
, fromList )
import IntervalAlgebra.Core
import IntervalAlgebra.Arbitrary
xor :: Bool -> Bool -> Bool
xor a b = a /= b
-- | Internal function for converting a number to a strictly positive value.
makePos :: (Ord b, Num b) => b -> b
makePos x
| x == 0 = x + 1
| x < 0 = negate x
| otherwise = x
-- | A set used for testing M1 defined so that the M1 condition is true.
data M1set a = M1set {
m11 :: Interval a
, m12 :: Interval a
, m13 :: Interval a
, m14 :: Interval a }
deriving (Show)
instance Arbitrary (M1set Int) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m1set x a b <$> arbitrary
instance Arbitrary (M1set DT.Day) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m1set x a b <$> arbitrary
instance Arbitrary (M1set DT.UTCTime) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m1set x a b <$> arbitrary
-- | A set used for testing M2 defined so that the M2 condition is true.
data M2set a = M2set {
m21 :: Interval a
, m22 :: Interval a
, m23 :: Interval a
, m24 :: Interval a }
deriving (Show)
instance Arbitrary (M2set Int) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m2set x a b <$> arbitrary
instance Arbitrary (M2set DT.Day) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m2set x a b <$> arbitrary
instance Arbitrary (M2set DT.UTCTime) where
arbitrary = do
x <- arbitrary
a <- arbitrary
b <- arbitrary
m2set x a b <$> arbitrary
-- | A set used for testing M5.
data M5set a = M5set {
m51 :: Interval a
, m52 :: Interval a }
deriving (Show)
instance Arbitrary (M5set Int) where
arbitrary = do
x <- arbitrary
a <- arbitrary
m5set x a <$> arbitrary
instance Arbitrary (M5set DT.Day) where
arbitrary = do
x <- arbitrary
a <- arbitrary
m5set x a <$> arbitrary
instance Arbitrary (M5set DT.UTCTime) where
arbitrary = do
x <- arbitrary
a <- arbitrary
m5set x a <$> arbitrary
-- | = "An Axiomatization of Interval Time".
class ( IntervalSizeable a b ) => IntervalAxioms a b where
-- | Smart constructor of 'M1set'.
m1set :: (IntervalSizeable a b) => Interval a -> b -> b -> b -> M1set a
m1set x a b c = M1set p1 p2 p3 p4
where p1 = x -- interval i in prop_IAaxiomM1
p2 = beginerval a (end x) -- interval j in prop_IAaxiomM1
p3 = beginerval b (end x) -- interval k in prop_IAaxiomM1
p4 = enderval (makePos c) (begin p2)
{- |
== Axiom M1
The first axiom of Allen and Hayes (1987) states that if "two periods both
meet a third, thn any period met by one must also be met by the other."
That is:
\[
\forall \text{ i,j,k,l } s.t. (i:j \text{ & } i:k \text{ & } l:j) \implies l:k
\]
-}
prop_IAaxiomM1 :: (Ord a) => M1set a -> Property
prop_IAaxiomM1 x =
(i `meets` j && i `meets` k && l `meets` j) ==> (l `meets` k)
where i = m11 x
j = m12 x
k = m13 x
l = m14 x
-- | Smart constructor of 'M2set'.
m2set :: (IntervalSizeable a b)=> Interval a -> Interval a -> b -> b -> M2set a
m2set x y a b = M2set p1 p2 p3 p4
where p1 = x -- interval i in prop_IAaxiomM2
p2 = beginerval a (end x) -- interval j in prop_IAaxiomM2
p3 = y -- interval k in prop_IAaxiomM2
p4 = beginerval b (end y) -- interval l in prop_IAaxiomM2
{- |
== Axiom M2
If period i meets period j and period k meets l,
then exactly one of the following holds:
1) i meets l;
2) there is an m such that i meets m and m meets l;
3) there is an n such that k meets n and n meets j.
That is,
\[
\forall i,j,k,l s.t. (i:j \text { & } k:l) \implies
i:l \oplus
(\exists m s.t. i:m:l) \oplus
(\exists m s.t. k:m:j)
\]
-}
prop_IAaxiomM2 :: (IntervalSizeable a b, Show a) =>
M2set a -> Property
prop_IAaxiomM2 x =
(i `meets` j && k `meets` l) ==>
(i `meets` l) `xor`
isRight m `xor`
isRight n
where i = m21 x
j = m22 x
k = m23 x
l = m24 x
m = parseInterval (end i) (begin l)
n = parseInterval (end k) (begin j)
{- |
== Axiom ML1
An interval cannot meet itself.
\[
\forall i \lnot i:i
\]
-}
prop_IAaxiomML1 :: (Ord a) => Interval a -> Property
prop_IAaxiomML1 x = not (x `meets` x) === True
{- |
== Axiom ML2
If i meets j then j does not meet i.
\[
\forall i,j i:j \implies \lnot j:i
\]
-}
prop_IAaxiomML2 :: (Ord a)=> M2set a -> Property
prop_IAaxiomML2 x =
(i `meets` j) ==> not (j `meets` i)
where i = m21 x
j = m22 x
{- |
== Axiom M3
Time does not start or stop:
\[
\forall i \exists j,k s.t. j:i:k
\]
-}
prop_IAaxiomM3 :: (IntervalSizeable a b)=>
b -> Interval a -> Property
prop_IAaxiomM3 b i =
(j `meets` i && i `meets` k) === True
where j = enderval b (begin i)
k = beginerval b (end i)
{- |
ML3 says that For all i, there does not exist m such that i meets m and
m meet i. Not testing that this axiom holds, as I'm not sure how I would
test the lack of existence easily.
-}
{- |
== Axiom M4
If two meets are separated by intervals, then this sequence is a longer interval.
\[
\forall i,j i:j \implies (\exists k,m,n s.t m:i:j:n \text { & } m:k:n)
\]
-}
prop_IAaxiomM4 :: (IntervalSizeable a b)=>
b -> M2set a -> Property
prop_IAaxiomM4 b x =
((m `meets` i && i `meets` j && j `meets` n) &&
(m `meets` k && k `meets` n)) === True
where i = m21 x
j = m22 x
m = enderval b (begin i)
n = beginerval b (end j)
k = beginerval g (end m)
g = diff (begin n) (end m)
-- | Smart constructor of 'M5set'.
m5set :: (IntervalSizeable a b)=> Interval a -> b -> b -> M5set a
m5set x a b = M5set p1 p2
where p1 = x -- interval i in prop_IAaxiomM5
p2 = beginerval a ps -- interval l in prop_IAaxiomM5
ps = end (expandr (makePos b) x) -- creating l by shifting and expanding i
{- |
== Axiom M5
There is only one time period between any two meeting places.
\[
\forall i,j,k,l (i:j:l \text{ & } i:k:l) \equiv j = k
\]
-}
prop_IAaxiomM5 :: (IntervalSizeable a b) =>
M5set a -> Property
prop_IAaxiomM5 x =
((i `meets` j && j `meets` l) &&
(i `meets` k && k `meets` l)) === (j == k)
where i = m51 x
j = beginerval g (end i)
k = beginerval g (end i)
g = diff (begin l) (end i)
l = m52 x
{- |
== Axiom M4.1
Ordered unions:
\[
\forall i,j i:j \implies (\exists m,n s.t. m:i:j:n \text{ & } m:(i+j):n)
\]
-}
prop_IAaxiomM4_1 :: (IntervalSizeable a b)=>
b -> M2set a -> Property
prop_IAaxiomM4_1 b x =
((m `meets` i && i `meets` j && j `meets` n) &&
(m `meets` ij && ij `meets` n)) === True
where i = m21 x
j = m22 x
m = enderval b (begin i)
n = beginerval b (end j)
ij = fromJust $ i .+. j
instance IntervalAxioms Int Int
instance IntervalAxioms Day Integer
instance IntervalAxioms UTCTime NominalDiffTime