A subsumption lattice is a mathematical structure used in the theoretical background of

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a maj ...

and other

symbolic computation In mathematics and computer science, computer algebra, also called symbolic computation or algebraic computation, is a scientific area that refers to the study and development of algorithms and software for manipulating mathematical expressions ...

applications.

Definition

term Term may refer to: * Terminology, or term, a noun or compound word used in a specific context, in particular: **Technical term, part of the specialized vocabulary of a particular field, specifically: ***Scientific terminology, terms used by scient ...

''t''₁ is said to ''subsume'' a term ''t''₂ if a

substitution Substitution may refer to: Arts and media *Chord substitution, in music, swapping one chord for a related one within a chord progression * Substitution (poetry), a variation in poetic scansion * "Substitution" (song), a 2009 song by Silversun Pi ...

''σ'' exists such that ''σ'' applied to ''t''₁ yields ''t''₂. In this case, ''t''₁ is also called ''more general than'' ''t''₂, and ''t''₂ is called ''more specific than'' ''t''₁, or ''an instance of'' ''t''₁. The set of all (first-order) terms over a given

signature A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...

can be made a

lattice Lattice may refer to: Arts and design * Latticework, an ornamental criss-crossed framework, an arrangement of crossing laths or other thin strips of material * Lattice (music), an organized grid model of pitch ratios * Lattice (pastry), an ornam ...

over the partial ordering relation "''... is more specific than ...''" as follows: * consider two terms equal if they differ only in their variable naming, * add an artificial minimal element Ω (the ''overspecified term''), which is considered to be more specific than any other term. This lattice is called the subsumption lattice. Two terms are said to be unifiable if their meet differs from Ω.

Properties

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 In mathematical logic, a ground term of a formal system is a term that does not contain any variables. Similarly, a ground formula is a formula that does not contain any variables. In first-order logic with identity, the sentence Q(a) \lor P(b) ...

, i.e. each term without variables, is an

atom Every atom is composed of a nucleus and one or more electrons bound to the nucleus. The nucleus is made of one or more protons and a number of neutrons. Only the most common variety of hydrogen has no neutrons. Every solid, liquid, gas, and ...

of the lattice. The lattice has infinite descending

chains A chain is a serial assembly of connected pieces, called links, typically made of metal, with an overall character similar to that of a rope in that it is flexible and curved in compression but linear, rigid, and load-bearing in tension. A c ...

, e.g. ''x'', ''g''(''x''), ''g''(''g''(''x'')), ''g''(''g''(''g''(''x''))), ..., but no infinite ascending ones. If ''f'' is a binary function 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 Broadly speaking, modularity is the degree to which a system's components may be separated and recombined, often with the benefit of flexibility and variety in use. The concept of modularity is used primarily to reduce complexity by breaking a sy ...

and hence also from being distributive. The set of terms unifiable with a given term need not be

closed Closed may refer to: Mathematics * Closure (mathematics), a set, along with operations, for which applying those operations on members always results in a member of the set * Closed set, a set which contains all its limit points * Closed interval, ...

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₁'') ⊆ 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'') = Gnd(''t₁'') ∩ Gnd(''t₂''), * if ''t'' is the join of ''t''₁ and ''t''₂, then Gnd(''t'') ⊇ Gnd(''t₁'') ∪ Gnd(''t₂'').

'Sublattice' of linear terms

The set of ''linear'' terms, that is of terms without multiple occurrences of a variable, is a sub-poset of the subsumption lattice, and is itself a lattice. This lattice, too, includes N₅ and the minimal non-distributive lattice M₃ as sublattices (see Pic. 3 and Pic. 4) and is hence not modular, let alone distributive. The ''meet'' operation yields always the same result in the lattice of all terms as in the lattice of linear terms. The ''join'' operation in the all terms lattice yields always an instance of the join in the linear terms lattice; for example, the (ground) terms ''f''(''a'',''a'') and ''f''(''b'',''b'') have the join ''f''(''x'',''x'') and ''f''(''x'',''y'') in the all terms lattice and in the linear terms lattice, respectively. As the join operations do not in general agree, the linear terms lattice is not properly speaking a sublattice of the all terms lattice. Join and meet of two proper linear terms, i.e. their anti-unification and unification, corresponds to intersection and union of their

path A path is a route for physical travel – see Trail. Path or PATH may also refer to: Physical paths of different types * Bicycle path * Bridle path, used by people on horseback * Course (navigation), the intended path of a vehicle * Desire p ...

sets, respectively. Therefore, every sublattice of the lattice of linear terms that does not contain Ω is isomorphic to a set lattice, and hence distributive (see Pic. 5).

Origin

Apparently, the subsumption lattice was first investigated by Gordon D. Plotkin, in 1970.

References

{{reflist Lattice theory Unification (computer science)