relprod.cppm File Reference

The relative product \(R;S\) over a FINITE ℕ-prefix middle: the generalization of :relational's Boolean-middle >> (which enumerates {false,true}) to a bounded ℕ carrier \([0,M)\). The \(\exists\)-over-the-middle is a short-circuiting scan (std::ranges::any_of: it stops at the first witness), and the bound M is carried on the composed type so repeated squaring (R;R, (R;R);(R;R), …) stays bounded — the semantic for-loop of bounded transitive closure (#795). More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <ranges>
#include <utility>
import dedekind.order;
import dedekind.sets;

Include dependency graph for relprod.cppm:

Classes
struct	dedekind::sequences::detail_relprod::IsMiddle< PR, PS, Pair >
	Whether b is a middle for \((a, c)\): \(R(a,b) \wedge S(b,c)\), with b the i-th element of ℕ. More...
struct	dedekind::sequences::ComposePrefixPred< PR, PS >
struct	dedekind::sequences::Comprehension< Base, Predicate >

Namespaces
namespace	dedekind::sequences::detail_relprod
	The composed predicate for \(R;S\) over the finite ℕ-prefix \([0,M)\) middle. Carries M (so the bound survives repeated squaring) and the two operand IsRelPredicate operands. The \(\exists\)-over-the-middle is the short-circuiting std::ranges::any_of over a lazy iota generator: it advances only to the first witness \(b\), so a hit returns immediately ( \(\top \vee x = \top\)) — O(1) memory (no bool accumulator threaded), O(M) steps worst-case, no array.

Concepts
concept	dedekind::sequences::HasPrefixBound
	A relation is bounded (composable over a finite middle) iff its predicate carries a prefix_bound.

Functions
template<typename Pp, typename K>
constexpr std::size_t	dedekind::sequences::prefix_bound (const dedekind::order::ProductRestrict< Pp, dedekind::sets::Cmp< dedekind::sets::Rel::Lt, dedekind::sets::Projection< 1 >, dedekind::sets::Const< K > > > &p)
	prefix_bound(p) — recover the finite-prefix bound M carried by a bounded relation's predicate p: either from the half-space restriction (a ProductRestrict wrapping the domain cut π_1 < M, whose bound is a VALUE), or from a prior compose (ComposePrefixPred carries its bound). Left undefined otherwise — an unbounded relation has no finite middle to compose over, so its >> stays the honest Rice wall. A function, not a trait: since the pivot rides in the value, so does the bound; it still folds at compile time when the relation is constexpr.
template<typename PR, typename PS>
constexpr std::size_t	dedekind::sequences::prefix_bound (const ComposePrefixPred< PR, PS > &p)
template<typename A, typename B, typename C, typename L, IsCardinality K1, IsCardinality K2, IsRelPredicate PR, IsRelPredicate PS> requires HasPrefixBound<PR>
constexpr auto	dedekind::sequences::operator>> (const Comprehension< 𝔸< std::pair< A, B >, L, K1 >, PR > &r, const Comprehension< 𝔸< std::pair< B, C >, L, K2 >, PS > &s)
	R >> S over the finite ℕ-prefix middle inferred from R's bound (no middle argument): \((R;S)(a,c) = \exists b \in [0,M).\, R(a,b) \wedge S(b,c)\), streamed as an OR-fold. The result is itself bounded (ComposePrefixPred carries M), so the squaring chain collatzM >> collatzM >> … composes without re-supplying the middle. Generalizes :relational's Boolean-middle >> to a bounded ℕ carrier (#795). Gated on HasPrefixBound so the unbounded >> is non-viable here (it stays the Boolean case in :relational).
constexpr Cardinality	dedekind::sequences::finite_cardinality (std::size_t n)
	Convenience constructor for finite cardinal values.

Detailed Description

The relative product \(R;S\) over a FINITE ℕ-prefix middle: the generalization of :relational's Boolean-middle >> (which enumerates {false,true}) to a bounded ℕ carrier \([0,M)\). The \(\exists\)-over-the-middle is a short-circuiting scan (std::ranges::any_of: it stops at the first witness), and the bound M is carried on the composed type so repeated squaring (R;R, (R;R);(R;R), …) stays bounded — the semantic for-loop of bounded transitive closure (#795).

@partition :relprod

Copyright

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

relprod__Why_Here

Homed downstream of relational (where the Boolean >> lives): the bound M is read from an order-level ProductRestrict (the domain cut R | (π_1 < M)), which relational — upstream of order — cannot see, so the bounded >> cannot live beside its Boolean sibling. It sits in sequences (the first module below both order and relational that the exhibit already imports); consumers reach the bare >> via using namespace dedekind::sequences.

Wikipedia: Composition of relations, Transitive closure, Relation algebra

Note

"The logical theory which is called the calculus of (binary) relations, and the development of which is the subject of this paper, has had a strange and rather capricious line of historical development." – Alfred Tarski, On the Calculus of Relations, Journal of Symbolic Logic 6 (1941), §1.