dedekind::category::HasLogicSpecies Concept Reference

The equational laws a lattice concept induces, as compile-time term-reduction rules over the term AST below. Each law is a decomposable, independently-testable part; the assembled reducer (:lattice_term) applies exactly the laws the supplied carrier proves. The richer the carrier's structure (a bounded chain is the sweet spot; bool the optimal witness), the more laws fire and the further a term collapses. More...

Concept definition

template<typename A>
concept dedekind::category::HasLogicSpecies = 
    requires { typename std::remove_cvref_t<A>::logic_species; }

Detailed Description

The equational laws a lattice concept induces, as compile-time term-reduction rules over the term AST below. Each law is a decomposable, independently-testable part; the assembled reducer (:lattice_term) applies exactly the laws the supplied carrier proves. The richer the carrier's structure (a bounded chain is the sweet spot; bool the optimal witness), the more laws fire and the further a term collapses.

lattice__Bounded_Canonical_Witnesses

lattice__Induced_Reduction_Laws

A law is a constexpr function on two already-reduced operand values; it returns the rewritten value or law_inactive (the law did not fire: the assembler then tries the next). Where the operand types differ the decision is on the types, so the result's type is the normal form's type and the assembler reads it inside decltype; the same function runs on values at run time. Order-dependent laws (units, glb/lub collapse) are keyed to the injected order Ord so that the boundary / comparison they use is the one this lattice's ∧/∨ induce, not another order the same carrier happens to bear (e.g. the numeric chain vs order::bit_subset_eq on an integer).

The term AST. Leaves are lattice-carrier types; the nodes combine them.

lattice__AST_dual_nature

A node is the combined set VALUE: constructed from operand values (aggregate init Meet<A,B>{a,b}), reduced as a value by the one fold, and its type is the compile-time reading of that same fold (reduce_t), so the type-level exhibits name Meet<A,B> in same_as contexts without instantiating a value.

When it is constructed from operand values, a node is the combined set: it carries the operands and evaluates pointwise through the operands' shared logic_species (∧ = L::AND, ∨ = L::OR, ¬ = L::RFL). The operator() is guarded, so it exists only when the operands are callable predicates over one logic. The type-level tag use is unaffected. This is the seam toward "the AST is the set" (#892): the set operators now return these nodes, and the predicate-nested collapse representation they replaced (the retired AndPredicate / OrPredicate) has been removed.

A predicate that names its logic: A::logic_species is formed, the species whose AND / OR / RFL a node evaluates through.

Template Parameters

A	the predicate.