packages feed

semibounded-lattices (empty) → 0.1.0.0

raw patch · 5 files changed

+224/−0 lines, 5 filesdep +basedep +containersdep +latticessetup-changed

Dependencies added: base, containers, lattices, semibounded-lattice

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Hao Xu (c) 2016++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 Author name here 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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ semibounded-lattices.cabal view
@@ -0,0 +1,35 @@+name:                semibounded-lattices+version:             0.1.0.0+synopsis:            A Haskell implementation of semibounded lattices+description:         Please see README.md+homepage:            https://github.com/xu-hao/semibounded-lattices#readme+license:             BSD3+license-file:        LICENSE+author:              Hao Xu+maintainer:          xuh@email.unc.edu+copyright:           2016 Hao Xu+category:            Data+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Algebra.SemiBoundedLattice+  build-depends:       base >= 4 && < 5,+                       lattices,+                       containers+  default-language:    Haskell2010++test-suite semibounded-lattice-test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             Spec.hs+  build-depends:       base+                     , semibounded-lattice+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N+  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/xu-hao/semibounded-lattices
+ src/Algebra/SemiBoundedLattice.hs view
@@ -0,0 +1,155 @@+{-# LANGUAGE FlexibleInstances #-}+{-|+Module      : Algebra.SemiBoundedLattice+Description : Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra+Copyright   : (c) Hao Xu, 2016+License     : BSD-3+Maintainer  : xuh@email.unc.edu+Stability   : experimental+Portability : portable++Haskell typeclasses and instances of semibounded lattices, Heyting algebra, co-Heyting algebra, and Boolean algebra+-}+module Algebra.SemiBoundedLattice (+  Complemented (..), (/\\), (//\),+  DistributiveLattice, LowerBoundedLattice, UpperBoundedLattice, LowerBoundedDistributiveLattice, UpperBoundedDistributiveLattice, BooleanAlgebra (..),+  HeytingAlgebra, CoHeytingAlgebra, SemiHeytingAlgebra (..), SemiCoHeytingAlgebra (..), BiHeytingAlgebra) where++-- import Data.List (union, intersect, (\\))+import Data.Set (union, intersection, (\\), Set)++import Algebra.Lattice++-- | The combination of a JoinSemiLattice and a BoundedMeetSemiLattice makes an UpperBoundedLattice if the absorption law holds:+--+-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a+class (JoinSemiLattice a, BoundedMeetSemiLattice a) => UpperBoundedLattice a where++-- | The combination of a BoundedJoinSemiLattice and a MeetSemiLattice makes an LowerBoundedLattice if the absorption law holds:+--+-- > Absorption: a \/ (a /\ b) == a /\ (a \/ b) == a+class (BoundedJoinSemiLattice a, MeetSemiLattice a) => LowerBoundedLattice a where++-- | A lattice is distributive if the distributivity law holds:+--+-- > Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)+-- see <https://en.wikipedia.org/wiki/Distributive_lattice>+class Lattice a => DistributiveLattice a where++-- | A lattice is distributive if the distributivity law holds:+--+-- > Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)+-- see <https://en.wikipedia.org/wiki/Distributive_lattice>+class LowerBoundedLattice a => LowerBoundedDistributiveLattice a where++-- | A lattice is distributive if the distributivity law holds:+--+-- > Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c)+-- see <https://en.wikipedia.org/wiki/Distributive_lattice>+class UpperBoundedLattice a => UpperBoundedDistributiveLattice a where++-- | A semi-co-Heyting Algebra is dual of a semi-Heyting algebra where the following law holds:+--+-- > x \\\ y <= z if and only if x <= y \/ z+-- see <https://ncatlab.org/nlab/show/co-Heyting+algebra>+class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where+  subtraction :: a -> a -> a+  (\\\) :: a -> a -> a+  (\\\) = subtraction+  subtraction = (\\\)++-- | supplement+-- see <https://ncatlab.org/nlab/show/co-Heyting+negation>+class (BoundedLattice a, SemiCoHeytingAlgebra a) => CoHeytingAlgebra a where+  supplement :: a -> a+  supplement a = top \\\ a++-- | In most literature, a Heyting algebra requires a bounded lattice.+-- We only require a UpperBoundedDistributiveLattice here for semi-Heyting algebra. (here the lattice must be upper bounded)+-- The following law holds:+--+-- > x /\ a <= b if and only if x <= (a --> b)+-- see <https://ncatlab.org/nlab/show/Heyting+algebra>+-- Heyting algebras are always distributive. see <https://en.wikipedia.org/wiki/Heyting_algebra#Distributivity>+--+class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where+  implication :: a -> a -> a+  (-->) :: a -> a -> a+  (-->) = implication+  implication = (-->)++-- | negation+-- see <https://ncatlab.org/nlab/show/Heyting+algebra>+class (BoundedLattice a, SemiHeytingAlgebra a) => HeytingAlgebra a where+  negation :: a -> a+  negation a = a --> bottom++-- | A lattice that is both a Heyting algebra and a co-Heyting algebra is a bi-Heyting algebra+class (HeytingAlgebra a, CoHeytingAlgebra a) => BiHeytingAlgebra a where++-- | A Boolean Algebra is a complemented distributive lattice, see <https://en.wikipedia.org/wiki/Boolean_algebra_(structure)>+-- or equivalently a Heyting algebra where+--+-- > negation (negation a) == a+-- in a Boolean algebra+--+-- > supplement == negation+class BiHeytingAlgebra a => BooleanAlgebra a where+  complement :: a -> a+  complement = supplement++data Complemented a = Include a | Exclude a deriving Show++instance SemiCoHeytingAlgebra a => JoinSemiLattice (Complemented a) where+    join (Include vars) (Include vars2) = Include (vars \/ vars2)+    join (Include vars) (Exclude vars2) = Exclude (vars2 \\\ vars)+    join (Exclude vars) (Include vars2) = Exclude (vars \\\ vars2)+    join (Exclude vars) (Exclude vars2) = Exclude (vars2 /\ vars)++instance SemiCoHeytingAlgebra a => MeetSemiLattice (Complemented a) where+    meet (Include vars) (Include vars2) = Include (vars /\ vars2)+    meet (Exclude vars) (Include vars2) = Include (vars2 \\\ vars)+    meet (Include vars) (Exclude vars2) = Include (vars \\\ vars2)+    meet (Exclude vars) (Exclude vars2) = Exclude (vars \/ vars2)++instance SemiCoHeytingAlgebra a => BoundedJoinSemiLattice (Complemented a) where+    bottom = bottom++instance SemiCoHeytingAlgebra a => BoundedMeetSemiLattice (Complemented a) where+    top = Exclude bottom++instance SemiCoHeytingAlgebra a => Lattice (Complemented a) where+instance SemiCoHeytingAlgebra a => LowerBoundedLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => UpperBoundedLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => BoundedLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => DistributiveLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => LowerBoundedDistributiveLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => UpperBoundedDistributiveLattice (Complemented a) where+instance SemiCoHeytingAlgebra a => SemiCoHeytingAlgebra (Complemented a) where+  Include a \\\ Include b = Include (a \\\ b)+  Include a \\\ Exclude b = Include (a /\ b)+  Exclude a \\\ Include b = Exclude (a \/ b)+  Exclude a \\\ Exclude b = Include (b \\\ a)++instance SemiCoHeytingAlgebra a => SemiHeytingAlgebra (Complemented a) where+  a --> b = (top \\\ a) \/ b++instance SemiCoHeytingAlgebra a => CoHeytingAlgebra (Complemented a) where+instance SemiCoHeytingAlgebra a => HeytingAlgebra (Complemented a) where+instance SemiCoHeytingAlgebra a => BiHeytingAlgebra (Complemented a) where+instance SemiCoHeytingAlgebra a => BooleanAlgebra (Complemented a) where++instance Ord a => LowerBoundedLattice (Set a)+instance Ord a => LowerBoundedDistributiveLattice (Set a)+instance Ord a => SemiCoHeytingAlgebra (Set a) where+  subtraction = (\\)++(/\\), rmeetproj :: SemiCoHeytingAlgebra a => a -> Complemented a -> a+rmeetproj vars (Include vars2) = vars /\ vars2+rmeetproj vars (Exclude vars2) = vars \\\ vars2+(/\\) = rmeetproj++(//\), lmeetproj :: SemiCoHeytingAlgebra a => Complemented a -> a -> a+lmeetproj (Include vars2) vars = vars /\ vars2+lmeetproj (Exclude vars2) vars = vars \\\ vars2+(//\) = lmeetproj
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"