Run lists over a finite chain: a subset of \([0, n)\) as the positions where its membership changes, the canonical form of a decidable set on a chain, bounded by its type and on the stack. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <ranges>
#include <type_traits>
#include <utility>
import dedekind.category:logic;

Include dependency graph for runs.cppm:

Classes
struct	dedekind::category::RunList< N, K >
	A subset of the counts held as its steps: the positions where membership flips, strictly increasing, from outside at 0. At most `K` steps, so at most `K` / 2 runs. More...
struct	dedekind::category::RunList< N, K >::Member
	The subobject surface: a member is a count the run list holds, and its inclusion into the counts is the count itself. More...
struct	dedekind::category::detail_runs::Sweep< N, J, K, Op >
	One position of a sweep: the operation's value there, kept as a step where it differs from the value before. More...
struct	dedekind::category::detail_runs::Sweep< N, J, K, Op >::State
struct	dedekind::category::detail_runs::Translated< N, K >
	One step of a preimage along a translation: a step past it moves down by it; one at or before it is absorbed into the value at 0. More...
struct	dedekind::category::RunCombine
	The run lists' domain meet and join, the reducer's leaf-combine: where two leaves are run lists on one chain, the sweep, its bound the sum of theirs. More...
struct	dedekind::category::detail_runs::Along< Pred, N, K >
	One count of a sweep along a predicate: a step where its value changes, nothing where the steps outgrow their bound. More...
struct	dedekind::category::detail_runs::Along< Pred, N, K >::State
struct	dedekind::category::detail_runs::Commutes< P, A, B >
	The pullback square at one count: the apex holds it exactly where both operands do, and its legs land on the count itself. More...
struct	dedekind::category::detail_runs::PullsBack< N, K >
	The pullback's law at one count: the closed form reads what the composite `P∘f` reads, `preimage(f, P)`(x) `=` `P(f(x))`. More...

Namespaces
namespace	dedekind::category

Typedefs
using	dedekind::category::detail_runs::Meet04_26 = decltype(as_pullback(run<2>(0uz, 4uz), run<2>(2uz, 6uz)))
using	dedekind::category::Runs4 = RunList<std::size_t, 4>

Functions
template<std::size_t K, IsCountWord N> requires (K >= 2)
constexpr RunList< N, K >	dedekind::category::run (N lo, std::type_identity_t< N > hi)
template<IsCountWord N, std::size_t J, std::size_t K, typename Op>
constexpr RunList< N, J+K >	dedekind::category::detail_runs::swept (const RunList< N, J > &a, const RunList< N, K > &b, Op op)
template<IsCountWord N, std::size_t J>
constexpr RunList< N, J+2 >	dedekind::category::detail_runs::restricted (const RunList< N, J > &r, const RunList< N, 2 > &w)
template<typename T>
constexpr auto	dedekind::category::reduced (const T &t)
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr RunList< N, J+K >	dedekind::category::operator\| (const RunList< N, J > &a, const RunList< N, K > &b)
	The union of two run lists, at once: the lattice's `Join` node folded by the one reducer, the sweep its leaf-combine, as the set grammar's \| folds through `SetCombine` (`sets`). Its bound is the sum of theirs. The strict form; the lazy one is the node itself, built and reduced later, as the predicates that opt in to :lattice's \| keep it (#1138).
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr RunList< N, J+K >	dedekind::category::operator& (const RunList< N, J > &a, const RunList< N, K > &b)
	The intersection, dual to the union; with a single run, by law a restriction.
template<std::size_t K, IsCountWord N, typename Pred> requires std::predicate<const Pred&, N>
constexpr Maybe< RunList< N, K > >	dedekind::category::run_list (N end, Pred holds)
	The run list of a predicate on \([0, \mathit{end})\): every count tested once, a step where the value changes.
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr auto	dedekind::category::as_pullback (const RunList< N, J > &a, const RunList< N, K > &b)
	The intersection as the pullback of the two inclusions into the counts, `category's` apex view over it (`IsPullback`): in the thin category of run lists, the meet is the pullback.
template<IsCountWord N, std::size_t J, std::size_t K>
constexpr auto	dedekind::category::as_pushout (const RunList< N, J > &a, const RunList< N, K > &b)
	The union as the pushout, dual to `as_pullback` (`IsPushout`).
template<std::size_t K, IsCountWord N, std::size_t J>
constexpr Maybe< RunList< N, K > >	dedekind::category::narrowed (const RunList< N, J > &r)
	A run list under a bound claimed, not proved by the types: the same set where its steps fit, nothing where they do not.
template<IsCountWord N, std::size_t K>
constexpr RunList< N, K >	dedekind::category::preimage (const Shift< N > &t, const RunList< N, K > &s)
	`preimage`(shift(d), `s`): the pullback of `s` along the translation, \(x \mapsto s(x + d)\), in closed form, a run list again: the closed-form overload of :morphism's `preimage(f, P)`, whose general form is the composite `P∘f`, as `algebra's` `halfspace_transport` gives one for an interval. The translation is read as a map of the chain, on its extent: the counts \(x\) with \(x + d\) below the word's top (`extent` in :periodic, where a shift's law holds), where the word does not wrap. `halfspace_transport` gates the same reading by the carrier's type (an ordered group, or ℕ, where \(x + k\) misses \(\{0, \ldots, k - 1\}\)); on the word, Pst's carrier, the extent is that gate, by value. The elements of `s` below `d`, whose preimages would wrap past the top, lie outside it and are not reported; the derivative (:automaton) meets its operand with the letter's interval first, so none exist there. The other reading, the word as the cyclic group \(\mathbb{Z}/2^w\) whose translation wraps, is `order's` `translate` (an image, a run through the end splitting in two) and `morphologies'` congruence preimage; it is a different arrow, and not this one (#1138).
template<IsCountWord N, std::size_t K>
constexpr RunList< N, K >	dedekind::category::operator>> (const Shift< N > &t, const RunList< N, K > &s)
	`shift(d)` `>>` `s`, the spelling of the preimage: precomposition with the translation.

Detailed Description

Run lists over a finite chain: a subset of \([0, n)\) as the positions where its membership changes, the canonical form of a decidable set on a chain, bounded by its type and on the stack.

@partition :runs

One set, one run list

A run list is a predicate on the counts, an arrow \(N \to \mathbb{B}\), held as its steps: the strictly increasing positions where its value flips, from outside at 0. The steps {2, 5, 7, 9} are the set \([2, 5) \cup [7, 9)\). Maximal runs are what makes the form canonical: two run lists are equal exactly when they hold the same elements, so == is the sets' equality, at compile time and at run time alike.

The lattice operations are :lattice's own vocabulary: a | b and a & b build Join and Meet nodes, and :lattice_term's reducer folds a term over run lists to one run list. Its induced laws fire first; the residual pair of leaves takes the run lists' own sweep, injected as the reducer's leaf-combine (RunCombine). Precomposition with a translation, shift(d) >> s, is the preimage of s along it on the translation's extent, the counts below the word's top less d, where the word does not wrap (the extent :periodic gives the shift's law): again a run list.

Over a finite chain only, by the type's bound K on the steps: Pst's run list. The order module's Runs, valued in any species over chains that may be infinite, stored in a map, is the general case; there a run list is a step source (order::RunListSteps), so the order's ext, merges, cuts and extensional equality read it, and a run list and an interval term are compared as sets. The step-source vocabulary they share is to move here, over finite chains (#1138).

Wikipedia: Run-length encoding, Step function, 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). The convention he chooses, \(2 \le i < 13\), is a run list's step: the order's run lists (order:runs) open with the same words, the two being one form.

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

Function Documentation

◆ restricted()

template<IsCountWord N, std::size_t J>

RunList< N, J+2 > dedekind::category::detail_runs::restricted	(	const RunList< N, J > &	r,
		const RunList< N, 2 > &	w )

constexpr

Parameters

r	a run list.
w	a single run \([lo, hi)\), or none.

Returns: r restricted to it: its steps strictly inside, opened at lo where lo is in r and closed at hi where hi - 1 is. Two bisections and a copy of what is kept, where the sweep tests every position of both.

◆ swept()

template<IsCountWord N, std::size_t J, std::size_t K, typename Op>

RunList< N, J+K > dedekind::category::detail_runs::swept	(	const RunList< N, J > &	a,
		const RunList< N, K > &	b,
		Op	op )

constexpr

Parameters

a

param b two run lists.

Parameters

op	a pointwise operation on truth values.

Returns: the run list of op on them: the steps of both, in order, kept where the value changes, so the runs are maximal. Its steps are among theirs, so its bound is the sum of theirs: total.

Classes

Namespaces

Typedefs

Functions

Detailed Description

One set, one run list

Function Documentation

◆ restricted()

◆ swept()