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.

Enter a string: xy+xz+yz \leq (x+y)(x+z)(y+z)

Check a random inequation   Max depth:   Max arity:   Variables:

// 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)
}