dedekind::category::CombinesMeet Concept Reference

The lattice-law reducer as the algebra of cata (:f_algebra, the one fold). A leaf reduces to itself. A Meet / Join assembles the induced laws over its two reduced operand values, most-collapsing first (bounded ▸ idempotent ▸ complement ▸ absorption ▸ distributivity ▸ glb/lub ▸ the injected leaf-combine), a law returning law_inactive ceding to the next; a rewrite (distributivity, the leaf-combine, De Morgan) is folded again. Less canonicalises the commutative residue. Every decision a law makes on the operand types is made inside decltype as well, so the normal form's type is reduce_t below and its value is this fold at run time: one law, two binding times. More...

Concept definition

template<typename C, typename A, typename B>
concept dedekind::category::CombinesMeet = 
    requires(const A& a, const B& b) { C::meet_value(a, b); }

Detailed Description

The lattice-law reducer as the algebra of cata (:f_algebra, the one fold). A leaf reduces to itself. A Meet / Join assembles the induced laws over its two reduced operand values, most-collapsing first (bounded ▸ idempotent ▸ complement ▸ absorption ▸ distributivity ▸ glb/lub ▸ the injected leaf-combine), a law returning law_inactive ceding to the next; a rewrite (distributivity, the leaf-combine, De Morgan) is folded again. Less canonicalises the commutative residue. Every decision a law makes on the operand types is made inside decltype as well, so the normal form's type is reduce_t below and its value is this fold at run time: one law, two binding times.

Template Parameters

Less	the injected total order (canonicalisation).
Ord	the semantic lattice order (boundedness, glb, distributivity).
Combine	the carrier's domain meet / join of two leaves, meet_value / join_value, each present only where the carrier combines that pair.

The injected leaf-combine has a domain meet (join) for this pair of leaves: C::meet_value(a, b) (join_value) is formed.

Template Parameters

C	the combine.
A,B	the leaves.