Residuated Lattice - Definition

Definition

In mathematics, a residuated lattice is an algebraic structure L = (L, ≤, •, I) such that

(i) (L, ≤) is a lattice.

(ii) (L, •, I) is a monoid.

(iii) For all z there exists for every x a greatest y, and for every y a greatest x, such that x•y ≤ z (the residuation properties).

In (iii), the "greatest y", being a function of z and x, is denoted x\z and called the right residual of z by x, thinking of it as what remains of z on the right after "dividing" z on the left by x. Dually the "greatest x" is denoted z/y and called the left residual of z by y. An equivalent more formal statement of (iii) that uses these operations to name these greatest values is

(iii)' for all x, y, z in L, y ≤ x\z ⇔ x•y ≤ z ⇔ x ≤ z/y.

As suggested by the notation the residuals are a form of quotient. More precisely, for a given x in L, the unary operations x• and x\ are respectively the lower and upper adjoints of a Galois connection on L, and dually for the two functions •y and /y. By the same reasoning that applies to any Galois connection, we have yet another definition of the residuals, namely,

x•(x\y) ≤ y ≤ x\(x•y), and

(y/x)•x ≤ y ≤ (y•x)/x,

together with the requirement that x•y be monotone in x and y. (When axiomatized using (iii) or (iii)' monotonicity becomes a theorem and hence not required in the axiomatization.) These give a sense in which the functions x• and x\ are pseudoinverses or adjoints of each other, and likewise for •x and /x.

This last definition is purely in terms of inequalities, noting that monotonicity can be axiomatized as x•y ≤ (x∨z)•y and similarly for the other operations and their arguments. Moreover any inequality x ≤ y can be expressed equivalently as an equation, either x∧y = x or x∨y = y. This along with the equations axiomatizing lattices and monoids then yields a purely equational definition of residuated lattices, provided the requisite operations are adjoined to the signature (L, ≤, •, I) thereby expanding it to (L, ∧, ∨, •, I, /, \). When thus organized, residuated lattices form an equational class or variety, whose homomorphisms respect the residuals as well as the lattice and monoid operations. Note that distributivity x•(y∨z) = (x•y) ∨ (x•z) and x•0 = 0 are consequences of these axioms and so do not need to be made part of the definition. This necessary distributivity of • over ∨ does not in general entail distributivity of ∧ over ∨, that is, a residuated lattice need not be a distributive lattice. However it does do so when • and ∧ are the same operation, a special case of residuated lattices called a Heyting algebra.

Alternative notations for x•y include x◦y, x;y (relation algebra), and x⊗y (linear logic). Alternatives for I include e and 1'. Alternative notations for the residuals are x → y for x\y and y ← x for y/x, suggested by the similarity between residuation and implication in logic, with the multiplication of the monoid understood as a form of conjunction that need not be commutative. When the monoid is commutative the two residuals coincide. When not commutative, the intuitive meaning of the monoid as conjunction and the residuals as implications can be understood as having a temporal quality: x•y means x and then y, x → y means had x (in the past) then y (now), and y ← x means if-ever x (in the future) then y (at that time), as illustrated by the natural language example at the end of the examples.