Copyright | (c) 2023 Dakotah Lambert |
---|---|
License | MIT |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module provides a general mechanism for constructing decision procedures given an equational characterization of a pseudovariety, or an inequational characterization of an ordered pseudovariety. One parses the collection of equations, quantifies universally over the bound variables, and determines whether all specified relationships hold.
Synopsis
- isVariety :: FiniteSemigroupRep s => String -> OrderedSemigroup s -> Maybe Bool
Documentation
A (pseudo)variety is specified here by a system of equations. These equations may contain (single-letter) variables, which are universally quantified. The grammar is as follows:
expr ::= '[' conj-list ']' conj-list ::= rel-list ';' conj-list | rel-list rel-list ::= value op rel-list | value op value op ::= '=' | '<' | '≤' | '>' | '≥' value ::= value value | iter iter ::= '0' | '1' | LETTER | '(' value ')' | iter '*'
Here, LETTER
refers to any character which Unicode deems a letter.
Concatenation is denoted by adjacency,
and x*
represents the unique element of the form
x
, xx
, and so on, such that x*x*=x*
.
A LETTER
represents a universally-quantified variable,
while 0
and 1
refer to the unique elements where for all x
it holds that 0x=0=x0
and 1x=x=x1
,
if such elements exist.
If 0
or 1
is used in an equation,
but the given structure lacks such an element,
then the structure of course does not satisfy the equality.
The equality x=y
asserts that,
for all possible variable instantiations,
the value of x
is the same as that of y
.
The inequality x<y
asserts that,
for all possible variable instantiations,
the value x
is less than that of y
in the specified order.
For longer chains of relations, adjacent pairs are tested.
That is, [a<b>c]
is equivalent to [a<b;b>c]
.
Essentially, the semicolon is an "and" operator.
Suppose we wish to express the \(*\)-variety
of idempotent and commutative monoids.
A monoid is idempotent if and only if it holds that xx=x
for all values x
, which can also be expressed as x*=x
.
It is commutative if and only if ab=ba
for all a
and b
.
This variety could then be expressed as [ab=ba;x*=x]
.
isVariety :: FiniteSemigroupRep s => String -> OrderedSemigroup s -> Maybe Bool Source #
Determine whether a given semigroup is in the pseudovariety described by the given equation set. Returns Nothing if and only if the equation set cannot be parsed. To check for a \(*\)-variety, pass in a monoid. For a \(+\)-variety, use a semigroup.