NLambda-1.1

NLambda

Description

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

Synopsis

# Formula

## Variable

data Variable Source

Free variable in a `Formula` or iteration variable in a `Set` or constant.

Creates a constant with a given value

Creates a variable with a given name.

Returns the name of the variable.

## Type

data Formula Source

First order formula with free variables and relations between variables.

## Constructors

Creates the tautology formula.

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.

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

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

Equivalent to `<==>`.

## Quantifiers

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

Creates a formula representing ∃x.f

Equivalent to `existsVar`.

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

Creates a formula representing ∀x.f

Equivalent to `forAllVars`.

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

Returns:

• `Just` `True` if formula is a tautology,
• `Just` `False` if formula is a contradiction,
• `Nothing` otherwise.

# 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

 Source Source Source Source Source Source Source Source Source Source Source Source (Ord a, BareNominalType a) => BareNominalType (Variants a) Source Source Source (BareNominalType a, BareNominalType b) => BareNominalType (Either a b) Source (BareNominalType a, BareNominalType b) => BareNominalType (a, b) Source (NominalType q, NominalType a) => BareNominalType (Automaton q a) Source (BareNominalType a, BareNominalType b, BareNominalType c) => BareNominalType (a, b, c) Source (BareNominalType a, BareNominalType b, BareNominalType c, BareNominalType d) => BareNominalType (a, b, c, d) Source (BareNominalType a, BareNominalType b, BareNominalType c, BareNominalType d, BareNominalType e) => BareNominalType (a, b, c, d, e) Source (BareNominalType a, BareNominalType b, BareNominalType c, BareNominalType d, BareNominalType e, BareNominalType f) => BareNominalType (a, b, c, d, e, f) Source (BareNominalType a, BareNominalType b, BareNominalType c, BareNominalType d, BareNominalType e, BareNominalType f, BareNominalType g) => BareNominalType (a, b, c, d, e, f, g) Source

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.

Instances

 Source Source Conditional a => Conditional [a] Source Ord a => Conditional (Variants a) Source NominalType a => Conditional (Set a) Source NominalType a => Conditional (Graph a) Source Conditional b => Conditional (a -> b) Source (Conditional a, Conditional b) => Conditional (a, b) Source (Conditional q, NominalType q, NominalType a) => Conditional (Automaton q a) Source (Conditional a, Conditional b, Conditional c) => Conditional (a, b, c) Source (Conditional a, Conditional b, Conditional c, Conditional d) => Conditional (a, b, c, d) Source (Conditional a, Conditional b, Conditional c, Conditional d, Conditional e) => Conditional (a, b, c, d, e) Source (Conditional a, Conditional b, Conditional c, Conditional d, Conditional e, Conditional f) => Conditional (a, b, c, d, e, f) Source (Conditional a, Conditional b, Conditional c, Conditional d, Conditional e, Conditional f, Conditional g) => Conditional (a, b, c, d, e, f, g) Source (Conditional a, Conditional b, Conditional c, Conditional d, Conditional e, Conditional f, Conditional g, Conditional h) => Conditional (a, b, c, d, e, f, g, h) Source

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

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

Instances

 Eq a => Eq (Variants a) Source Ord a => Ord (Variants a) Source Show a => Show (Variants a) Source 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

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

Variants of variables.

Creates atom with the given name.

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.

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.

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.

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

Returns a condition under which the variants have a `Just` value.

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

 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 Source type Rep (Set a) Source

## Construction

Returns an empty set.

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.

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

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

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.

Creates a set of all atoms pairs.

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

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 n = replicateSet n atoms`
`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

The closed interval of atoms with given minimum and maximum.

The open interval of atoms with given infimum and suprememum.

Checks whether a given atom is the lower bound of a set.

Checks whether a set has the lower bound.

Checks whether a given atom is the upper bound of a set.

Checks whether a set has the upper bound.

Checks whether an atom is the minimum of a set.

Checks whether a set has the minimum.

Checks whether an atom is the maximum of a set.

Checks whether a set has the maximum.

Checks whether an atom is the infumum of a set.

Checks whether an atom is the supremum of a set.

Checks whether a set is connected.

Checks whether a set is open.

Checks whether a set is closed.

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 Fieldsvertices :: Set a edges :: Set (a, a)

Instances

 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 Source

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

A graph constructor.

An empty graph.

A graph with atoms vertices.

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.

A complete graph with atoms vertices.

simpleClique :: NominalType a => Set a -> Graph a Source

A clique without loops.

A clique with atoms vertices and without loops.

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

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.

Checks whether a graph is strongly connected.

Checks whether a graph is weakly connected.

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

Checks whether a graph has a cycle.

Checks whether a graph has a even-length cycle.

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.

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.

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 Fieldsstates :: Set q alphabet :: Set a delta :: Set (q, a, q) initialStates :: Set q finalStates :: Set q

Instances

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