diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/semibounded-lattices.cabal b/semibounded-lattices.cabal new file mode 100644 --- /dev/null +++ b/semibounded-lattices.cabal @@ -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 diff --git a/src/Algebra/SemiBoundedLattice.hs b/src/Algebra/SemiBoundedLattice.hs new file mode 100644 --- /dev/null +++ b/src/Algebra/SemiBoundedLattice.hs @@ -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 +class Lattice a => DistributiveLattice a where + +-- | A lattice is distributive if the distributivity law holds: +-- +-- > Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c) +-- see +class LowerBoundedLattice a => LowerBoundedDistributiveLattice a where + +-- | A lattice is distributive if the distributivity law holds: +-- +-- > Distributivity: a /\ (b \/ c) == (a /\ b) \/ (a /\ c) +-- see +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 +class LowerBoundedDistributiveLattice a => SemiCoHeytingAlgebra a where + subtraction :: a -> a -> a + (\\\) :: a -> a -> a + (\\\) = subtraction + subtraction = (\\\) + +-- | supplement +-- see +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 +-- Heyting algebras are always distributive. see +-- +class UpperBoundedDistributiveLattice a => SemiHeytingAlgebra a where + implication :: a -> a -> a + (-->) :: a -> a -> a + (-->) = implication + implication = (-->) + +-- | negation +-- see +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 +-- 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 diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,2 @@ +main :: IO () +main = putStrLn "Test suite not yet implemented"