Stability  experimental 

Safe Haskell  None 
Language  Haskell98 
Module supports computations over infinite structures using logical formulas and SMT solving.
 data Variable
 constantVar :: String > Variable
 variable :: String > Variable
 variableName :: Variable > String
 data Formula
 true :: Formula
 false :: Formula
 fromBool :: Bool > Formula
 (/\) :: Formula > Formula > Formula
 and :: [Formula] > Formula
 (\/) :: Formula > Formula > Formula
 or :: [Formula] > Formula
 not :: Formula > Formula
 (==>) :: Formula > Formula > Formula
 (<==) :: Formula > Formula > Formula
 implies :: Formula > Formula > Formula
 (<==>) :: Formula > Formula > Formula
 iff :: Formula > Formula > Formula
 existsVar :: AtomsLogic => Variable > Formula > Formula
 (∃) :: Variable > Formula > Formula
 forAllVars :: AtomsLogic => Variable > Formula > Formula
 (∀) :: Variable > Formula > Formula
 isTrue :: AtomsLogic => Formula > Bool
 isFalse :: AtomsLogic => Formula > Bool
 simplifyFormula :: AtomsLogic => Formula > Formula
 solve :: Formula > Maybe Bool
 data Scope
 type MapVarFun = (Scope, Variable > Variable)
 type FoldVarFun b = (Scope, Variable > b > b)
 class BareNominalType a where
 eq :: a > a > Formula
 variants :: a > Variants a
 mapVariables :: MapVarFun > a > a
 foldVariables :: FoldVarFun b > b > a > b
 type NominalType a = (Ord a, BareNominalType a)
 neq :: BareNominalType a => a > a > Formula
 class Conditional a where
 ite :: Conditional a => Formula > a > a > a
 class Contextual a where
 simplify :: Contextual a => a > a
 data Variants a
 variant :: a > Variants a
 fromVariant :: Variants a > a
 iteV :: Ord a => Formula > a > a > Variants a
 type Atom = Variants Variable
 atom :: String > Atom
 constant :: Constant > Atom
 lt :: Atom > Atom > Formula
 le :: Atom > Atom > Formula
 gt :: Atom > Atom > Formula
 ge :: Atom > Atom > Formula
 type AtomsSpace = State [String]
 newAtom :: AtomsSpace Atom
 runNLambda :: AtomsSpace a > a
 type NominalEither a b = Variants (Either a b)
 left :: a > NominalEither a b
 right :: b > NominalEither a b
 fromLeft :: Ord a => NominalEither a b > Variants a
 fromRight :: Ord b => NominalEither a b > Variants b
 fromEither :: Ord a => NominalEither a a > Variants a
 isLeft :: NominalEither a b > Formula
 isRight :: NominalEither a b > Formula
 type NominalMaybe a = Variants (Maybe a)
 nothing :: NominalMaybe a
 just :: a > NominalMaybe a
 fromJust :: Ord a => NominalMaybe a > Variants a
 fromMaybe :: Ord a => a > NominalMaybe a > Variants a
 maybe :: Ord b => b > (a > b) > NominalMaybe a > Variants b
 isJust :: NominalMaybe a > Formula
 isNothing :: NominalMaybe a > Formula
 maybeIf :: Ord a => Formula > a > NominalMaybe a
 data Set a
 empty :: Set a
 atoms :: Set Atom
 fromList :: NominalType a => [a] > Set a
 singleton :: NominalType a => a > Set a
 insert :: NominalType a => a > Set a > Set a
 insertAll :: NominalType a => [a] > Set a > Set a
 delete :: NominalType a => a > Set a > Set a
 deleteAll :: NominalType a => [a] > Set a > Set a
 isEmpty :: Set a > Formula
 isNotEmpty :: Set a > Formula
 map :: (NominalType a, NominalType b) => (a > b) > Set a > Set b
 filter :: NominalType a => (a > Formula) > Set a > Set a
 mapFilter :: (NominalType a, NominalType b) => (a > NominalMaybe b) > Set a > Set b
 sum :: NominalType a => Set (Set a) > Set a
 exists :: NominalType a => (a > Formula) > Set a > Formula
 forAll :: NominalType a => (a > Formula) > Set a > Formula
 partition :: NominalType a => (a > Formula) > Set a > (Set a, Set a)
 contains :: NominalType a => Set a > a > Formula
 notContains :: NominalType a => Set a > a > Formula
 member :: NominalType a => a > Set a > Formula
 notMember :: NominalType a => a > Set a > Formula
 isSubsetOf :: NominalType a => Set a > Set a > Formula
 isNotSubsetOf :: NominalType a => Set a > Set a > Formula
 isProperSubsetOf :: NominalType a => Set a > Set a > Formula
 isNotProperSubsetOf :: NominalType a => Set a > Set a > Formula
 union :: NominalType a => Set a > Set a > Set a
 unions :: NominalType a => [Set a] > Set a
 intersection :: NominalType a => Set a > Set a > Set a
 intersect :: NominalType a => Set a > Set a > Formula
 disjoint :: NominalType a => Set a > Set a > Formula
 difference :: NominalType a => Set a > Set a > Set a
 (\\) :: NominalType a => Set a > Set a > Set a
 pairs :: (NominalType a, NominalType b) => Set a > Set b > Set (a, b)
 pairsWith :: (NominalType a, NominalType b, NominalType c) => (a > b > c) > Set a > Set b > Set c
 pairsWithFilter :: (NominalType a, NominalType b, NominalType c) => (a > b > NominalMaybe c) > Set a > Set b > Set c
 square :: NominalType a => Set a > Set (a, a)
 atomsPairs :: Set (Atom, Atom)
 differentAtomsPairs :: Set (Atom, Atom)
 triples :: (NominalType a, NominalType b, NominalType c) => Set a > Set b > Set c > Set (a, b, c)
 triplesWith :: (NominalType a, NominalType b, NominalType c, NominalType d) => (a > b > c > d) > Set a > Set b > Set c > Set d
 triplesWithFilter :: (NominalType a, NominalType b, NominalType c, NominalType d) => (a > b > c > NominalMaybe d) > Set a > Set b > Set c > Set d
 atomsTriples :: Set (Atom, Atom, Atom)
 mapList :: (NominalType a, NominalType b) => ([a] > b) > [Set a] > Set b
 replicateSet :: NominalType a => Int > Set a > Set [a]
 replicateSetUntil :: NominalType a => Int > Set a > Set [a]
 replicateAtoms :: Int > Set [Atom]
 replicateAtomsUntil :: Int > Set [Atom]
 hasSizeLessThan :: NominalType a => Set a > Int > Formula
 hasSize :: NominalType a => Set a > Int > Formula
 listSize :: NominalType a => [a] > Variants Int
 listSizeWith :: (a > a > Formula) > [a] > Variants Int
 listMaxSize :: NominalType a => [a] > Int
 listMaxSizeWith :: (a > a > Formula) > [a] > Int
 size :: (Contextual a, NominalType a) => Set a > Variants Int
 sizeWith :: (Contextual a, NominalType a) => (a > a > Formula) > Set a > Variants Int
 maxSize :: (Contextual a, NominalType a) => Set a > Int
 maxSizeWith :: (Contextual a, NominalType a) => (a > a > Formula) > Set a > Int
 isSingleton :: NominalType a => Set a > Formula
 range :: Atom > Atom > Set Atom
 openRange :: Atom > Atom > Set Atom
 isLowerBound :: Atom > Set Atom > Formula
 hasLowerBound :: Set Atom > Formula
 isUpperBound :: Atom > Set Atom > Formula
 hasUpperBound :: Set Atom > Formula
 isMinimum :: Atom > Set Atom > Formula
 hasMinimum :: Set Atom > Formula
 isMaximum :: Atom > Set Atom > Formula
 hasMaximum :: Set Atom > Formula
 isInfimum :: Atom > Set Atom > Formula
 isSupremum :: Atom > Set Atom > Formula
 isConnected :: Set Atom > Formula
 isOpen :: Set Atom > Formula
 isClosed :: Set Atom > Formula
 isCompact :: Set Atom > Formula
 support :: NominalType a => a > [Atom]
 leastSupport :: NominalType a => a > [Atom]
 supports :: NominalType a => [Atom] > a > Formula
 isEquivariant :: NominalType a => a > Formula
 groupAction :: NominalType a => (Atom > Atom) > a > a
 orbit :: NominalType a => [Atom] > a > Set a
 hull :: NominalType a => [Atom] > Set a > Set a
 setOrbit :: NominalType a => Set a > a > Set a
 setOrbits :: NominalType a => Set a > Set (Set a)
 setOrbitsNumber :: (Contextual a, NominalType a) => Set a > Variants Int
 setOrbitsMaxNumber :: (Contextual a, NominalType a) => Set a > Int
 inTheSameOrbit :: NominalType a => [Atom] > a > a > Formula
 inTheSameSetOrbit :: NominalType a => Set a > a > a > Formula
 equivariantSubsets :: (Contextual a, NominalType a) => Set a > Set (Set a)
 data Graph a = Graph {}
 graph :: Set a > Set (a, a) > Graph a
 emptyGraph :: Graph a
 atomsGraph :: Set (Atom, Atom) > Graph Atom
 emptyAtomsGraph :: Graph Atom
 clique :: NominalType a => Set a > Graph a
 atomsClique :: Graph Atom
 simpleClique :: NominalType a => Set a > Graph a
 simpleAtomsClique :: Graph Atom
 monotonicGraph :: Graph Atom
 addVertex :: NominalType a => a > Graph a > Graph a
 removeVertex :: NominalType a => a > Graph a > Graph a
 addEdge :: NominalType a => (a, a) > Graph a > Graph a
 removeEdge :: NominalType a => (a, a) > Graph a > Graph a
 addLoops :: NominalType a => Graph a > Graph a
 removeLoops :: NominalType a => Graph a > Graph a
 reverseEdges :: NominalType a => Graph a > Graph a
 composeEdges :: NominalType a => Set (a, a) > Set (a, a) > Set (a, a)
 compose :: NominalType a => Graph a > Graph a > Graph a
 undirected :: NominalType a => Graph a > Graph a
 subgraph :: NominalType a => Graph a > Set a > Graph a
 hasLoop :: NominalType a => Graph a > Formula
 isSimple :: NominalType a => Graph a > Formula
 containsEdge :: NominalType a => Graph a > (a, a) > Formula
 preds :: NominalType a => Graph a > a > Set a
 succs :: NominalType a => Graph a > a > Set a
 neighbors :: NominalType a => Graph a > a > Set a
 transitiveClosure :: NominalType a => Graph a > Graph a
 existsPath :: NominalType a => Graph a > a > a > Formula
 isStronglyConnected :: NominalType a => Graph a > Formula
 isWeaklyConnected :: NominalType a => Graph a > Formula
 hasCycle :: NominalType a => Graph a > Formula
 hasEvenLengthCycle :: NominalType a => Graph a > Formula
 hasOddLengthCycle :: NominalType a => Graph a > Formula
 isBipartite :: NominalType a => Graph a > Formula
 reachable :: NominalType a => Graph a > a > Set a
 reachableFromSet :: NominalType a => Graph a > Set a > Set a
 weaklyConnectedComponent :: NominalType a => Graph a > a > Graph a
 weaklyConnectedComponents :: NominalType a => Graph a > Set (Graph a)
 stronglyConnectedComponent :: NominalType a => Graph a > a > Graph a
 stronglyConnectedComponents :: NominalType a => Graph a > Set (Graph a)
 isColoringOf :: (NominalType a, NominalType b) => (a > b) > Graph a > Formula
 hasEquivariantColoring :: (Contextual a, NominalType a) => Graph a > Int > Formula
 data Automaton q a = Automaton {
 states :: Set q
 alphabet :: Set a
 delta :: Set (q, a, q)
 initialStates :: Set q
 finalStates :: Set q
 automaton :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton q a
 automatonWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton (Maybe q) a
 accepts :: (NominalType q, NominalType a) => Automaton q a > [a] > Formula
 isNotEmptyAutomaton :: (NominalType q, NominalType a) => Automaton q a > Formula
 isEmptyAutomaton :: (NominalType q, NominalType a) => Automaton q a > Formula
 unionAutomaton :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (Either q1 q2) a
 intersectionAutomaton :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a
 minimize :: (NominalType q, NominalType a) => Automaton q a > Automaton (Set q) a
 da :: (NominalType q, NominalType a) => Set q > Set a > (q > a > q) > q > Set q > Automaton q a
 daWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > (q > a > q) > q > Set q > Automaton (Maybe q) a
 atomsDA :: NominalType q => Set q > (q > Atom > q) > q > Set q > Automaton q Atom
 atomsDAWithTrashCan :: NominalType q => Set q > (q > Atom > q) > q > Set q > Automaton (Maybe q) Atom
 isDeterministic :: (NominalType q, NominalType a) => Automaton q a > Formula
 unionDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a
 complementDA :: NominalType q => Automaton q a > Automaton q a
 differenceDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a
 equivalentDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Formula
 na :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton q a
 naWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton (Maybe q) a
 atomsNA :: NominalType q => Set q > Set (q, Atom, q) > Set q > Set q > Automaton q Atom
 atomsNAWithTrashCan :: NominalType q => Set q > Set (q, Atom, q) > Set q > Set q > Automaton (Maybe q) Atom
 isNondeterministic :: (NominalType q, NominalType a) => Automaton q a > Formula
Formula
Variable
constantVar :: String > Variable Source
Creates a constant with a given value
variableName :: Variable > String Source
Returns the name of the variable.
Type
First order formula with free variables and relations between variables.
Constructors
Connectives
(/\) :: Formula > Formula > Formula infixr 4 Source
Creates a logical conjunction of two given formulas, e.g.
f /\ false == false f /\ true == f f /\ g == g /\ f
(\/) :: Formula > Formula > Formula infixr 3 Source
Creates a logical disjunction of two given formulas, e.g.
f \/ true == true f \/ false == f f \/ g == g \/ f
not :: Formula > Formula Source
Creates a negation of a given formula, e.g.
not true == false not false == true not (not f) == f
(==>) :: Formula > Formula > Formula infix 2 Source
Creates an implication of given formulas, e.g.
false ==> f == true f ==> true == true f ==> g == g <== f
(<==) :: Formula > Formula > Formula infix 2 Source
Creates an implication of given formulas, e.g.
f <== false == true true <== f == true f <== g == g ==> f
implies :: Formula > Formula > Formula Source
Creates a implication of given formulas, equivalent to ==>
.
(<==>) :: Formula > Formula > Formula infix 2 Source
Creates a formula representing "if and only if" relation between given formulas, e.g.
f <==> f == true f <==> not f == false f <==> g == (f /\ g \/ not f /\ not g)
Quantifiers
forAllVars :: AtomsLogic => Variable > Formula > Formula Source
Creates a formula representing ∀x.f
Formula solving
simplifyFormula :: AtomsLogic => Formula > Formula Source
Simplify given formula.
Nominal type
type FoldVarFun b = (Scope, Variable > b > b) Source
Fold function for variables from a scope.
class BareNominalType a where Source
Basic type in NLambda
required by most of functions in the module (without Ord class).
Nothing
eq :: a > a > Formula Source
Checks equivalence of two given elements.
variants :: a > Variants a Source
If a is a variant type then returns variants values.
mapVariables :: MapVarFun > a > a Source
Map all variables from a given scope.
foldVariables :: FoldVarFun b > b > a > b Source
Fold all variables form a given scope.
type NominalType a = (Ord a, BareNominalType a) Source
Basic type in NLambda
required by most of functions in the module.
neq :: BareNominalType a => a > a > Formula Source
Checks whether two elements are not equivalent.
Conditional
class Conditional a where Source
Class of types implementing conditional statements.
cond :: Formula > a > a > a Source
Join two values or returns two variants for undetermined condition in conditional statement.
ite :: Conditional a => Formula > a > a > a Source
if ... then ... else ... with condition solving.
Contextual
class Contextual a where Source
Class of types of expressions to evaluating with a given context.
Nothing
simplify :: Contextual a => a > a Source
Evaluates an expression in the context of a true
formula. In practice all formulas in expressions are solved.
simplify = when true
Variants
Storing values under various conditions, which could not be solved as true
or false
.
Is often the result of ite
or iteV
functions.
Eq a => Eq (Variants a) Source  
Ord a => Ord (Variants a) Source  
Show a => Show (Variants a) Source  
Generic (Variants a) Source  
NFData a => NFData (Variants a) Source  
Ord a => Conditional (Variants a) Source  
(Contextual a, Ord a) => Contextual (Variants a) Source  
(Ord a, BareNominalType a) => BareNominalType (Variants a) Source  
type Rep (Variants a) Source 
fromVariant :: Variants a > a Source
Returns value of a single variant.
iteV :: Ord a => Formula > a > a > Variants a Source
If ... then ... else ... for types that are not instances of Conditional
class.
Atom
lt :: Atom > Atom > Formula Source
Creates a formula that describes the "<" relation between given atoms.
lt a a == false lt a b == gt b a
le :: Atom > Atom > Formula Source
Creates a formula that describes the "≤" relation between given atoms.
le a a == true le a b == ge b a
gt :: Atom > Atom > Formula Source
Creates a formula that describes the ">" relation between given atoms.
gt a a == false gt a b == lt b a
ge :: Atom > Atom > Formula Source
Creates a formula that describes the "≥" relation between given atoms.
ge a a == true ge a b == le b a
type AtomsSpace = State [String] Source
Space with free atoms names.
newAtom :: AtomsSpace Atom Source
Creates a new atom with a previously unused name.
runNLambda :: AtomsSpace a > a Source
Evaluates given value having newAtom
commands.
Either
type NominalEither a b = Variants (Either a b) Source
Variants of Either
values.
left :: a > NominalEither a b Source
Creates a single variant with a Left
value.
right :: b > NominalEither a b Source
Creates a single variant with a Right
value.
fromLeft :: Ord a => NominalEither a b > Variants a Source
fromRight :: Ord b => NominalEither a b > Variants b Source
fromEither :: Ord a => NominalEither a a > Variants a Source
Transforms Either
variants to values variants.
isLeft :: NominalEither a b > Formula Source
Returns a formula describing the condition of occurrence of Left
values in variants.
isRight :: NominalEither a b > Formula Source
Returns a formula describing the condition of occurrence of Right
values in variants.
Maybe
type NominalMaybe a = Variants (Maybe a) Source
Variants of Maybe
values.
nothing :: NominalMaybe a Source
Creates a single variant with Nothing
.
just :: a > NominalMaybe a Source
Creates a single variant with Just
value.
fromJust :: Ord a => NominalMaybe a > Variants a Source
fromMaybe :: Ord a => a > NominalMaybe a > Variants a Source
maybe :: Ord b => b > (a > b) > NominalMaybe a > Variants b Source
isJust :: NominalMaybe a > Formula Source
Returns a condition under which the variants have a Just
value.
isNothing :: NominalMaybe a > Formula Source
Returns a condition under which the variants have a Nothing
value.
maybeIf :: Ord a => Formula > a > NominalMaybe a Source
Nominal set
The set of elements, can be infinite.
Eq a => Eq (Set a) Source  
Ord a => Ord (Set a) Source  
Show a => Show (Set a) Source  
Generic (Set a) Source  
NFData a => NFData (Set a) Source  
NominalType a => Conditional (Set a) Source  
(Contextual a, Ord a) => Contextual (Set a) Source  
NominalType a => BareNominalType (Set a) Source  
type Rep (Set a) Source 
Construction
fromList :: NominalType a => [a] > Set a Source
Create a set from a list of elements.
singleton :: NominalType a => a > Set a Source
Create a set with one given element.
insert :: NominalType a => a > Set a > Set a Source
Insert an element to a set.
insertAll :: NominalType a => [a] > Set a > Set a Source
Insert all elements from a list to a set.
delete :: NominalType a => a > Set a > Set a Source
Delete an element from a set.
deleteAll :: NominalType a => [a] > Set a > Set a Source
Delete all elements from a list from a set.
Emptiness
isNotEmpty :: Set a > Formula Source
Checks whether the set is not empty.
Map and filter
map :: (NominalType a, NominalType b) => (a > b) > Set a > Set b Source
Applies function to all elements of a set and returns a new set.
filter :: NominalType a => (a > Formula) > Set a > Set a Source
Filter all elements that satisfy the predicate.
mapFilter :: (NominalType a, NominalType b) => (a > NominalMaybe b) > Set a > Set b Source
sum :: NominalType a => Set (Set a) > Set a Source
For a set of sets returns the union of these sets.
exists :: NominalType a => (a > Formula) > Set a > Formula Source
Returns a formula describing the membership of an element that satisfy the predicate.
forAll :: NominalType a => (a > Formula) > Set a > Formula Source
Returns a formula describing the condition that all elements of a set satisfy the predicate.
partition :: NominalType a => (a > Formula) > Set a > (Set a, Set a) Source
Partition the set into two sets, one with all elements that satisfy the predicate and one with all elements that don't satisfy the predicate.
Membership
contains :: NominalType a => Set a > a > Formula Source
Returns a formula describing the membership of an element in a set.
notContains :: NominalType a => Set a > a > Formula Source
Returns a formula describing the lack of an element in a set.
member :: NominalType a => a > Set a > Formula Source
Returns a formula describing the membership of an element in a set.
notMember :: NominalType a => a > Set a > Formula Source
Returns a formula describing the lack of an element in a set.
Subsets
isSubsetOf :: NominalType a => Set a > Set a > Formula Source
Returns a formula describing that the first set is a subset of the second set.
isNotSubsetOf :: NominalType a => Set a > Set a > Formula Source
Returns a formula describing that the first set is not a subset of the second set.
isProperSubsetOf :: NominalType a => Set a > Set a > Formula Source
Returns a formula describing that the first set is a proper subset of the second set.
isNotProperSubsetOf :: NominalType a => Set a > Set a > Formula Source
Returns a formula describing that the first set is not a proper subset of the second set.
Combine
unions :: NominalType a => [Set a] > Set a Source
Returns union of sets from a list.
intersection :: NominalType a => Set a > Set a > Set a Source
Returns an intersetion of two sets.
difference :: NominalType a => Set a > Set a > Set a Source
Returns a difference of two sets.
(\\) :: NominalType a => Set a > Set a > Set a infixl 9 Source
See difference
.
Pairs and triples
pairs :: (NominalType a, NominalType b) => Set a > Set b > Set (a, b) Source
Creates a set of pairs of elements from two sets.
pairsWith :: (NominalType a, NominalType b, NominalType c) => (a > b > c) > Set a > Set b > Set c Source
Creates a set of results of applying a function to elements from two sets.
pairsWithFilter :: (NominalType a, NominalType b, NominalType c) => (a > b > NominalMaybe c) > Set a > Set b > Set c Source
square :: NominalType a => Set a > Set (a, a) Source
Creates a set of all pairs of elements from a set.
atomsPairs :: Set (Atom, Atom) Source
Creates a set of all atoms pairs.
differentAtomsPairs :: Set (Atom, Atom) Source
Creates a set of all pairs of different atoms.
triples :: (NominalType a, NominalType b, NominalType c) => Set a > Set b > Set c > Set (a, b, c) Source
Creates a set of triples of elements from three sets.
triplesWith :: (NominalType a, NominalType b, NominalType c, NominalType d) => (a > b > c > d) > Set a > Set b > Set c > Set d Source
Creates a set of results of applying a function to elements from three sets.
triplesWithFilter :: (NominalType a, NominalType b, NominalType c, NominalType d) => (a > b > c > NominalMaybe d) > Set a > Set b > Set c > Set d Source
The composition of triplesWith
and mapFilter
.
mapList :: (NominalType a, NominalType b) => ([a] > b) > [Set a] > Set b Source
Applies a function to all lists of elements from a list of sets, e.g.
>>>
mapList id [atoms, fromList [a,b]]
{[a₁,a] : for a₁ ∊ 𝔸, [a₁,b] : for a₁ ∊ 𝔸}
Replicate
replicateSet :: NominalType a => Int > Set a > Set [a] Source
Creates a set of lists of a given length of elements from a set, e.g.
>>>
replicateSet 3 atoms
{[a₁,a₂,a₃] : for a₁,a₂,a₃ ∊ 𝔸}
replicateSetUntil :: NominalType a => Int > Set a > Set [a] Source
Creates a set of lists up to a given length of elements from a set, e.g.
>>>
replicateSetUntil 3 atoms
{[], [a₁] : for a₁ ∊ 𝔸, [a₁,a₂] : for a₁,a₂ ∊ 𝔸, [a₁,a₂,a₃] : for a₁,a₂,a₃ ∊ 𝔸}
replicateAtoms :: Int > Set [Atom] Source
replicateAtoms n = replicateSet n atoms
replicateAtomsUntil :: Int > Set [Atom] Source
replicateAtomsUntil n = replicateSetUntil n atoms
Size
hasSizeLessThan :: NominalType a => Set a > Int > Formula Source
Returns a formula describing condition that a set has a size less than a given number. It is an inefficient function for large sets and will not return the answer for the infinite sets.
hasSize :: NominalType a => Set a > Int > Formula Source
Returns a formula describing condition that a set has a given size. It is an inefficient function for large sets and will not return the answer for the infinite sets.
listSize :: NominalType a => [a] > Variants Int Source
Returns a variants of numbers of the size of a list.
listSizeWith :: (a > a > Formula) > [a] > Variants Int Source
Returns a variants of numbers of the size of a list with given equality relation.
listMaxSize :: NominalType a => [a] > Int Source
Returns the maximum size of a list for all free atoms constraints.
listMaxSizeWith :: (a > a > Formula) > [a] > Int Source
Returns the maximum size of a list for all free atoms constraints with given equality relation.
size :: (Contextual a, NominalType a) => Set a > Variants Int Source
Returns a variants of numbers of the size of a set. It is an inefficient function for large sets and will not return the answer for the infinite sets.
sizeWith :: (Contextual a, NominalType a) => (a > a > Formula) > Set a > Variants Int Source
Returns a variants of numbers of the size of a set with given equality relation. It will not return the answer for the infinite sets.
maxSize :: (Contextual a, NominalType a) => Set a > Int Source
Returns the maximum size of a set for all free atoms constraints. It is an inefficient function for large sets and will not return the answer for the infinite sets.
maxSizeWith :: (Contextual a, NominalType a) => (a > a > Formula) > Set a > Int Source
Returns the maximum size of a set for all free atoms constraints with given equality relation. It will not return the answer for the infinite sets.
isSingleton :: NominalType a => Set a > Formula Source
Returns a formula describing condition that a set has exacly one element.
Set of atoms properties
range :: Atom > Atom > Set Atom Source
The closed interval of atoms with given minimum and maximum.
openRange :: Atom > Atom > Set Atom Source
The open interval of atoms with given infimum and suprememum.
isLowerBound :: Atom > Set Atom > Formula Source
Checks whether a given atom is the lower bound of a set.
hasLowerBound :: Set Atom > Formula Source
Checks whether a set has the lower bound.
isUpperBound :: Atom > Set Atom > Formula Source
Checks whether a given atom is the upper bound of a set.
hasUpperBound :: Set Atom > Formula Source
Checks whether a set has the upper bound.
hasMinimum :: Set Atom > Formula Source
Checks whether a set has the minimum.
hasMaximum :: Set Atom > Formula Source
Checks whether a set has the maximum.
isConnected :: Set Atom > Formula Source
Checks whether a set is connected.
Group action, support and orbits
support :: NominalType a => a > [Atom] Source
Returns all free atoms of an element. The result list is also support of an element, but not always the least one.
leastSupport :: NominalType a => a > [Atom] Source
Returns the least support of an element. From the result of support
function it removes atoms and check if it is still support.
supports :: NominalType a => [Atom] > a > Formula Source
Checks whether a list of atoms supports an element.
isEquivariant :: NominalType a => a > Formula Source
Checks whether an element is equivariant, i.e. it has empty support.
groupAction :: NominalType a => (Atom > Atom) > a > a Source
Applies permutations of atoms to all atoms in an element.
orbit :: NominalType a => [Atom] > a > Set a Source
Returns an orbit of an element with a given support.
hull :: NominalType a => [Atom] > Set a > Set a Source
For a given list of atoms and a set returns the closure of the set under all automorphisms of atoms that fix every element of the list.
setOrbit :: NominalType a => Set a > a > Set a Source
Returns an orbit of an element in a set.
setOrbitsNumber :: (Contextual a, NominalType a) => Set a > Variants Int Source
Returns a number of orbits of a set.
It uses size
function which is inefficient for large sets and will not return the answer for the infinite sets.
setOrbitsMaxNumber :: (Contextual a, NominalType a) => Set a > Int Source
Returns a maximum number of orbits of a set.
It uses maxSize
function which is inefficient for large sets and will not return the answer for the infinite sets.
inTheSameOrbit :: NominalType a => [Atom] > a > a > Formula Source
Checks whether two elements are in the same orbit with a given support.
inTheSameSetOrbit :: NominalType a => Set a > a > a > Formula Source
Checks whether two elements are in the same orbit of a set.
equivariantSubsets :: (Contextual a, NominalType a) => Set a > Set (Set a) Source
Returns a set of all equivariant subsets of a given set
Graph
A directed graph with vertices of type a and set of pairs representing edges.
Eq a => Eq (Graph a) Source  
Ord a => Ord (Graph a) Source  
Show a => Show (Graph a) Source  
NominalType a => Conditional (Graph a) Source  
(Contextual a, Ord a) => Contextual (Graph a) Source  
NominalType a => BareNominalType (Graph a) Source 
emptyGraph :: Graph a Source
An empty graph.
emptyAtomsGraph :: Graph Atom Source
An empty graph with an Atom
type of vertices.
clique :: NominalType a => Set a > Graph a Source
A graph with complete set of edges. Every pair of vertices are connected.
atomsClique :: Graph Atom Source
A complete graph with atoms vertices.
simpleClique :: NominalType a => Set a > Graph a Source
A clique without loops.
simpleAtomsClique :: Graph Atom Source
A clique with atoms vertices and without loops.
monotonicGraph :: Graph Atom Source
A group with atoms vertices where two atoms are connected if the first one is smaller than the second one.
addVertex :: NominalType a => a > Graph a > Graph a Source
Adds vertex to a graph.
removeVertex :: NominalType a => a > Graph a > Graph a Source
Removes vertex from a graph.
addEdge :: NominalType a => (a, a) > Graph a > Graph a Source
Adds an edge to a graph
removeEdge :: NominalType a => (a, a) > Graph a > Graph a Source
Removes an edge from a graph
addLoops :: NominalType a => Graph a > Graph a Source
Add loops for all vertices in a graph.
removeLoops :: NominalType a => Graph a > Graph a Source
Removes all loops from a graph.
reverseEdges :: NominalType a => Graph a > Graph a Source
Reverses all edges in a graph.
composeEdges :: NominalType a => Set (a, a) > Set (a, a) > Set (a, a) Source
Produces a set of edges containing edges that are obtained by composition of edges in a given set.
compose :: NominalType a => Graph a > Graph a > Graph a Source
Produces a graph with edges that are obtained by composition of edges in a given graph.
undirected :: NominalType a => Graph a > Graph a Source
Adds all reverse edges to existing edges in a graph.
subgraph :: NominalType a => Graph a > Set a > Graph a Source
Returns a subgraph limited to a set of vertices.
hasLoop :: NominalType a => Graph a > Formula Source
Checks whether a graph has a loop.
isSimple :: NominalType a => Graph a > Formula Source
Checks whether a graph does not have a loop
containsEdge :: NominalType a => Graph a > (a, a) > Formula Source
Checks whether a graph has a given edge.
preds :: NominalType a => Graph a > a > Set a Source
Returns all predecessors of a vertex.
succs :: NominalType a => Graph a > a > Set a Source
Returns all successors of a vertex.
neighbors :: NominalType a => Graph a > a > Set a Source
Returns all neighbours of an element in a graph.
transitiveClosure :: NominalType a => Graph a > Graph a Source
Returns a transitive closure of a graph.
existsPath :: NominalType a => Graph a > a > a > Formula Source
Checks whether there is a path from one vertex to the second one in a graph.
isStronglyConnected :: NominalType a => Graph a > Formula Source
Checks whether a graph is strongly connected.
isWeaklyConnected :: NominalType a => Graph a > Formula Source
Checks whether a graph is weakly connected.
hasCycle :: NominalType a => Graph a > Formula Source
Checks whether a graph has a cycle.
hasEvenLengthCycle :: NominalType a => Graph a > Formula Source
Checks whether a graph has a evenlength cycle.
hasOddLengthCycle :: NominalType a => Graph a > Formula Source
Checks whether a graph has a oddlength cycle.
isBipartite :: NominalType a => Graph a > Formula Source
Checks whether a graph (treated as undirected) is bipartite in the sense that it does not have oddlength cycle
reachable :: NominalType a => Graph a > a > Set a Source
Returns all vertices reachable from a vertex in a graph.
reachableFromSet :: NominalType a => Graph a > Set a > Set a Source
Returns all vertices reachable from a set of vertices in a graph.
weaklyConnectedComponent :: NominalType a => Graph a > a > Graph a Source
Returns a weakly connected component of a graph containing a vertex.
weaklyConnectedComponents :: NominalType a => Graph a > Set (Graph a) Source
Returns all weakly connected components of a graph.
stronglyConnectedComponent :: NominalType a => Graph a > a > Graph a Source
Returns a strongly connected component of a graph containing a vertex.
stronglyConnectedComponents :: NominalType a => Graph a > Set (Graph a) Source
Returns all strongly connected components of a graph.
isColoringOf :: (NominalType a, NominalType b) => (a > b) > Graph a > Formula Source
Checks whether a given function is the proper coloring of a graph.
hasEquivariantColoring :: (Contextual a, NominalType a) => Graph a > Int > Formula Source
Checks whether a graph has an equivariant kcoloring.
Automaton
An automaton with a set of state with type q accepting/rejecting words from an alphabet with type a.
Automaton  

(Eq q, Eq a) => Eq (Automaton q a) Source  
(Ord q, Ord a) => Ord (Automaton q a) Source  
(Show q, Show a) => Show (Automaton q a) Source  
(Conditional q, NominalType q, NominalType a) => Conditional (Automaton q a) Source  
(Contextual q, Contextual a, Ord q, Ord a) => Contextual (Automaton q a) Source  
(NominalType q, NominalType a) => BareNominalType (Automaton q a) Source 
automaton :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton q a Source
An automaton constructor.
automatonWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton (Maybe q) a Source
An automaton constructor with additional not accepting state.
accepts :: (NominalType q, NominalType a) => Automaton q a > [a] > Formula Source
Checks whether an automaton accepts a word.
isNotEmptyAutomaton :: (NominalType q, NominalType a) => Automaton q a > Formula Source
Checks whether an automaton accepts any word.
isEmptyAutomaton :: (NominalType q, NominalType a) => Automaton q a > Formula Source
Checks whether an automaton rejects all words.
unionAutomaton :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (Either q1 q2) a Source
Returns an automaton that accepts the union of languages accepted by two automata.
intersectionAutomaton :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a Source
Returns an automaton that accepts the intersection of languages accepted by two automata.
minimize :: (NominalType q, NominalType a) => Automaton q a > Automaton (Set q) a Source
Returns a minimal automaton accepting the same language as a given automaton.
Deterministic automaton
da :: (NominalType q, NominalType a) => Set q > Set a > (q > a > q) > q > Set q > Automaton q a Source
The constructor of a deterministic automaton.
daWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > (q > a > q) > q > Set q > Automaton (Maybe q) a Source
The constructor of a deterministic automaton with additional not accepting state.
atomsDA :: NominalType q => Set q > (q > Atom > q) > q > Set q > Automaton q Atom Source
The constructor of a deterministic automaton with atoms as states.
atomsDAWithTrashCan :: NominalType q => Set q > (q > Atom > q) > q > Set q > Automaton (Maybe q) Atom Source
The constructor of a deterministic automaton with atoms as states with additional not accepting state.
isDeterministic :: (NominalType q, NominalType a) => Automaton q a > Formula Source
Checks whether an automaton is deterministic.
unionDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a Source
Returns a deterministic automaton that accepts the union of languages accepted by two deterministic automata.
complementDA :: NominalType q => Automaton q a > Automaton q a Source
Returns a deterministic automaton that accepts only words rejected by a given automaton.
differenceDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Automaton (q1, q2) a Source
Returns a deterministic automaton that accepts only words accepted by the first automaton and rejeceted by the second.
equivalentDA :: (NominalType q1, NominalType q2, NominalType a) => Automaton q1 a > Automaton q2 a > Formula Source
Checks whether two automata accepts the same languages.
Nondeterministic automaton
na :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton q a Source
The constructor of a nondeterministic automaton.
naWithTrashCan :: (NominalType q, NominalType a) => Set q > Set a > Set (q, a, q) > Set q > Set q > Automaton (Maybe q) a Source
The constructor of a nondeterministic automaton with additional not accepting state.
atomsNA :: NominalType q => Set q > Set (q, Atom, q) > Set q > Set q > Automaton q Atom Source
The constructor of a nondeterministic automaton with atoms as states.
atomsNAWithTrashCan :: NominalType q => Set q > Set (q, Atom, q) > Set q > Set q > Automaton (Maybe q) Atom Source
The constructor of a nondeterministic automaton with atoms as states with additional not accepting state.
isNondeterministic :: (NominalType q, NominalType a) => Automaton q a > Formula Source
Checks whether an automaton is nondeterministic.