page_title: Subsumption lattice
section_title: Properties
hierarchical_section_title: Subsumption lattice / Properties
caption_attribution_description: English: Shows a part of the subsumption lattice, demonstrating that the terms f(a,x), f(x,x), and f(x,c), do not have a common instance other than the bottom term Ω (introduced by Reynolds to indicate non-unifiability), although each two of them are syntactically unifiable. The setting assumes that f is a binary function symbol (omitted in the picture), a and c are constants, and x and y are variables. All involved terms term have f(x,y) as a common upper bound; all its instances by variables or constants are shown, the relevant ones highlighted in red.
context_page_description: A subsumption lattice is a mathematical structure used in the theoretical background of automated theorem proving and other symbolic computation applications.
context_section_description: The join and the meet operation in this lattice are called anti-unification and unification, respectively. A variable x and the artificial element Ω are the top and the bottom element of the lattice, respectively. Each ground term, i.e. each term without variables, is an atom of the lattice. The lattice has infinite descending chains, e.g. x, g(x), g(g(x)), g(g(g(x))), ..., but no infinite ascending ones.
  If f is a binary fuction symbol, g is a unary function symbol, and x and y denote variables, then the terms f(x,y), f(g(x),y), f(g(x),g(y)), f(x,x), and f(g(x),g(x)) form the minimal non-modular lattice N₅ (see Pic. 1); its appearance prevents the subsumption lattice from being modular and hence also from being distributive.
  The set of terms unifiable with a given term need not be closed with respect to meet; Pic. 2 shows a counter-example.
  Denoting by Gnd(t) the set of all ground instances of a term t, the following properties hold:
  t equals the join of all members of Gnd(t), modulo renaming,
  t₁ is an instance of t₂ if and only if Gnd(t₁) is a subset of Gnd(t₂),
  terms with the same set of ground instances are equal modulo renaming,
  if t is the meet of t₁ and t₂, then Gnd(t) is the intersection of Gnd(t₁) and Gnd(t₂),
  if t is the join of t₁ and t₂, then Gnd(t) includes the union of Gnd(t₁) and Gnd(t₂).
caption: Pic. 2: Part of the subsumption lattice showing that the terms f(a,x), f(x,x), and f(x,c) are pairwise unifiable, but not simultaneously. (f omitted for brevity.)