it.unimi.dsi.lama4j

## Class Sum

• All Implemented Interfaces:
Lattice

```public class Sum
extends AbstractDistributiveLattice```
The (categorical) sum (a.k.a. free direct product) of distributive lattices.

As for every algebraic theory, elements are terms built from the elements of the two lattices, and quotiented w.r.t. all equations of the theory and all equations that are true in either summand. Each element of a summand is thus identified with an element of the sum, which can be obtained by injection.

In this implementation, to avoid equivalence classes and make the sum computable we restrict to distributive lattices and use Grätzer–Lakser's (disjunctive) canonical representatives (see “Chain conditions in the distributive free product of lattices”, Trans. Amer. Math. Soc., 144:301−312, 1969) described in clausal form.

A clause is a set of elements from the summands. A reduced clause is a clause containing at most one element from each summand. A (clausal) formula is a set of clauses.

Formulae can be interpreted in a disjunctive or conjunctive way (i.e., as a join of meets or a meet of joins), and both intepretations are used during computations. A (disjunctive or conjunctive) reduced formula is a set of reduced clauses in which no clause can be eliminated without affecting the formula's value. Elements of a sum are stored as disjunctive reduced formulae.

Warning: if one of the summands is trivial (just one element) it will not annihilate the sum (as it should happen) but rather it will behave like a neutral element (a rôle actually played by the two-element Boolean lattice). This unfortunate restriction is caused by the difficulty of detecting whether one of the summands is trivial (as `Lattice.elements()` is optional).

• ### Fields inherited from interface it.unimi.dsi.lama4j.Lattice

`RING, UTF8`
• ### Method Summary

All Methods
Modifier and Type Method and Description
`boolean` ```comp(Element x, Element y)```
Check whether two elements are comparable using `Lattice.meet(Element[])`.
`Collection<Element>` `elements()`
Generate iteratively all elements of this lattice.
`Collection<Element>` `generators()`
Return a collection of generators for the lattice.
`Element` ```inj(int k, Element element)```
Inject an element of a summand into this sum.
`Element` `join(Element... element)`
Return the join of the provided elements.
`boolean` ```leq(Element x, Element y)```
Check whether an element is smaller than or equal to another element using `Lattice.meet(Element[])`.
`Element` `meet(Element... element)`
Return the meet of the provided elements.
`static Lattice` `of(Lattice... distributiveLattice)`
Return the sum of the given distributive lattices.
`static Lattice` ```of(Lattice[] distributiveLattice, String[] name)```
Return the sum of the given distributive lattices, giving them specified names.
`Element` `one()`
Return the one of this lattice.
`String` `toString()`
`Element` `valueOf(String name)`
Return an element of this lattice, given its name.
`Element` `zero()`
Return the zero of this lattice.
• ### Methods inherited from class it.unimi.dsi.lama4j.AbstractDistributiveLattice

`isDistributive`
• ### Methods inherited from class it.unimi.dsi.lama4j.AbstractLattice

`coveringRelation, ensureElementsInLattice, ensureElementsInLattice, ensureElementsInLattice, pscomp, psdiff, symdiff, valueOfZeroOrOne`
• ### Methods inherited from class java.lang.Object

`clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait`
• ### Method Detail

• #### of

`public static Lattice of(Lattice... distributiveLattice)`
Return the sum of the given distributive lattices.
Parameters:
`distributiveLattice` - the distributive lattices whose sum has to be computed.
Returns:
the sum of the specified distributive lattices.
• #### of

```public static Lattice of(Lattice[] distributiveLattice,
String[] name)```
Return the sum of the given distributive lattices, giving them specified names.
Parameters:
`distributiveLattice` - the distributive lattices whose sum has to be computed.
`name` - a parallel list of names for each `distributiveLattice`.
Returns:
the sum of the specified distributive lattices.
• #### generators

`public Collection<Element> generators()`
Description copied from interface: `Lattice`
Return a collection of generators for the lattice. The set will not include `zero` or `one`. There is no guarantee of freeness or minimality.
Returns:
a collection of generators.
• #### elements

`public Collection<Element> elements()`
Description copied from class: `AbstractLattice`
Generate iteratively all elements of this lattice.

This methods uses `Lattice.generators()` to obtain an initial set of elements, and then computes joins and meets of all available elements until no new elements are generated. It is expected that concrete subclasses will override this method with an ad hoc, more efficient implementation.

It is strongly suggested that concrete subclasses that do not override this method cache its result internally.

Specified by:
`elements` in interface `Lattice`
Overrides:
`elements` in class `AbstractLattice`
Returns:
the set of elements of this lattice.
• #### valueOf

`public Element valueOf(String name)`
Description copied from interface: `Lattice`
Return an element of this lattice, given its name.

Certain lattices make it possible to define names for elements. This method returns the element corresponding to the provided name.

Parameters:
`name` - the name of an element of this lattice.
Returns:
the element of this lattice named `name`.
• #### inj

```public Element inj(int k,
Element element)```
Inject an element of a summand into this sum.
Parameters:
`k` - the index of a summand.
`element` - an element of the `k`-th summand.
Returns:
the corresponding element of this sum.
• #### zero

`public Element zero()`
Description copied from interface: `Lattice`
Return the zero of this lattice.

Note that there is no guarantee that the returned element is the only element representing zero in this lattice. Other zeroes may arise from computations, but they will always be equal to the element returned by this method.

Returns:
the zero of this lattice.
• #### one

`public Element one()`
Description copied from interface: `Lattice`
Return the one of this lattice.

Note that there is no guarantee that the returned element is the only element representing one in this lattice. Other ones may arise from computations, but they will always be equal to the element returned by this method.

Returns:
the one of this lattice.
• #### meet

`public Element meet(Element... element)`
Description copied from interface: `Lattice`
Return the meet of the provided elements. In particular, upon the empty list of arguments returns `one`, and upon a singleton list the only specified element.
Parameters:
`element` - the elements whose meet has to be computed.
Returns:
the meet of the provided elements.
• #### join

`public Element join(Element... element)`
Description copied from interface: `Lattice`
Return the join of the provided elements. In particular, upon the empty list of arguments returns `zero`, and upon a singleton list the only specified element.
Parameters:
`element` - the elements whose join has to be computed.
Returns:
the join of the provided elements.
• #### toString

`public String toString()`
Overrides:
`toString` in class `Object`
• #### comp

```public boolean comp(Element x,
Element y)```
Description copied from class: `AbstractLattice`
Check whether two elements are comparable using `Lattice.meet(Element[])`.
Specified by:
`comp` in interface `Lattice`
Overrides:
`comp` in class `AbstractLattice`
Parameters:
`x` - an element.
`y` - another element.
Returns:
true iff `x.meet(y)` equals `x` or `y`.
• #### leq

```public boolean leq(Element x,
Element y)```
Description copied from class: `AbstractLattice`
Check whether an element is smaller than or equal to another element using `Lattice.meet(Element[])`.
Specified by:
`leq` in interface `Lattice`
Overrides:
`leq` in class `AbstractLattice`
Parameters:
`x` - an element.
`y` - another element.
Returns:
true iff `x.meet(y)` equals `x`.