Agda-2.4.2.5: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell98

Agda.Utils.SemiRing

Synopsis

Documentation

class SemiRing a where Source

Semirings (https://en.wikipedia.org/wiki/Semiring).

Methods

ozero :: a Source

oone :: a Source

oplus :: a -> a -> a Source

otimes :: a -> a -> a Source

Instances

SemiRing Weight Source 
SemiRing Occurrence Source

Occurrence is a complete lattice with least element Mixed and greatest element Unused.

It forms a commutative semiring where oplus is meet (glb) and otimes is composition. Both operations are idempotent.

For oplus, Unused is neutral (zero) and Mixed is dominant. For otimes, StrictPos is neutral (one) and Unused is dominant.

SemiRing Edge Source

These operations form a semiring if we quotient by the relation "the Occurrence components are equal".

SemiRing a => SemiRing (Maybe a) Source 

class SemiRing a => StarSemiRing a where Source

Star semirings (https://en.wikipedia.org/wiki/Semiring#Star_semirings).

Methods

ostar :: a -> a Source

Instances

StarSemiRing Occurrence Source 
StarSemiRing Edge Source

As OccursWhere does not have an oplus we cannot do something meaningful for the OccursWhere here.

E.g. ostar (Edge JustNeg w) = Edge Mixed (w oplus (w >*< w)) would probably more sense, if we could do it.

StarSemiRing a => StarSemiRing (Maybe a) Source