The bridge between order's intervals and std::ranges iota views, and the bounded sets built on it. More...
#include <array>#include <concepts>#include <cstddef>#include <cstdint>#include <functional>#include <iterator>#include <limits>#include <optional>#include <ranges>#include <stdexcept>#include <type_traits>import dedekind.sequences:path;import dedekind.sets;import dedekind.order;import dedekind.category;
Classes | |
| struct | dedekind::sequences::detail::IotaBounds< T > |
The to_iota_view and from_iota_view): the Interval / Singleton / Empty kinds of a Interval, read off its value endpoints. An unbounded kind (Halfspace / Universe) has no finite range and yields the empty bounds; a per-arm overload will refuse it once the set is a coproduct (#970). More... | |
| 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. More... | |
| struct | dedekind::sequences::DominanceRefinement< T, OI, Cost, Order > |
The dominance-refinement predicate of an argmax: x is optimal iff no member x' of the (finite) domain beats it under order∘cost, i.e. \(\forall x' \in \mathrm{dom}.\ \mathrm{order}(\mathrm{cost}(x'),
\mathrm{cost}(x))\). A named functor rather than a capturing lambda, so the refinement is an inspectable type carried in the BoundedSet signature argmax returns — the ∀-filter made visible at compile time. More... | |
| struct | dedekind::sequences::IotaIntersection |
std::ranges::iota_view as a Form-chain object: an order::IsOrderMeetSemilattice under subset-inclusion, with intersection as the meet. More... | |
| class | dedekind::sequences::chain_view< C > |
Namespaces | |
| namespace | dedekind::sequences::detail |
The interval ↔ iota_view bridge: order's Interval<T,L>, a value, read as the half-open std::ranges::iota_view bound), and back, as a total inverse. | |
| namespace | dedekind::sequences::detail_boundedset_witness |
Witness: BoundedSet is a set. IsSet is reached by inheriting dedekind::sets::SetExpr and supplying the χ — the same opt-in surface Comprehension uses; nominal, never a precondition. | |
| namespace | dedekind::sequences::halfspace_iota_witness |
| namespace | dedekind::sequences::bridge_meet_witness |
| namespace | dedekind::category |
Typedefs | |
| using | dedekind::sequences::detail_boundedset_witness::WOI = dedekind::order::Interval<int, dedekind::category::Boole> |
Enumerations | |
| enum class | dedekind::sequences::halfspace_iota_witness::Strictness |
| Whether the boundary is strict (>, <) or inclusive (>=, <=). | |
| enum class | dedekind::sequences::bridge_meet_witness::Strictness |
| Whether the boundary is strict (>, <) or inclusive (>=, <=). | |
Functions | |
| template<std::integral T, typename L> | |
| constexpr IotaBounds< T > | dedekind::sequences::detail::iota_bounds (const dedekind::order::Interval< T, L > &s) |
| template<std::integral T, typename L> | |
| constexpr std::ranges::iota_view< T, T > | dedekind::sequences::to_iota_view (const dedekind::order::Interval< T, L > &s) |
The typed→runtime half of the iso: project a finite value set (the reduced meet, e.g. structured_and of two intervals) to its canonical std::ranges::iota_view — the same set of integers viewed as a range rather than a predicate. | |
| template<std::integral T, typename L, typename Chi> | |
| auto | dedekind::sequences::ext (const dedekind::order::Interval< T, L > &oi, Chi chi) |
Realise a finite interval domain into its ExtensionalSet, keeping the members that satisfy chi. The interval is the bounded meet that carries the finiteness certificate (cardinality_type = Finite, so IsExtensional); to_iota_view is the only on-ramp from that bounded meet to a scannable range, and the fold is the existing dedekind::sets::ext. An unbounded set has no to_iota_view and cannot reach here — the Rice wall made structural rather than checked. Two-argument form takes the argmax (or any) predicate; the one-argument form realises the whole interval (chi = ⊤). | |
| template<std::integral T, typename L> | |
| auto | dedekind::sequences::ext (const dedekind::order::Interval< T, L > &oi) |
One-argument overload: realise the whole finite interval (every member kept). The chi = ⊤ case of the two-argument ext — it delegates there with the canonical tautology / top predicate dedekind::category::classifier_true. | |
| template<std::integral T, typename L, typename Cost, typename Order = std::less_equal<>> | |
| constexpr auto | dedekind::sequences::argmax (const dedekind::order::Interval< T, L > &dom, Cost cost, Order order={}) |
argmax over a bounded (closed-interval) domain: the §3.3 forall- filter {x ∈ dom | ∀x'∈dom. cost(x') ≤ cost(x)}, with ≤ pulled back through cost. Returns a BoundedSet — intensional (the ∀ is decidable because dom is finite) and carrying its domain, so ext realises it. IsSet-valued: ∅ / singleton (unique optimiser, a function) / larger (ties, a proper relation). | |
| template<typename OI, typename P> | |
| auto | dedekind::sequences::ext (const BoundedSet< OI, P > &bs) |
ext a BoundedSet: scan its domain, keep the members its predicate accepts — an ordered ExtensionalSet (the std::set flavour). This is the single-argument call the endorsed ext(argmax(dom, cost)) surface makes. | |
| template<std::size_t N, typename Seq> | |
| constexpr std::array< typename std::remove_cvref_t< Seq >::Codomain, N > | dedekind::sequences::ext (const Seq &s) |
The sequence flavour of ext: realise the first N terms of a sequence (a bra/ket / Path / any index→value arrow) into a std::array — positional and indexed, dual to the set flavour's std::set. The compile-time N is the Kleene bound (the finite prefix); this is the QM realise — an infinite bra/ket, bounded to N (ext<N>(seq)); the no-N form realises a bounded set instead. | |
| template<dedekind::order::Strictness SL, dedekind::order::Strictness SU, typename L = dedekind::category::Boole, std::integral T> | |
| constexpr dedekind::order::Interval< T, L > | dedekind::sequences::from_iota_view (const std::ranges::iota_view< T, T > &iv) |
The runtime→typed half of the iso, a total inverse: rebuild the interval from the iota_view's | |
Detailed Description
The bridge between order's intervals and std::ranges iota views, and the bounded sets built on it.
@partition :ranges
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
ranges__Interval_as_Range
An interval is order's two-sided cut Interval<T,SL,SU,L> — two bounds, values, over a discrete chain. This partition reads it as the half-open std::ranges::iota_view [start, bound) and back: to_iota_view normalises the strictness of the bounds through the NNO step, and from_iota_view is its total inverse. Everything finite about a bounded set — its size, its enumeration ext, argmax over a cost — is derived from that reading rather than stored, so a set stays a predicate and the range is a view of it.
Wikipedia: Interval (mathematics), Half-open interval, Range (computer programming)
- Note
- "Die Zahlen sind freie Schöpfungen des menschlichen Geistes, sie dienen als ein Mittel, um die Verschiedenheit der Dinge leichter und schärfer aufzufassen." – Richard Dedekind, Was sind und was sollen die Zahlen?, Vorwort (1888) [Trans: "The numbers are free creations of the human mind; they serve as a means of grasping the diversity of things more easily and more sharply."]
Function Documentation
◆ ext()
|
export |
Realise a finite interval domain into its ExtensionalSet, keeping the members that satisfy chi. The interval is the bounded meet that carries the finiteness certificate (cardinality_type = Finite, so IsExtensional); to_iota_view is the only on-ramp from that bounded meet to a scannable range, and the fold is the existing dedekind::sets::ext. An unbounded set has no to_iota_view and cannot reach here — the Rice wall made structural rather than checked. Two-argument form takes the argmax (or any) predicate; the one-argument form realises the whole interval (chi = ⊤).
— the last plank of the bridge
intensional → intensional-finite → ext → extensional.
◆ from_iota_view()
|
constexprexport |
The runtime→typed half of the iso, a total inverse: rebuild the interval from the iota_view's [start, bound) by undoing the strictness offsets, read as the strictness pair asked for; every iota_view names an interval (an empty view names the empty interval).
The NTTP form could only verify a view against a target type, since the bounds lived in the type; with the endpoints as values the inverse simply constructs, and from_iota_view ∘ to_iota_view is the identity on the endpoints. Undoing a Strict lower offset at T's min is the mirror of the to_iota_view precondition.
