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

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.SemiRing

Synopsis

Documentation

class SemiRing a where #

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

Minimal complete definition

ozero, oone, oplus, otimes

Methods

ozero :: a #

oone :: a #

oplus :: a -> a -> a #

otimes :: a -> a -> a #

Instances

SemiRing Occurrence #

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 Weight # 
SemiRing Edge #

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

Methods

ozero :: Edge #

oone :: Edge #

oplus :: Edge -> Edge -> Edge #

otimes :: Edge -> Edge -> Edge #

SemiRing a => SemiRing (Maybe a) # 

Methods

ozero :: Maybe a #

oone :: Maybe a #

oplus :: Maybe a -> Maybe a -> Maybe a #

otimes :: Maybe a -> Maybe a -> Maybe a #

class SemiRing a => StarSemiRing a where #

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

Minimal complete definition

ostar

Methods

ostar :: a -> a #

Instances

StarSemiRing Occurrence # 
StarSemiRing Edge #

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.

Methods

ostar :: Edge -> Edge #

StarSemiRing a => StarSemiRing (Maybe a) # 

Methods

ostar :: Maybe a -> Maybe a #