# Deciding Equations and Inequations in Lattices

#### Peter Jipsen, Chapman University, May 2017

The algorithm implemented here is due to P. M. Whitman (Free lattices, Annals of Math. (2) 42 (1941), 325-330), as presented in Listing 11.16 by R. Freese, J. Jezek and J. B. Nation in "Free Lattices", Math. Surveys and Monographs, Amer. Math. Soc., 1995, viii+293 pages.

The (in)equations are in the language of lattices, using the following LaTeX or ascii symbols:

• "\le", "\leq", "<=", "\lt", "<", "\ge", "\geq", ">=", "\gt", ">", "=" or "==" between two lattice terms
• "\vee", "\join", "\jn", "V", or "+" for join and
• "\wedge", "\meet", "\mt", "\cdot", "^", "*" or " " for meet.
Variables are alphanumeric strings that can also use "\,_,{,}".
In the absence of parentheses, meet takes priority over join.

Enter a string:

${}$

Max depth:   Max arity:   Variables:

Here is Whitman's algorithm in JavaScript:
// x+y*z+w is represented internally as ["+",["x",["*",["y","z"]],"w"]]

val={} // global hash table to record computed subterms

function setval(u,v,bool) {
if (val[u]==undefined) val[u]={}
val[u][v]=bool
return bool
}

function leq(u,v) {  // Whitman's algorithm, as in Listing 11.16 in
// Freese-Jezek-Nation's book "Free Lattices", Amer. Math. Soc., 1995
var i
if (val[u]!=undefined && val[u][v]!=undefined) return val[u][v]
if (u[0]!="+" && u[0]!="*" && v[0]!="+" && v[0]!="*") return u[0]==v[0]
if (u[0]=="+") {
for (i in u[1]) if (!leq(u[1][i],v)) return false
return true
}
if (v[0]=="*") {
for (i in v[1]) if (!leq(u,v[1][i])) return false
return true
}
if (u[0]!="+" && u[0]!="*") {
for (i in v[1]) if (leq(u,v[1][i])) return setval(u,v[1][i],true)
return setval(u,v,false)
}
if (v[0]!="+" && v[0]!="*") {
for (i in u[1]) if (leq(u[1][i],v)) return setval(u[1][i],v,true)
return setval(u,v,false)
}
for (i in u[1]) if (leq(u[1][i],v)) return setval(u[1][i],v,true)
for (i in v[1]) if (leq(u,v[1][i])) return setval(u,v[1][i],true)
return setval(u,v,false)
}