Copyright	(c) 2023 Dakotah Lambert
License	MIT
Safe Haskell	Safe-Inferred
Language	Haskell2010

LTK.Decide.Variety

Description

This module provides a general mechanism for constructing decision procedures given an equational characterization of a pseudovariety. One parses the collection of equations, quantifies universally over the bound variables, and determines whether all specified relationships hold.

Since: 1.1

Synopsis

isVariety :: (Ord n, Ord e) => Bool -> String -> FSA n e -> Maybe Bool
isVarietyM :: (Ord n, Ord e) => Bool -> String -> SynMon n e -> Maybe Bool

Documentation

isVariety :: (Ord n, Ord e) => Bool -> String -> FSA n e -> Maybe Bool #

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. The Boolean operand determines whether to check for a *-variety (True) or a +-variety (False). In other words, it determines whether the class containing the empty string is included if that is the only string in the class.

isVarietyM :: (Ord n, Ord e) => Bool -> String -> SynMon n e -> Maybe Bool #

The isVarietyM star desc function is equivalent to isVariety star desc.