it.unimi.dsi.lama4j
Class Sum

java.lang.Object
  it.unimi.dsi.lama4j.AbstractLattice
      it.unimi.dsi.lama4j.AbstractDistributiveLattice
          it.unimi.dsi.lama4j.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&rdquo, 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).

Field Summary

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

RING, UTF8

Method Summary

boolean	comp(Element x, Element y) Checks whether two elements are comparable using Lattice.meet(Element[]).
Set<Element>	elements() Generates iteratively all elements of this lattice.
Set<Element>	generators() Returns a set of generators for the lattice.
Element	inj(int k, Element element) Injects an element of a summand into this sum.
Element	join(Element... element) Returns the join of the provided elements.
boolean	leq(Element x, Element y) Checks whether an element is smaller than or equal to another element using Lattice.meet(Element[]).
Element	meet(Element... element) Returns the meet of the provided elements.
static Lattice	of(Lattice... distributiveLattice) Returns the sum of the given distributive lattices.
static Lattice	of(Lattice[] distributiveLattice, String[] name) Returns the sum of the given distributive lattices, giving them specified names.
Element	one() Returns the one of this lattice.
String	toString()
Element	valueOf(String name) Returns an element of this lattice, given its name.
Element	zero() Returns 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, minus, pscomp, 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)

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

Returns 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 Set<Element> generators()

Description copied from interface: Lattice

Returns a set of generators for the lattice. The set will not include zero or one. There is no guarantee of freeness or minimality.

Returns:

a set of generators.

elements

public Set<Element> elements()

Description copied from class: AbstractLattice

Generates 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

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

Injects 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

Returns 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

Returns 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

Returns 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

Returns 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

Checks 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

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