Copyright | (c) David Janin, 2016 |
---|---|
License | see the LICENSE file in the distribution |
Maintainer | janin@labri.fr |
Stability | experimental |
Safe Haskell | Safe |
Language | Haskell2010 |
Embbeds Num data types into a complete lattice.
- data Min a = Min [a]
- data Max a = Max [a]
- insertMin :: POrd a => a -> Min a -> Min a
- reduceMin :: POrd a => Min a -> Min a
- minCovered :: POrd a => Min a -> a -> Bool
- pMinLeq :: POrd a => Min a -> Min a -> Bool
- compareMin :: POrd a => Min a -> Min a -> Maybe Ordering
- toMin :: a -> Min a
- insertMax :: POrd a => a -> Max a -> Max a
- reduceMax :: POrd a => Max a -> Max a
- maxCovered :: POrd a => Max a -> a -> Bool
- pMaxLeq :: POrd a => Max a -> Max a -> Bool
- compareMax :: POrd a => Max a -> Max a -> Maybe Ordering
- toMax :: a -> Max a
- type MinMax a = Min (Max a)
- type MaxMin a = Max (Min a)
- meetMin :: POrd a => Min a -> Min a -> Min a
- joinMin :: POrd a => MinMax a -> MinMax a -> MinMax a
- meetMinL :: POrd a => [Min a] -> Min a
- joinMinL :: POrd a => [MinMax a] -> Min (Max a)
- joinMax :: POrd a => Max a -> Max a -> Max a
- meetMax :: POrd a => MaxMin a -> MaxMin a -> MaxMin a
- meetMaxL :: POrd a => [MaxMin a] -> Max (Min a)
- joinMaxL :: POrd a => [Max a] -> Max a
- maxMin2MinMax :: POrd a => MaxMin a -> MinMax a
- minMax2MaxMin :: POrd a => MinMax a -> MaxMin a
- fmap1Min :: POrd a => (a -> a) -> Min a -> Min a
- fmap1Max :: POrd a => (a -> a) -> Max a -> Max a
- fmap1MinMax :: POrd a => (a -> a) -> MinMax a -> MinMax a
- fmap1MaxMin :: POrd a => (a -> a) -> MaxMin a -> MaxMin a
- fmap2Min :: POrd a => (a -> a -> a) -> Min a -> Min a -> Min a
- fmap2Max :: POrd a => (a -> a -> a) -> Max a -> Max a -> Max a
- fmap2MinMax :: POrd a => (a -> a -> a) -> MinMax a -> MinMax a -> MinMax a
- fmap2MaxMin :: POrd a => (a -> a -> a) -> MaxMin a -> MaxMin a -> MaxMin a
- fmapRMin :: POrd a => (a -> b) -> Min a -> Max b
- fmapRMax :: POrd a => (a -> b) -> Max a -> Min b
- fmapRMinMax :: POrd a => (a -> a) -> MinMax a -> MaxMin a
- fmapRMaxMin :: POrd a => (a -> a) -> MaxMin a -> MinMax a
- meetM :: POrd a => [MinMax a] -> MinMax a
- joinM :: POrd a => [MinMax a] -> MinMax a
- reduceMM :: POrd a => MinMax a -> MinMax a
- justMM :: a -> Min (Max a)
The Min and Max completions
Min l represents the least upper bound of elements of l henceforth with Min[] as top element.
The mapping 'a -> Min [a]' is an embedding of a into Min a
Min [a] |
POrd a => Eq (Min a) Source # | Equality instance derived from the partial order |
(Fractional a, POrd a) => Fractional (MinMax a) Source # | Derived Fractional instance (to be checked) |
(Num a, POrd a) => Num (MinMax a) Source # | Derived Num instance (to be checked) |
POrd d => Ord (Min (Max d)) Source # | Derived total order with possible errors; to be used either with care, or as syntactic sugar.. |
Show a => Show (Min a) Source # | |
POrd a => POrd (Min a) Source # | Min completion as a pOrd. |
(POrd a, Num a) => Lattice (MinMax a) Source # | Derived Lattice instance |
Min l represents the greates lower bound of elements of l henceforth with Max[] as bottom.
The mapping 'a -> Max [a]' is an embedding of a into Max a
Max [a] |
POrd a => Eq (Max a) Source # | Derived equality instance |
(Fractional a, POrd a) => Fractional (MinMax a) Source # | Derived Fractional instance (to be checked) |
(Num a, POrd a) => Num (MinMax a) Source # | Derived Num instance (to be checked) |
POrd d => Ord (Min (Max d)) Source # | Derived total order with possible errors; to be used either with care, or as syntactic sugar.. |
Show a => Show (Max a) Source # | |
POrd a => POrd (Max a) Source # | Derived partial order |
(POrd a, Num a) => Lattice (MinMax a) Source # | Derived Lattice instance |
The Min completion
insertMin :: POrd a => a -> Min a -> Min a Source #
Inserts an element x into a list l of minimal elements if l is an antichain then so is insertMin x l
reduceMin :: POrd a => Min a -> Min a Source #
Reduces a Min list by removing greater comparable elements. The resulting list is an antichain.
minCovered :: POrd a => Min a -> a -> Bool Source #
Equals True when one element of its first arguement is smaller than or equal to its second arguement. False otherwise
pMinLeq :: POrd a => Min a -> Min a -> Bool Source #
Induced partial order. The boolean pMinLeq m1 m2 is True when every element of m2 is greater than or equal to an element of m1, it is False otherwise
Natural embedding with the property that under (POrd a) hypothesis,
partialCompare a b == partialCompare (toMin a) (toMin b)
that is to say, toMin
is a partial order embeding of a into Min a
The Max completion
insertMax :: POrd a => a -> Max a -> Max a Source #
Inserts an element x into a list l of maximal elements; if l is an antichain then so is insertMax x l.
reduceMax :: POrd a => Max a -> Max a Source #
Reduces a Max list by removing smaller comparable elements. The resulting list is an antichain.
maxCovered :: POrd a => Max a -> a -> Bool Source #
Equals True when one element of its first arguement is greater than or equal to its second arguement. False otherwise
pMaxLeq :: POrd a => Max a -> Max a -> Bool Source #
Induced partial order. The boolean pMaxLeq m1 m2 is True when every element of m1 is smaller than or equal to an element of m1, it is False otherwise
Natural embedding with the property that under (POrd a) hypothesis,
partialCompare a b == partialCompare (toMax a) (toMax b)
that is to say, toMax
is a partial order embeding of a into Max a
The MinMax and MaxMin completion -
type MaxMin a = Max (Min a) Source #
MaxMin completion
MaxMin a and MinMax a are both equiped with a derived order relation such that : * both MinMax and MaxMin are (isomorphic) lattices * both a -> Min [Max a] and a -> Max [Min a] are partial order embeddings
Incidentaly: Max[] and Max [Min []] are the least and the greatest element of MaxMin, and Min[] and Min [Max []] are the least and the greatest element in MinMax
joinMin :: POrd a => MinMax a -> MinMax a -> MinMax a Source #
The join in MinMax completion (with exponential blow up)
meetMax :: POrd a => MaxMin a -> MaxMin a -> MaxMin a Source #
The meet in MaxMin completion (with exponential blow up)
maxMin2MinMax :: POrd a => MaxMin a -> MinMax a Source #
Emebedding of MaxMin into MinMax (warning : exponential blow up)
minMax2MaxMin :: POrd a => MinMax a -> MaxMin a Source #
Emebedding of MinMax into MaxMin (warning : exponential blow up)
Functor like functions
fmap2MinMax :: POrd a => (a -> a -> a) -> MinMax a -> MinMax a -> MinMax a Source #
Binary lift for MinMax
fmap2MaxMin :: POrd a => (a -> a -> a) -> MaxMin a -> MaxMin a -> MaxMin a Source #
Binary lift for MaxMin
fmapRMinMax :: POrd a => (a -> a) -> MinMax a -> MaxMin a Source #
Unary contravariant lift for MinMax