lattice_term.cppm File Reference

The assembled lattice-law term reducer: the normal form of a term over a bounded lattice, built from the induced laws in :lattice, as one algebra for cata, its type at compile time and its value at run time. More...

#include <concepts>
#include <functional>
#include <type_traits>
#include <utility>
import dedekind.category:f_algebra;

Include dependency graph for lattice_term.cppm:

Classes
struct	dedekind::category::lattice_less_logic< Less >
	The logic species a comparator reports in: Boole (a bool decision) unless the comparator names its own logic typedef (e.g. Kleene, so an undecidable comparison can be Unknown). More...
struct	dedekind::category::lattice_less_logic< Less >
struct	dedekind::category::no_leaf_combine
	The default leaf-combiner performs no domain combination. Two order-incomparable leaves stay a Meet / Join node. A downstream carrier (e.g. sets) injects a Combine that computes the actual domain meet / join of two compatible leaves. structured_and of two halfspaces yields an Interval, say. Combine returns law_inactive when no domain combination applies. This injected policy lets the reducer's incomparable-leaf residual fall through to the carrier's own ∧/∨. More...
struct	dedekind::category::no_canonical_order
	No order for the reducer to canonicalise by: a carrier without one keeps the residue in its authored order, then combines it. More...
struct	dedekind::category::Reduce< Less, Ord, Combine >

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsLatticeLess
	The injected total order: a caller-supplied comparator with a static consteval less<X,Y>() returning a logic value in its lattice_less_logic (default Boole, i.e. bool). The reported logic must be a full IsOckhamAlgebra, so ::True (accessed by lattice_definitely_less) is guaranteed present. The reducer canonicalises only on a definitely-True result, so an Unknown (undecidable) comparison leaves the operands in authoring order. Total-ness is the caller's obligation (Jlt: asserted downstream), not checked here.
concept	dedekind::category::Fires
	Whether a law fired: its result is not law_inactive.
concept	dedekind::category::CombinesMeet
	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.
concept	dedekind::category::CombinesJoin

Typedefs
template<typename Less>
using	dedekind::category::lattice_less_logic_t = typename lattice_less_logic<Less>::type
template<typename Term, typename Less, typename Ord = canonical_order, typename Combine = no_leaf_combine>
using	dedekind::category::reduce_t
	The normal form of Term under Reduce<Less, Ord, Combine>: the type the fold produces, read without running it.

Functions
template<typename Less, typename X, typename Y>
consteval bool	dedekind::category::lattice_definitely_less ()
	Did the comparator decide definitely True? (Unknown/False ⟹ don't reorder: keep authoring order.).

Detailed Description

The assembled lattice-law term reducer: the normal form of a term over a bounded lattice, built from the induced laws in :lattice, as one algebra for cata, its type at compile time and its value at run time.

@partition :lattice_term

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

lattice_term__Overview

:lattice defines the term AST (Meet, Join, Not) and, next to each lattice concept, the equational law it induces as a decomposable, independently testable part. This partition is the assembly: Reduce is the algebra that folds those parts into one normal form under cata (:f_algebra), applying exactly the laws the carrier proves; reduce_t is that normal form's type. Terms are compared only as normal forms, where structural equality is equality of what they denote: a node-by-node == on unreduced terms would give false negatives (a∧b against b∧a), so the term nodes define none (#1116). Reduction power scales with the carrier's structure: a bounded chain collapses the most, and bool (the two-element Boolean lattice) is the optimal witness where every law fires.

It is the engine of the set-expression collapse (epic #888/#890): sets maps & ↦ Meet, | ↦ Join, ~ ↦ Not, 𝔸 ↦ ⊤, Ø ↦ ⊥ and injects the carrier's structured_and / structured_or as the leaf-combine.

lattice_term__Law_Surface

The induced laws assembled here (all in :lattice): unit / annihilator (meet_bounded_law), idempotence (idempotent_law), structural absorption a∧(a∨b)=a (meet_structural_absorption_law), glb/lub collapse of ≤-comparable operands (meet_glb_law), distributivity X∧(P∨Q)→(X∧P)∨(X∧Q) toward DNF (meet_distributivity_law; one direction — meet over join — for termination, not the join-over-meet CNF dual), and De Morgan negation ¬¬A→A / ¬(A∧B)→¬A∨¬B (de_morgan_law), plus commutative canonicalisation by an injected total order. The complement collapse a∧¬a→⊥ (needing a genuinely complemented lattice) and associativity-flattening remain deferred (#890).

lattice_term__Ordering

Two orders enter, both injected (the Juliet posture: the engine clicks against a concept, the caller asserts it over exactly its carriers):

• the semantic order Ord that defines the glb/lub collapse and boundedness (see :lattice); default canonical_order is the carrier's std::less_equal chain. A carrier may bear several lattice orders, so the caller supplies the one its ∧/∨ induce.
• the total order Less, used only to canonicalise commutative operands. It is partial-safe: an Unknown (undecidable) comparison leaves the operands in authoring order (the honest fallback).

Wikipedia: "Lattice (order)", "Absorption law", "Rewriting".

Note

"Never in the history of mathematics has a mathematical theory been the object of such vociferous vituperation as lattice theory." — Gian-Carlo Rota, "The Many Lives of Lattice Theory", Notices of the AMS 44(11), 1997, p. 1440.