dedekind::category::IsClosedUnder Concept Reference

(S, Op) is closed under a binary operation: Op{}(s_1, s_2) returns a value of type S for any S-typed operands. The textbook closure axiom expressed structurally — no opt-in trait needed because closure is deducible from the operator's signature. More...

Concept definition

template<typename S, typename Op>
concept dedekind::category::IsClosedUnder =  requires(const S& a, const S& b) {
  { Op{}(a, b) } -> std::same_as<S>;
}

Detailed Description

(S, Op) is closed under a binary operation: Op{}(s_1, s_2) returns a value of type S for any S-typed operands. The textbook closure axiom expressed structurally — no opt-in trait needed because closure is deducible from the operator's signature.

Relationship to IsTotal (defined further down): IsTotal is the stronger axiomatic claim that the operation is total as a function S × S → S (defined for all inputs, achieved via one of the periodic / idempotent / saturating / exact paths). IsClosedUnder is purely about the operator's return type; it does not promise totality. So IsTotal<T, Op> implies IsClosedUnder<T, Op>, but not vice-versa: int under std::plus<> satisfies IsClosedUnder (the operator returns int) but not IsTotal (signed overflow is UB). The three concepts IsClosedUnder / IsTotal / IsClosureForcing (in :total) are siblings:

• IsClosedUnder<S, Op> — structural: signature returns S.
• IsTotal<S, Op> — axiomatic: defined for all inputs AND returns S.
• IsClosureForcing<Op, S, T> — operation is total with a wider codomain T, and T is the universal recipient (the smallest carrier closing Op over S inputs).

Used positively as a witness ("ℕ is closed under +") and negatively in HasClosureForcingShape ("ℕ is @b not closed under −, which is why @c -Cardinality returns @c SignedCardinality"). See docs/design/carrier-lattice.md, the "elementwise dual" section.