GMeet algorithms

October 2022. This document presents the implementation and tests of GMeetStar, GMeetMonoStar, GMeetMonoLazy and GMeetPlus. Paper experiments: Playground:

Notation

Throughout this document we use the following notation. $L$ is a non-empty finite lattice with order $\sqleq$ and join and meet operators $\join, \meet$. The bottom element of $L$ is $\bot$. The set of all endomorphisms (functions $f:L\to L$) is denoted as $\calF$, and it is a lattice with the order $f \sqleqF g \iff (\forall x\in L)\ f(x)\sqleq g(x).$ The join and meet operators in $\calF$ (i.e. $\joinF$ and $\meetF$) are the pointwise join and meet operators in $L$. The endomorphisms that preserve least upper bounds and map $\bot$ to $\bot$ are called join-endomorphisms, and $\calE\subseteq\calF$ is the set of all join-endomorphisms, that is,$\calE\eqdef\set{f:L\to L \given f(\bot)=\bot \,\wedge\, \lr{\forall a,b\in L}\,f(a\join b)= f(a)\join f(b)}.$ The order $\sqleqE$ for $\calE$ is defined as the restriction of $\sqleqF$ to $\calE$, and with this order, $\calE$ is also a lattice. The join operator $\joinE$ coincides with $\joinF$ (pointwise $\join$), but the meet $\meetF$ does not coincide with $\meetF$.

Algorithms of reference

All the algorithms presented compute the maximal join-endomorphism below a given endomorphism.The implementations are based on the following abstract algorithms that do not indicate how to find the pairs $a,b$.

$\mathtt{GMeet}(h)$:

while $\exists a,b\in L$ with $h(a\join b) \neq h(a)\join h(b)$:

if $h(a\join b) \sqgt h(a) \join h(b)$:

$h(a\join b) \leftarrow h(a) \join h(b)$

else:

$h(a) \leftarrow h(a) \meet h(a\join b)$
$h(b) \leftarrow h(b) \meet h(a\join b)$

return $h$

$\mathtt{GMeetMono}(f, g)$:

$h \eqdef f \meetF g$
while $\exists a,b\in L$ with $h(a\join b) \neq h(a)\join h(b)$:

if $h(a\join b) \sqgt h(a) \join h(b)$:

$c = h(a) \join h(b)$
for each $x \sqleq a\join b$

$h(x) \leftarrow h(x) \meet c$

return $h$

Implementations

Notation following variables that are used in the algorithms are present in the lattice L and are assumed to be precomputed: Notation: n is the number of nodes in the lattice. m is the number of edges in the Hasse diagram of the lattice. lub[a][b] is the join (least upper bound) of a and b. glb[a][b] is the meet (greatest lower bound). leq[a][b] is the boolean for $a \sqleq b$. geq[a][b] is the boolean for $a \sqgeq b$. lt[a][b] is the boolean for $a \sqlt b$. gt[a][b] is the boolean for $a \sqgt b$. children[b] is the list of (direct) children of $b$. parents[a] is the list of (direct) parents of $a$. The implementation of the algorithms, including the counters is shown below.
See the full code.