Compile-time halfspace predicates on ordered carriers. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <optional>
#include <ranges>
#include <type_traits>
#include <utility>
import dedekind.order:runs;
import dedekind.relational;
import dedekind.sets;
import dedekind.category;

Include dependency graph for halfspace.cppm:

Classes
struct	dedekind::order::Interval< V, L >
	A convex subset of a chain as a VALUE — an interval: each side an optional `Bound`, with a runtime-evaluable membership χ. Closed under ∩; a union or a complement leaves it unless one operand covers the other. No side is the universe; both sides closed at one value is a point; no `Span` at all is the one empty set, to which crossing bounds normalise. The bounds ride as values, never as NTTPs. Consume it through `&`, \|, `==`, `<=`, membership and the `half` / `point` / `empty` / `universe` / `bounded` factories. More...
struct	dedekind::order::detail_steps::Opaque
	Not a step source: a leaf the run lists do not read (an opaque predicate), or a node over one. More...
struct	dedekind::order::detail_steps::Steps< L >
	The normal form of a set term as the algebra of `cata:` an interval's sides, a stored run list read in place, the boundaries as constants; a meet or join the merge of its legs' steps under ∧ or ∨, a complement their relabelling by ¬. Lazy: nothing is stored, the steps are pulled by the query that reads them. More...
struct	dedekind::order::detail_interval::AsInterval< V >
	A piece as the interval it is. More...
struct	dedekind::order::ProductRestrict< P, RP >
	The product's own membership conjoined with a relational restriction, so a bind over a restricted product keeps that membership and cannot admit pairs outside it (a full product contributes a trivially-true `product`). More...
struct	dedekind::order::InSlot< I, S >
	\(\pi_I^{-1}(S)\): the cylinder of a set `S` on axis `I` of a pair, a relational predicate. More...
struct	dedekind::order::detail_cover_witness::Walk
	A walk along the cover: where it is, and whether it met `b`. More...
struct	dedekind::order::detail_cover_witness::StepToward
	One successor step of a walk that looks for `b`. More...
struct	dedekind::order::detail_cover_witness::AgreesFrom
	For a fixed `a`, every `b` agrees: `a` < `b` iff reached. More...
struct	dedekind::order::detail_cover_witness::AgreesOn
	Every `a` in the window agrees with every `b`. More...

Namespaces
namespace	dedekind::sets
namespace	dedekind::order::detail_interval
namespace	dedekind::order::detail_pointfree_decidability
namespace	dedekind::order::detail_axis
	A meet of cylinders: the factor on axis `I` is the intersection of both children's factors on that axis, so two bounds on the same axis (`π_1<=5` `&&` `π_1<=3`) meet to the tighter one rather than dropping either.
namespace	dedekind::order::detail_cover_witness
namespace	dedekind::category

Concepts
concept	dedekind::order::IsStepTerm
	A set term whose normal form the run lists read.
concept	dedekind::order::detail_axis::IsUniversalBoundary
	A factor that does not constrain its axis: the universal boundary.

Typedefs
using	dedekind::order::detail_pointfree_decidability::PointFree = decltype(ℕ & (π > 5))
template<typename K>
using	dedekind::order::Translation
	The translation graph `π_1` `+` `k` `==` `π_2` and the scaling graph `π_1` `*` `k` `==` `π_2`, as the atoms the grammar builds for them.
template<typename K>
using	dedekind::order::Scaling
using	dedekind::order::detail_interval_witness::Cardinality
	Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.
using	dedekind::order::detail_interval_witness::ℵ_0
	Countable Infinity.

Enumerations
enum class	dedekind::order::detail_interval_witness::Ternary
	A three-valued propositional logic for handling partial information. More...
enum class	dedekind::order::Rel
	The comparison an atom makes.

Functions
constexpr Direction	dedekind::order::dir_of (Rel r)
	The `Direction` a comparison `Rel` lifts a halfspace to.
constexpr Strictness	dedekind::order::strict_of (Rel r)
	The `Strictness` a comparison `Rel` lifts a halfspace to.
constexpr bool	dedekind::order::is_order_rel (Rel r)
	Whether a `Rel` is one of the four order comparisons (not Eq/Ne).
template<dedekind::order::IsTotallyOrdered T, dedekind::category::IsOckhamAlgebra L, IsCardinality C, Rel R, typename K> requires (dedekind::order::is_order_rel(R))
constexpr dedekind::order::Interval< T, L >	dedekind::sets::operator& (const 𝔸< T, L, C > &, const Cmp< R, Projection< 0 >, Const< K > > &c)
	An order atom `π` `⋈` `k` on a chain is the ray it names, whatever the constant's type: the constant meets the carrier exactly or the binding raises. Declared beside `𝔸` and the atom, so ADL finds it.
template<typename V>
constexpr std::optional< Bound< V > >	dedekind::order::detail_interval::tighter_lower (const std::optional< Bound< V > > &a, const std::optional< Bound< V > > &b)
	The tighter of two lower sides: the larger bound; at a tie the strict one. An absent side is no constraint.
template<typename V>
constexpr std::optional< Bound< V > >	dedekind::order::detail_interval::tighter_upper (const std::optional< Bound< V > > &a, const std::optional< Bound< V > > &b)
	The dual: the smaller bound; at a tie the strict one.
template<typename V, typename L>
constexpr Interval< V, L >	dedekind::order::reduce_meet (const Interval< V, L > &a, const Interval< V, L > &b)
	The ONE meet law: the tighter side on each end, collapsed by `bounded` (crossing sides to `Ø`, a single admitted element to its point). `constexpr`, so evaluable at compile time or runtime.
constexpr Rel	dedekind::order::detail_steps::converse (Rel r)
	The converse of a comparison: `k` `r` `π` is `π` `conv(r)` `k`.
template<IsTotallyOrdered V, IsOckhamAlgebra L, typename K>
Runs< V, L >	dedekind::order::detail_steps::order_fragment (const Pred< K > &p)
	The run list of a predicate built at run time over a chain, in the order fragment: the atoms `π` `⋈` `k` (and, on a machine word, `π` `±` `c` `⋈` `k:` the atom's run list translated), under ∧ and ∨, a comparison of two constants decided; conditionals lifted first (`lift_conditionals`). The shape is a value, so the run list is materialised piece by piece. An atom outside the fragment has no normal form here and is refused.
template<typename T> requires requires { typename T::logic_species; }
constexpr auto	dedekind::order::steps (const T &t)
	The normal form of a set term of a chain, as a lazy step source. A stored run list inside the term is read in place, so the source must not outlive the term.
template<IsStepTerm T>
auto	dedekind::order::ext (const T &t)
	The extension of a set term: its normal form, materialised as a stored run list. The explicit step; every query reads `steps(t)` lazily without it.
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::operator== (const A &a, const B &b)
	Equality of two set terms of a chain as sets of the carrier, in the species: one traversal of their normal forms, so it is extensional ((0, 3) and [1, 3) are the same set of ℤ).
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && (!std::same_as<typename A::logic_species, typename B::logic_species>) && HaveLogicJoin<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::order::operator== (const A &a, const B &b)
	Equality across two species of one chain, read in their join: a Boolean set beside a K₃-valued one is compared in K₃.
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const Ø< T, L > &, const S &s)
	A set term against the boundaries, in its species: `Ø` `==` `S` is \(\neg\bigvee\chi\), `𝔸` `==` `S` is \(\bigwedge\chi\), read over the carrier's own elements (on K₃, `Unknown` is a verdict).
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const S &s, const Ø< T, L > &e)
template<IsTotallyOrdered T, IsOckhamAlgebra L, IsCardinality CU, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const 𝔸< T, L, CU > &, const S &s)
template<IsTotallyOrdered T, IsOckhamAlgebra L, IsCardinality CU, typename S> requires std::same_as<typename S::Domain, T> && (!IsBoundaryObject<S>) && IsStepTerm<S>
constexpr auto	dedekind::order::operator== (const S &s, const 𝔸< T, L, CU > &u)
template<IsTotallyOrdered V, IsOckhamAlgebra L>
constexpr Interval< V, L >	dedekind::order::structured_and (const Interval< V, L > &a, const Interval< V, L > &b)
	The meet of two intervals, under the reducer's customization-point name: the one `reduce_meet`. Declared here, before `axis_factor`, so the recursion over a `RelAnd` tree is closed over its own outputs (#872).
template<IsStepSource S> requires std::same_as<typename S::logic_species, Boole>
constexpr auto	dedekind::order::intervals (const S &s)
	The runs of a two-valued source as intervals, in order along the chain: a view, nothing stored.
template<typename T1, typename T2, typename L, typename C, IsRelPredicate RP> requires (!dedekind::sets::contains_self_v<RP>)
constexpr auto	dedekind::order::operator& (const 𝔸< std::pair< T1, T2 >, L, C > &, RP rp)
	`𝔸` `&` `relPred` — the relation as a set object on `A×B`. The universal product carries no factor restriction, so the relation's membership is the rel-predicate: the pure product universe refined to a subobject.
template<typename S, IsRelPredicate RP> requires dedekind::sets::IsSetObject<S> && requires { typename S::Domain::first_type; typename S::Domain::second_type; } && (!dedekind::sets::contains_self_v<RP>)
constexpr auto	dedekind::order::operator& (const S &prod, RP rp)
	`product` `&` `relPred` — the relation as a set object on `A×B`, keeping the product's own membership (so a restricted product bounds the relation).
constexpr Rel	dedekind::order::rel_of (Direction d, Strictness s)
	A restricted factor lifts to a cylinder on its axis, so `operator*` keeps the factor predicates instead of dropping them.
template<IsTotallyOrdered T, IsOckhamAlgebra L, typename T2, IsCardinality C2>
constexpr auto	dedekind::order::operator* (const Interval< T, L > &a, const 𝔸< T2, L, C2 > &)
template<typename T1, IsCardinality C1, IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr auto	dedekind::order::operator* (const 𝔸< T1, L, C1 > &, const Interval< T, L > &b)
template<IsTotallyOrdered Ta, IsTotallyOrdered Tb, IsOckhamAlgebra L>
constexpr auto	dedekind::order::operator* (const Interval< Ta, L > &a, const Interval< Tb, L > &b)
template<IsRingIntegral auto I, typename TI, typename L, typename P>
constexpr auto	dedekind::order::axis_factor (const P &)
	`dom` / `cod` as the projections \(\pi_A / \pi_B\), recovering the factor from the relation's structure (the inverse of `cylinder`).
template<IsRingIntegral auto I, IsTotallyOrdered TI, IsOckhamAlgebra L, IsRingIntegral auto Slot, Rel R, typename K> requires (is_order_rel(R) && Slot == I)
constexpr auto	dedekind::order::axis_factor (const Cmp< R, Projection< Slot >, Const< K > > &c)
	An order atom on axis `I`, `π_I` `⋈` `c:` the ray it names (Eq/Ne fall to the default). The slot is matched to the axis by value, so two integral spellings of one axis agree.
template<IsRingIntegral auto I, IsTotallyOrdered TI, IsOckhamAlgebra L, IsRingIntegral auto Slot, typename S> requires (Slot == I)
constexpr S	dedekind::order::axis_factor (const InSlot< Slot, S > &c)
	A cylinder on axis `I:` its set.
template<IsRingIntegral auto I, typename TI, typename L, typename A, typename B>
constexpr auto	dedekind::order::axis_factor (const dedekind::relational::RelAnd< A, B > &r)
template<IsRingIntegral auto I, typename TI, typename L, typename Pp, typename RP>
constexpr auto	dedekind::order::axis_factor (const ProductRestrict< Pp, RP > &r)
	A restricted product bounding a graph: the factor lives on the product (cylinder) side; the graph `rp` couples the axes, so it is transparent to a single-axis projection.
template<typename T1, typename T2, typename L, IsRelPredicate P, typename C>
constexpr auto	dedekind::order::dom (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	\(\pi_A(R)\) — the domain factor, recovered structurally (preserving the relation's logic species `L`).
template<typename T1, typename T2, typename L, IsRelPredicate P, typename C>
constexpr auto	dedekind::order::cod (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	\(\pi_B(R)\) — the codomain factor, recovered structurally.
template<IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr Interval< T, L >	dedekind::order::upperbounds (const Interval< T, L > &s)
	`upperbounds(S)` — the \(\forall\)-projection \(R/\ni\): the region dominating all of `S`, and the pluggable point of the extremum (Bird & de~Moor [2]).
template<IsTotallyOrdered T, IsOckhamAlgebra L>
constexpr Interval< T, L >	dedekind::order::lowerbounds (const Interval< T, L > &s)
	The dual: lower bounds, `{x` ≤ inf}.
template<IsOckhamAlgebra L, IsCardinality C>
constexpr auto	dedekind::order::upperbounds (const 𝔸< bool, L, C > &)
template<IsOckhamAlgebra L, IsCardinality C>
constexpr auto	dedekind::order::lowerbounds (const 𝔸< bool, L, C > &)
template<typename S> requires IsPartiallyOrdered<typename S::Domain> && requires(const S& s) { s & upperbounds(s); }
constexpr auto	dedekind::order::max (const S &s)
	`max(S)` — the generic extremum: `S` met (`∩`) with its own \(\forall\)-dominators, \(S \cap \mathrm{upperbounds}(S)\). `min` is the dual (`S` met with its minorants).
template<typename S> requires IsPartiallyOrdered<typename S::Domain> && requires(const S& s) { s & lowerbounds(s); }
constexpr auto	dedekind::order::min (const S &s)
template<typename T, typename K1, typename K2, typename L, typename C, typename CU> requires dedekind::category::IsSaturating<T>
constexpr bool	dedekind::order::operator== (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K1 > > &a, const Comprehension< 𝔸< std::pair< T, T >, L, CU >, Translation< K2 > > &b)
	Two translation graphs are the same relation iff they carry the same shift, read in the carrier. Gated on `IsSaturating:` the shift arithmetic is faithful only where the carrier's `+` is (on `bool`, `+1` and `+2` are the same graph, so a comparison of shifts would separate them).
template<typename T, typename K1, typename K2, typename L, typename C, typename CU> requires dedekind::category::IsSaturating<T>
constexpr auto	dedekind::order::operator>> (const Comprehension< 𝔸< std::pair< T, T >, L, C >, Translation< K1 > > &a, const Comprehension< 𝔸< std::pair< T, T >, L, CU >, Translation< K2 > > &b)
	Symbolic composition of translation graphs, \(T_a \circ T_b = T_{a+b}\): the shifts added in the carrier, with no \(\exists\) over the intermediate. Gated on `IsSaturating`, where the symbolic `a+b` is the actual composite.
constexpr bool	dedekind::order::detail_cover_witness::reaches (int a, int b, int k)
	Whether `b` is reached from `a` in 1 to `k` − 1 cover steps.
consteval bool	dedekind::order::detail_cover_witness::order_is_cover_star (int k)
template<std::ranges::view V, std::size_t Sigma, std::size_t Q> requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>
constexpr auto	dedekind::order::operator>> (V letters, const Maybe< Matches< Sigma, Q > > &m)
template<typename P, typename S, IsArrow T>
constexpr Prefixed< P, S, T >	dedekind::order::operator& (const Symmetric< P, S, T > &s, const Prefix &p)
constexpr Ternary	dedekind::order::predecessor (Ternary a) noexcept
constexpr Ternary	dedekind::order::successor (Ternary a) noexcept
	K₃'s step: the cover False → Unknown → True, saturating at the top (and its dual at the bottom), the NNO step of the chain (:nno).
constexpr Rel	dedekind::order::negate (Rel r)
	The De Morgan dual of a comparison: `!`(x `R` `y`) is `x` `negate(R)` `y`.
template<Rel R, typename X, typename Y>
constexpr bool	dedekind::order::rel_apply (const X &x, const Y &y)
	`x` `R` `y`.
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::sets::operator== (const A &a, const B &b)
	Equality of two set terms of a chain as sets of the carrier, in the species: one traversal of their normal forms, so it is extensional ((0, 3) and [1, 3) are the same set of ℤ).
template<typename P, typename S, IsArrow T>
constexpr Prefixed< P, S, T >	dedekind::sets::operator& (const Symmetric< P, S, T > &s, const Prefix &p)

Variables
constexpr auto	dedekind::order::ℤ
constexpr auto	dedekind::order::le5 = ℕ & (π <= 5)
constexpr auto	dedekind::order::ge5 = ℕ & (π >= 5)
template<typename A, typename B, typename L, typename P, typename RP, typename C>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, C >, dedekind::order::ProductRestrict< P, RP > > >

Detailed Description

Compile-time halfspace predicates on ordered carriers.

@partition :halfspace

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

halfspace__Intervals_As_Values

The order reading of the term grammar on a chain: an order atom π ⋈ c on 𝔸<T> is an Interval, a value whose sides (each an optional bound, open or closed) and pivots are values. Meets reduce in constant evaluation where the pivots are constants and at runtime otherwise; unions and complements are run lists (:runs), of which an interval is the generator.

halfspace__DSL_Surface

constexpr auto big   = ℕ & (π > 5);
constexpr auto small = ℕ & (π < 3);
static_assert((big & small) == Ø<Cardinality>{});

Wikipedia: Half-space (geometry), Separating hyperplane theorem,

Note: "Was beweisbar ist, soll in der Wissenschaft nicht ohne Beweis geglaubt werden." — Richard Dedekind, Was sind und was sollen die Zahlen? (1888), Vorwort. [Trans: "What is provable should not be believed without proof in science."]

Typedef Documentation

◆ Cardinality

using dedekind::sets::Cardinality

Sum type for finite vs countably infinite cardinalities; the library's bona-fide proxy for \(\mathbb{N}\) modulo physical limits.

The variant (ExtensionalCardinal<>, ℵ_0) is not a cyclic carrier (it does not wrap modulo capacity); on overflow it escalates — saturates — into ℵ_0 via the add / mul helpers below. The explicit overflow story is "you reached countable infinity" rather than the C++ default of silent wrap or UB. The finite fragment is ExtensionalCardinal<>, one std::size_t word (so the variant is not a bignum). The ℵ_0 alternative marks the saturation regime that takes over once the word cannot hold the result.

Strictly mathematically, \(\mathbb{N} \cup \{\aleph_0\}\) is not a monoid in the textbook sense (e.g. left-cancellation fails on the saturating element). The library's pragmatic certificate accepts it as a proxy for \(\mathbb{N}\) because the finite fragment is \(\mathbb{N}\) exactly and the saturation is the explicit overflow contract: "if you compute beyond memory limits, you saturate at @c ℵ_0". Downstream code that requires strict-ℕ behaviour should test the finite-fragment alternative (std::holds_alternative<ExtensionalCardinal<>>). See the sibling SignedCardinality below for the ℤ proxy on the same pattern.

◆ Scaling

template<typename K>

using dedekind::order::Scaling

export

Initial value:

Cmp<Rel::Eq, BinOp<std::multiplies<>, Projection<1>, Const<K>>,

Projection<2>>

dedekind::category::Projection

The projection π_k: the k-th component of a product.

Definition limit.cppm:329

dedekind::sets::Cmp

The atom a R b over two terms, a relational predicate.

Definition terms.cppm:1495

dedekind::sets::Const

A constant, carried as a value.

Definition terms.cppm:245

◆ Translation

template<typename K>

using dedekind::order::Translation

export

Initial value:

Cmp<Rel::Eq, BinOp<std::plus<>, Projection<1>, Const<K>>, Projection<2>>

The translation graph π_1 + k == π_2 and the scaling graph π_1 * k == π_2, as the atoms the grammar builds for them.

Template Parameters

K	the constant's type.

Enumeration Type Documentation

◆ Ternary

enum class dedekind::category::Ternary : std::int8_t

strong

A three-valued propositional logic for handling partial information.

logic__Species_2

Indeterminacy)

Unlike Boole, Kleene's three-valued logic allows for an 'Unknown' state, modeling undecidability or missing knowledge within a predicate. This implementation follows Kleene's strong logic of indeterminacy (K3).

@values

False (-1): The absolute negative.
Unknown (0): The indeterminate or undecidable state.
True (1): The absolute positive.

Function Documentation

◆ axis_factor()

template<IsRingIntegral auto I, typename TI, typename L, typename P>

auto dedekind::order::axis_factor ( const P & )

constexprexport

dom / cod as the projections \(\pi_A / \pi_B\), recovering the factor from the relation's structure (the inverse of cylinder).

halfspace__Projections

These are the π_A / π_B side of Table 3 (the four properties of a relation): dom is \(\pi_A(R)\), cod is \(\pi_B(R)\). Read off the axis- \(I\) cylinder atom structurally: a comparison bound becomes the halfspace factor, no axis- \(I\) bound leaves the declared universe 𝔸<T_I> (honest exactly when R is entire on that side). This is the free case; the existential \(\{a\mid\exists b.R(a,b)\}\) that a coupled, non-entire relation needs is the separate Rice-gated operation. The order-layer overloads specialise the sets-layer 𝔸<T1> fallback (they win by IsRelPredicate).

Recover the axis-I factor from a relational predicate. Default: no axis-I structure, so the declared universe 𝔸<TI>.

◆ ext()

template<IsStepTerm T>

auto dedekind::order::ext ( const T & t )

export

The extension of a set term: its normal form, materialised as a stored run list. The explicit step; every query reads steps(t) lazily without it.

Parameters

t the term.

◆ intervals()

template<IsStepSource S>
requires std::same_as<typename S::logic_species, Boole>

auto dedekind::order::intervals ( const S & s )

constexprexport

The runs of a two-valued source as intervals, in order along the chain: a view, nothing stored.

Parameters

s	the source.

◆ max()

template<typename S>
requires IsPartiallyOrdered<typename S::Domain> && requires(const S& s) { s & upperbounds(s); }

auto dedekind::order::max ( const S & s )

constexprexport

max(S) — the generic extremum: S met (∩) with its own \(\forall\)-dominators, \(S \cap \mathrm{upperbounds}(S)\). min is the dual (S met with its minorants).

One definition for any ordered S whose upperbounds and meet are defined; the structural collapse lives entirely in upperbounds and the meet, so there is no generic search. Gated on the SEMANTIC order: greatest/least element is a partial-order notion, so the domain must certify IsPartiallyOrdered (dedekind's reflexive/transitive/antisymmetric axioms, which subsume std::totally_ordered one level up in IsTotallyOrdered). A carrier without a certified order — a raw float, whose NaN breaks reflexivity — is honestly rejected: you cannot take the max of a set that may contain a NaN.

◆ negate()

Rel dedekind::sets::negate ( Rel r )

constexpr

The De Morgan dual of a comparison: !(x R y) is x negate(R) y.

Parameters

r	the comparison.

◆ operator&() [1/3]

template<typename T1, typename T2, typename L, typename C, IsRelPredicate RP>
requires (!dedekind::sets::contains_self_v<RP>)

auto dedekind::order::operator&	(	const 𝔸< std::pair< T1, T2 >, L, C > &	,
		RP	rp )

constexprexport

𝔸 & relPred — the relation as a set object on A×B. The universal product carries no factor restriction, so the relation's membership is the rel-predicate: the pure product universe refined to a subobject.

Template Parameters

T1,T2	the factor carriers;
L	the logic;
C	the product's cardinality class;
RP	the rel-predicate.

Parameters

rp	the rel-predicate on pairs.

Returns: Set<pair<T1,T2>, L, RP>.

◆ operator&() [2/3]

template<typename S, IsRelPredicate RP>
requires dedekind::sets::IsSetObject<S> && requires { typename S::Domain::first_type; typename S::Domain::second_type; } && (!dedekind::sets::contains_self_v<RP>)

auto dedekind::order::operator&	(	const S &	prod,
		RP	rp )

constexprexport

product & relPred — the relation as a set object on A×B, keeping the product's own membership (so a restricted product bounds the relation).

Generic over any set object on a pair carrier (a Set<pair,…>, a lattice node, a comprehension): the restricted χ datum is the product's classifier leg — P for a Set, the node itself for a node.

Template Parameters

S	an `IsSetObject` whose `Domain` is a pair;
RP	the rel-predicate.

Parameters

prod	the product set object;
rp	the rel-predicate on pairs.

Returns: Set<Domain, L, ProductRestrict<classifier, RP>>.

◆ operator&() [3/3]

template<typename P, typename S, IsArrow T>

Prefixed< P, S, T > dedekind::category::operator&	(	const Symmetric< P, S, T > &	s,
		const Prefix &	p )

constexpr

Parameters

s	the section.
p	the prefix.

Returns: their meet.

◆ operator>>()

template<std::ranges::view V, std::size_t Sigma, std::size_t Q>
requires std::ranges::random_access_range<V> && std::ranges::sized_range<V> && std::semiregular<V>

auto dedekind::category::operator>>	(	V	letters,
		const Maybe< Matches< Sigma, Q > > &	m )

constexpr

Parameters

letters	a text read as letters.
m	the stage, or nothing.

Returns: the query, or nothing: Maybe's action on the stage.

◆ order_fragment()

template<IsTotallyOrdered V, IsOckhamAlgebra L, typename K>

Runs< V, L > dedekind::order::detail_steps::order_fragment ( const Pred< K > & p )

The run list of a predicate built at run time over a chain, in the order fragment: the atoms π ⋈ k (and, on a machine word, π ± c ⋈ k: the atom's run list translated), under ∧ and ∨, a comparison of two constants decided; conditionals lifted first (lift_conditionals). The shape is a value, so the run list is materialised piece by piece. An atom outside the fragment has no normal form here and is refused.

Template Parameters

V	the chain.
L	the species.
K	the constants' type.

Parameters

p	the predicate.

◆ rel_apply()

template<Rel R, typename X, typename Y>

bool dedekind::sets::rel_apply	(	const X &	x,
		const Y &	y )

constexpr

x R y.

Template Parameters

R	the comparison.

Parameters

x	the left value.
y	the right value.

◆ rel_of()

Rel dedekind::order::rel_of	(	Direction	d,
		Strictness	s )

constexprexport

A restricted factor lifts to a cylinder on its axis, so operator* keeps the factor predicates instead of dropping them.

halfspace__Restricted_Products

The product is the universal set of products 𝔸<pair> refined by the two cylinders \(A\times B = \pi_1^{-1}(A)\cap\pi_2^{-1}(B)\). A total factor's cylinder is the whole universe (nothing to add); a halfspace factor \(\{x \bowtie p\}\) lifts to the projection halfspace \(\pi_I \bowtie p\) — the same comparison atom the graph surface uses, so a restricted domain and a functional graph read in one vocabulary and dom can recover the factor from the π_I conjunct.

The comparison a halfspace (Direction, Strictness) lifts to.

◆ steps()

template<typename T>
requires requires { typename T::logic_species; }

auto dedekind::order::steps ( const T & t )

constexprexport

The normal form of a set term of a chain, as a lazy step source. A stored run list inside the term is read in place, so the source must not outlive the term.

Parameters

t the term.

◆ structured_and()

template<IsTotallyOrdered V, IsOckhamAlgebra L>

Interval< V, L > dedekind::order::structured_and	(	const Interval< V, L > &	a,
		const Interval< V, L > &	b )

constexprexport

The meet of two intervals, under the reducer's customization-point name: the one reduce_meet. Declared here, before axis_factor, so the recursion over a RelAnd tree is closed over its own outputs (#872).

— ADL hooks for operator&&.

◆ upperbounds()

template<IsTotallyOrdered T, IsOckhamAlgebra L>

Interval< T, L > dedekind::order::upperbounds ( const Interval< T, L > & s )

constexprexport

upperbounds(S) — the \(\forall\)-projection \(R/\ni\): the region dominating all of S, and the pluggable point of the extremum (Bird & de~Moor [2]).

(relational surface)

max is one GENERIC definition, the \(\forall\)-projection of the order relation onto its second coordinate:

\[ \max S \;=\; \{\pi_2 \in S \mid \forall \pi_1 \in S.\; \pi_1 \le \pi_2\} \;=\; S \cap \mathrm{upperbounds}(S) \;=\; (\in) \cap (R/\ni). \]

upperbounds is the pluggable point (as \(\forall\) / \(\exists\) plug into Ø::operator==), decided SYMBOLICALLY per structure so no candidate is enumerated: a halfspace bounded ABOVE ({x≤p}) is dominated exactly by {x≥p}; one unbounded above ({x≥p}) has no upper bound (Ø). lowerbounds is the dual. The generic max/min then meet S with them, and the meet structured_and collapses the interval to the attained pivot ({x≤p} ∩ {x≥p} = {p}) or, when the sup is unattained (strict) or absent (unbounded), to Ø.

Upper bounds of an interval, {x ≥ sup}: a strict upper bound is attained at its predecessor on a discrete carrier (so max {x<p} is p−1), and kept on a dense one (so the meet is empty, no max); an interval unbounded above has none; everything bounds Ø.

Variable Documentation

◆ ℤ

auto dedekind::order::ℤ

inlineconstexpr

Initial value:

=

𝔸<SignedCardinality>{}

dedekind::sets::𝔸

The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint.

Definition boundaries.cppm:296

Classes

Namespaces

Concepts

Typedefs

Enumerations

Functions

Variables

Detailed Description

halfspace__Intervals_As_Values

halfspace__DSL_Surface

Typedef Documentation

◆ Cardinality

◆ Scaling

◆ Translation

Enumeration Type Documentation

◆ Ternary

logic__Species_2

Function Documentation

◆ axis_factor()

halfspace__Projections

◆ ext()

◆ intervals()

◆ max()

◆ negate()

◆ operator&() [1/3]

◆ operator&() [2/3]

◆ operator&() [3/3]

◆ operator>>()

◆ order_fragment()

◆ rel_apply()

◆ rel_of()

halfspace__Restricted_Products

◆ steps()

◆ structured_and()

— ADL hooks for operator&&.

◆ upperbounds()

(relational surface)

Variable Documentation

◆ ℤ