A subsumption lattice is a mathematical structure used in the theoretical background of automated theorem proving and other symbolic computation applications.
A subsumption lattice is a mathematical structure used in the theoretical background of automated theorem proving and other symbolic computation applications.
A term t1 is said to subsume a term t2 if a substitution σ exists such that σ applied to t1 yields t2. In this case, t1 is also called more general thant2, and t2 is called more specific thant1, or an instance oft1.
The set of all (first-order) terms over a given signature can be made a lattice over the partial ordering relation "... is more specific than ..." as follows:
This lattice is called the subsumption lattice. Two terms are said to be unifiable if their meet differs from Ω.
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 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 N5 (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: [2]
 |
 |
 |
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 N5 and the minimal non-distributive lattice M3 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 [3] linear terms, i.e. their anti-unification and unification, corresponds to intersection and union of their path 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).
Apparently, the subsumption lattice was first investigated by Gordon D. Plotkin, in 1970. [4]
In mathematics, pointless topology is an approach to topology that avoids mentioning points, and in which the lattices of open sets are the primitive notions.
In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum (join) and an infimum (meet). Specifically, every non-empty finite lattice is complete. Complete lattices appear in many applications in mathematics and computer science. Being a special instance of lattices, they are studied both in order theory and universal algebra.
In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.
In mathematics, an algebraic structure consists of a nonempty set A, a collection of operations on A of finite arity, and a finite set of identities, known as axioms, that these operations must satisfy.
In mathematics, a Heyting algebra is a bounded lattice equipped with a binary operation a → b of implication such that ≤ b is equivalent to c ≤. From a logical standpoint, A → B is by this definition the weakest proposition for which modus ponens, the inference rule A → B, A ⊢ B, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.
In mathematics, a distributive lattice is a lattice in which the operations of join and meet distribute over each other. The prototypical examples of such structures are collections of sets for which the lattice operations can be given by set union and intersection. Indeed, these lattices of sets describe the scenery completely: every distributive lattice is—up to isomorphism—given as such a lattice of sets.
In mathematics, there is an ample supply of categorical dualities between certain categories of topological spaces and categories of partially ordered sets. Today, these dualities are usually collected under the label Stone duality, since they form a natural generalization of Stone's representation theorem for Boolean algebras. These concepts are named in honor of Marshall Stone. Stone-type dualities also provide the foundation for pointless topology and are exploited in theoretical computer science for the study of formal semantics.
This is a glossary of some terms used in various branches of mathematics that are related to the fields of order, lattice, and domain theory. Note that there is a structured list of order topics available as well. Other helpful resources might be the following overview articles:
A lattice is an abstract structure studied in the mathematical subdisciplines of order theory and abstract algebra. It consists of a partially ordered set in which every pair of elements has a unique supremum and a unique infimum. An example is given by the power set of a set, partially ordered by inclusion, for which the supremum is the union and the infimum is the intersection. Another example is given by the natural numbers, partially ordered by divisibility, for which the supremum is the least common multiple and the infimum is the greatest common divisor.
In mathematics, an antimatroid is a formal system that describes processes in which a set is built up by including elements one at a time, and in which an element, once available for inclusion, remains available until it is included. Antimatroids are commonly axiomatized in two equivalent ways, either as a set system modeling the possible states of such a process, or as a formal language modeling the different sequences in which elements may be included. Dilworth (1940) was the first to study antimatroids, using yet another axiomatization based on lattice theory, and they have been frequently rediscovered in other contexts.
In mathematics, a join-semilattice is a partially ordered set that has a join for any nonempty finite subset. Dually, a meet-semilattice is a partially ordered set which has a meet for any nonempty finite subset. Every join-semilattice is a meet-semilattice in the inverse order and vice versa.
In the branch of mathematics called order theory, a modular lattice is a lattice that satisfies the following self-dual condition,
In mathematics, the lattice of subgroups of a group is the lattice whose elements are the subgroups of , with the partial order relation being set inclusion. In this lattice, the join of two subgroups is the subgroup generated by their union, and the meet of two subgroups is their intersection.
Substitution is a fundamental concept in logic. A substitution is a syntactic transformation on formal expressions. To apply a substitution to an expression means to consistently replace its variable, or placeholder, symbols by other expressions. The resulting expression is called a substitution instance, or instance for short, of the original expression.
In mathematics, the congruence lattice problem asks whether every algebraic distributive lattice is isomorphic to the congruence lattice of some other lattice. The problem was posed by Robert P. Dilworth, and for many years it was one of the most famous and long-standing open problems in lattice theory; it had a deep impact on the development of lattice theory itself. The conjecture that every distributive lattice is a congruence lattice is true for all distributive lattices with at most ℵ1 compact elements, but F. Wehrung provided a counterexample for distributive lattices with ℵ2 compact elements using a construction based on Kuratowski's free set theorem.
In graph theory, a division of mathematics, a median graph is an undirected graph in which every three vertices a, b, and c have a unique median: a vertex m(a,b,c) that belongs to shortest paths between each pair of a, b, and c.
In mathematics, Birkhoff's representation theorem for distributive lattices states that the elements of any finite distributive lattice can be represented as finite sets, in such a way that the lattice operations correspond to unions and intersections of sets. The theorem can be interpreted as providing a one-to-one correspondence between distributive lattices and partial orders, between quasi-ordinal knowledge spaces and preorders, or between finite topological spaces and preorders. It is named after Garrett Birkhoff, who published a proof of it in 1937.
In mathematics, the Dedekind numbers are a rapidly growing sequence of integers named after Richard Dedekind, who defined them in 1897. The Dedekind number M(n) counts the number of monotone boolean functions of n variables. Equivalently, it counts the number of antichains of subsets of an n-element set, the number of elements in a free distributive lattice with n generators, or the number of abstract simplicial complexes with n elements.
In mathematics, the Young–Fibonacci graph and Young–Fibonacci lattice, named after Alfred Young and Leonardo Fibonacci, are two closely related structures involving sequences of the digits 1 and 2. Any digit sequence of this type can be assigned a rank, the sum of its digits: for instance, the rank of 11212 is 1 + 1 + 2 + 1 + 2 = 7. As was already known in ancient India, the number of sequences with a given rank is a Fibonacci number. The Young–Fibonacci lattice is an infinite modular lattice having these digit sequences as its elements, compatible with this rank structure. The Young–Fibonacci graph is the graph of this lattice, and has a vertex for each digit sequence. As the graph of a modular lattice, it is a modular graph.
In mathematics, particularly in order theory, a pseudocomplement is one generalization of the notion of complement. In a lattice L with bottom element 0, an element x ∈ L is said to have a pseudocomplement if there exists a greatest element x* ∈ L, with the property that x ∧ x* = 0. More formally, x* = max{ y ∈ L | x ∧ y = 0 }. The lattice L itself is called a pseudocomplemented lattice if every element of L is pseudocomplemented. Every pseudocomplemented lattice is necessarily bounded, i.e. it has a 1 as well. Since the pseudocomplement is unique by definition, a pseudocomplemented lattice can be endowed with a unary operation * mapping every element to its pseudocomplement; this structure is sometimes called a p-algebra. However this latter term may have other meanings in other areas of mathematics.