|
Dedekind 0.0.0
A structuralist C++23 Module Library
|
Semiring-generic low-rank transfer operators: the bra·ket inner product, the ⊕/⊗ matrix-product kernel, and the rank-1 collapse D² = λ a transfer power analytic.
More...· makesD that
#include <array>#include <concepts>#include <cstddef>#include <functional>#include <type_traits>#include <utility>import dedekind.linear_algebra:matnxn;import dedekind.sets;import dedekind.relational;import dedekind.category;import dedekind.order;import dedekind.algebra;
Classes | |
| struct | dedekind::linear_algebra::Scaled< F, Mult > |
The scalar ⊗-action on an arrow f : D → S: \((c \odot f)(x) = c \otimes f(x)\). An IsArrow (the scaled vector), carrying the scalar c and the arrow f. More... | |
| struct | dedekind::linear_algebra::PointwiseSum< F, G, Add > |
The pointwise ⊕ of two arrows over a shared domain: \((f \boxplus g)(x) = f(x) \oplus g(x)\). An IsArrow (the sum vector). More... | |
| struct | dedekind::linear_algebra::Reflected< F > |
Reflect an arrow through the origin of its domain: \((U f)(x) =
f(-x)\) — the parity operator U precomposed onto f. The third intensional combinator (beside Scaled / PointwiseSum) that completes the surface: with them it ASSEMBLES the even projector \(P = \tfrac12(I+U)\) as scaled(½, pointwise_sum(f, reflected(f))), rather than hand-rolling pointwise + and scalar ·. Requires the domain to carry unary negation (found by ADL on the domain type). More... | |
| struct | dedekind::linear_algebra::detail_transfer::QuadDiagRule |
| struct | dedekind::linear_algebra::detail_transfer::EdgeSucc |
The path DAG's edge relation i → i+1, a NAMED predicate carrier (un-lambda'd, so it is a typed relation the DSL converse and relation traits attach to). More... | |
| struct | dedekind::linear_algebra::detail_transfer::WeightedUnitPath |
| struct | dedekind::linear_algebra::detail_transfer::CyclicShift |
Namespaces | |
| namespace | dedekind::linear_algebra::detail_transfer |
Typedefs | |
| template<typename S, std::size_t N> | |
| using | dedekind::linear_algebra::SquareMatrix = MatNxNV<S, N> |
A dense N×N semiring matrix — the extensional adjacency carrier a relation materialises to. Finite N by construction, hence the IsExtensional witness the star's fixpoint needs. This is Mat(S) (MatNxNV, :matnxn), the certified matrix semiring; the alias keeps the transfer-local spelling while ⊕/⊗ and the *-closure come from semiring_ops<Mat(S)>, not hand-rolled here. | |
| template<typename Rel> | |
| using | dedekind::linear_algebra::rel_codomain_t |
| using | dedekind::linear_algebra::detail_transfer::MP = MaxPlus<unsigned long long> |
| using | dedekind::linear_algebra::detail_transfer::TropMult = typename dedekind::algebra::semiring_ops<MP>::mult |
| using | dedekind::linear_algebra::detail_transfer::Idx2 = std::pair<std::size_t, std::size_t> |
| using | dedekind::linear_algebra::detail_transfer::TropAdd = typename dedekind::algebra::semiring_ops<MP>::add |
| using | dedekind::linear_algebra::detail_transfer::PMat = std::remove_cvref_t<decltype(Pmat)> |
| using | dedekind::linear_algebra::detail_transfer::PDagger = TransposeF<bool, 4> |
| using | dedekind::linear_algebra::detail_transfer::PMatMult |
| template<typename T> | |
| using | dedekind::linear_algebra::detail_transfer::MaxPlus |
Functions | |
| template<typename Add, typename S, typename Term, std::size_t... K> | |
| constexpr S | dedekind::linear_algebra::add_fold (std::index_sequence< K... >, S zero, Term term) |
The one reduction the transfer surface keeps: a structured ⊕-fold ⊕_{k<N} term(k) over the (low, fixed) rank index, the empty fold being the ⊕-identity. A fold-expression, not an imperative loop — the DSL folds structurally, so the reduction stays intensional until an optimum "means it". | |
| template<std::size_t N, typename Bra, typename Ket, typename S = typename std::remove_cvref_t<Bra>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<Bra> && dedekind::category::IsArrow<Ket> && dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr S | dedekind::linear_algebra::inner_product (const Bra &w, const Ket &v) |
The bra·ket inner product ⟨w|v⟩ = ⊕_{k<N} w(k) ⊗ v(k) over a semiring. Bra w and ket v are IsArrow factors (index → scalar); N is the shared dimension. | |
| template<typename S, typename Add, typename Mult> | |
| constexpr std::pair< S, S > | dedekind::linear_algebra::detail_geom::geo_pair (const S &r, std::size_t N) |
\((\sum_{k<N} r^k,\ r^N)\) by O(log N) doubling, division-free (only the semiring ⊕/, so correct over any rig and free of an overflow-prone unconditional final square. S(2m)=S(m)⊕rᵐ⊗S(m); the odd step adds the trailing term and advances the running power. | |
| template<typename S, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr S | dedekind::linear_algebra::geometric_sum (const S &r, std::size_t N) |
| The structure-directed finite geometric sum \(\sum_{k=0}^{N-1} r^k\), in closed form. | |
| template<typename F, typename S = typename std::remove_cvref_t<F>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<F> && std::same_as<std::remove_cvref_t<S>, typename std::remove_cvref_t<F>::Codomain> && dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr Scaled< std::remove_cvref_t< F >, Mult > | dedekind::linear_algebra::scaled (S c, F f) |
| Scale an arrow by a scalar — the \(c \odot f\) semimodule action. | |
| template<typename F, typename G, typename S = typename std::remove_cvref_t<F>::Codomain, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsArrow<F> && dedekind::category::IsArrow<G> && std::same_as<typename std::remove_cvref_t<F>::Domain, typename std::remove_cvref_t<G>::Domain> && std::same_as<S, typename std::remove_cvref_t<G>::Codomain> && dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr PointwiseSum< std::remove_cvref_t< F >, std::remove_cvref_t< G >, Add > | dedekind::linear_algebra::pointwise_sum (F f, G g) |
Add two arrows pointwise — the \(f \boxplus g\) semimodule addition. Both factors must share Domain and Codomain. | |
| template<typename F> requires dedekind::category::IsArrow<F> && requires(const std::remove_cvref_t<F>& cf, const typename std::remove_cvref_t<F>::Domain& x) { cf(-x); } | |
| constexpr Reflected< std::remove_cvref_t< F > > | dedekind::linear_algebra::reflected (F f) |
Reflect an arrow through its domain origin — the parity U. | |
| template<std::size_t N, typename A, typename B, typename S = std::remove_cvref_t<std::invoke_result_t<A, std::size_t, std::size_t>>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr S | dedekind::linear_algebra::matmul_entry (const A &a, const B &b, std::size_t i, std::size_t j) |
The semiring matrix-product entry (A⊗(i,j) = A and B are any (i,j)→ maps (e.g. an OuterProduct); N is the contracted (middle) dimension. | |
| template<std::size_t N, typename U, typename V, typename Mult> | |
| constexpr auto | dedekind::linear_algebra::eigenvalue (const OuterProduct< U, V, Mult > &m) |
The rank-1 eigenvalue of a dyad M = |v⟩⟨w|: λ = ⟨w|v⟩. Over a commutative semiring M² = λ central, so it factors out of M²(i,j) = v_i ⊗ λ ⊗ w_j; the tropical carriers (max-plus / min-plus) are commutative. Over a noncommutative semiring the middle scalar stays put (v_i ⊗ λ ⊗ w_j) and does not collapse to λ the dyad's factors straight off the OuterProduct. | |
|
template<std::size_t L, typename Bead, typename S = std::remove_cvref_t<std::invoke_result_t<Bead, std::size_t>>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr S | dedekind::linear_algebra::transfer_chain (Bead bead) |
The closure of a length-L chain of transfers: the ⊗-fold of their per-bead eigenvalues ⊗_{m<L} bead(m). A structured fold whose accumulator is a single scalar — because each transfer is rank-1, that scalar is the entire memo (dim = rank = 1). Intensional: bead is an index→λ map, and nothing materialises until the value is forced ("realize it when you mean
it"). | |
| template<typename Rel> | |
| constexpr auto | dedekind::linear_algebra::rel_entry (const Rel &rel, std::size_t i, std::size_t j) |
Read a relation's (i,j) entry, accepting EITHER the two-index weighted call rel(i,j) (a semiring-adjacency arrow) OR the point-free DSL call rel({i,j}) (a Set<pair> relation). This one seam is what lets a typed Ddk relation — not a raw lambda — feed ext. | |
|
template<std::size_t N, typename Rel, typename S = rel_codomain_t<Rel>, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr SquareMatrix< S, N > | dedekind::linear_algebra::ext (const Rel &rel) |
THE JOINT: materialise a binary endorelation on a semiring into its dense extensional adjacency SquareMatrix — the generic (black-box) fiber of the relation→matrix map (§ the paper's classification table). rel is (i,j)→ the same finite index carrier [0,N) on both sides (hence endo, hence square), with the codomain S an IsSemiring (so ⊕/⊗ and thus star are defined). The compile-time bound N is the extensionality constraint: an infinite relation has no such N and cannot form a matrix, so the Rice wall lives in this signature. Structured relations (functional, bijective, rank-1) admit specialised fibers (sparse, orthogonal, low-rank); this is the base case. | |
| template<std::size_t N, typename S, typename Add = typename dedekind::algebra::semiring_ops<S>::add, typename Mult = typename dedekind::algebra::semiring_ops<S>::mult> requires dedekind::category::IsSemiring<S, Add, Mult> | |
| constexpr SquareMatrix< S, N > | dedekind::linear_algebra::star (const SquareMatrix< S, N > &A) |
The Kleene star A* = ⨆ₙ Aⁿ = Δ ⊕ A ⊕ A² ⊕ … — R* as a running corollary of the generic closure, iterating M ↦ Δ ⊕ M⊗A to its fixpoint on the extensional matrix. Over Bool it is reachability; over MaxPlus the longest path (the algebraic path problem). Discharges FIXME(#786) for R* as a matrix corollary; the SquareMatrix argument is the extensionality the intensional relation lacked. | |
| template<std::size_t N, typename S> | |
| constexpr SquareMatrix< S, N > | dedekind::linear_algebra::transpose (const SquareMatrix< S, N > &A) |
The extensional dagger: the transpose Aᵀ (swap i,j) of an already-materialised matrix. The dagger itself is converse (the intensional predicate swap R°(i,j) = R(j,i), see the witnesses); this transpose is only its materialised realisation, worth forming when a physical layout is wanted (cache locality) rather than as the operation. On Rel the dagger is converse, on a real space the transpose, on a Hilbert space the adjoint; it reverses every arrow, so (R°)* = (R*)° is CPM's backward pass (the latest-start times). | |
Variables | |
| constexpr Ket< MP, 2 > | dedekind::linear_algebra::detail_transfer::v_entry {{MP::of(3), MP::of(5)}} |
| constexpr Bra< MP, 2 > | dedekind::linear_algebra::detail_transfer::w_exit {{MP::of(5), MP::of(2)}} |
| constexpr MP | dedekind::linear_algebra::detail_transfer::lambda = inner_product<2>(w_exit, v_entry) |
| constexpr OuterProduct< Ket< MP, 2 >, Bra< MP, 2 >, TropMult > | dedekind::linear_algebra::detail_transfer::bead |
| constexpr Ket< unsigned, 2 > | dedekind::linear_algebra::detail_transfer::qa {{2u, 3u}} |
| constexpr Diagonal< dim_finite< 2 >, QuadDiagRule > | dedekind::linear_algebra::detail_transfer::qD {} |
| constexpr diagonal_product_rule< QuadDiagRule, Ket< unsigned, 2 > > | dedekind::linear_algebra::detail_transfer::qDa |
| constexpr Ket< bool, 2 > | dedekind::linear_algebra::detail_transfer::v_present {{true, true}} |
| constexpr Bra< bool, 2 > | dedekind::linear_algebra::detail_transfer::w_first {{true, false}} |
| constexpr auto | dedekind::linear_algebra::detail_transfer::path_rel |
| constexpr auto | dedekind::linear_algebra::detail_transfer::Bstar = star<4>(ext<4>(path_rel)) |
| constexpr MP | dedekind::linear_algebra::detail_transfer::mp_bot = dedekind::category::unit<MP>(TropAdd{}) |
| constexpr WeightedUnitPath | dedekind::linear_algebra::detail_transfer::wpath {} |
| constexpr auto | dedekind::linear_algebra::detail_transfer::Tstar = star<4>(ext<4>(wpath)) |
| constexpr auto | dedekind::linear_algebra::detail_transfer::perm_rel |
| constexpr auto | dedekind::linear_algebra::detail_transfer::Pmat = ext<4>(perm_rel) |
| constexpr auto | dedekind::linear_algebra::detail_transfer::PdaggerMat |
Semiring-generic low-rank transfer operators: the bra·ket inner product, the ⊕/⊗ matrix-product kernel, and the rank-1 collapse D² = λ a transfer power analytic. · makesD that
@partition :transfer
The dense :mat2x2 and the intensional :diagonal carriers multiply entries with the built-in ring · — so a max-plus dioid, which has no C++ operator*, cannot be an entry type. This partition supplies the missing semiring surface, routing every scalar product through an Mult = ⊗ functor and every scalar sum through Add = ⊕, defaulted (like dedekind::optimization::semiring_closure) from dedekind::algebra::semiring_ops. The one gate is dedekind::category::IsSemiring — never HasRingOperators.
A rank-1 dyad M = |v⟩⟨w| (an OuterProduct with a semiring Mult) composes with itself in closed form:
\[ (M \cdot M)(i,j) \;=\; \bigoplus_k v_i \otimes w_k \otimes v_k \otimes w_j \;=\; v_i \otimes \Big(\underbrace{\bigoplus_k w_k \otimes v_k}_{\lambda \,=\, \langle w | v \rangle}\Big) \otimes w_j \;\stackrel{\text{comm.}}{=}\; \lambda \otimes M(i,j). \]
The last step (moving λ left past v_i) needs a commutative ⊗, so λ is central; the tropical carriers (max-plus / min-plus) are commutative. Over a noncommutative semiring the middle scalar stays put (M²(i,j) = v_i ⊗ λ ⊗ w_j) and does not collapse. So (for commutative ⊗) M^n = λ^{n-1} the transfer power never iterates: the whole memo is the one scalar M andλ. This is rank = 1 of the Fliess / Carlyle–Paz law rank(Hankel) = dim(minimal memo). For a max-plus carrier λ = ⟨w|v⟩ = max_k(w_k + v_k) is the tropical eigenvalue; the choice of semiring is the choice of problem (bool ⟹ reachability, MaxPlus ⟹ critical path).
star, named as such, and components. | using dedekind::linear_algebra::rel_codomain_t |
|
export |
A dense N×N semiring matrix — the extensional adjacency carrier a relation materialises to. Finite N by construction, hence the IsExtensional witness the star's fixpoint needs. This is Mat(S) (MatNxNV, :matnxn), the certified matrix semiring; the alias keeps the transfer-local spelling while ⊕/⊗ and the *-closure come from semiring_ops<Mat(S)>, not hand-rolled here.
The secret sauce that turns the general theorem R* = closure(Δ, λS.S;R) into an executable corollary: the map from an intensional relation (a predicate over a possibly-infinite carrier, whose type grows under ; and ∪) to its extensional adjacency matrix (a fixed, type-stable carrier), on which a fixpoint can run. The extensionality constraint is spelled out in the type: ext demands the finite bound N (the IsExtensional licence), and star only accepts the resulting SquareMatrix. So R* = star(ext<N>(R)) type-checks exactly when the carrier is finite; the infinite case is a type error, not a runtime check — the Rice wall, made structural.
|
constexpr |
The one reduction the transfer surface keeps: a structured ⊕-fold ⊕_{k<N} term(k) over the (low, fixed) rank index, the empty fold being the ⊕-identity. A fold-expression, not an imperative loop — the DSL folds structurally, so the reduction stays intensional until an optimum "means it".
| Add | The ⊕ functor. |
| zero | The ⊕-identity (0-bar), the value of the empty (N=0) fold. |
| term | The intensional summand k ↦ term(k). |
|
constexprexport |
The structure-directed finite geometric sum \(\sum_{k=0}^{N-1} r^k\), in closed form.
The closed-form sibling of inner_product's add_fold: it collapses the geometric sum by doubling in O(log N) rather than walking the N terms, using only the semiring ⊕/ division-free, hence correct over any rig (tropical, ⊗ —bool, ℤ/2^w, and a field alike; no truncating-division or modular-cancellation hazard). Over a field, for a primitive N-th root of unity \(\zeta\) and any exponent m, the ratio \(r=\zeta^m\) gives the DFT / character orthogonality \(\sum_{k\in\mathbb{Z}/N}\zeta^{\,mk} = N\,[\,N \mid m\,]\) — \(N\cdot 1\) when \(N\mid m\) ( \(r=1\)), else exactly \(0\) — decided without touching a single grid point. The doubling realises it: the top factor \(1\oplus\zeta^{N/2}=0\) ONLY in the even-N, coprime-m case ( \(\zeta^{N/2}=-1\) needs N even); for odd N or a non-primitive \(r=\zeta^m\) (smaller order, e.g. \(\zeta_8^2=i\) with \(i^4=1\neq -1\)) the sum still vanishes, the cancellation occurring lower in the recursion. That vanishing is field-specific (it needs the additive inverse \(-1\)): the sum is semiring-generic but need not vanish over a bare rig where merely \(r^N=1\) (e.g. \(r=3\) in ℤ/8, where \(3^2=1\) yet the sum is \(1+3=4\neq 0\)).
Scope: this is the first concrete structured reduction — the finite geometric / cyclic case (N is a finite size_t, r a single ratio). The general intensional \(\Sigma_d\) over an infinite function-space domain (the L² inner product) adds a domain / reduction abstraction on top of this and is the tracked follow-up; geometric_sum itself does not yet represent it.
|
constexprexport |
The bra·ket inner product ⟨w|v⟩ = ⊕_{k<N} w(k) ⊗ v(k) over a semiring. Bra w and ket v are IsArrow factors (index → scalar); N is the shared dimension.
For a tropical carrier this is max_k(w_k + v_k) — the max-plus eigenvalue that governs the rank-1 transfer power. The ⊕-fold over the (low) rank dimension is the matrix-contraction kernel, evaluated as a bounded compile-time reduction.
geometric_sum below, the finite geometric / cyclic closed form (from which the DFT — Discrete Fourier Transform — / character orthogonality falls out with no walk of the index). A truly intensional \(\Sigma_d\) over an infinite domain is the tracked follow-up; both share this reduction role, differing in strategy.
|
constexprexport |
The semiring matrix-product entry (A⊗(i,j) B)= ⊕_{k<N} A(i,k) ⊗ B(k,j).A and B are any (i,j)→ maps (e.g. an OuterProduct); S entryN is the contracted (middle) dimension.
This is the ⊕/⊗ kernel the ring-wired :mat2x2 lacked. It is rank-agnostic; the inner_product above is its 1×1 face.
|
constexprexport |
Add two arrows pointwise — the \(f \boxplus g\) semimodule addition. Both factors must share Domain and Codomain.
|
constexprexport |
Reflect an arrow through its domain origin — the parity U.
|
constexprexport |
Scale an arrow by a scalar — the \(c \odot f\) semimodule action.
|
constexprexport |
The Kleene star A* = ⨆ₙ Aⁿ = Δ ⊕ A ⊕ A² ⊕ … — R* as a running corollary of the generic closure, iterating M ↦ Δ ⊕ M⊗A to its fixpoint on the extensional matrix. Over Bool it is reachability; over MaxPlus the longest path (the algebraic path problem). Discharges FIXME(#786) for R* as a matrix corollary; the SquareMatrix argument is the extensionality the intensional relation lacked.
⊕/⊗ and Δ are not hand-rolled: they are Mat(S)'s own semiring operations (semiring_ops<Mat(S)> = MatPlus / MatTimes) and unit (identity_matrix), so star is literally the *-closure of the certified matrix semiring — the same generic closure that computes any semiring's star, instantiated at Mat(S).