Dedekind 0.0.0
A structuralist C++23 Module Library
Loading...
Searching...
No Matches
samples.cppm File Reference

Named §3 page-2 sample sequences: is_even and fibonacci. More...

#include <cstddef>
#include <functional>
#include <utility>
import dedekind.sequences:path;
import dedekind.sets;
import dedekind.order;
import dedekind.category;
Include dependency graph for samples.cppm:

Typedefs

using dedekind::sequences::ℕ_Form = dedekind::sets::ExtensionalCardinal<>

Variables

const auto dedekind::sequences::is_even
 is_even : ℕ → 𝔹 — the parity sequence as a Path<Truth<Boole>> .
template<dedekind::sets::IsRingIntegral T>
const auto dedekind::sequences::fibonacci_of = iterate(std::plus<T>{}, T(0u), T(1u))
 fibonacci_of<T> : ℕ → T — the canonical Fibonacci sequence 0, 1, 1, 2, 3, 5, 8, 13, ... in any IsRingIntegral carrier T .
const auto & dedekind::sequences::fibonacci = fibonacci_of<ℕ_Form>
 fibonacci — named default at T = ℕ_Form (ExtensionalCardinal<> ) for paper citation.

Detailed Description

Named §3 page-2 sample sequences: is_even and fibonacci.

@partition :samples

samples__Purpose

Paper §3 page-2 (the Sequences half of "Sets and Sequences") leans on two named, non-trivial Path<T> sequences whose graphs can be lifted via as_relation and joined relationally — the page-2 anchor for the θ-join via σ ∘ × beat. Naming them in code (rather than inlining anonymous closures at the call sites) lets the paper prose cite them by their exported names, and lets downstream exhibits (the §3 page-2 listing, the §3 reshape PR) compose against a stable surface.

The_Sample_Pair

  • is_even : Path<Truth<Boole>> — gives the join row a heterogeneous codomain (ℕ × 𝔹 × ℕ ), exhibiting tuples-not-lists.
  • fibonacci_of<T> : Path<T> — the canonical recurrence, expressed via the n-ary iterate(op, seeds...) primitive in :sequences:path . Fibonacci is the iterate(std::plus<T>{}, T(0u), T(1u)) instance — one named primitive, one binary operator, two seeds, no fanout / projection / explicit-product-type ceremony. Parameterised on the same algebraic gate IsSequence imposes on its Domain (:sets:cardinality:IsRingIntegral , the gate used by #755 ): any ring-integral carrier T whose seed T(0u) and T(1u) are well-formed. The named default fibonacci = fibonacci_of <ℕ_Form> (ExtensionalCardinal<> at the carrier role) is what the paper listing cites; alternative IsRingIntegral carriers (std::size_t , unsigned, ExtensionalCardinal<W>, …) instantiate the same recurrence at no extra cost. The variant Cardinality / SignedCardinality Forms require the finite_cardinality(0) factory rather than brace-init and are a Sollbruchstelle for a future arrow-based zero/one oracle (post #602's set-level embeddings).

    The structural pattern "binary @em op @em applied @em recursively" is captured by the n-ary iterate primitive directly; Tribonacci is iterate(λ(a,b,c). a+b+c, ...) , GCD-via-Euclid is iterate(modulus, ...) , etc. iterate is the unique NNO morphism ℕ → carrier making Lawvere's NNO recursion diagram commute (Mac Lane CWM §V.5), generalised to n -dimensional state.

@build_order 5 @dependency dedekind.category, dedekind.order, dedekind.sequences:path

Note
"Examples are the schoolmaster of fools." — Edmund Burke, Reflections on the Revolution in France (1790), turning the saw on its head: well-chosen examples are the schoolmaster of the wise, too.

Variable Documentation

◆ fibonacci

const auto& dedekind::sequences::fibonacci = fibonacci_of<ℕ_Form>
inlineexport

fibonacci — named default at T = ℕ_Form (ExtensionalCardinal<> ) for paper citation.

The §3 page-2 listing cites this name directly: fibonacci is the Form-shaped canonical instantiation at the carrier role (T = ExtensionalCardinal<> ); the same recurrence lifts to any other IsRingIntegral carrier via fibonacci_of<T> . The returned Path 's Index defaults to std::size_t because the n-ary iterate primitive doesn't yet propagate the Index Form (see the FIXME in :sequences:path around the n-ary iterate body). is_even above carries ExtensionalCardinal<> at the Path's Index role directly, since it constructs its Path explicitly.

◆ fibonacci_of

const auto dedekind::sequences::fibonacci_of = iterate(std::plus<T>{}, T(0u), T(1u))
inlineexport

fibonacci_of<T> : ℕ → T — the canonical Fibonacci sequence 0, 1, 1, 2, 3, 5, 8, 13, ... in any IsRingIntegral carrier T .

Expressed via the n-ary iterate primitive (in :sequences:path ): Fibonacci is the (op = +, seeds = (0, 1)) instance of the "binary op applied recursively" pattern. The carrier T is parameterised on the same algebraic gate IsSequence imposes on its Domain (IsRingIntegral at :sets:cardinality ); the requires-clause narrows to those carriers where the unsigned-literal brace-init T(0u), T(1u) is well-formed.

Template Parameters
TAny IsRingIntegral inhabitant constructible from the unsigned literals 0u and 1u — i.e. std::integral types and the ExtensionalCardinal<W> / SignedExtensionalCardinal ring-integral carriers. The variant Cardinality / SignedCardinality Forms are excluded by the brace-init requirement; they need finite_cardinality factories rather than T(0u) (a Sollbruchstelle named in the partition docstring above).

◆ is_even

const auto dedekind::sequences::is_even
inlineexport
Initial value:
=
Path<Truth<Boole>, ℵ_0, ℕ_Form>{[](ℕ_Form n) -> Truth<Boole> {
return Truth<Boole>{n % ℕ_Form{2u} == ℕ_Form{0u}};
}}
ℵ< 0 > ℵ_0
Countable Infinity.
Definition cardinality.cppm:118
The Monic Wrapper for a Logical Species (Ω).
Definition logic.cppm:911
A sequence F: ℕ → T.
Definition path.cppm:82

is_even : ℕ → 𝔹 — the parity sequence as a Path<Truth<Boole>> .

Boolean codomain by design: the §3 page-2 join exhibit relationally joins is_even and fibonacci on the shared index column, producing rows of type (ℕ, 𝔹, ℕ) — a heterogeneous triple, not a list of one type. The join's tuples-not-lists character is the page-2 beat the paper prose lands on.

The same property as an arrow on the counts, with its period declared, is dedekind::category::is_even (:periodic), the residue class congruent(2, 0). This sequence reads it on ℕ_Form as a path; it cannot simply call that arrow yet, since ℕ_Form saturates at ℵ_0 and the word does not, so the cast is not total (#1035).