Inductive sets: χ, the classifier under definition, inside its own comprehension; the former closes the recursion and admits only a descent. More...
#include <concepts>#include <cstddef>#include <functional>#include <optional>#include <stdexcept>#include <tuple>#include <type_traits>#include <utility>import dedekind.sets:singleton;import dedekind.category;
Classes | |
| struct | dedekind::sets::descent< T > |
A descent: \(\pi_i - c\), a slot stepped down by a constant, and the slot it steps on. c > 0 is checked when the χ node is built. That the descent ends is Archimedes' axiom, that enough steps of c exceed any magnitude [1]. More... | |
| struct | dedekind::sets::descent< BinOp< std::minus<>, Projection< I >, Const< K > > > |
| struct | dedekind::sets::Env< T, R > |
The point and the set under definition, threaded through a body: the term nodes read it as the point (conversion, and term_value below), Self reads it as the set. More... | |
| struct | dedekind::sets::Self< Terms > |
The set under definition pulled back along the terms: χ(t₁, …) is \(x \mapsto \chi(t_1(x), \ldots)\) with \(\chi\) the comprehension's own classifier, unknown until the former closes it. A relational predicate (an operand of && / ||), evaluable only through an Env. More... | |
| struct | dedekind::sets::ChiTag |
The classifier under definition: χ(terms…) in a former's body is the set being formed, applied to the terms. More... | |
| struct | dedekind::sets::DescendsAt< X, J > |
The measure algebra at the points X for position J: a χ node passes when its argument in position J descends on the coordinate J stands for; every node when all its legs pass; any other leaf vacuously. More... | |
| struct | dedekind::sets::BindArgs< X > |
The binding of the arguments of every χ in a body at the points X: each a term bound there, a constant cast into its coordinate's carrier. The body's own binding treats a χ as a leaf, so its arguments are bound here. More... | |
| struct | dedekind::sets::Rec< S, Body > |
The recursion, closed: the base's membership, then the body evaluated with this very predicate in scope for its Self nodes. More... | |
Namespaces | |
| namespace | dedekind::sets |
| namespace | dedekind::sets::detail_recursion_witness |
Concepts | |
| concept | dedekind::sets::WellFounded |
| A carrier a descent terminates on: the unsigned words, ℕ's shadows, with 0 at the bottom. (Cardinality joins once its monus is a term.). | |
| concept | dedekind::sets::HasTermValueAt |
A term with a value at the points X: term_value(t, x) is formed. | |
| concept | dedekind::sets::BindsAt |
A term that binds at the points X: bind_check<X>(t) is formed. | |
| concept | dedekind::sets::detail_recursion_witness::FormsNonDescendingRecursion |
| concept | dedekind::sets::detail_recursion_witness::FormsDescendingRecursion |
| concept | dedekind::sets::detail_recursion_witness::FormsSamePointRecursion |
| concept | dedekind::sets::detail_recursion_witness::FormsCyclingRecursion |
| concept | dedekind::sets::detail_recursion_witness::FormsMeasuredRecursion |
Typedefs | |
| using | dedekind::sets::detail_recursion_witness::N = std::size_t |
| using | dedekind::sets::detail_recursion_witness::NN = std::pair<N, N> |
| using | dedekind::sets::detail_recursion_witness::FiniteN = 𝔸<unsigned, dedekind::category::Boole, Finite> |
Functions | |
| template<IsRingIntegral auto I, typename K> requires std::copyable<K> | |
| constexpr Projection< I > | dedekind::sets::descent_slot (const BinOp< std::minus<>, Projection< I >, Const< K > > &t) |
The legs of a descent \(\pi_i - c\): the slot it steps on and the step c. Read through these on the descent's own shape, so a body generic in the term names no member of it (Rule 2). | |
|
template<IsRingIntegral auto I, typename K> requires std::copyable<K> | |
| constexpr K | dedekind::sets::descent_step (const BinOp< std::minus<>, Projection< I >, Const< K > > &t) |
| template<typename T, typename X> requires HasTermValueAt<T, X> | |
| constexpr std::optional< value_at_t< X, T > > | dedekind::sets::self_arg (const T &t, const X &x) |
A χ argument's value at a point: the term's value, or nullopt for a descent below the carrier's bottom (no point of the universe, so the pulled-back membership is false there). | |
| template<IsRingIntegral auto I, typename T, typename R> | |
| constexpr decltype(auto) | dedekind::sets::term_value (Projection< I > p, const Env< T, R > &e) |
A projection read at an Env is read at its point. | |
| template<typename T, typename... Vs> | |
| constexpr T | dedekind::sets::point_of (const Vs &... vs) |
A point of T from the terms' values: the scalar, or the pair. | |
| template<typename Term, typename X, std::size_t S> | |
| consteval bool | dedekind::sets::descends_on () |
Whether Term is a descent on slot S at points of X: the shape descent names, on that slot, whose carrier is well-founded. | |
| template<typename Node, typename X, std::size_t... Js> | |
| consteval bool | dedekind::sets::some_measure (std::index_sequence< Js... >) |
| template<typename K> requires std::copyable<K> | |
| constexpr K | dedekind::sets::constant_value (const Const< K > &c) |
| The value of a constant term, read on its own shape. | |
| template<IsSetObject S, typename Body> requires contains_self_v<Body> && self_descends_v<Body, typename S::Domain> && std::same_as< std::invoke_result_t<const S&, const typename S::Domain&>, bool> | |
| constexpr auto | dedekind::sets::operator& (const S &base, Body body) |
The former that closes a recursion: S & body with a χ in the body is \(\{x \in S \mid body(x)\}\) where χ is that set. Viable only for a structural recursion over a decidable base; general recursion finds no former. | |
Variables | |
| template<typename T> | |
| constexpr bool | dedekind::sets::is_descent_v = descent<T>::value |
| constexpr ChiTag | dedekind::sets::χ {} |
| template<typename... Ts> | |
| constexpr bool | dedekind::sets::is_self_v< Self< Ts... > > = true |
| template<typename X, std::size_t J> | |
| constexpr std::size_t | dedekind::sets::slot_at |
The coordinate a position of χ's arguments stands for at points of X: the point itself (slot 0) for a scalar, slot J + 1 of a pair. | |
| template<typename X> | |
| constexpr std::size_t | dedekind::sets::arity_v |
The number of coordinates of a point of X. | |
| template<typename Term, typename X, std::size_t S> | |
| constexpr bool | dedekind::sets::descends_on_v = descends_on<Term, X, S>() |
| template<typename Node, typename T> | |
| constexpr bool | dedekind::sets::self_descends_v |
The structural-recursion gate: one coordinate on which every Self in the body descends. Vacuous without a Self. | |
| constexpr auto | dedekind::sets::detail_recursion_witness::multiples_of_3 = 𝔸<N>{} & ((π == N{0}) || χ(π - N{3})) |
| constexpr auto | dedekind::sets::detail_recursion_witness::naturals = 𝔸<N>{} & ((π == N{0}) || χ(π - N{1})) |
| constexpr auto | dedekind::sets::detail_recursion_witness::y_zero_or_x_positive |
| constexpr auto | dedekind::sets::detail_recursion_witness::finite_evens = FiniteN{} & ((π == 0u) || χ(π - 2u)) |
Detailed Description
Inductive sets: χ, the classifier under definition, inside its own comprehension; the former closes the recursion and admits only a descent.
@partition :recursion
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
recursion__Overview
An inductive definition names the set it defines: the multiples of three are \(\{n \mid n = 0 \vee \chi(n - 3)\}\) with \(\chi\) the characteristic arrow of that very set. Here χ is a tag whose application to terms builds a Self node, a relational predicate standing for the set under definition pulled back along the terms. The former S & body, seeing a Self in body, closes the recursion into Rec: a predicate that evaluates the body on an Env the term nodes read as the point (a projection at an Env is read at its point) and Self reads as the set.
The recursion is admitted only when it is structural, with one measure for the whole body: a coordinate i such that every Self has \(\pi_i - c\), \(c > 0\), in position i, on a well-founded carrier. That coordinate then strictly decreases on every call, so an unfolding takes at most its value in steps (primitive recursion on the coordinate; the parametrised NNO). A subtraction somewhere is not enough: χ(π_2 − 1, π_2) calls itself on the same point, and χ(π_1 − 1, π_2 + 1) || χ(π_1 + 1, π_2 − 1) cycles. A body without such a measure is general recursion, and no former is viable for it: the Rice boundary, refused where it would be written. The former binds the body and every argument of every χ when the set is built, as the ordinary formers do, and admits only a decidable base (a bool-valued χ). A descent below the carrier's bottom is no point of the universe and the pulled-back membership is false there, so a base case needs no guard against it.
Wikipedia: Recursive definition, Primitive recursive function, Least fixed point, Datalog
- Note
- Richard Dedekind, Was sind und was sollen die Zahlen? (1888), §126, "Satz der Definition durch Induktion": for a map θ of a system Ω into itself and an element ω of Ω there is one and only one map ψ of the number series with ψ(1) = ω and ψ(n') = θψ(n). (Paraphrased.) The descent admitted here is that theorem read backwards along a coordinate.
