Package 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”, 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).

  • Method Details

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