dyadic.cppm File Reference

Tarski's calculus of (dyadic) relations: converse R°, the relative product R;S, union/meet, the diagonal Δ, over Set<pair> — the BASE partition of dedekind.relational. More...

#include <array>
#include <concepts>
#include <functional>
#include <initializer_list>
#include <type_traits>
#include <utility>
import dedekind.sets;
import dedekind.category;

Include dependency graph for dyadic.cppm:

Classes
struct	dedekind::relational::FibrePredicate< Rel, T1 >
	The reified fibre of a relation R at a point x: the predicate \(b \mapsto (x,b)\in R\). Named (the sibling of GraphPredicate / PreimagePredicate) so the fibre is stable and inspectable rather than a lambda blackbox (#840). More...
struct	dedekind::relational::SwapPred< P >
	The swapped predicate for converse: \(R^\smile(b,a) = R(a,b)\). More...
struct	dedekind::relational::ComposePred< PR, PS, B >
	The composed predicate for the relative product \(R;S\) over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}. More...
struct	dedekind::relational::Intersect< R, S, Meet >
	The point-free composite meet R∩S = Δ† ∘ (R⊗S) ∘ Δ: copy the shared domain, run both legs in parallel, merge their codomain outputs where they agree. The arrow-level (spider) realisation of the relational intersection, whose (Copy,Merge) legs are certified by IsMeetAsRightAdjoint — the same R∩S the extensional operator& above computes over Set<pair>, spelled point-free. More...
struct	dedekind::relational::DiagPred< A >
	The equality-of-coordinates predicate for the diagonal \(\Delta = \{(a,a)\}\). A plain std::equality_comparable check — the diagonal is pure equality, no ordering, so it lives here at the base. More...
struct	dedekind::relational::PairwisePred< Op >
	A binary predicate on A read at the pair ⟨a, b⟩: the other direction of the bridge a set over a product crosses (#1047), so std::less_equal<bool> is a set of pairs. Named, so it carries op and the set inherits every law op has on A (the rules below). More...
struct	dedekind::relational::CoreflexivePred< S >
	The coreflexive predicate for \(\Delta_S = \{(x,x) \mid x \in S\}\) — the diagonal restricted to a unary set S (a partial identity): on the diagonal and in S. Carries S by value so it stays inspectable (no lambda). More...
struct	dedekind::relational::NodeAt
	The engine at one node and one law, as a function of the law; the converse reads its operand at the dagger law. More...
struct	dedekind::category::is_equality< A, Endo< A, L, C, DiagPred< A > > >
struct	dedekind::category::is_equality< A, Endo< A, L, C, PairwisePred< Op > > >
struct	dedekind::relational::Comprehension< Base, Predicate >
struct	dedekind::relational::𝔸< T, L, C >
	The universal set over the carrier T: the terminal object ⊤ of Sub(T), the reified type constraint. More...
struct	dedekind::relational::RelAnd< A, B >
	Meet (conjunction) of two relational predicates, the result of && on them. More...
struct	dedekind::relational::RelOr< A, B >
	Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd. More...
struct	dedekind::category::ComposePred< PR, PS, B >
	The composed predicate for the relative product \(R;S\) over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}. More...
struct	dedekind::category::DiagPred< A >
	The equality-of-coordinates predicate for the diagonal \(\Delta = \{(a,a)\}\). A plain std::equality_comparable check — the diagonal is pure equality, no ordering, so it lives here at the base. More...
struct	dedekind::category::PairwisePred< Op >
	A binary predicate on A read at the pair ⟨a, b⟩: the other direction of the bridge a set over a product crosses (#1047), so std::less_equal<bool> is a set of pairs. Named, so it carries op and the set inherits every law op has on A (the rules below). More...
struct	dedekind::category::SwapPred< P >
	The swapped predicate for converse: \(R^\smile(b,a) = R(a,b)\). More...
struct	dedekind::category::RelAnd< A, B >
	Meet (conjunction) of two relational predicates, the result of && on them. More...
struct	dedekind::category::RelOr< A, B >
	Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::relational::IsRelation
	Concept: a set S whose ambient type is std::pair<T1,T2> is a valid binary relation on T1 and T2.
concept	dedekind::relational::IsPairLike
	Pair-like carrier: both coordinates present — the shape every relation (converse, reflexive, symmetric, is_relation) assumes.

Typedefs
template<typename T1, typename T2, typename L, typename P>
using	dedekind::relational::Relation = Comprehension<𝔸<std::pair<T1, T2>, L>, P>
	A Relation from A to B is a set of pairs: a subset of A × B.
template<typename T1, typename T2, typename L, typename P>
using	dedekind::relational::SetFunction = Relation<T1, T2, L, P>
	A (set-level) Function is a Relation where each domain element maps to exactly one codomain element. The alias admits the same structure as a Relation; functional totality and single-valuedness are enforced at the call-site via witness elements.
template<typename Pair>
using	dedekind::relational::swapped_t
	The pair (b, a) of a pair (a, b): the shape the converse reads its operand at.
using	dedekind::relational::Laws = dedekind::category::Profile<Law, 4>
	The laws an arrow is certified: one answer in K₃ per law, a profile (category::Profile) over the four. A constexpr value, so the engine is read by the compiler on a typed relation (the traits of :cartesian, below) and by the program over a RelExpr (relational:rows, laws): one engine, two readers.
template<typename A, typename L, typename C, typename P>
using	dedekind::category::detail_endo_laws::Endo
template<typename A, typename L, typename C, typename P>
using	dedekind::category::Endo

Enumerations
enum class	dedekind::relational::Law : unsigned { Total , Univalent , Injective , Surjective }
	A law of an arrow of Rel, an inclusion: total \(\Delta \le R;R^\circ\), univalent \(R^\circ;R \le \Delta\), injective \(R;R^\circ \le \Delta\), surjective \(\Delta \le R^\circ;R\). Each names the set of the arrows with that law (𝔸<Re> & Total<Re>{}, relational:rows); a map is total and univalent, an isomorphism all four: meets of those sets, with nothing of their own.
enum class	dedekind::relational::Node {   Universe , Comprehension , Meet , Join ,   Not , Converse , Tensor , Compose ,   Sum }
	The nodes of a relational term: its two leaves (the full relation, a comprehension) and the operations of the calculus. RelExpr's Kind (relational:rows), and what the engine reads, free of the representation (a run-time node, a typed predicate).
enum class	dedekind::relational::detail_laws_witness::Ternary
	A three-valued propositional logic for handling partial information. More...

Functions
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::dom (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	The declared domain of a relation R ⊆ A×B: the universal set 𝔸 over the first factor — π₁'s codomain.
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::cod (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r)
	The declared codomain of a relation R ⊆ A×B: 𝔸, the second factor (π₂'s codomain). Dual to dom.
template<typename T1, typename T2, typename L, typename P, typename C>
constexpr auto	dedekind::relational::apply (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x)
	Relational application: the image of x under R, the fibre \(\{b \in B \mid (x,b) \in R\}\) as a Set on the codomain.
template<typename T1, typename T2, typename L, typename P, typename C> requires std::invocable<const Comprehension<𝔸<std::pair<T1, T2>, L, C>, P>&, std::pair<T1, T2>>
constexpr auto	dedekind::relational::fibre (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x)
	fibre(R, x) = the fibre \(\{b \mid (x,b)\in R\}\) as a named comprehension — the lambda-free sibling of apply (#840): the power transpose \(\Lambda R : A \to \mathcal{P}(B)\) read as a first-class subobject.
template<typename T1, typename T2, typename L, typename P, typename C, std::same_as< T1 >... Xs> requires (sizeof...(Xs) >= 1)
constexpr auto	dedekind::relational::fibre (const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > &r, const T1 &x0, const Xs &... xs)
	The relational IMAGE of a finite set of points, given as a pack: \(R[\{x_0,\dots,x_n\}] = \bigcup_i \mathrm{fibre}(R, x_i)\) — the power transpose extended from a point to a finite set, distributing over the join (image preserves unions, the left-adjoint law). Point-free and lambda-free: the structural | union of the named point-fibres, with no enumeration carrier (no array, no ∃). Probes only the given points, so it stays in the point-fibre's complexity class.
template<typename T1, typename T2, typename L, typename P> requires requires(const T2& y) { { y == y } -> dedekind::category::LiftableInto< typename SetFunction<T1, T2, L, P>::logic_species>; }
constexpr auto	dedekind::relational::is_single_valued_at (const SetFunction< T1, T2, L, P > &f, const T1 &x, const T2 &y1, const T2 &y2)
	Point-wise single-valuedness witness for a set-function relation.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain>
constexpr auto	dedekind::relational::converse (const R &r)
	converse(R) — the transpose \(R^\smile \subseteq B \times A\) of a relation \(R \subseteq A \times B\) (Tarski's \(R^\smile\)).
template<typename S>
consteval bool	dedekind::relational::is_relation (const S &)
	is_relation(R) — the bracket-free query: R is a relation, an IsSet whose Domain is a product \(A \times B\).
template<typename A, typename B, typename C, typename L, typename PR, typename PS, typename CR, typename CS> requires std::same_as<B, bool>
constexpr auto	dedekind::relational::operator>> (const Comprehension< 𝔸< std::pair< A, B >, L, CR >, PR > &r, const Comprehension< 𝔸< std::pair< B, C >, L, CS >, PS > &s)
	R >> S — the relative product of two relations over a Boolean intermediate, the ∃-over-the-middle enumerated on {false, true}. A larger intermediate needs the finite-quotient handle (§3.1); there is deliberately no overload, so it is an honest compile error. FIXME(#795): generalise the intermediate beyond bool.
template<typename A, typename B, typename L, typename PR, typename PS, typename C, typename CU>
constexpr auto	dedekind::relational::operator& (const Comprehension< 𝔸< std::pair< A, B >, L, C >, PR > &r, const Comprehension< 𝔸< std::pair< A, B >, L, CU >, PS > &s)
	R & S — the INTERSECTION (meet) of two relations over the same product, dual to the union | (Join): membership is both predicates (RelAnd). The Boolean-lattice ∩ on relations.
template<typename A, typename L = dedekind::category::Boole, typename Op>
constexpr auto	dedekind::relational::relation_of (Op op)
	relation_of<A>(op): the relation \(\{(a, b) \mid op(a, b)\} \subseteq A \times A\) of a binary predicate on A.
template<typename A, typename L = dedekind::category::Boole> requires std::equality_comparable<A>
constexpr auto	dedekind::relational::diag ()
	The DIAGONAL (identity relation) \(\Delta = \{(a,a)\}\) on a carrier A — {π_1==π_2} — the reflexive-closure unit and the 1 of the relation algebra.
template<typename S> requires dedekind::category::IsLSet<S>
constexpr auto	dedekind::relational::diag (const S &s)
	diag(S) — the coreflexive \(\Delta_S = \{(x,x) \mid x \in S\}\), the partial identity on a unary set (Tarski's monotype). Generalizes the full diagonal (diag(𝔸) recovers it) and is the restrictor for a relative product's endpoints, so a set pre-image is \(\mathrm{dom}(R \mathbin{;} \mathrm{diag}(S))\) without leaving the point-free surface.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain> && std::same_as<typename R::Domain::first_type, typename R::Domain::second_type>
constexpr auto	dedekind::relational::reflexive (const R &r)
	reflexive(R) = R | Δ — the smallest reflexive relation containing an endorelation R (add the self-loops). P is constrained to a genuine pair-predicate (invocable on a carrier pair \(\langle A,A \rangle\)) so a mis-typed R fails at the call, not deep inside the union.
template<typename R> requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain> && std::same_as<typename R::Domain::first_type, typename R::Domain::second_type>
constexpr auto	dedekind::relational::symmetric (const R &r)
	symmetric(R) = R | R° — the smallest symmetric relation containing R (add the reversed edges; R° is the converse).
constexpr auto	dedekind::relational::conv (const auto &r)
constexpr auto	dedekind::relational::dagger (const auto &r)
constexpr auto	dedekind::relational::refl (const auto &r)
constexpr auto	dedekind::relational::sym (const auto &r)
constexpr auto	dedekind::relational::Δ (const auto &s)
constexpr bool	dedekind::relational::closed_under (Law w, Node n)
	Closure: the arrows with the law w form a sub-algebra under n. Each of the four is closed under ; and ⊗. The + of this calculus is the sum of two tables, \(1 \to A + B\) (not the direct sum of arrows \(1 + 1 \to A + B\)): one input, both outputs, so it keeps totality, surjectivity and injectivity but not univalence.
constexpr bool	dedekind::relational::is_up_set (Law w)
	Variance in the inclusion order: total and surjective are up-sets (R ≤ S and R total ⇒ S total), univalent and injective down-sets (S univalent ⇒ R univalent).
constexpr Law	dedekind::relational::dagger (Law w)
	The dagger's action: ° carries total to surjective and univalent to injective, an involution on the laws.
constexpr dedekind::category::Ternary	dedekind::relational::infer (Law w, Node n, dedekind::category::Ternary a, dedekind::category::Ternary b=dedekind::category::Ternary::Unknown)
	The engine, one for every law and every representation: a node's answer in K₃ from the law's facts and its legs' answers a, b. Where the set is closed under the node, both legs; a down-set holds f & g when it holds f or g (f & g ≤ f), an up-set holds f | g likewise; ° is answered by the operand at the dagger law (a, looked up by the caller); ~ by no fact. True where inferred, Unknown where no fact applies, never False: the facts certify, they do not refute (sound, not complete). So for a closed set S, S(f) ∧ S(g) ≤ S(f >> g): a law of the sets' χ, tested in rows_test.
constexpr Laws	dedekind::relational::laws_from (bool total, bool univalent, bool injective, bool surjective)
	Declared answers, read off four witnesses.
constexpr Laws	dedekind::relational::node_laws (Node n, const Laws &a, const Laws &b={})
	The engine at a node, law by law: the legs' answers in, the node's out; ° reads its operand at the dagger law.

Variables
constexpr std::array< Law, 4 >	dedekind::relational::every_law
template<typename R>
constexpr Laws	dedekind::relational::laws_of_v
	The engine read for a typed relation: its four laws as the :cartesian traits answer them, declared on a leaf or inferred on a node (the readers in the category namespace below).
template<typename A, typename L, typename C>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, A >, L, C >, dedekind::relational::DiagPred< A > > > = true
template<typename A, typename L, typename C>
constexpr bool	dedekind::category::is_left_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, A >, L, C >, dedekind::relational::DiagPred< A > > > = true
template<typename A, typename L, typename C>
constexpr bool	dedekind::category::is_left_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, A >, L, C >, dedekind::relational::DiagPred< A > > > = true
template<typename A, typename L, typename C>
constexpr bool	dedekind::category::is_right_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, A >, L, C >, dedekind::relational::DiagPred< A > > > = true
template<typename A, typename C, typename L, typename PR, typename PS, typename B, typename Card>
constexpr bool	dedekind::category::is_left_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, C >, L, Card >, dedekind::relational::ComposePred< PR, PS, B > > >
template<typename A, typename C, typename L, typename PR, typename PS, typename B, typename Card>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, C >, L, Card >, dedekind::relational::ComposePred< PR, PS, B > > >
template<typename A, typename C, typename L, typename PR, typename PS, typename B, typename Card>
constexpr bool	dedekind::category::is_left_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, C >, L, Card >, dedekind::relational::ComposePred< PR, PS, B > > >
template<typename A, typename C, typename L, typename PR, typename PS, typename B, typename Card>
constexpr bool	dedekind::category::is_right_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, C >, L, Card >, dedekind::relational::ComposePred< PR, PS, B > > >
template<typename B, typename A, typename L, typename Card, typename P>
constexpr bool	dedekind::category::is_left_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< B, A >, L, Card >, dedekind::relational::SwapPred< P > > >
template<typename B, typename A, typename L, typename Card, typename P>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< B, A >, L, Card >, dedekind::relational::SwapPred< P > > >
template<typename B, typename A, typename L, typename Card, typename P>
constexpr bool	dedekind::category::is_left_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< B, A >, L, Card >, dedekind::relational::SwapPred< P > > >
template<typename B, typename A, typename L, typename Card, typename P>
constexpr bool	dedekind::category::is_right_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< B, A >, L, Card >, dedekind::relational::SwapPred< P > > >
template<typename A, typename B, typename L, typename Card, typename PR, typename PS>
constexpr bool	dedekind::category::is_left_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, Card >, dedekind::sets::RelAnd< PR, PS > > >
template<typename A, typename B, typename L, typename Card, typename PR, typename PS>
constexpr bool	dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, Card >, dedekind::sets::RelAnd< PR, PS > > >
template<typename A, typename B, typename L, typename Card, typename PR, typename PS>
constexpr bool	dedekind::category::is_left_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, Card >, dedekind::sets::RelAnd< PR, PS > > >
template<typename A, typename B, typename L, typename Card, typename PR, typename PS>
constexpr bool	dedekind::category::is_right_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, Card >, dedekind::sets::RelAnd< PR, PS > > >
template<typename A, typename L, typename C, typename Op>
constexpr bool	dedekind::category::is_reflexive_v< A, Endo< A, L, C, PairwisePred< Op > > >
template<typename A, typename L, typename C, typename Op>
constexpr bool	dedekind::category::is_symmetric_v< A, Endo< A, L, C, PairwisePred< Op > > >
template<typename A, typename L, typename C, typename Op>
constexpr bool	dedekind::category::is_transitive_v< A, Endo< A, L, C, PairwisePred< Op > > >
template<typename A, typename L, typename C, typename Op>
constexpr bool	dedekind::category::is_antisymmetric_v< A, Endo< A, L, C, PairwisePred< Op > > >
template<typename A, typename L, typename C, typename Op>
constexpr bool	dedekind::category::is_connex_v< A, Endo< A, L, C, PairwisePred< Op > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_reflexive_v< A, Endo< A, L, C, RelAnd< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_symmetric_v< A, Endo< A, L, C, RelAnd< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_transitive_v< A, Endo< A, L, C, RelAnd< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_antisymmetric_v< A, Endo< A, L, C, RelAnd< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_reflexive_v< A, Endo< A, L, C, RelOr< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_symmetric_v< A, Endo< A, L, C, RelOr< PR, PS > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_connex_v< A, Endo< A, L, C, RelOr< PR, PS > > >
template<typename A, typename L, typename C, typename P>
constexpr bool	dedekind::category::is_reflexive_v< A, Endo< A, L, C, SwapPred< P > > >
template<typename A, typename L, typename C, typename P>
constexpr bool	dedekind::category::is_symmetric_v< A, Endo< A, L, C, SwapPred< P > > >
template<typename A, typename L, typename C, typename P>
constexpr bool	dedekind::category::is_transitive_v< A, Endo< A, L, C, SwapPred< P > > >
template<typename A, typename L, typename C, typename P>
constexpr bool	dedekind::category::is_antisymmetric_v< A, Endo< A, L, C, SwapPred< P > > >
template<typename A, typename L, typename C, typename P>
constexpr bool	dedekind::category::is_connex_v< A, Endo< A, L, C, SwapPred< P > > >
template<typename A, typename L, typename C, typename PR, typename PS>
constexpr bool	dedekind::category::is_reflexive_v< A, Endo< A, L, C, ComposePred< PR, PS, A > > >

Detailed Description

Tarski's calculus of (dyadic) relations: converse R°, the relative product R;S, union/meet, the diagonal Δ, over Set<pair> — the BASE partition of dedekind.relational.

@partition :dyadic

Copyright

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

dyadic__The_Base

Every relation in Trsk is a Set<std::pair<A,B>> — a dyad. Tarski's calculus of relations (Tarski 1941, "On the Calculus of Relations") is the Boolean involutive monoid on that carrier: converse \(R^{\circ}\) (converse / SwapPred), relative product \(R;S\) (operator>> / ComposePred), union \(R\cup S\) (the set-grammar | / Join), meet \(R\cap S\) (operator& / RelAnd), the diagonal \(\Delta\) (diag), and the derived reflexive / symmetric closures. The reflexive-transitive closure \(R^{*}\) would be the Kleene star over \((\cup,;)\) — not yet a provided operator (>> is Boolean-middle only; FIXME(#786)).

These combinators moved DOWN out of order/halfspace.cppm (#792): they are pure Set<pair> algebra with no ordering, so they belong below order. The term grammar (projections, atoms, && / ||) lives in sets:terms; order keeps the reading of order atoms as halfspaces and the relation witnesses that need an order.

dyadic__Base_Of_The_Others

:graph (graphs of arrows) and :tables (Codd's n-ary model) both build on this base: :dyadic → (:graph, :tables). A graph \(\Gamma_f=\{(a,f(a))\}\) is a dyad; and Codd's natural_join \(R_1\bowtie R_2\) IS the relative product \(R_1;R_2\) with the pivot retained (one \(\exists\) apart from >>).

dyadic__Seeded_Intentions

Two algebraic reframings are seeded here as dependency + intention, not yet wired (deferred to the post-architecture algebraic phase):

• FIXME(#798): re-target :tables' natural_join onto operator>> so Codd's ⋈ is literally Tarski's ; (tagged vs. projected relative product).
• FIXME(#799): frame n-ary products as flat std::tuple rather than nested std::pair (get / apply / structured bindings for free).

Note

These :dyadic symbols were dedekind::order on the halfspace; they now live in the dedekind::relational namespace — the module's OWN namespace, so the symbols match the module. The carrier they operate on (Set<pair>) stays dedekind::sets::Set; relations simply are sets of pairs. Migration impact: converse / is_relation / reflexive / symmetric / preimage take a Set argument, so they were ADL-reachable from dedekind::sets and now need qualification or a using; so do the infix operators >> / & (union is the set-grammar |). (Only graph — called on an arrow — and the relation/function concepts never ADL-reached sets.) A consumer that wants the bare forms brings them in with using namespace dedekind::relational once; callers that spelled dedekind::sets::converse / is_relation / ComposePred repoint to dedekind::relational::.

Typedef Documentation

Endo

template<typename A, typename L, typename C, typename P>

using dedekind::category::detail_endo_laws::Endo

Initial value:

 
    dedekind::sets::Comprehension<dedekind::sets::𝔸<std::pair<A, A>, L, C>, P>

Relation

template<typename T1, typename T2, typename L, typename P>

using dedekind::relational::Relation = Comprehension<𝔸<std::pair<T1, T2>, L>, P>

export

A Relation from A to B is a set of pairs: a subset of A × B.

ETCS reading: relations are subobjects of products.

See also

Lambek and Scott [5]

SetFunction

template<typename T1, typename T2, typename L, typename P>

using dedekind::relational::SetFunction = Relation<T1, T2, L, P>

export

A (set-level) Function is a Relation where each domain element maps to exactly one codomain element. The alias admits the same structure as a Relation; functional totality and single-valuedness are enforced at the call-site via witness elements.

See also

Pierce [10]

swapped_t

template<typename Pair>

using dedekind::relational::swapped_t

Initial value:

 
    std::pair<typename Pair::second_type, typename Pair::first_type>

The pair (b, a) of a pair (a, b): the shape the converse reads its operand at.

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

apply()

template<typename T1, typename T2, typename L, typename P, typename C>

auto dedekind::relational::apply ( const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > & r, const T1 & x )

constexprexport

Relational application: the image of x under R, the fibre \(\{b \in B \mid (x,b) \in R\}\) as a Set on the codomain.

This is the power transpose \(\Lambda R : A \to \mathcal{P}(B)\) of Bird & de~Moor [2] — the relation read as a set-valued map — and it is the form on which the optimisation calculus is built: argmax is \(\max R \cdot \Lambda F\) (§3.3 / §4). The general form. R IS-A relation (and IsFunction refines IsRelation), so a functional R gives a singleton fibre — the value f(x) — and a general relation the full image; the degenerate cases fall out as the fibre's cardinality, with no special-casing (the singleton-valued specialisation is a later overload gated on the functional certificate). The fibre is lazy and membership-testable (apply(R,x)(b) is (x,b)∈R), so it types in for any relation and the existential — is it nonempty? what is its max? — is deferred to whoever reduces it.

Deprecated

(documentation-level; #840). apply returns the fibre as a capturing lambda, so its Set carries an opaque, anonymous, non-equality_comparable predicate type: two apply results are never type-equal and the Set cannot round-trip through as_relation. Prefer fibre(R,x) below — it reifies the same fibre as the named FibrePredicate (a stable, inspectable, GraphPredicate / PreimagePredicate-style type). apply is retained (no [[deprecated]] attribute, to keep its existing call sites -Werror-clean) only for the throw-away, reduce-it-now case.

converse()

template<typename R>
requires dedekind::sets::IsSetObject<R> && IsPairLike<typename R::Domain>

auto dedekind::relational::converse ( const R & r )

constexprexport

converse(R) — the transpose \(R^\smile \subseteq B \times A\) of a relation \(R \subseteq A \times B\) (Tarski's \(R^\smile\)).

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

Template Parameters

R	an IsSetObject whose Domain is a pair A×B.

Parameters

r	the relation.

Returns

the relation Set<pair<B,A>, L, SwapPred<classifier>>.

diag()

template<typename S>
requires dedekind::category::IsLSet<S>

auto dedekind::relational::diag ( const S & s )

constexprexport

diag(S) — the coreflexive \(\Delta_S = \{(x,x) \mid x \in S\}\), the partial identity on a unary set (Tarski's monotype). Generalizes the full diagonal (diag(𝔸) recovers it) and is the restrictor for a relative product's endpoints, so a set pre-image is \(\mathrm{dom}(R \mathbin{;} \mathrm{diag}(S))\) without leaving the point-free surface.

Note

Linear-algebra incarnation: given a suitable domain/codomain — a finite, indexable carrier A (a dimension D) and the logic semiring 𝔹 as scalar — this coreflexive is a diagonal matrix dedekind::linear_algebra::Diagonal<D, χ_S>, whose diagonal rule is exactly S's characteristic function (CoreflexivePred::s is the diagonal rule F, both point-free). The full diagonal diag(𝔸) is then the Identity<D> matrix. So diag on the two surfaces is one partial-identity operator. FIXME(#873): the concrete coreflexive→Diagonal bridge (needs the finite-carrier→dimension indexing).

dom()

template<typename T1, typename T2, typename L, typename P, typename C>

auto dedekind::relational::dom ( const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > & r )

constexprexport

The declared domain of a relation R ⊆ A×B: the universal set 𝔸 over the first factor — π₁'s codomain.

A relation is a Set on the product carrier pair<A,B>, so it is IsProduct and its projections fall out of the type: the factor type A survives in R::Domain (pair<A,B>) even though the factor set is not retained, so the declared domain 𝔸 is recoverable total and free, with no ∃. This is deliberately not the effective domain \(\{a \mid \exists b.\ R(a,b)\}\) (the π₁-image), which is a separate existential carrying its own decidability certificate — the Rice wall stays quarantined to that one operation.

fibre()

template<typename T1, typename T2, typename L, typename P, typename C, std::same_as< T1 >... Xs>
requires (sizeof...(Xs) >= 1)

auto dedekind::relational::fibre ( const Comprehension< 𝔸< std::pair< T1, T2 >, L, C >, P > & r, const T1 & x0, const Xs &... xs )

constexprexport

The relational IMAGE of a finite set of points, given as a pack: \(R[\{x_0,\dots,x_n\}] = \bigcup_i \mathrm{fibre}(R, x_i)\) — the power transpose extended from a point to a finite set, distributing over the join (image preserves unions, the left-adjoint law). Point-free and lambda-free: the structural | union of the named point-fibres, with no enumeration carrier (no array, no ∃). Probes only the given points, so it stays in the point-fibre's complexity class.

Note

A set-valued argument (fibre(R, S) for an intensional S) is the power-set-monad image, which needs a constexpr enumerable finite-set carrier — FIXME(#691). The pack is the honest finite instance.

is_single_valued_at()

template<typename T1, typename T2, typename L, typename P>
requires requires(const T2& y) { { y == y } -> dedekind::category::LiftableInto< typename SetFunction<T1, T2, L, P>::logic_species>; }

auto dedekind::relational::is_single_valued_at ( const SetFunction< T1, T2, L, P > & f, const T1 & x, const T2 & y1, const T2 & y2 )

constexprexport

Point-wise single-valuedness witness for a set-function relation.

If both y1 and y2 are related to x, they must be equal. Computed in the function's own species, not its base's tag.

Variable Documentation

every_law

std::array<Law, 4> dedekind::relational::every_law

inlineconstexprexport

Initial value:

{
    Law::Total, Law::Univalent, Law::Injective, Law::Surjective}

laws_of_v

template<typename R>

Laws dedekind::relational::laws_of_v

inlineconstexprexport

Initial value:

=
    laws_from(dedekind::category::is_left_total_v<R>,
              dedekind::category::is_right_unique_v<R>,
              dedekind::category::is_left_unique_v<R>,
              dedekind::category::is_right_total_v<R>)

The engine read for a typed relation: its four laws as the :cartesian traits answer them, declared on a leaf or inferred on a node (the readers in the category namespace below).