Welcome to Nλ console.

The atoms structure can be selected below:

Click the following examples to see how the language works:

Atoms and formulas
Sets
Conditional
Support and orbits

Atoms

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.

Formulas

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

Solving

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