A quantale is a monoid in complete join-semilattices: a complete join-semilattice equipped with an associative multiplication (*) and unit (one) that distributes over arbitrary joins.

a * joins xs == joins (fmap (a *) xs)
joins xs * a == joins (fmap (* a) xs)
a * bottom == bottom
bottom * a == bottom

If a quantale is also a StarSemiring, then star is the least fixed point, equivalently the join of the geometric series:

star a == joins (iterate (a *) one)

A KleeneAlgebra is therefore the fragment of a (commutative) quantale that only needs these iterative joins, while a quantale admits arbitrary joins.

A residuated quantale: a quantale equipped with the left and right residuals of multiplication.

In any quantale, multiplication by a fixed element preserves joins, so it has both left and right adjoints. These adjoints are the residuals:

a * lres a b <= b
lres a b == joins [ x | a * x <= b ]

rres a b * a <= b
rres a b == joins [ x | x * a <= b ]

The order <= is the one induced by the join-semilattice: x <= y iff x / y == y.

For commutative quantales the two residuals coincide: lres = rres.

A star-autonomous quantale: a quantale with an involutive, order-reversing linear negation.

The negation is an anti-automorphism of the underlying quantale:

neg (neg a) == a
joinLeq a b == joinLeq (neg b) (neg a)
neg (a * b) == neg b * neg a

Multiplicative disjunction (par) and its unit (bot) are the duals of (*) and one:

par a b == neg (neg a * neg b)
bot == neg one

This is the missing connective that turns a quantale into a model of classical linear logic.