function.cppm File Reference

Concept anchoring for function spaces — #537 slice 1. More...

#include <concepts>
#include <cstddef>
import dedekind.sets;
import dedekind.sequences;

Include dependency graph for function.cppm:

Concepts
concept	dedekind::geometry::IsFunctionSpace
	W is a function space T^D — eval f(d), pointwise +, and scalar · over T.

Detailed Description

Concept anchoring for function spaces — #537 slice 1.

@partition :function

Copyright

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

function__Motivation

A function f: D → T over an infinite domain D (typically ℕ or ℝ) is morally an infinite-dimensional vector — its components are the values f(d) indexed by d ∈ D. The codebase already has rule-based intensional carriers that play this role at the algebraic / sequence layer:

• dedekind::sequences::Path<T, Cardinality> — domain std::size_t (≅ ℕ when Cardinality = ℵ_0), codomain T.
• dedekind::linear_algebra::Diagonal<D, F>'s rule type F (#534) — itself an IsArrow with a scalar codomain, hence a function-space inhabitant.
• dedekind::linear_algebra::OuterProduct<U, V>'s factor types U and V (#534) — same reading.

This partition adds the concept-side anchoring:

• IsFunctionSpace<W, D, T> — concept witnessing that W carries the structural commitments of a function space: eval f(d), pointwise +, scalar · (vector-space operations under T as the scalar field).
• Path<T, ℵ_0> registered as IsFunctionSpace<Path<T>, std::size_t, T> via the pointwise operators added in sequences:path under this issue.

function__Pairing_With_Inner_And_Outer_Product

Function spaces are the natural inhabitant of L²-flavoured inner / outer products at infinite dimension. :inner_product already carries HasInnerProduct<V, F> / IsInnerProductSpace for finite-dim Vector<F, N>; the obvious follow-up is an L²(ℕ) / L²(D) carrier whose inner product is a series ⟨f, g⟩ = Σ_{d∈D} f(d) · g(d) (subject to summability). The summability question is deferred to a measure- theoretic follow-up; this partition only scopes the vector-space surface (eval, +, scalar ·) without committing to a measure.

function__Why_Geometry

Three plausible homes were weighed in #537: geometry:function (chosen here, named symmetrically with :inner_product and :outer_product), linear_algebra:function (pairs with the :diagonal carrier), and analysis:function (pairs with future measure / convergence content). The geometric home wins on partition naming consistency and on the natural pairing with the existing inner / outer-product anchorings.

Wikipedia: Function space, Sequence space, L^p space

Note

"Le but général de l'analyse, c'est de soumettre tous les phénomènes au calcul, et de réduire ainsi à des problèmes d'algèbre les questions les plus difficiles de la mécanique et de l'astronomie." [Trans: "The general aim of analysis is to subject all phenomena to calculation, and so reduce the most difficult questions of mechanics and astronomy to problems of algebra."] — Joseph Fourier, Théorie analytique de la chaleur (1822), Discours préliminaire. The function- space anchoring here lifts that Fourier-style "function as infinite vector" reading into the type system.