PresheafValuationAlgebra.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wall -Werror #-}

-- | The presheaf formulation of a valuation algebra, following
-- Shenoy & Shafer (1990), Kohlas (2003), and Abramsky & Carù (2019).
--
-- In this formulation, valuations form a presheaf F over a domain lattice:
--
-- * For each domain d, F(d) is the set of valuations with domain d
-- * For d' <= d, the restriction map rho_{d,d'}: F(d) -> F(d') implements marginalisation
-- * Combination is a family of maps: F(d1) x F(d2) -> F(d1 \/ d2)
--
-- A 'PresheafValuationAlgebra' bundles a 'DomainLattice' with a 'ValuationAlgebra',
-- providing all the structure needed for the presheaf formulation with
-- operations that work directly on 'Valuation' values.
module Data.Valuation.PresheafValuationAlgebra
  ( PresheafValuationAlgebra (..),
    PresheafValuationAlgebra',
    SetPresheafValuationAlgebra,
    SetPresheafValuationAlgebra',
    HasPresheafValuationAlgebra (..),
    AsPresheafValuationAlgebra (..),
    marginalise,
    combine,
    neutralValuation,
    nullValuation,
    presheafCombineSemigroup,

    -- * laws
    lawTransitivity,
    lawCombinationDomain,
    lawMarginalisationIdentity,
    lawNeutralCombination,
    lawNullCombination,
    lawCombinationCommutative,
  )
where

import Control.Lens (Lens', Prism', review, view, _Wrapped)
import Data.Set (Set)
import Data.Valuation.DomainLattice
  ( DomainLattice (..),
    HasDomainLattice (..),
    runDomainJoin,
    runDomainLeq,
  )
import Data.Valuation.ProjectValuation (HasProjectValuation (..))
import Data.Valuation.SemiValuationAlgebra
  ( HasSemiValuationAlgebra (..),
  )
import Data.Valuation.Semigroup
  ( HasSemigroup (..),
    Semigroup',
    applySemigroup,
    runSemigroup,
  )
import Data.Valuation.Valuation
  ( HasValuation (valuationDomain, valuationInformation),
    Valuation (..),
  )
import Data.Valuation.ValuationAlgebra
  ( HasValuationAlgebra (..),
    ValuationAlgebra (..),
  )
import Prelude hiding (Semigroup)

-- $setup
-- >>> :set -Wno-name-shadowing -Wno-type-defaults
-- >>> import qualified Data.Set as Set
-- >>> import Control.Lens (review)
-- >>> import Data.Valuation.Semigroup (applySemigroup, runSemigroup)
-- >>> import Data.Valuation.DomainLattice (setDomainLattice, runDomainJoin)
-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
-- >>> import Prelude hiding (Semigroup)

-- |
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> let v1 = Valuation (Set.fromList [1,2]) 10 :: Valuation Set Int Int
-- >>> let v2 = Valuation (Set.fromList [2,3]) 20
-- >>> combine pva v1 v2
-- Valuation (fromList [1,2,3]) 30
data PresheafValuationAlgebra p q r s v set var
  = PresheafValuationAlgebra
      -- | lattice structure on domains
      (DomainLattice p (set var) (set var))
      -- | the valuation algebra
      (ValuationAlgebra q r s v set var)

type PresheafValuationAlgebra' v set var =
  PresheafValuationAlgebra (->) (->) (->) (->) v set var

-- | A 'PresheafValuationAlgebra' specialised to 'Set'.
type SetPresheafValuationAlgebra p q r s v var =
  PresheafValuationAlgebra p q r s v Set var

type SetPresheafValuationAlgebra' v var =
  SetPresheafValuationAlgebra (->) (->) (->) (->) v var

-- | Classy lens for types that contain a 'PresheafValuationAlgebra'.
class HasPresheafValuationAlgebra c p q r s v set var | c -> p q r s v set var where
  presheafValuationAlgebra :: Lens' c (PresheafValuationAlgebra p q r s v set var)

instance HasPresheafValuationAlgebra (PresheafValuationAlgebra p q r s v set var) p q r s v set var where
  presheafValuationAlgebra = id

-- | Classy prism for types that can be constructed from a 'PresheafValuationAlgebra'.
class AsPresheafValuationAlgebra c p q r s v set var | c -> p q r s v set var where
  _PresheafValuationAlgebra :: Prism' c (PresheafValuationAlgebra p q r s v set var)

instance AsPresheafValuationAlgebra (PresheafValuationAlgebra p q r s v set var) p q r s v set var where
  _PresheafValuationAlgebra = id

instance HasDomainLattice (PresheafValuationAlgebra p q r s v set var) p (set var) (set var) where
  domainLattice f (PresheafValuationAlgebra l a) = fmap (`PresheafValuationAlgebra` a) (f l)

instance HasValuationAlgebra (PresheafValuationAlgebra p q r s v set var) q r s v set var where
  valuationAlgebra f (PresheafValuationAlgebra l a) = fmap (PresheafValuationAlgebra l) (f a)

instance HasSemiValuationAlgebra (PresheafValuationAlgebra p q r s v set var) q r s v set var where
  semiValuationAlgebra = valuationAlgebra . semiValuationAlgebra

instance HasSemigroup (PresheafValuationAlgebra p q r s v set var) q v where
  semigroup = semiValuationAlgebra . semigroup

instance HasProjectValuation (PresheafValuationAlgebra p q r s v set var) r s v set var where
  projectValuation = semiValuationAlgebra . projectValuation

-- | Marginalise a valuation to a subdomain: the restriction map of the presheaf.
--
-- Given a target domain @d'@ and a valuation phi with domain @d@,
-- computes @phi↓d'@ with @d(phi↓d') = d'@.
--
-- This is the presheaf restriction map: @rho_{d,d'}: F(d) -> F(d')@.
--
-- The caller should ensure @d' <= d(phi)@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + Set.size s))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> marginalise pva (Set.fromList [1]) (Valuation (Set.fromList [1,2]) 10)
-- Valuation (fromList [1]) 11
{-# SPECIALIZE marginalise ::
  PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Valuation set var v
  #-}
marginalise :: (HasProjectValuation algebra (->) (->) v set var, HasValuation valuation set' var' v) => algebra -> set var -> valuation -> Valuation set var v
marginalise algebra targetDomain =
  Valuation targetDomain . view (projectValuation . _Wrapped) algebra targetDomain . view valuationInformation

-- | Combine two valuations: the combination operation of the valuation algebra.
--
-- Computes @phi ⊗ psi@ with @d(phi ⊗ psi) = d(phi) \/ d(psi)@.
--
-- The information values are combined using the algebra's semigroup,
-- and the result has the joined domain.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> combine pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20)
-- Valuation (fromList [1,2,3]) 30
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> combine pva (Valuation (Set.fromList [1]) 3) (Valuation (Set.fromList [2]) 4)
-- Valuation (fromList [1,2]) 12
{-# SPECIALIZE combine ::
  PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v
  #-}
combine ::
  (HasSemigroup s1 (->) a, HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Valuation set var a
combine alg phi =
  Valuation . runSemigroup (view domainLatticeJoin alg) (view valuationDomain phi) . view valuationDomain <*> runSemigroup (view semigroup alg) (view valuationInformation phi) . view valuationInformation

-- | The neutral valuation for a domain: @e_d@ such that @e_d ⊗ phi = phi@
-- for all phi with @d(phi) <= d@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> neutralValuation pva (Set.fromList [1,2])
-- Valuation (fromList [1,2]) 0
{-# SPECIALIZE neutralValuation ::
  PresheafValuationAlgebra' v set var -> set var -> Valuation set var v
  #-}
neutralValuation :: (HasValuationAlgebra s (->) (->) (->) a set var) => s -> set var -> Valuation set var a
neutralValuation algebra =
  Valuation <*> view (valuationAlgebra . valuationAlgebraUnit . _Wrapped) algebra

-- | The null/zero valuation for a domain: @z_d@ such that @z_d ⊗ phi = z_{d \/ d(phi)}@
-- for all phi.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> nullValuation pva (Set.fromList [1,2])
-- Valuation (fromList [1,2]) 99
{-# SPECIALIZE nullValuation ::
  PresheafValuationAlgebra' v set var -> set var -> Valuation set var v
  #-}
nullValuation :: (HasValuationAlgebra s (->) (->) (->) a set var) => s -> set var -> Valuation set var a
nullValuation algebra =
  Valuation <*> view (valuationAlgebra . valuationAlgebraZero . _Wrapped) algebra

-- | A first-class 'Semigroup' on 'Valuation' derived from the presheaf algebra's
-- combination operation.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> let sg = presheafCombineSemigroup pva
-- >>> runSemigroup sg (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20)
-- Valuation (fromList [1,2]) 30
{-# SPECIALIZE presheafCombineSemigroup ::
  PresheafValuationAlgebra' v set var -> Semigroup' (Valuation set var v)
  #-}
presheafCombineSemigroup :: (HasSemigroup algebra (->) v, HasDomainLattice algebra (->) (set var) (set var)) => algebra -> Semigroup' (Valuation set var v)
presheafCombineSemigroup = review applySemigroup . combine

-- | Transitivity of marginalisation: @(phi↓d')↓d'' = phi↓d''@ for @d'' <= d' <= d(phi)@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> let phi = Valuation (Set.fromList [1,2,3]) 10
-- >>> lawTransitivity pva (Set.fromList [1,2]) (Set.fromList [1]) phi
-- True
{-# SPECIALIZE lawTransitivity ::
  (Eq v) => PresheafValuationAlgebra' v set var -> set var -> set var -> Valuation set var v -> Bool
  #-}
lawTransitivity :: (Eq a, HasProjectValuation p (->) (->) a set var, HasValuation q set' var' a) => p -> set var -> set var -> q -> Bool
lawTransitivity pva d' d'' phi =
  let step = marginalise pva d'' (marginalise pva d' phi)
      direct = marginalise pva d'' phi
      valuationInfo = view valuationInformation
   in valuationInfo step == valuationInfo direct

-- | Domain of combination: @d(phi ⊗ psi) = d(phi) \/ d(psi)@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> lawCombinationDomain pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20)
-- True
{-# SPECIALIZE lawCombinationDomain ::
  (Eq (set var)) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Bool
  #-}
lawCombinationDomain :: (HasSemigroup s1 (->) a, Eq (set var), HasValuation s2 set var a, HasValuation s3 set var a, HasDomainLattice s1 (->) (set var) (set var)) => s1 -> s2 -> s3 -> Bool
lawCombinationDomain pva val1 val2 =
  let lat = view domainLattice pva
      d1 = view valuationDomain val1
      d2 = view valuationDomain val2
      d = view valuationDomain (combine pva val1 val2)
   in d == runDomainJoin lat d1 d2

-- | Marginalisation identity: @phi↓d(phi) = phi@ (marginalising to own domain is identity).
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> lawMarginalisationIdentity pva (Valuation (Set.fromList [1,2]) 42)
-- True
{-# SPECIALIZE lawMarginalisationIdentity ::
  (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Bool
  #-}
lawMarginalisationIdentity :: (Eq a, Eq (set var), HasValuation s set var a, HasProjectValuation p (->) (->) a set var) => p -> s -> Bool
lawMarginalisationIdentity pva val =
  let d = view valuationDomain val
      v = view valuationInformation val
      Valuation d' v' = marginalise pva d val
   in d' == d && v' == v

-- | Neutral element axiom: @combine pva (neutralValuation pva d) phi = phi@
-- when @d(phi) <= d@ (the neutral valuation is an identity for combination).
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> let phi = Valuation (Set.fromList [1]) 42
-- >>> lawNeutralCombination pva (Set.fromList [1,2]) phi
-- True
{-# SPECIALIZE lawNeutralCombination ::
  (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Bool
  #-}
lawNeutralCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuationAlgebra s1 (->) (->) (->) a set var) => s1 -> set var -> s2 -> Bool
lawNeutralCombination pva d phi =
  let lat = view domainLattice pva
      dPhi = view valuationDomain phi
      vPhi = view valuationInformation phi
   in not (runDomainLeq lat dPhi d)
        || let Valuation d' v' = combine pva (neutralValuation pva d) phi
               expectedDomain = runDomainJoin lat d dPhi
            in d' == expectedDomain && v' == vPhi

-- | Null element axiom: @combine pva (nullValuation pva d) phi = nullValuation pva (d \/ d(phi))@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> let phi = Valuation (Set.fromList [1]) 42
-- >>> lawNullCombination pva (Set.fromList [2]) phi
-- True
{-# SPECIALIZE lawNullCombination ::
  (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> set var -> Valuation set var v -> Bool
  #-}
lawNullCombination :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasValuation s2 set var a, HasDomainLattice s1 (->) (set var) (set var), HasValuationAlgebra s1 (->) (->) (->) a set var) => s1 -> set var -> s2 -> Bool
lawNullCombination pva d phi =
  let lat = view domainLattice pva
      dPhi = view valuationDomain phi
      lhs = combine pva (nullValuation pva d) phi
      expectedDomain = runDomainJoin lat d dPhi
      rhs = nullValuation pva expectedDomain
      valuationDom = view valuationDomain
      valuationInfo = view valuationInformation
   in valuationDom lhs == valuationDom rhs && valuationInfo lhs == valuationInfo rhs

-- | Combination is commutative: @phi ⊗ psi = psi ⊗ phi@.
--
-- >>> let lat = setDomainLattice :: DomainLattice (->) (Set Int) (Set Int)
-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra (->) (->) (->) Int Set Int
-- >>> let pva = PresheafValuationAlgebra lat va
-- >>> lawCombinationCommutative pva (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20)
-- True
{-# SPECIALIZE lawCombinationCommutative ::
  (Eq (set var), Eq v) => PresheafValuationAlgebra' v set var -> Valuation set var v -> Valuation set var v -> Bool
  #-}
lawCombinationCommutative :: (HasSemigroup s1 (->) a, Eq a, Eq (set var), HasDomainLattice s1 (->) (set var) (set var), HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Bool
lawCombinationCommutative pva phi psi =
  let Valuation d1 v1 = combine pva phi psi
      Valuation d2 v2 = combine pva psi phi
   in d1 == d2 && v1 == v2