NLambda-1.1

Stabilityexperimental
Safe HaskellNone
LanguageHaskell98

NLambda

Contents

Description

Module supports computations over infinite structures using logical formulas and SMT solving.

Synopsis

Formula

Variable

constantVar :: String -> Variable Source

Creates a constant with a given value

variable :: String -> Variable Source

Creates a variable with a given name.

variableName :: Variable -> String Source

Returns the name of the variable.

Type

data Formula Source

First order formula with free variables and relations between variables.

Constructors

true :: Formula Source

Creates the tautology formula.

false :: Formula Source

Creates the contradiction formula.

fromBool :: Bool -> Formula Source

Creates a formula based on a given Bool value.

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

and :: [Formula] -> Formula Source

Creates a logical conjunction of a given list of formulas.

(\/) :: 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

or :: [Formula] -> Formula Source

Creates a logical disjunction of a given list of formulas.

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)

iff :: Formula -> Formula -> Formula Source

Equivalent to <==>.

Quantifiers

existsVar :: AtomsLogic => Variable -> Formula -> Formula Source

Creates a formula representing ∃x.f

(∃) :: Variable -> Formula -> Formula Source

Equivalent to existsVar.

forAllVars :: AtomsLogic => Variable -> Formula -> Formula Source

Creates a formula representing ∀x.f

Formula solving

isTrue :: AtomsLogic => Formula -> Bool Source

Checks whether the formula is a tautology.

isFalse :: AtomsLogic => Formula -> Bool Source

Checks whether the formula is a contradiction.

simplifyFormula :: AtomsLogic => Formula -> Formula Source

Simplify given formula.

solve :: Formula -> Maybe Bool Source

Returns:

Nominal type

data Scope Source

Variables scope.

Constructors

All

All variables.

Free

Only free variables.

type MapVarFun = (Scope, Variable -> Variable) Source

Map function for variables from a scope.

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).

Minimal complete definition

Nothing

Methods

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.

Instances

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.

Methods

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.

Minimal complete definition

Nothing

Methods

when :: Formula -> a -> a Source

Evaluates an expression in the context of a given formula.

Instances

Contextual Bool Source 
Contextual Char Source 
Contextual Double Source 
Contextual Float Source 
Contextual Int Source 
Contextual Integer Source 
Contextual Ordering Source 
Contextual () Source 
Contextual Variable Source 
Contextual Formula Source 
Contextual a => Contextual [a] Source 
Contextual a => Contextual (Maybe a) Source 
(Contextual a, Ord a) => Contextual (Set a) Source 
(Contextual a, Ord a) => Contextual (Variants a) Source 
(Contextual a, Ord a) => Contextual (Set a) Source 
(Contextual a, Ord a) => Contextual (Graph a) Source 
Contextual b => Contextual (a -> b) Source 
(Contextual a, Contextual b) => Contextual (Either a b) Source 
(Contextual a, Contextual b) => Contextual (a, b) Source 
(Contextual k, Contextual v, Ord k, Ord v) => Contextual (Map k v) Source 
(Contextual q, Contextual a, Ord q, Ord a) => Contextual (Automaton q a) Source 
(Contextual a, Contextual b, Contextual c) => Contextual (a, b, c) Source 
(Contextual a, Contextual b, Contextual c, Contextual d) => Contextual (a, b, c, d) Source 
(Contextual a, Contextual b, Contextual c, Contextual d, Contextual e) => Contextual (a, b, c, d, e) Source 
(Contextual a, Contextual b, Contextual c, Contextual d, Contextual e, Contextual f) => Contextual (a, b, c, d, e, f) Source 
(Contextual a, Contextual b, Contextual c, Contextual d, Contextual e, Contextual f, Contextual g) => Contextual (a, b, c, d, e, f, g) Source 
(Contextual a, Contextual b, Contextual c, Contextual d, Contextual e, Contextual f, Contextual g, Contextual h) => Contextual (a, b, c, d, e, f, g, h) Source 

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

data Variants a Source

Storing values under various conditions, which could not be solved as true or false. Is often the result of ite or iteV functions.

variant :: a -> Variants a Source

Creates a single variant.

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

type Atom = Variants Variable Source

Variants of variables.

atom :: String -> Atom Source

Creates atom with the given name.

constant :: Constant -> Atom Source

Creates atom representing given constant

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

Transforms Left variants to values variants, crashes if variants contain a Right value.

fromRight :: Ord b => NominalEither a b -> Variants b Source

Transforms Right variants to values variants, crashes if variants contain a Left value.

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

Transforms Just variants to values variants, crashes if variants contain a Nothing value.

fromMaybe :: Ord a => a -> NominalMaybe a -> Variants a Source

Takes a default value and Maybe variants and returns a variants of values from Just and default value instead of Nothing.

maybe :: Ord b => b -> (a -> b) -> NominalMaybe a -> Variants b Source

Takes a default value, function and Maybe variants and applies function to the values inside the Just or returns the default value instead of Nothing.

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

If a given condition is satisfied returns Just value otherwise returns Nothing.

Nominal set

data Set a Source

The set of elements, can be infinite.

Instances

Construction

empty :: Set a Source

Returns an empty set.

atoms :: Set Atom Source

Returns the set of all atoms.

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

isEmpty :: Set a -> Formula Source

Checks whether the set is empty.

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

Applies function to all elements of a set and extract value from Just results and remove elements with Nothing results.

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

union :: NominalType a => Set a -> Set a -> Set a Source

Returns union of two given sets.

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.

intersect :: NominalType a => Set a -> Set a -> Formula Source

Checks whether two sets intersect.

disjoint :: NominalType a => Set a -> Set a -> Formula Source

Checks whether two sets are disjoint.

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

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

The composition of pairsWith and mapFilter.

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.

atomsTriples :: Set (Atom, Atom, Atom) Source

Creates a set of all atoms triples.

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.

isMinimum :: Atom -> Set Atom -> Formula Source

Checks whether an atom is the minimum of a set.

hasMinimum :: Set Atom -> Formula Source

Checks whether a set has the minimum.

isMaximum :: Atom -> Set Atom -> Formula Source

Checks whether an atom is the maximum of a set.

hasMaximum :: Set Atom -> Formula Source

Checks whether a set has the maximum.

isInfimum :: Atom -> Set Atom -> Formula Source

Checks whether an atom is the infumum of a set.

isSupremum :: Atom -> Set Atom -> Formula Source

Checks whether an atom is the supremum of a set.

isConnected :: Set Atom -> Formula Source

Checks whether a set is connected.

isOpen :: Set Atom -> Formula Source

Checks whether a set is open.

isClosed :: Set Atom -> Formula Source

Checks whether a set is closed.

isCompact :: Set Atom -> Formula Source

Checks whether a set is compact.

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.

setOrbits :: NominalType a => Set a -> Set (Set a) Source

Returns all orbits of 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

data Graph a Source

A directed graph with vertices of type a and set of pairs representing edges.

Constructors

Graph 

Fields

vertices :: Set a
 
edges :: Set (a, a)
 

graph :: Set a -> Set (a, a) -> Graph a Source

A graph constructor.

emptyGraph :: Graph a Source

An empty graph.

atomsGraph :: Set (Atom, Atom) -> Graph Atom Source

A graph with atoms vertices.

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 even-length cycle.

hasOddLengthCycle :: NominalType a => Graph a -> Formula Source

Checks whether a graph has a odd-length 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 odd-length 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 k-coloring.

Automaton

data Automaton q a Source

An automaton with a set of state with type q accepting/rejecting words from an alphabet with type a.

Constructors

Automaton 

Fields

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 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.