Free atoms are defined in the language by single letters: `a`

, `b`

, `c`

, etc. In addition, a free atom can be defined by `atom`

constructor: `atom "free"`

.

Atoms can be compared as follows: `eq a b`

, `neq a b`

, `lt a b`

, `le a b`

, `ge a b`

, `gt a b`

. For equality atoms only the first two comparisons are defined.

The tautology and contradiction are created by functions: `true`

and `false`

. More complex formulas are formed by connectives functions: `/\`

(conjunction), `\/`

(disjunction), `not`

(negation), `==>`

, `<==`

(implications) and `<==>`

(equivalence). For example:

`not (eq a b /\ neq a c) \/ eq b c`

, `(eq a b /\ eq a c) ==> eq b c`

To directly check whether the formula is equal to `true`

or `false`

we have the following functions: `isTrue`

, `isFalse`

, `solve`

. We can solve the above formula as follows:

`solve $ not (eq a b /\ neq a c) \/ eq b c`

, `solve $ (eq a b /\ eq a c) ==> eq b c`

We can also use the function `simplify`

which returns the formula after solving:

`simplify $ not (eq a b /\ neq a c) \/ eq b c`

, `simplify $ (eq a b /\ eq a c) ==> eq b c`

An empty set is created as a result of the function `empty`

. If you simply type `empty`

there is no result because Haskell must know the object type. The type can be determined for example as follows: `empty::Set Atom`

.

To get the set of all atoms we just type: `atoms`

. The elements can be added to a set using `insert`

function: `insert a empty`

and removed by `delete`

function: `delete a atoms`

.

The set can be mapped: `map singleton atoms`

or filtered: `filter (eq a) atoms`

. To compute the union of a family of sets we type: ` sum $ map singleton atoms`

.

We can check the emptiness of a set by: `isEmpty $ filter (\x -> eq a x /\ eq b x) atoms`

. If we are interested whether an element belongs to the set, we can use `member`

or `contains`

function: `member a atoms`

.

The sets can be also compared: ` eq (delete a atoms) (delete b atoms)`

, `isSubsetOf atoms (delete a atoms)`

.

We have also the possibility of calculating the set `union`

, `intersection`

, `difference`

, etc.

Many programs need to operate over the set of atoms tuples. To obtain the set of atoms pairs we can type: `sum $ map (\x -> map (\y -> (x,y)) atoms) atoms`

or simply use a prepared function: `atomsPairs`

.

The function `size`

returns the size of the set: `size (fromList [a,b])`

. Certainly one can expect the answer in finite time only for finite sets. The command `size atoms`

will exceed the time limit.

Conditional expressions are handled by `ite`

function with similar functionality as the classic *if ... then ... else ...* statement. Some examples are presented below:

`ite (eq a b) a b`

(note that the result is equal to`b`

:`eq b (ite (eq a b) a b)`

)`ite (eq a b) (eq a b) (neq a b)`

(formula type)`ite (eq a b) (singleton c) atoms`

(set type)`(ite (eq a b) (const c) id) d`

(function type)`ite (eq a b) (c,d) (d,c)`

(tuple type)`ite (eq a b) [c,d] [d,c]`

(list type, but`ite (eq a b) [] [c]`

will report error)

For types that do not implement *Conditional* class the function `iteV`

can be used:

`iteV (eq a b) 1 2`

`iteV (eq a b) 'a' 'b'`

`iteV (eq a b) True False`

As we can see in the examples above the type *Variants* is used.

Nλ allows to examine sets structure in detail. For this purpose we have the following functions::

- to compute the least support of the element:
`leastSupport a`

,`leastSupport atoms`

- to check whether an element is equivariant:
`isEquivariant a`

,`isEquivariant atoms`

- to find the orbit of an element:
`orbit [] a`

,`orbit [a] a`

,`orbit [b] a`

- to count the number of orbit in a set:
`setOrbitsNumber atoms`

,`setOrbitsNumber atomsPairs`

The latter result depends on the choice of the atoms structure. Function `setOrbitsNumber`

is inefficient for larger tuples due to the use of `size`

function.