Run lists: the normal form of the sets of a chain built from intervals, valued in a species. More...

#include <algorithm>
#include <array>
#include <compare>
#include <concepts>
#include <cstddef>
#include <functional>
#include <iterator>
#include <map>
#include <optional>
#include <ranges>
#include <type_traits>
#include <utility>
#include <vector>
import dedekind.order:total;
import dedekind.sets;
import dedekind.category;

Include dependency graph for runs.cppm:

Classes
struct	dedekind::order::carrier_cardinality< T >
	Cardinality class of a halfspace's carrier `T` (#848/#927). More...
struct	dedekind::order::carrier_cardinality< T >
struct	dedekind::order::detail_halfspace_witness::UnrelatedCardinalityAlias
struct	dedekind::order::Bound< V >
	One side of an interval as a value: the bound and whether it is attained (non-strict) or not (strict). More...
struct	dedekind::order::Span< V >
	The sides of an inhabited convex set; an absent side is unbounded. More...
struct	dedekind::order::Position< V >
	A position on the chain: just below `at`, or just above it. More...
struct	dedekind::order::Step< V, L >
	Where the value changes, and to what. A source holds its steps by value (an interval's two sides, an iterator's current step), so the carrier and the truth values are default-initialisable. More...
struct	dedekind::order::detail_runs::And< L >
	The species' operations as named functions on `L::Ω`. More...
struct	dedekind::order::detail_runs::Or< L >
struct	dedekind::order::detail_runs::Rfl< L >
struct	dedekind::order::detail_runs::Iff< L >
	`a` ⇔ `b` in the species: both, or neither. More...
struct	dedekind::order::detail_runs::LiftInto< J >
	A value lifted along the dominance into the species `J`. More...
struct	dedekind::order::detail_runs::AtLeast< Ω >
	Whether a value reaches a level, and whether it is the level: the α-cut and the fibre, pointwise. More...
struct	dedekind::order::detail_runs::EqualTo< Ω >
struct	dedekind::order::detail_runs::MapValue< F, L2 >
	A step with its value mapped into the species `L2`. More...
struct	dedekind::order::detail_runs::SameValue
	Two steps with one value; the first step of a chunk; a step at a given value: the parts of dropping repeats. More...
struct	dedekind::order::detail_runs::Front
struct	dedekind::order::detail_runs::ValueIs< Ω >
struct	dedekind::order::SpanSteps< V, L >
	An interval's sides as a source, valued `value` on it and ⊥ elsewhere: at most two steps. No sides is the whole carrier, no span the empty set, so the constants are spans too. More...
struct	dedekind::order::RunListSteps< N, K >
	Pst's run list (`category:runs`) as a step source: each of its steps the position just below it, the value from there on alternating from outside. Where both apply, on a finite chain with Boolean values, the order's run lists read it as any source, so `ext`, the merges and the cuts take it; the vocabulary they share is to move into `category` (#1138). More...
struct	dedekind::order::RunListSteps< N, K >::AsStep
	The `i-th` step as the order's: below its position, in where `i` is even. More...
struct	dedekind::order::SourceRef< S >
	A source read through a reference: a stored run list inside a term is traversed where it is, not copied. More...
struct	dedekind::order::RelabelSteps< A, F, L2 >
	A source with every value relabelled into the species `L2:` a complement, a lift into a wider species, an α-cut. More...
class	dedekind::order::MergeView< RA, RB, F, V, L >
	The steps of two ranges merged along the chain, each read as `f` of the two values there: the one lazy merge C++23 does not ship. A forward view; repeats are dropped by the caller. More...
class	dedekind::order::MergeView< RA, RB, F, V, L >::iterator
struct	dedekind::order::MergeSteps< A, B, F >
	Two sources merged along the chain under a pointwise operation: the steps of both, each read as `f` of the two values there. More...
struct	dedekind::order::detail_runs::ToItself< C, L >
	An element as the step to its own value: χ = id. More...
struct	dedekind::order::IdentitySteps< C >
	χ(x) = x on a finite chain, valued in the chain's own species: a step at every element above the least (none on a one-element chain). More...
struct	dedekind::order::detail_runs::NotPast< V >
	A step at or before `x:` its position is not past `x`. More...
struct	dedekind::order::detail_runs::LastValue
	The value of the later step: a fold that keeps the last one. More...
struct	dedekind::order::detail_runs::FoldPieces< Op, L >
	The species' fold of the values over the carrier's own pieces: a step before every element sets the first value, one after every element ends the fold. More...
struct	dedekind::order::detail_runs::FoldPieces< Op, L >::State
	The value of the piece being read, and the fold of the pieces before it, none before the first piece inside the carrier. More...
struct	dedekind::order::detail_runs::NotAfterAll
	A step inside or below the carrier: the fold ends at the first one above every element. More...
struct	dedekind::order::Piece< V >
	A piece on which a two-valued source holds: a start (`nullopt` below every element) and an end (`nullopt` above). More...
class	dedekind::order::PiecesView< R, V >
	The pieces of a two-valued source over the carrier, in order: its steps read in enter / leave pairs, a step outside the carrier read as the carrier's end. A forward view. More...
class	dedekind::order::PiecesView< R, V >::iterator
struct	dedekind::order::Run< C >
	A maximal run of membership as its closed ends, [lo, hi]. More...
struct	dedekind::order::detail_runs::Closed< C >
	A piece of a discrete chain with ends, read closed: a canonical start is just below its first element, an end just below the element after its last; an absent side at the carrier's end. More...
struct	dedekind::order::Runs< V, L >
	A set of the chain `V` valued in `L`, materialised: its breakpoints, each the value from that position on, and the value before them. The one stored form, for a value that must outlive the term it was read from (a Python handle); a source like any other, its steps a view of the map. More...
struct	dedekind::order::detail_runs::ToStep< V, L >
	A breakpoint of a map as a step. More...
struct	dedekind::order::detail_runs::MapSteps< V, L >
	A sorted map of breakpoints as a source. More...
struct	dedekind::order::detail_connective::OfKind< K >
	Whether a predicate is of the kind `k` (a bound to fold). More...
struct	dedekind::order::detail_connective::StructurallyBefore
	`a` before `b` in the structural order. More...
struct	dedekind::order::detail_connective::StructurallySame
	`a` and `b` the same tree (equivalent in the structural order). More...
class	dedekind::order::chain_view< C >

Namespaces
namespace	dedekind::order::detail_runs
	χ(x): the value of the last step at or before `x`.
namespace	dedekind::order::detail_runs_witness

Concepts
concept	dedekind::order::detail_position::HasLatticeBottomValue
	Whether the carrier registers its lattice bottom (top) under `<=` as a value, as the machine words do.
concept	dedekind::order::detail_position::HasLatticeTopValue
concept	dedekind::order::IsStepSource
	A step source: the carrier and species, the value before every step, and the steps as a forward range, in order along the chain.

Typedefs
template<typename T>
using	dedekind::order::carrier_cardinality_t = typename carrier_cardinality<T>::type
using	dedekind::order::detail_runs_witness::B = SpanSteps<int, Boole>
using	dedekind::order::detail_runs_witness::And = detail_runs::And<Boole>
using	dedekind::order::detail_runs_witness::Or = detail_runs::Or<Boole>

Enumerations
enum class	dedekind::order::Direction { Upward , Downward }
	Orientation of a halfspace along the chain.
enum class	dedekind::order::Strictness { Strict , NonStrict }
	Whether the boundary is strict (>, <) or inclusive (>=, <=).
enum class	dedekind::order::Side : bool { Below , Above }
	Which side of its value a position sits on. More...

Functions
constexpr Direction	dedekind::order::flip (Direction d)
	Flip a `Direction` — the direction half of a halfspace complement (`~{x>P}` is `{x≤P}`). Reused by the reflection-image pushforward (`dedekind.algebra:halfspace_transport`) to flip a halfspace's sense under \(x \mapsto -x\).
constexpr Strictness	dedekind::order::flip (Strictness s)
	Flip a `Strictness` — the strictness half of the same complement (`~{x>P}` is `{x≤P}`: `>` relaxes to `≤`).
template<typename V>
constexpr Position< V >	dedekind::order::detail_position::start_of (const Bound< V > &b)
	The position a lower side starts at: below an attained bound, above a strict one.
template<typename V>
constexpr Position< V >	dedekind::order::detail_position::end_of (const Bound< V > &b)
	The position an upper side ends at: above an attained bound, below a strict one.
template<typename V>
constexpr Bound< V >	dedekind::order::detail_position::lower_at (const Position< V > &p)
	The lower side starting at `p`.
template<typename V>
constexpr Bound< V >	dedekind::order::detail_position::upper_at (const Position< V > &p)
	The upper side ending at `p`.
template<typename V>
constexpr std::optional< V >	dedekind::order::detail_position::least ()
	The carrier's least element, where it has one as a value: a registered lattice bottom (the machine words), ℕ's 0 and ℤ's −ℵ₀, a truth chain's ⊥.
template<typename V>
constexpr std::optional< V >	dedekind::order::detail_position::greatest ()
	The carrier's greatest element, where it has one as a value, dual to least (ℵ₀ on ℕ).
template<typename V>
constexpr Position< V >	dedekind::order::detail_position::canonical (Position< V > p)
	A position in its canonical form: just above a value is just below the element covering it, where there is one, so on a discrete chain (0, 3) and [1, 3) have the same positions.
template<typename V>
constexpr bool	dedekind::order::detail_position::before_all (const Position< V > &p)
	Whether `p` lies before every element of the carrier.
template<typename V>
constexpr bool	dedekind::order::detail_position::after_all (const Position< V > &p)
	Whether `p` lies after every element of the carrier.
template<typename V>
constexpr Position< V >	dedekind::order::canonical (const Position< V > &p)
	A position in its canonical form: closed where the chain has the step.
template<std::ranges::view R, typename Ω>
constexpr auto	dedekind::order::distinct_steps (R r, Ω first)
	Steps with no step repeating the value before it, as a view: runs of one value kept by their first step, and a first step at the start value dropped. A view, taken by value as Rule 1 asks; a container or an array is passed as `std::views::all` of it.
template<dedekind::category::IsCountWord N, std::size_t K>
constexpr RunListSteps< N, K >	dedekind::order::steps (const dedekind::category::RunList< N, K > &r)
template<IsStepSource S>
constexpr auto	dedekind::order::alpha_cut (const S &s, typename S::logic_species::Ω level)
	The decidable sets of an L-valued source: the α-cut \(\{\chi \ge \ell\}\) and the fibre \(\chi^{-1}(\ell)\).
template<IsStepSource S>
constexpr auto	dedekind::order::fibre (const S &s, typename S::logic_species::Ω level)
consteval bool	dedekind::order::detail_chain_view_witness::walks (auto view, auto... expected)
template<typename Op, IsStepSource S> requires std::invocable<const Op&, typename S::logic_species::Ω, typename S::logic_species::Ω>
constexpr auto	dedekind::order::detail_runs::fold_over_carrier (const S &s, Op op)
template<IsStepSource S> requires std::same_as<typename S::logic_species, Boole>
constexpr auto	dedekind::order::pieces (const S &s)
	The pieces of a two-valued source, as a forward view.
template<IsStepSource S> requires IsFiniteChain<typename S::Domain> && HasNNOStep<typename S::Domain> && (detail_position::least<typename S::Domain>().has_value())
constexpr auto	dedekind::order::runs (const S &s)
	The runs of a two-valued source of a finite chain, as a view of closed pairs: every run that ends does so just below an element with a lower cover (ℕ's proxy, whose ℵ₀ has none, is read through positions).
template<std::unsigned_integral V, typename L> requires IsAbelianGroup<V, std::plus<V>>
Runs< V, L >	dedekind::order::translate (const Runs< V, L > &s, V k)
	The translate of a run list by `k` on a machine word, the chain read as the cyclic group ℤ/2^w it is: \(x \mapsto x + k\) wraps at the word's end, so a run through the end splits in two. It is the image of the set under the translation, and the preimage under the inverse one. The other reading of the same word, as the chain, is Pst's `category::preimage`(shift(d), `s`) on a `RunList:` the translation as a map of the chain, on its extent, where the word does not wrap; the two agree exactly where nothing lies below `d`, and differ by the segment at the word's top otherwise (witnessed in `runs_test`). Two arrows on one word; the chain's is the derivative's (:automaton), the group's is this.
constexpr B	dedekind::order::detail_runs_witness::span (int lo, int hi)
constexpr RelabelSteps< B, detail_runs::Rfl< Boole > >	dedekind::order::detail_runs_witness::without (int p)
template<typename K> requires requires(const K& a, const K& b) { std::weak_order(a, b); }
std::weak_ordering	dedekind::order::constant_order (const K &a, const K &b)
	The order of two constants of the grammar: their own weak (or strong) three-way comparison where they have one; a constant type with none, or only a partial one, names a total order beside it (found by argument-dependent lookup, as `carrier_cast`).
template<typename K>
std::weak_ordering	dedekind::order::structural_order (const Pred< K > &a, const Pred< K > &b)
	The structural order of two predicates (#884): by kind first, so the comparisons (decided, Δ) precede the connectives and the quantifiers (∃ Σ, then ∀ Π); a comparison by its left term, its relation, its right term; a connective by its operands; a quantifier by its sort, slot and body. The key `canonical` sorts a conjunction / disjunction by.
template<typename K>
std::weak_ordering	dedekind::order::structural_order (const Term< K > &a, const Term< K > &b)
	The structural order of two terms (#884): by kind (a projection, a constant, an operation, a conditional), then a projection by its slot, a constant by `constant_order`, an operation by its operator and operands, a conditional by its guard and branches. Total; two terms are equivalent in it exactly when they are the same tree.
template<typename K>
Pred< K >	dedekind::order::connective (typename Pred< K >::Kind k, std::vector< Pred< K > > ops)
	The connective `k` (`And` or `Or`) of the operands, with the order, grouping and repetition forgotten (#884): the bounds folded (the unit dropped, an absorber absorbing), the operands sorted by `structural_order`, each kept once, folded left. None left: the unit.
Queries: one traversal of a source
template<IsStepSource S>
constexpr auto	dedekind::order::value_at (const S &s, const typename S::Domain &x)
template<IsStepSource S>
constexpr auto	dedekind::order::forall (const S &s)
	\(\bigwedge_x \chi(x)\) and \(\bigvee_x \chi(x)\) in the species over the carrier's own elements: on `Ø` both are ⊥, on `𝔸` both ⊤.
template<IsStepSource S>
constexpr auto	dedekind::order::exists (const S &s)
template<IsStepSource A, IsStepSource B> requires std::same_as<typename A::Domain, typename B::Domain> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::equal (const A &a, const B &b)
	Equality of two sources as sets of the carrier, in the species: \(\bigwedge_x (\chi_a(x) \Leftrightarrow \chi_b(x))\), so over K₃ two sets agree to degree U where either is U.

Variables
constexpr auto	dedekind::order::detail_runs_witness::closed = Strictness::NonStrict

Detailed Description

Run lists: the normal form of the sets of a chain built from intervals, valued in a species.

@partition :runs

Copyright: 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

runs__Normal_Form

A set of a chain valued in a species L, built from intervals with the species' ∧, ∨ and ¬, is a step function: a value before the first step, and finitely many steps, each a position on the chain where the value changes. In canonical form the positions are closed where the chain has the step and no step repeats the value before it, so each set has one run list, and &, |, ~ are total on the one type. It is the canonical form of the Boolean (De Morgan) algebra the intervals generate, quotiented by the chain's order; Interval (:halfspace) is its generator. A step at the carrier's own end is kept ({x ≤ max} on a machine word read as a window of ℤ stays bounded above); equality reads the carrier's ends.

Wikipedia: Step function, Run-length encoding, Dedekind cut.

Note: "To denote the subsequence of natural numbers 2, 3, ..., 12 without the pernicious three dots, four conventions are open to us." – Edsger W. Dijkstra, Why numbering should start at zero, EWD831 (1982). A position names the cut before or after a value, which is how the four conventions become one.

Enumeration Type Documentation

◆ Side

enum class dedekind::order::Side : bool

exportstrong

Which side of its value a position sits on.

runs__Positions

The places on a chain a side can sit: just below a value or just above it, a Dedekind cut named by the value beside it. An interval's sides and a run list's steps are positions, so both compare, close and read the carrier's ends through this one layer.

Function Documentation

◆ after_all()

template<typename V>

bool dedekind::order::detail_position::after_all ( const Position< V > & p )

constexpr

Whether p lies after every element of the carrier.

Template Parameters

V	the carrier.

◆ alpha_cut()

template<IsStepSource S>

auto dedekind::order::alpha_cut	(	const S &	s,
		typename S::logic_species::Ω	level )

constexprexport

The decidable sets of an L-valued source: the α-cut \(\{\chi \ge \ell\}\) and the fibre \(\chi^{-1}(\ell)\).

Parameters

s	the source.
level	the level.

◆ before_all()

template<typename V>

bool dedekind::order::detail_position::before_all ( const Position< V > & p )

constexpr

Whether p lies before every element of the carrier.

Template Parameters

V	the carrier.

◆ canonical() [1/2]

template<typename V>

Position< V > dedekind::order::canonical ( const Position< V > & p )

constexprexport

A position in its canonical form: closed where the chain has the step.

Template Parameters

V	the carrier.

◆ canonical() [2/2]

template<typename V>

Position< V > dedekind::order::detail_position::canonical ( Position< V > p )

constexpr

A position in its canonical form: just above a value is just below the element covering it, where there is one, so on a discrete chain (0, 3) and [1, 3) have the same positions.

Template Parameters

V	the carrier.

◆ connective()

template<typename K>

Pred< K > dedekind::order::connective	(	typename Pred< K >::Kind	k,
		std::vector< Pred< K > >	ops )

export

The connective k (And or Or) of the operands, with the order, grouping and repetition forgotten (#884): the bounds folded (the unit dropped, an absorber absorbing), the operands sorted by structural_order, each kept once, folded left. None left: the unit.

Parameters

k	the connective.
ops	its operands (not chains of `k`).

◆ constant_order()

template<typename K>
requires requires(const K& a, const K& b) { std::weak_order(a, b); }

std::weak_ordering dedekind::order::constant_order	(	const K &	a,
		const K &	b )

export

The order of two constants of the grammar: their own weak (or strong) three-way comparison where they have one; a constant type with none, or only a partial one, names a total order beside it (found by argument-dependent lookup, as carrier_cast).

runs__Opaque_Tier

The other half of the normal form (#970, #884): a predicate no run list reads (an equation of a ring, a quantifier) keeps its atoms, and its connectives forget the order, grouping and repetition of their operands. The operands are sorted by a total order on the term trees, by kind first (the decided comparisons before ∃ before ∀), then structurally; a constant through its carrier's own order or the hook beside the carrier.

Parameters

a,b	the constants.

◆ distinct_steps()

template<std::ranges::view R, typename Ω>

auto dedekind::order::distinct_steps	(	R	r,
		Ω	first )

constexprexport

Steps with no step repeating the value before it, as a view: runs of one value kept by their first step, and a first step at the start value dropped. A view, taken by value as Rule 1 asks; a container or an array is passed as std::views::all of it.

Parameters

r	the steps.
first	the value before them.

◆ end_of()

template<typename V>

Position< V > dedekind::order::detail_position::end_of ( const Bound< V > & b )

constexpr

The position an upper side ends at: above an attained bound, below a strict one.

Template Parameters

V	the carrier.

◆ greatest()

template<typename V>

std::optional< V > dedekind::order::detail_position::greatest ( )

constexpr

The carrier's greatest element, where it has one as a value, dual to least (ℵ₀ on ℕ).

Template Parameters

V	the carrier.

◆ least()

template<typename V>

std::optional< V > dedekind::order::detail_position::least ( )

constexpr

The carrier's least element, where it has one as a value: a registered lattice bottom (the machine words), ℕ's 0 and ℤ's −ℵ₀, a truth chain's ⊥.

Template Parameters

V	the carrier.

◆ lower_at()

template<typename V>

Bound< V > dedekind::order::detail_position::lower_at ( const Position< V > & p )

constexpr

The lower side starting at p.

Template Parameters

V	the carrier.

◆ start_of()

template<typename V>

Position< V > dedekind::order::detail_position::start_of ( const Bound< V > & b )

constexpr

The position a lower side starts at: below an attained bound, above a strict one.

Template Parameters

V	the carrier.

◆ steps()

template<dedekind::category::IsCountWord N, std::size_t K>

RunListSteps< N, K > dedekind::order::steps ( const dedekind::category::RunList< N, K > & r )

constexprexport

Parameters

r	Pst's run list.

Returns: it as a step source.

◆ structural_order() [1/2]

template<typename K>

std::weak_ordering dedekind::order::structural_order	(	const Pred< K > &	a,
		const Pred< K > &	b )

export

The structural order of two predicates (#884): by kind first, so the comparisons (decided, Δ) precede the connectives and the quantifiers (∃ Σ, then ∀ Π); a comparison by its left term, its relation, its right term; a connective by its operands; a quantifier by its sort, slot and body. The key canonical sorts a conjunction / disjunction by.

Parameters

a,b	the predicates.

◆ structural_order() [2/2]

template<typename K>

std::weak_ordering dedekind::order::structural_order	(	const Term< K > &	a,
		const Term< K > &	b )

export

The structural order of two terms (#884): by kind (a projection, a constant, an operation, a conditional), then a projection by its slot, a constant by constant_order, an operation by its operator and operands, a conditional by its guard and branches. Total; two terms are equivalent in it exactly when they are the same tree.

Parameters

a,b	the terms.

◆ translate()

template<std::unsigned_integral V, typename L>
requires IsAbelianGroup<V, std::plus<V>>

Runs< V, L > dedekind::order::translate	(	const Runs< V, L > &	s,
		V	k )

export

The translate of a run list by k on a machine word, the chain read as the cyclic group ℤ/2^w it is: \(x \mapsto x + k\) wraps at the word's end, so a run through the end splits in two. It is the image of the set under the translation, and the preimage under the inverse one. The other reading of the same word, as the chain, is Pst's category::preimage(shift(d), s) on a RunList: the translation as a map of the chain, on its extent, where the word does not wrap; the two agree exactly where nothing lies below d, and differ by the segment at the word's top otherwise (witnessed in runs_test). Two arrows on one word; the chain's is the derivative's (:automaton), the group's is this.

Template Parameters

V	an unsigned word.
L	the species.

Parameters

s	the set.
k	the shift.

◆ upper_at()

template<typename V>

Bound< V > dedekind::order::detail_position::upper_at ( const Position< V > & p )

constexpr

The upper side ending at p.

Template Parameters

V	the carrier.

Classes

Namespaces

Concepts

Typedefs

Enumerations

Functions

Variables

Detailed Description

runs__Normal_Form

Enumeration Type Documentation

◆ Side

runs__Positions

Function Documentation

◆ after_all()

◆ alpha_cut()

◆ before_all()

◆ canonical() [1/2]

◆ canonical() [2/2]

◆ connective()

◆ constant_order()

runs__Opaque_Tier

◆ distinct_steps()

◆ end_of()

◆ greatest()

◆ least()

◆ lower_at()

◆ start_of()

◆ steps()

◆ structural_order() [1/2]

◆ structural_order() [2/2]

◆ translate()

◆ upper_at()