Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Data.Connection.Property
Description
Galois connections have the same properties as adjunctions defined over other categories:
∀x,y:f⊣g⇒f(x)≤b⇔x≤g(y)
∀x:f⊣g⇒x≤g∘f(x)
∀x:f⊣g⇒f∘g(x)≤x
Synopsis
- adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
- adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
- adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
- adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
- closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool
- closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool
- closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool
- kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool
- kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool
- kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool
- invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
- monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool
- monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool
- monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool
- monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
- idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool
- idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
- idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
- projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b
Adjointness
adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool Source #
∀x,y:f⊣g⇒f(x)≤y⇔x≤g(y)
A Galois connection is an adjunction of preorders. This is a required property.
adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool Source #
∀a:fa≤b⇔a≤gb
A monotone Galois connection is defined by adjunction (<~) (<~)
,
while an antitone Galois connection is defined by adjunction (>~) (<~)
.
Closure
closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool Source #
∀x:f⊣g⇒x≤g∘f(x)
This is a required property.
kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool Source #
∀x:f⊣g⇒x≤g∘f(x)
This is a required property.
invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b Source #
∀a:f(ga)∼a
Monotonicity
monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool Source #
monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool Source #
∀x,y:x≤y⇒f(x)≤f(y)
This is a required property.
Idempotence
idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool Source #
∀x:f⊣g⇒counit∘f(x)∼f(x)∧unit∘g(x)∼g(x)
projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b Source #
∀a:g∘f(a)∼f(a)