Subsumption lattice
 | This article, Subsumption lattice, has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
A term t1 is said to subsume a term t2 if a substitution s exists such that s applied to t1 yields t2. In this case, t1 is also called more general than t2, and t2 is called more specific than t1.
The set of all terms over a given signature can be made a lattice over the partial ordering relation "... is more specific than ..." as follows:
- two terms are considered equal if they differ only in their variable namings,
- an artificial minimal element Ω ("the overspecified term") is added, which is considered to be more specific than any other term.
This lattice is called the subsumption lattice.
The join and the meet operation in this lattice are called anti-unification and unification, respectively. A variable x and the artificial element Ω is the top and the bottom element of the lattice, respectively. Each ground term is an atom of the lattice.
If f and g is a binary and unary function symbol, respectively, and x and y denote variables, then the terms f(x,y), f(x,x), f(g(x),g(x)), f(g(x),y), and f(g(x),g(y)) form the minimal non-modular lattice N5; its appearance prevents the subsumption lattice from being modular and hence also from being distributive. Non-modular sublattice N5 in subsumption lattice
Apparently, the subsumption lattice has first been investigated by Gordon D. Plotkin in 1970[1].