| Copyright | (c) NoviSci Inc 2020 |
|---|---|
| License | BSD3 |
| Maintainer | bsaul@novisci.com |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
IntervalAlgebra.Axioms
Description
This module exports a single typeclass IntervalAxioms which contains
property-based tests for the axioms in section 1 of Allen and Hayes (1987).
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.
Synopsis
- class IntervalSizeable a b => IntervalAxioms a b where
- m1set :: IntervalSizeable a b => Interval a -> b -> b -> b -> M1set a
- prop_IAaxiomM1 :: Ord a => M1set a -> Property
- m2set :: IntervalSizeable a b => Interval a -> Interval a -> b -> b -> M2set a
- prop_IAaxiomM2 :: (IntervalSizeable a b, Show a) => M2set a -> Property
- prop_IAaxiomML1 :: Ord a => Interval a -> Property
- prop_IAaxiomML2 :: Ord a => M2set a -> Property
- prop_IAaxiomM3 :: IntervalSizeable a b => b -> Interval a -> Property
- prop_IAaxiomM4 :: IntervalSizeable a b => b -> M2set a -> Property
- m5set :: IntervalSizeable a b => Interval a -> b -> b -> M5set a
- prop_IAaxiomM5 :: IntervalSizeable a b => M5set a -> Property
- prop_IAaxiomM4_1 :: IntervalSizeable a b => b -> M2set a -> Property
- data M1set a = M1set {}
- data M2set a = M2set {}
- data M5set a = M5set {}
Documentation
class IntervalSizeable a b => IntervalAxioms a b where Source #
"An Axiomatization of Interval Time".
Minimal complete definition
Nothing
Methods
m1set :: IntervalSizeable a b => Interval a -> b -> b -> b -> M1set a Source #
Smart constructor of M1set.
prop_IAaxiomM1 :: Ord a => M1set a -> Property Source #
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:
∀ i,j,k,l s.t.(i:j & i:k & l:j)⟹l:k
m2set :: IntervalSizeable a b => Interval a -> Interval a -> b -> b -> M2set a Source #
Smart constructor of M2set.
prop_IAaxiomM2 :: (IntervalSizeable a b, Show a) => M2set a -> Property Source #
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,
∀i,j,k,ls.t.(i:j & k:l)⟹i:l⊕(∃ms.t.i:m:l)⊕(∃ms.t.k:m:j)
prop_IAaxiomML1 :: Ord a => Interval a -> Property Source #
Axiom ML1
An interval cannot meet itself.
∀i¬i:i
prop_IAaxiomML2 :: Ord a => M2set a -> Property Source #
Axiom ML2
If i meets j then j does not meet i.
∀i,ji:j⟹¬j:i
prop_IAaxiomM3 :: IntervalSizeable a b => b -> Interval a -> Property Source #
Axiom M3
Time does not start or stop:
∀i∃j,ks.t.j:i:k
prop_IAaxiomM4 :: IntervalSizeable a b => b -> M2set a -> Property Source #
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.
∀i,ji:j⟹(∃k,m,ns.tm:i:j:n & m:k:n)
m5set :: IntervalSizeable a b => Interval a -> b -> b -> M5set a Source #
Smart constructor of M5set.
prop_IAaxiomM5 :: IntervalSizeable a b => M5set a -> Property Source #
Axiom M5
There is only one time period between any two meeting places.
∀i,j,k,l(i:j:l & i:k:l)≡j=k
prop_IAaxiomM4_1 :: IntervalSizeable a b => b -> M2set a -> Property Source #
Axiom M4.1
Ordered unions:
∀i,ji:j⟹(∃m,ns.t.m:i:j:n & m:(i+j):n)
Instances
A set used for testing M1 defined so that the M1 condition is true.
A set used for testing M2 defined so that the M2 condition is true.