- Generated by
1.15.0
|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
Bridge the species' static-method ops (L::AND / L::OR / L::RFL) to the function-object types the :species / :total law registry is keyed on.
More...
Public Member Functions | |
| constexpr L::Ω | operator() (typename L::Ω a) const |
Bridge the species' static-method ops (L::AND / L::OR / L::RFL) to the function-object types the :species / :total law registry is keyed on.
The logic negation ¬ = L::RFL as a callable object. It exists so the :involution machinery can witness that the negation is an involution (¬¬ = id). :sets consults the witness to eliminate double negation at the type level (!!A ≡ A).
The :species / :total law machinery (distributive<T>(Join{}, Meet{}), unit<T>(Op{}), IsDistributiveLattice / IsBoundedLattice) keys every law on the operation's type (a function object such as std::logical_or<bool>, dedekind::category::Sup, dedekind::category::Inf). The logic species carry their ops as static methods on L, which have no type the registry can look up. So each species publishes the op-types its AND / OR / RFL are, as the member aliases JoinOp (∨) / MeetOp (∧) / RflOp (¬):
Boole: JoinOp = std::logical_or<bool>, MeetOp = std::logical_and<bool> (its OR / AND are || / &&, and the Boolean-algebra + complement laws are registered under those types).Kleene / Chain<T>: JoinOp = Sup, MeetOp = Inf (their OR / AND are max / min, the value-returning chain ops from RflOp = logic_complement<L>: the reflection ¬ = L::RFL as a callable (already the With these, distributive<L::Ω>(L::JoinOp{}, L::MeetOp{}) and the whole :total lattice ladder resolve structurally from the species' declared ops — no bespoke logic_is_distributive_v<L> tag ("inference composes,
tagging explodes"). The carrier-level variety witnesses (IsDistributiveLattice / IsBoundedLattice) live in :total (downstream), so they are pinned in logic_lattice_structure_test.cpp; the :species-level trait witnesses are asserted below. Consuming this bridge to gate the full Ockham laws in the IsOckhamAlgebra family is #907.
Boole and Kleene are certified end-to-end (distributive + bounded). Chain<T> publishes the aliases and is asserted distributive only — its boundedness (machine-int numeric_limits poles vs unbounded ℤ) is a deferred design decision, FIXME(#941). Percent is not bridged: its Percentage::v, so generic Sup / Inf (no clamp) do not agree with Percent::OR / AND, and certifying it as a bounded lattice would be unsound; that bridge is FIXME(#940). 1.15.0