The value-semantic comprehension \(\{x \in \mathrm{dom} \mid
P(x)\}\) over a finite domain: an argmax result (or any refinement of a bounded interval), carrying both the interval (the finite range ext scans via to_iota_view) and the refinement predicate P.
More...
Public Types | |
| using | Domain = typename OI::Domain |
| using | cardinality_type = dedekind::sets::Finite |
The interval is finite, so the comprehension over it is too. This cardinality_type is metadata (the Finite tag), not a gate ext reads: ext scans to_iota_view of the concrete Interval. | |
| Public Types inherited from dedekind::sets::SetExpr< BoundedSet< OI, P >, OI::Domain, OI::logic_species > | |
| using | Domain |
| using | Codomain |
| using | logic_species |
Public Member Functions | |
| constexpr | BoundedSet (OI d, P p) |
Explicit two-argument constructor. dedekind::sets::SetExpr is a base class, so BoundedSet is no longer an aggregate — the BoundedSet{dom, pred} site in argmax routes here instead of through aggregate init. | |
| constexpr auto | operator() (const Domain &x) const |
χ / membership: x ∈ {dom P} ⟺ in the domain and P-optimal. A comprehension is its own characteristic map, which (with dedekind::sets::SetExpr) makes BoundedSet an IsSet — a first-class DSL citizen, not a bespoke struct. | |
| constexpr std::size_t | size () const |
The domain's cardinality as an addressable size_t. Metadata (the finite bound), not a gate ext reads. | |
| Public Member Functions inherited from dedekind::sets::SetExpr< BoundedSet< OI, P >, OI::Domain, OI::logic_species > | |
| constexpr OI::Domain | ι (const Member &m) const |
Public Attributes | |
| OI | domain |
| P | pred |
Detailed Description
struct dedekind::sequences::BoundedSet< OI, P >
The value-semantic comprehension \(\{x \in \mathrm{dom} \mid
P(x)\}\) over a finite domain: an argmax result (or any refinement of a bounded interval), carrying both the interval (the finite range ext scans via to_iota_view) and the refinement predicate P.
ranges__Argmax_Over_A_Bounded_Domain
The optimum as a filtration, carried with its own finite domain so it flows straight into ext as the single argument the endorsed surface ext(argmax(𝔸|[0,N], cost)) calls.
Both this and dedekind::sets::Comprehension (the DSL's \(\{S\mid P\}\)) are now IsSet via dedekind::sets::SetExpr, and both are callable. The one contract Comprehension does not meet as an argmax result is value ownership: Comprehension holds const Base& (a reference into a named ambient set), whereas an argmax result must own its Interval domain by value to be returned safely — the interval carries its two endpoint values, so the scannable bounds travel with the result. So BoundedSet is precisely the value-owning finite comprehension. Its membership χ is x ∈ {dom | P} ⟺ dom(x) ∧ P(x). ext realises it by scanning to_iota_view of the stored Interval domain, whose endpoint values make the enumeration finite — that to_iota_view gate is what ext reads, not an IsExtensional concept and not size() (which reports the cardinality, not what ext scans).
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/sequences/ranges.cppm
