pst.cppm File Reference

The Pst fragment's normal form: a decidable set over a finite chain, folded into its run list as the chain is walked. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <iterator>
#include <optional>
#include <ranges>
#include <tuple>
#include <type_traits>
#include <utility>
import dedekind.sequences:ranges;
import dedekind.order;
import dedekind.sets;
import dedekind.category;

Include dependency graph for pst.cppm:

Classes
struct	dedekind::sequences::detail_pst::ToMembership< S >
	An element of the walk as the step to its membership, ⊥ past the window's top. More...
struct	dedekind::sequences::ScanSteps< S >
	The normal form of s on the window [lo, hi], by exhaustion: a step source that walks the window (and the element after it) along chain_view and steps where χ changes, ⊥ outside the window. Lazy: one walk per traversal, nothing stored. More...
struct	dedekind::sequences::Ø< T, L >
	∅: The Initial Object. Extensional (Size 0). More...
struct	dedekind::sequences::𝔸< T, L, C >
	The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...
struct	dedekind::sequences::detail_pst_witness::Run< C >
	A maximal run of membership as its closed ends, [lo, hi]. More...

Namespaces
namespace	dedekind::sequences::detail_pst_witness

Concepts
concept	dedekind::sequences::IsPstSet
	A decidable set object over a finite chain with the covering step: a leaf or a lattice node whose χ answers in \(\mathbb{B}\) (the Δ grade). An L-valued set enters through its α-cuts.

Functions
template<IsPstSet S>
constexpr auto	dedekind::sequences::runs (const S &s, const typename S::Domain &lo, const typename S::Domain &hi)
	The runs of s on the window, read off its normal form.
template<IsPstSet S> requires IsPst<typename S::Domain>
constexpr auto	dedekind::sequences::runs (const S &s)
	The runs over a whole truth chain, ⊥ to ⊤.
template<typename View>
consteval auto	dedekind::sequences::detail_pst_witness::summary (View v)
	A run list's runs as (count, first, last).
template<typename A>
constexpr Maybe< std::decay_t< A > >	dedekind::sequences::detail_pst_witness::η (A value)
	The Maybe endofunctor T, implemented via std::optional.

Variables
constexpr auto	dedekind::sequences::detail_pst_witness::above_bottom = 𝔸<Ternary>{} & (π > Ternary::False)
constexpr auto	dedekind::sequences::detail_pst_witness::above5 = 𝔸<int>{} & (π > 5)
constexpr auto	dedekind::sequences::detail_pst_witness::below3 = 𝔸<int>{} & (π < 3)
constexpr auto	dedekind::sequences::detail_pst_witness::hedge = 𝔸<Ternary, Kleene>{} & Identity<Ternary>{}
constexpr auto	dedekind::sequences::detail_pst_witness::cut_u
constexpr auto	dedekind::sequences::detail_pst_witness::fibre_u
constexpr Projection< 0 >	dedekind::sequences::detail_pst_witness::π
	The unary projection, the identity: the variable of a comprehension over one carrier.

Detailed Description

The Pst fragment's normal form: a decidable set over a finite chain, folded into its run list as the chain is walked.

@partition :pst

Copyright

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

pst__Overview

A set over a finite chain is a finite table \(\chi : C \to L\). Equality, and with it the quantifiers and the subset identity, is exhaustion of the chain and lives upstream (sets:boundaries, sets:quantifier). What needs the walk is here: a decidable set whose χ is opaque reaches its normal form, a run list (order:runs), by exhausting the chain along chain_view, on a window whose ends are values or on a whole truth chain; its runs are then read off that normal form. O(N) steps.

An L-valued set is read through its decidable sets on \(\Omega\), pulled back along χ with the generic preimage (category:morphism): the fibre of χ at \(\ell\), \(\chi^{-1}(\ell) = @c preimage(χ, η(ℓ))\), and the α-cut \(\{\chi \ge \ell\} = @c preimage(χ, 𝔸<Ω> & (π ≥ ℓ))\). The α-cuts are nested in \(\ell\) and are the Pst normal form; their runs are this partition's. Not here: ℤ (the walk would have to jump between the term's cut points) and the dense carriers (no step).

Wikipedia: Alpha cut (fuzzy set), Fiber (mathematics), Run-length encoding, Dedekind cut

Note

"Zerfallen alle Punkte der Geraden in zwei Klassen von der Art, daß jeder Punkt der ersten Klasse links von jedem Punkt der zweiten Klasse liegt, so existiert ein und nur ein Punkt, welcher diese Einteilung aller Punkte in zwei Klassen hervorbringt." – Richard Dedekind, Stetigkeit und irrationale Zahlen (1872), §3. [Trans: "If all points of the line fall into two classes such that every point of the first class lies to the left of every point of the second, then there exists one and only one point which produces this division of all points into two classes." An α-cut on a chain is that division, read off χ's table rather than the continuum.]

Function Documentation

runs()

template<IsPstSet S>
requires IsPst<typename S::Domain>

auto dedekind::sequences::runs ( const S & s )

constexprexport

The runs over a whole truth chain, ⊥ to ⊤.

Template Parameters

S	a set over a truth chain.