Safe Haskell	None
Language	GHC2024

NumHask.Free.StarSemiring

Description

Free star semiring — the initial encoding of StarSemiring.

The counting profile: Plus does not collapse duplicates. For the idempotent profile, see kleeneSimplify.

Synopsis

data StarSemiring a
- = Zero
- | One
- | Plus (StarSemiring a) (StarSemiring a)
- | Times (StarSemiring a) (StarSemiring a)
- | Star (StarSemiring a)
- | Embed a
zero :: StarSemiring a
one :: StarSemiring a
plus :: StarSemiring a -> StarSemiring a -> StarSemiring a
times :: StarSemiring a -> StarSemiring a -> StarSemiring a
star :: StarSemiring a -> StarSemiring a
plusS :: StarSemiring a -> StarSemiring a
embed :: a -> StarSemiring a
lift :: (Eq a, StarSemiring a) => a -> StarSemiring a
normalize :: (Eq a, StarSemiring a) => StarSemiring a -> StarSemiring a
eval :: StarSemiring a => StarSemiring a -> a
foldStarSemiring :: b -> b -> (b -> b -> b) -> (b -> b -> b) -> (b -> b) -> (a -> b) -> StarSemiring a -> b
fromAdditive :: Additive a -> StarSemiring a
fromMultiplicative :: Multiplicative a -> StarSemiring a
kleeneSimplify :: Ord a => StarSemiring a -> StarSemiring a

Documentation

data StarSemiring a Source #

Free star semiring over a carrier type.

The initial encoding of StarSemiring. Extends the free semiring with the Kleene star.

Negate is absent — StarSemiring requires only Distributive, not Subtractive.

Constructors

Zero
One
Plus (StarSemiring a) (StarSemiring a)
Times (StarSemiring a) (StarSemiring a)
Star (StarSemiring a)
Embed a

Instances

Instances details

Eq a => Eq (StarSemiring a) Source #
Instance details Defined in NumHask.Free.StarSemiring Methods (==) :: StarSemiring a -> StarSemiring a -> Bool # (/=) :: StarSemiring a -> StarSemiring a -> Bool #
Ord a => Ord (StarSemiring a) Source #
Instance details Defined in NumHask.Free.StarSemiring Methods compare :: StarSemiring a -> StarSemiring a -> Ordering # (<) :: StarSemiring a -> StarSemiring a -> Bool # (<=) :: StarSemiring a -> StarSemiring a -> Bool # (>) :: StarSemiring a -> StarSemiring a -> Bool # (>=) :: StarSemiring a -> StarSemiring a -> Bool # max :: StarSemiring a -> StarSemiring a -> StarSemiring a # min :: StarSemiring a -> StarSemiring a -> StarSemiring a #
Show a => Show (StarSemiring a) Source #
Instance details Defined in NumHask.Free.StarSemiring Methods showsPrec :: Int -> StarSemiring a -> ShowS # show :: StarSemiring a -> String # showList :: [StarSemiring a] -> ShowS #
Additive (StarSemiring a) Source #	Methods are the smart constructors, so identity absorption happens during a matrix-star computation's block recursion rather than after it. `>>>` `import qualified NumHask.Algebra.Ring as NHR``>>>` `NHR.star (one :: StarSemiring String)`Star One
Instance details Defined in NumHask.Free.StarSemiring Methods (+) :: StarSemiring a -> StarSemiring a -> StarSemiring a Source # zero :: StarSemiring a Source #
Multiplicative (StarSemiring a) Source #
Instance details Defined in NumHask.Free.StarSemiring Methods (*) :: StarSemiring a -> StarSemiring a -> StarSemiring a Source # one :: StarSemiring a Source #
StarSemiring (StarSemiring a) Source #
Instance details Defined in NumHask.Free.StarSemiring Methods star :: StarSemiring a -> StarSemiring a Source # plus :: StarSemiring a -> StarSemiring a Source #

zero :: StarSemiring a Source #

Additive identity.

one :: StarSemiring a Source #

Multiplicative identity.

plus :: StarSemiring a -> StarSemiring a -> StarSemiring a Source #

Addition with identity absorption.

times :: StarSemiring a -> StarSemiring a -> StarSemiring a Source #

Multiplication with identity absorption.

star :: StarSemiring a -> StarSemiring a Source #

Kleene star with universally-lawful simplifications.

star Zero = One holds in every star semiring (star 0 = 1 + 0·star 0). The rules star One = One and star (star a) = star a are not applied — they hold only in Kleene algebra (idempotent profile), not in the counting profile where star 1 = ∞ ≠ 1.

>>> star zero
One

plusS :: StarSemiring a -> StarSemiring a Source #

Positive closure: a⁺ = a · a*.

embed :: a -> StarSemiring a Source #

Embed a carrier value as an atomic generator.

lift :: (Eq a, StarSemiring a) => a -> StarSemiring a Source #

Lift a carrier value, absorbing additive and multiplicative identities.

>>> lift False
Zero
>>> lift True
One

normalize :: (Eq a, StarSemiring a) => StarSemiring a -> StarSemiring a Source #

Normalize a term with respect to star-semiring laws.

>>> normalize (embed False)
Zero

eval :: StarSemiring a => StarSemiring a -> a Source #

Evaluate a term into any StarSemiring.

This is the unique homomorphism out of the free star semiring.

foldStarSemiring :: b -> b -> (b -> b -> b) -> (b -> b -> b) -> (b -> b) -> (a -> b) -> StarSemiring a -> b Source #

Universal property: fold with a target star semiring.

fromAdditive :: Additive a -> StarSemiring a Source #

Inject an additive term into the free star semiring.

fromMultiplicative :: Multiplicative a -> StarSemiring a Source #

Inject a multiplicative term into the free star semiring.

kleeneSimplify :: Ord a => StarSemiring a -> StarSemiring a Source #

ACIZ simplification — Associativity, Commutativity, Idempotence of Plus, with Zero absorption.

Collapses duplicates under Plus and absorbs Zero. Recurse into Times and Star children. This is shallow: full Kleene algebra canonical form (automata minimisation) is not attempted.

Sound only when evaluated into an idempotent (Kleene algebra) target; for counting targets (ℕ), kleeneSimplify changes the value of evaluation.

>>> let x = embed "x" :: StarSemiring String
>>> let y = embed "y"
>>> -- top-level duplicate collapses
>>> kleeneSimplify (plus x x)
Embed "x"
>>> -- child duplicate also collapses
>>> kleeneSimplify (times (plus x x) y)
Times (Embed "x") (Embed "y")
>>> -- star child normalised
>>> kleeneSimplify (star (plus x x))
Star (Embed "x")

Value-preserving for idempotent targets — executable witness over the Warshall Kleene algebra (a law, not a proof; the Arbitrary-powered property awaits a test-suite home rather than a doctest):

>>> import NumHask.Free.Carriers (Warshall (..))
>>> let t = times (plus (embed (Warshall True)) (embed (Warshall True))) (embed (Warshall False))
>>> (eval (kleeneSimplify t), eval t)
(Warshall False,Warshall False)