terms.cppm File Reference

The term grammar of comprehensions: projections, constants carried as values, arithmetic, arrows applied to terms, conditionals; the comparison atom over two terms; the pointwise connectives of relational predicates. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <cstdint>
#include <functional>
#include <iterator>
#include <limits>
#include <memory>
#include <optional>
#include <ranges>
#include <stdexcept>
#include <string>
#include <tuple>
#include <type_traits>
#include <utility>
#include <variant>
#include <vector>
import dedekind.sets:cardinality;
import dedekind.category;

Include dependency graph for terms.cppm:

Classes
struct	dedekind::sets::RelAnd< A, B >
	Meet (conjunction) of two relational predicates, the result of && on them. More...
struct	dedekind::sets::RelOr< A, B >
	Join (disjunction) of two relational predicates, the result of || on them, dual to RelAnd. More...
struct	dedekind::sets::Const< K >
	A constant, carried as a value. More...
struct	dedekind::sets::BinOp< Op, A, B >
	a op b, the operator a standard functor (std::plus<>, minus, multiplies, divides, modulus) applied in one carrier. More...
struct	dedekind::sets::Ap< F, A >
	An arrow applied to a term, f(a). More...
struct	dedekind::sets::CondT< P, A, B >
	McCarthy's conditional on terms: a where p holds, else b. More...
struct	dedekind::sets::Slots
	The slot algebra: the slots a term or a relational predicate mentions, as a bit mask (bit i for π_i, bit 0 for the unary π). A node mentions the union of its legs' slots; a predicate the grammar does not know mentions every slot, so no certificate reads more into it than it says. More...
struct	dedekind::sets::On< C >
	The carrier a rule is stated for, as a tag. A rule admits(On<C>, key, divisor_is_constant) says that the operator key is in the signature of C: a symbol one of the carrier's certified varieties has. It is declared in this namespace beside the certificate and found by ADL, so it is in force where that module is imported: the comparisons beside the partial orders (order:poset), // and % beside IsDividableChain (order:completeness), a field's / beside IsField (algebra:field); + - * and == != here, whose certificates are category's. Without a rule an operator is not in the signature. More...
struct	dedekind::sets::FieldDivision
	The two divisions Python tells apart, as keys: a field's, and the Euclidean one of an ordered carrier with remainder. The typed grammar's std::divides<> is the carrier's own, admitted where either is. More...
struct	dedekind::sets::EuclideanDivision
struct	dedekind::sets::rel_key< Rel::Lt >
struct	dedekind::sets::rel_key< Rel::Le >
struct	dedekind::sets::rel_key< Rel::Gt >
struct	dedekind::sets::rel_key< Rel::Ge >
struct	dedekind::sets::rel_key< Rel::Eq >
struct	dedekind::sets::rel_key< Rel::Ne >
struct	dedekind::sets::not_admitted
	Refused at the carrier: an operator not total there, a division by a term, an order comparison on an unordered carrier, a slot the points have not. Raised when a term built at run time is bound. More...
struct	dedekind::sets::point_sorts< P >
	The sorts of a point type: the carriers of its coordinates, each once. A carrier value has one sort; a pair of two carriers two (one where they agree). A term built at run time names no carrier until it is bound, and every node then has a sort: a projection its slot's, a constant its context's, an operator its operands' common one, a comparison 𝔹. More...
struct	dedekind::sets::point_sorts< std::pair< A, B > >
struct	dedekind::sets::Row< Cs >
	A row: a point of an n-ary product whose arity and columns' sorts are data. Each cell is a value of one of the carriers Cs, and the cell's alternative is its column's sort, so a row is its own schema. Slots are π_1 … π_n. More...
struct	dedekind::sets::point_sorts< Row< Cs... > >
struct	dedekind::sets::with_carrier< std::tuple< Cs... >, C >
struct	dedekind::sets::value_sum< std::tuple< A > >
struct	dedekind::sets::value_sum< std::tuple< A, B, Cs... > >
struct	dedekind::sets::ReadAs< C >
	The coordinate slot of the point p, read in the sort C the dispatch chose; the point itself for the unary π. More...
struct	dedekind::sets::EmbedsAt< P >
	Whether the sort b embeds into the sort a, at points of P. More...
struct	dedekind::sets::EmbedsAt< P >::From< A >
struct	dedekind::sets::ConstantAs< P, C, K >
	A constant read in the sort C: a numeral cast into it, a constant of a sort (a bool, a Ternary) read in its own and embedded. More...
struct	dedekind::sets::Value< P >
	The value algebra: a term or a predicate folded at the point p. A projection reads its coordinate, a constant is its value, a predicate the grammar does not know is evaluated as itself; an operator or a comparison combines its operands in the carrier of the non-constant one; an applied arrow converts its argument into its domain. More...
struct	dedekind::sets::Verdict< P, K >
struct	dedekind::sets::Verdict< P, K >::FiniteSort
	Whether a sort is a finite chain, enumerated exactly. More...
struct	dedekind::sets::Verdict< P, K >::Search
struct	dedekind::sets::Cmp< R, A, B >
	The atom a R b over two terms, a relational predicate. More...
struct	dedekind::sets::Bound
	The result of a binding: nothing but the checks that ran. More...
struct	dedekind::sets::Bind< X >
	The binding algebra at the points X: a constant beside a term (a, b of an operator, a comparison or a conditional) meets the term's carrier now; a constant under an arrow meets the arrow's domain. A leaf binds trivially. More...
struct	dedekind::sets::Term< K >
	A term built at run time, the grammar with its shape a value; defined after the binding below. More...
struct	dedekind::sets::Term< K >::SubstOne
	The one-slot substitution as a slot map. More...
struct	dedekind::sets::Pred< K >
	A relational predicate built at run time: comparisons of terms and their connectives; defined after the binding below. More...
struct	dedekind::sets::PinConstant< K, Lift >
	A numeral read in the sort C and written back as a constant of that sort, through lift; a carrier lift has no constant for keeps the numeral. More...
struct	dedekind::sets::Definition< K >
	A slot's definition: the term t of a conjunct π_slot == t (or t == π_slot) with t free of the slot, and the conjunction without it. ∃π_slot. P is then the rest with t for π_slot: the existential is eliminated by substitution. Dually, under ∀ a disjunct π_slot != t defines it: ∀g. (g ≠ t ∨ Q) ≡ Q[t/g]. More...
struct	dedekind::sets::NoConstants
	No carrier value as a constant: the lift that names nothing, so eliminate_quantifiers eliminates by definition alone and leaves every quantifier over a chain to the search. More...
struct	dedekind::sets::ChainValues< K, Lift >
	The values of a finite chain as constants, through lift: the cases of Shannon's expansion; none for any other carrier. More...
struct	dedekind::sets::ShiftDown< K >
	The slots above an eliminated bound slot, moved down by one. More...
struct	dedekind::sets::CondSplit< K >
	A term with its first conditional taken out: the condition, and the term with the conditional replaced by each branch. More...
struct	dedekind::sets::Total< X >
	The totality algebra at the points X: a node is total when its legs are, and an operator when it is admitted on its carrier (admits, the gate the value algebra enforces: total there, or dividing by a nonzero constant), an applied arrow when the arrow is total and its argument already has the arrow's domain (a conversion may fail). A predicate the grammar does not know is not certified. More...
struct	dedekind::sets::graph_atom< P >
	π_2 == t, or t == π_2, with t mentioning only the first slot: the graph of the function x ↦ t(x). term is t. More...
struct	dedekind::sets::graph_atom< Cmp< Rel::Eq, T, Projection< 2 > > >
struct	dedekind::sets::graph_atom< Cmp< Rel::Eq, Projection< 2 >, T > >
struct	dedekind::sets::MentionsSelf
	The self algebra: a term or predicate mentions the set under definition when one of its leaves is a χ node; every node passes it up. More...
struct	dedekind::sets::detail_terms_witness::Foreign
struct	dedekind::sets::Projection< K >
	The projection π_k: the k-th component of a product. More...

Namespaces
namespace	dedekind::sets
namespace	dedekind::category

Concepts
concept	dedekind::sets::IsRelPredicate
	A relational predicate: a predicate on the points of a product (or of a carrier, for an atom on π), tagged is_rel_predicate; it meets its universe only at the former &.
concept	dedekind::sets::IsTerm
	A term of the grammar.
concept	dedekind::sets::IsConstant
	A value that can stand as a constant beside a term: copyable, with state, and not itself part of the grammar (a term, a predicate, an arrow, or an empty tag). The term test comes first, so asking this of a carrier never asks for the carrier's own equality.
concept	dedekind::sets::TermOperands
	The operands of an operator of the grammar: at least one term, the other a term or a constant.
concept	dedekind::sets::EmbedsInto
	A value of the sort D is read in the sort C: the same sort, or a truth chain along the dominance into C's species (𝔹 ↪ K₃, the registered lift_logic). The one coercion of the grammar; any other pair of carriers meets through an arrow applied, never implied.
concept	dedekind::sets::IsGraphAtom
	An atom that is the graph of a function of the first slot.

Typedefs
template<typename A, typename B, typename RA, typename RB>
using	dedekind::sets::meet_t = typename decltype(meet_type<A, B, RA, RB>())::type
template<Rel R>
using	dedekind::sets::rel_key_t = typename rel_key<R>::type
template<typename P>
using	dedekind::sets::point_sorts_t = typename point_sorts<P>::type
template<typename P>
using	dedekind::sets::term_sorts_t
	The sorts a term at points of P takes: the points' carriers first (a slot's sort is its index there), then the truth chains a set applied to a term lands in, ap(S, t) of sort S's codomain.
template<typename P>
using	dedekind::sets::rt_value_t = typename value_sum<point_sorts_t<P>>::type
template<typename X, typename T>
using	dedekind::sets::value_at_t
	The value type a term takes at a point of type X.
template<IsGraphAtom P>
using	dedekind::sets::graph_term_t = typename graph_atom<P>::term
	The term of a graph atom.
using	dedekind::sets::detail_terms_witness::P = std::pair<unsigned, unsigned>
using	dedekind::sets::detail_terms_witness::N2 = std::pair<Cardinality, Cardinality>

Enumerations
enum class	dedekind::sets::Rel {   Lt , Le , Gt , Ge ,   Eq , Ne }
	The comparison an atom makes.
enum class	dedekind::sets::Arith {   Add , Sub , Mul , Div ,   FloorDiv , Mod }
	An operator of a term built at run time. Python's / and // are both the carrier's division; what differs is where each is admitted (a field, an ordered word).

Functions
template<Rel R, typename X, typename Y>
constexpr bool	dedekind::sets::rel_apply (const X &x, const Y &y)
	x R y.
constexpr Rel	dedekind::sets::negate (Rel r)
	The De Morgan dual of a comparison: !(x R y) is x negate(R) y.
template<typename X>
constexpr auto	dedekind::sets::term_of (X x)
	A term as itself, a constant as Const.
template<typename Op, typename A, typename B>
constexpr auto	dedekind::sets::make_binop (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator+ (A a, B b)
	The arithmetic of terms.
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator- (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator* (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator/ (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator% (A a, B b)
template<typename F, typename A> requires IsArrow<std::remove_cvref_t<F>> && IsTerm<A>
constexpr Ap< std::remove_cvref_t< F >, A >	dedekind::sets::ap (F f, A a)
	ap(f, a): the arrow f applied to the term a.
template<typename P, typename A, typename B> requires IsRelPredicate<P> && TermOperands<A, B>
constexpr auto	dedekind::sets::cond (P p, A a, B b)
	cond(p, a, b): a where p holds, else b.
constexpr bool	dedekind::sets::only_slot (unsigned mask, unsigned slot)
	Whether a mask names at most the given slot.
template<std::integral T, std::floating_point F>
constexpr bool	dedekind::sets::in_integer_range (F x)
template<typename C, typename K>
constexpr C	dedekind::sets::carrier_cast (const K &k)
	A constant converted into the carrier C it meets: exactly, or not at all. Between built-in types: in range, then a round trip that keeps the sign. A carrier with its own rule states it beside its definition as carrier_cast(std::type_identity<C>, k), found by ADL (ℕ refuses a negative constant); any other class carrier converts by its constructor.
template<IsRingIntegral auto I, typename P>
constexpr decltype(auto)	dedekind::sets::term_value (Projection< I >, const P &p)
	A projection read at a point: its coordinate, or the point itself for the unary π. An overload for another kind of point (an environment) is found by ADL.
template<typename A, typename B, typename RA, typename RB>
constexpr auto	dedekind::sets::meet_type ()
	The carrier two operands meet in: a constant takes the other's, two terms their common type.
template<typename V, typename T, typename R>
constexpr V	dedekind::sets::into (const R &x)
	The value x of the operand T placed in the carrier V: a constant exactly or not at all (carrier_cast), a term's value by conversion.
template<typename Op, typename C> requires requires { typename Op::is_transparent; }
constexpr auto	dedekind::sets::apply_at (const C &a, const C &b)
	The transparent operator Op applied at the carrier C, as the typed std::plus<C> would apply it: an arithmetic result is converted back to C, so a narrow carrier wraps instead of promoting, and a comparison keeps its bool. No type constructor is taken as an argument.
template<typename C, typename Key>
constexpr bool	dedekind::sets::admits (On< C >, Key, bool)
	No rule: not admitted.
template<typename C> requires IsCommutativeMonoid<C, std::plus<C>>
constexpr bool	dedekind::sets::admits (On< C >, std::plus<>, bool)
	+ - * where the carrier's certified laws have the symbol: + on a commutative monoid, - on an abelian group (a - b is a + (-b)), * on a monoid. A magma is total and closed, so the Pst total operator surface is inside the laws; ℕ's monus is not, until its variety is named.
template<typename C> requires IsAbelianGroup<C, std::plus<C>> && IsClosedUnder<C, std::minus<>>
constexpr bool	dedekind::sets::admits (On< C >, std::minus<>, bool)
template<typename C> requires IsMonoid<C, std::multiplies<C>>
constexpr bool	dedekind::sets::admits (On< C >, std::multiplies<>, bool)
template<typename C>
constexpr bool	dedekind::sets::admits (On< C > c, std::divides<>, bool divisor_is_constant)
	The carrier's own division, by a nonzero constant: a field's or the Euclidean one, whichever rule the carrier has.
template<std::equality_comparable C>
constexpr bool	dedekind::sets::admits (On< C >, std::equal_to<>, bool)
	== and != where the carrier compares.
template<std::equality_comparable C>
constexpr bool	dedekind::sets::admits (On< C >, std::not_equal_to<>, bool)
constexpr const char *	dedekind::sets::spelling (Arith op)
	The spelling of an operator, for a refusal.
template<typename P>
constexpr std::size_t	dedekind::sets::slot_sort (unsigned slot, const P &rep=P{})
	The sort of the slot slot at points of P, an index into point_sorts_t.
template<typename P>
constexpr std::size_t	dedekind::sets::one_sort (const P &rep=P{})
	The points' one sort, where every slot has the same; no_sort on a product of several.
template<typename P>
constexpr std::size_t	dedekind::sets::default_sort (std::size_t s, const P &rep=P{})
	The sort of a tree of constants without a context: the points' one sort where they have one.
template<typename P, std::size_t I = 0, typename F>
constexpr auto	dedekind::sets::with_sort (std::size_t s, const F &f)
	Apply f to the sort s of P as a type: f(type_identity<C>). s is a valid index (the caller joined the sorts).
template<typename C, typename D> requires EmbedsInto<D, C>
constexpr C	dedekind::sets::embed_into (const D &d)
	d read in the sort C.
template<typename C, typename D>
constexpr C	dedekind::sets::read_as (const D &d)
	d read in the sort C where it embeds, refused elsewhere.
template<typename C, typename P>
constexpr C	dedekind::sets::coordinate_as (unsigned slot, const P &p)
template<typename C>
constexpr bool	dedekind::sets::op_admitted (Arith op, bool divisor_is_constant)
	Whether op is admitted on the carrier C, with the divisor a constant (nonzero, checked when the term was built) or a term: the rules above and beside their certificates, read at run time.
template<typename C>
constexpr bool	dedekind::sets::rel_admitted (Rel r)
	Whether the comparison r is admitted on C: == and != where it compares, the order comparisons where the order's rule is in force (order:poset).
template<typename C>
constexpr C	dedekind::sets::apply_op (Arith op, const C &x, const C &y)
	x op y in the carrier C, for an admitted operator, through the typed functor; a branch whose expression the carrier has not is not instantiated (the typed functor's body would be, so the guard asks the expression).
template<typename C>
constexpr bool	dedekind::sets::compare_rel (Rel r, const C &x, const C &y)
	x r y for a comparison known at run time, admitted when the term was bound; the branches a carrier has not are not instantiated.
template<typename P, std::size_t I = 0, typename K>
constexpr std::size_t	dedekind::sets::constant_sort (const K &k)
	The sort a constant names by itself, at points of P: the first sort C with constant_of(type_identity<C>, k) (found by ADL) true, for a constant written as a value of C (a bool, a Ternary) rather than a numeral; no_sort otherwise, a numeral taking its context's sort.
template<typename P>
constexpr std::size_t	dedekind::sets::join_sorts (std::size_t a, std::size_t b)
	The common sort of two operands at points of P: a constant takes the other's, and a truth chain meets its dominance in the larger (𝔹 and K₃ in K₃).
template<typename P>
constexpr bool	dedekind::sets::sort_embeds (std::size_t from, std::size_t into)
	Whether a value of the sort from is read in the sort into at points of P (EmbedsInto): the same sort, or along the dominance.
template<std::size_t I, typename... Cs>
constexpr std::variant< Cs... >	dedekind::sets::default_cell (std::size_t sort)
	A cell of the sort sort, its carrier's default value: a row built from a schema is a representative of its points.
template<typename... Cs>
constexpr Row< Cs... >	dedekind::sets::with_bound (const Row< Cs... > &rep, std::size_t sort)
	The row rep extended by a column of the sort sort: the point a quantifier's body is read at. Any other point has no column to bind.
template<typename P>
constexpr P	dedekind::sets::with_bound (const P &, std::size_t)
template<typename C, typename... Cs>
constexpr void	dedekind::sets::set_bound (Row< Cs... > &row, const C &v)
	The last cell of row set to v, of the sort C: the bound column's value under a quantifier.
template<typename C, typename P>
constexpr void	dedekind::sets::set_bound (P &, const C &)
template<typename C>
constexpr C	dedekind::sets::search_value (std::uint64_t i)
	The i-th value of a carrier for a bounded search: a finite chain cycles through its values from ⊥, an unsigned word counts up, and any other carrier states its enumeration as nth_value(type_identity<C>, i), found by ADL beside its definition (Modular: 0, 1, −1, 2, −2, …).
template<typename... Cs>
constexpr Row< Cs... >	dedekind::sets::row_of_sorts (const std::vector< std::size_t > &sorts)
	The row whose columns have the sorts sorts: a representative of the points of that schema, for binding and normal forms.
template<typename P, typename C, typename K>
constexpr C	dedekind::sets::constant_as (const K &k)
template<typename P, typename K>
constexpr std::size_t	dedekind::sets::sort_of (const Term< K > &t, const P &rep=P{})
	The sort of a term built at run time at points of P, from its projections and its constants of a sort (constant_sort): no_sort for a tree of numerals, which takes its context's. Defined with Term.
template<typename P, typename K>
constexpr dedekind::category::Ternary	dedekind::sets::verdict (const Pred< K > &t, const P &point, std::uint64_t budget=std::uint64_t{1}<< 16)
	The verdict of a predicate at a point, in K₃: a comparison or a quantifier over a finite chain is decided (⊤ or ⊥); a quantifier over an infinite carrier searches its first budget values (search_value): a witness of ∃ is ⊤, a counterexample to ∀ is ⊥, and an exhausted budget is U, never the other verdict (Σ, respectively Π: the run-time reading of Semidecided). Same-kind quantifiers over infinite carriers nested below (a middle object of several columns) share the budget, b values each with b^k ≤ budget; an opposite quantifier over an infinite carrier inside answers U. The connectives are Kleene's.
constexpr bool	dedekind::sets::power_within (std::uint64_t b, unsigned k, std::uint64_t n)
	Whether b^k ≤ n, without overflow.
constexpr std::uint64_t	dedekind::sets::root_within (std::uint64_t n, unsigned k)
	The largest b with b^k ≤ n (n ≥ 1): the values each of k nested searches may try within a budget of n, found by bisection, logarithmic in n.
template<typename T, typename P>
constexpr auto	dedekind::sets::term_value (const T &t, const P &p)
	The value of a term or predicate at a point.
template<typename C, typename K, typename P>
constexpr C	dedekind::sets::term_value_as (const Term< K > &t, const P &p)
	A term built at run time read in the sort C its context names (the other side of a graph atom, say), at the point p.
template<Rel R, typename A, typename B>
constexpr auto	dedekind::sets::make_cmp (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator== (A a, B b)
	The comparisons of terms. The term operand is tested first, so a candidate never asks a carrier for its own equality.
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator!= (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator< (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator<= (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator> (A a, B b)
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::sets::operator>= (A a, B b)
template<IsRelPredicate A, IsRelPredicate B>
constexpr RelAnd< A, B >	dedekind::sets::structured_and (A a, B b)
	The meet and join of two relational predicates under the reducer's customization-point names, so the set-level & / | on two relations over one product collapse to one comprehension.
template<IsRelPredicate A, IsRelPredicate B>
constexpr RelOr< A, B >	dedekind::sets::structured_or (A a, B b)
template<Rel R, typename A, typename B>
constexpr Cmp< negate(R), A, B >	dedekind::sets::operator! (const Cmp< R, A, B > &c)
	!atom flips the comparison.
template<typename A, typename B>
constexpr auto	dedekind::sets::operator! (const RelAnd< A, B > &p)
	De Morgan on the connectives: !(p && q) is !p || !q, and dually.
template<typename A, typename B>
constexpr auto	dedekind::sets::operator! (const RelOr< A, B > &p)
template<typename X, typename T>
constexpr void	dedekind::sets::bind_check (const T &t, const X &rep=X{})
	Bind a term or atom to the points X it is evaluated at: every constant meets the carrier of the term beside it now, so a constant the carrier cannot hold raises at construction, not at the first evaluation (a compile error in constexpr code).
template<typename K>
constexpr bool	dedekind::sets::has_quantifier (const Pred< K > &p)
	Whether a predicate has a quantifier anywhere, a conditional's guard in a comparison's operands included.
template<typename K>
constexpr bool	dedekind::sets::has_quantifier (const Term< K > &t)
	Whether a term has a quantifier in a conditional's guard.
template<typename K>
constexpr unsigned	dedekind::sets::slots (const Term< K > &t)
	The slots a term built at run time mentions, as a mask: the run-time twin of slots_v, read with the same only_slot.
template<typename K>
constexpr unsigned	dedekind::sets::slots (const Pred< K > &p)
template<typename P, typename K, typename Lift>
constexpr Pred< K >	dedekind::sets::pin_constants (const Pred< K > &p, const Lift &lift, const P &rep)
	The predicate with every numeral pinned to the sort its context gives it at points of P: the constant then names its sort itself, so the term keeps its meaning when it moves (substituted into another context by ap, or split by lift_conditionals into an atom with no slot left).
template<typename P, typename K, typename Lift>
constexpr Term< K >	dedekind::sets::pin_term (const Term< K > &t, std::size_t s, const Lift &lift, const P &rep)
	The term t, of the sort s at points of P, with every numeral pinned to it.
template<typename K>
constexpr std::optional< Definition< K > >	dedekind::sets::defining_term (const Pred< K > &p, unsigned slot, bool universal=false)
	The first conjunct of p, leftmost, that defines the slot (the first disjunct, for universal); nothing where none does.
template<typename K>
constexpr std::optional< dedekind::sets::Definition< K > >	dedekind::sets::defined_through (const dedekind::sets::Pred< K > &q, unsigned slot, bool universal, unsigned bound)
	A definition of the slot found through a block of quantifiers of the same kind (which commute): the defining atom's term, free of the slots those quantifiers bind, and the block with that atom removed.
template<typename P, typename K, typename Lift>
constexpr dedekind::sets::Pred< K >	dedekind::sets::eliminate_quantifiers (const dedekind::sets::Pred< K > &p, const Lift &lift, const P &rep=P{})
	The predicate with every quantifier eliminated that can be, the atoms left as written: innermost first, by substitution where an atom defines the bound column (a conjunct π_h == t under ∃, a disjunct π_h != t under ∀: the fusion law), else by Shannon's expansion over a finite chain (∨ under ∃, ∧ under ∀). A quantifier over an infinite carrier no atom defines is kept, as is one over a chain whose values lift cannot name (NoConstants: by definition only). Read on the predicate as written (pinned, conditionals not lifted): normalising an atom first would turn the defining shape π_h == t into π_h − t == 0.
constexpr bool	dedekind::sets::only_arguments (unsigned mask, unsigned n)
	Whether a mask names only slots among π_1 … π_{n−1}, the arguments of a graph whose result is π_n.
template<typename K>
constexpr const Term< K > *	dedekind::sets::graph_term (const Pred< K > &p, unsigned n=2)
	The term of a graph atom built at run time, π_n == t or t == π_n with t mentioning only π_1 … π_{n−1}; nullptr for any other predicate. The run-time twin of IsGraphAtom: such a relation is functional by its shape, and entire once bound, since binding admits every operator only where it is total on the carrier (or divides by a nonzero constant).
template<typename K>
constexpr bool	dedekind::sets::same_shape (const Term< K > &x, const Term< K > &y)
	The same tree: the same nodes, slots, operators and comparisons, and equal constants. Syntactic, so sound for equality of what two normal forms denote and silent on two different trees.
template<typename K>
constexpr bool	dedekind::sets::same_shape (const Pred< K > &x, const Pred< K > &y)
	The same predicate tree, atom by atom.
template<typename K>
constexpr std::optional< CondSplit< K > >	dedekind::sets::split_cond (const Term< K > &t)
	The first conditional of t, leftmost, split out; nullopt for a term without one.
template<typename K>
constexpr Pred< K >	dedekind::sets::lift_conditionals (const Pred< K > &p)
	The predicate with every conditional lifted out of its atoms: cond(q, a, b) R c is (q ∧ a R c) ∨ (¬q ∧ b R c), the law of McCarthy's conditional, until no atom has one. The same set at every point; an applied set ap(S, t) == ⊤, the conditional cond(χ_S[π:=t], ⊤, ⊥) compared, becomes χ_S[π:=t] once the decided atoms are folded (algebra:polynomial's canonical).
template<typename K>
constexpr Pred< K >	dedekind::sets::by_cases (const Pred< K > &q, const Pred< K > &x, const Pred< K > &y)
	(q ∧ x) ∨ (¬q ∧ y), each part lifted.
template<IsGraphAtom P>
constexpr graph_term_t< P >	dedekind::sets::graph_term (const P &p)
	The term of a graph atom, the side that is not π_2.
template<IsArrow F, IsArrow G>
constexpr SumArrow< F, G >	dedekind::category::operator+ (const F &f, const G &g)
template<IsArrow F> requires std::unsigned_integral<Cod<F>> && (!std::same_as<Cod<F>, bool>)
constexpr auto	dedekind::category::operator- (const F &f)
constexpr 𝔽64	dedekind::category::operator* (bool s, 𝔽64 v) noexcept
	Scalar action of \(\mathbb{F}_2\) (witnessed on bool) on 𝔽64, via the natural embedding \(\mathbb{F}_2 \hookrightarrow \mathbb{F}_{64}\) ( \(0 \mapsto 0\), \(1 \mapsto 1\)).
constexpr Cardinality	dedekind::category::operator/ (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean division on Cardinality. Convention follows the ExtensionalCardinal<> totalisation: division by zero yields zero; finite / ℵ_0 yields zero (the limit); ℵ_0 / finite-non-zero yields ℵ_0; ℵ_0 / ℵ_0 yields ℵ_0 (saturation rather than indeterminate — Cardinality has no NaZ-equivalent sentinel; the ℕ proxy keeps the policy total).
constexpr Cardinality	dedekind::category::operator% (const Cardinality &lhs, const Cardinality &rhs) noexcept
	Euclidean remainder on Cardinality. Mirrors the operator/ convention: finite % finite delegates to the underlying ExtensionalCardinal<>'s %; finite % ℵ_0 returns the lhs (the limit-style "remainder is the original" reading); operations with ℵ_0 on the lhs saturate to ℵ_0.
template<typename A, typename B> requires requires { typename A::Domain; typename B::Domain; } && std::same_as<typename A::Domain, typename B::Domain> && (!IsBoundaryObject<A>) && (!IsBoundaryObject<B>) && IsStepTerm<A> && IsStepTerm<B> && std::same_as<typename A::logic_species, typename B::logic_species>
constexpr auto	dedekind::category::operator== (const A &a, const B &b)
	Equality of two set terms of a chain as sets of the carrier, in the species: one traversal of their normal forms, so it is extensional ((0, 3) and [1, 3) are the same set of ℤ).
template<typename A, typename B> requires TermOperands<A, B>
constexpr auto	dedekind::category::operator!= (A a, B b)
template<typename A, typename B> requires HasProperSubset<A, B>
constexpr A::logic_species::Ω	dedekind::category::operator< (const A &a, const B &b)
template<typename A, typename B> requires DecidableMeetSubset<A, B>
constexpr A::logic_species::Ω	dedekind::category::operator<= (const A &a, const B &b)
	\(A \subseteq B \iff A \cap B = A\) — the generic identity. More-specialized per-carrier <= (Set / Ø / 𝔸, the Singleton membership and Interval endpoints below) win by partial ordering; this fills the gaps (Halfspace ⊆ Halfspace).
template<typename A, typename B> requires HasProperSubset<B, A>
constexpr A::logic_species::Ω	dedekind::category::operator> (const A &a, const B &b)
template<typename A, typename B> requires HasSubset<B, A>
constexpr A::logic_species::Ω	dedekind::category::operator>= (const A &a, const B &b)
	Superset, proper subset, proper superset — each once from <= and ==, gated on HasSubset so they ride any decidable <= (generic or specialised). Together they supply HasPartialOrderOperators.
The legs of a node, for @c cata (@c category::f_algebra)
The term functor stated once per node: the sub-terms, by reference. A projection, a constant, and a predicate the grammar does not know are leaves. An arrow applied to a term has one leg, the term (the arrow is a datum of the node).
template<typename Op, typename A, typename B>
constexpr auto	dedekind::sets::legs (const BinOp< Op, A, B > &t)
template<typename F, typename A>
constexpr auto	dedekind::sets::legs (const Ap< F, A > &t)
template<typename P, typename A, typename B>
constexpr auto	dedekind::sets::legs (const CondT< P, A, B > &t)
template<Rel R, typename A, typename B>
constexpr auto	dedekind::sets::legs (const Cmp< R, A, B > &t)
template<typename A, typename B>
constexpr auto	dedekind::sets::legs (const RelAnd< A, B > &t)
template<typename A, typename B>
constexpr auto	dedekind::sets::legs (const RelOr< A, B > &t)

Variables
constexpr Projection< 1 >	dedekind::sets::𝑥 {}
constexpr Projection< 2 >	dedekind::sets::𝑦 {}
constexpr Projection< 3 >	dedekind::sets::𝑧 {}
template<typename T>
constexpr bool	dedekind::sets::is_runtime_term_v = false
template<typename K>
constexpr bool	dedekind::sets::is_runtime_term_v< Term< K > > = true
template<typename T>
constexpr bool	dedekind::sets::is_term_v = false
template<IsRingIntegral auto I>
constexpr bool	dedekind::sets::is_term_v< Projection< I > > = true
template<typename K>
constexpr bool	dedekind::sets::is_term_v< Const< K > > = true
template<typename Op, typename A, typename B>
constexpr bool	dedekind::sets::is_term_v< BinOp< Op, A, B > > = true
template<typename F, typename A>
constexpr bool	dedekind::sets::is_term_v< Ap< F, A > > = true
template<typename P, typename A, typename B>
constexpr bool	dedekind::sets::is_term_v< CondT< P, A, B > > = true
template<typename T>
constexpr unsigned	dedekind::sets::slots_v
	The slots T mentions, through any cv-ref (a constexpr variable's decltype is const).
template<typename T>
constexpr bool	dedekind::sets::is_const_v = false
template<typename K>
constexpr bool	dedekind::sets::is_const_v< Const< K > > = true
template<typename P>
constexpr bool	dedekind::sets::is_row_v = false
template<typename... Cs>
constexpr bool	dedekind::sets::is_row_v< Row< Cs... > > = true
template<typename C, typename S>
constexpr bool	dedekind::sets::is_sort_of_v = false
	Whether C is one of the sorts S.
template<typename C, typename... Cs>
constexpr bool	dedekind::sets::is_sort_of_v< C, std::tuple< Cs... > >
constexpr std::size_t	dedekind::sets::no_sort = static_cast<std::size_t>(-1)
	No sort yet: a tree of constants alone, which takes the sort of its context.
template<typename X, typename T>
constexpr bool	dedekind::sets::is_total_term_v
	A term total at every point of type X.
template<typename T>
constexpr bool	dedekind::sets::is_self_v = false
	Whether a leaf is the set under definition, a χ node; :recursion registers it.
template<typename T>
constexpr bool	dedekind::sets::contains_self_v
	Whether T mentions the set under definition.
constexpr auto	dedekind::sets::detail_terms_witness::succ_graph = π_1 + 1 == π_2
constexpr auto	dedekind::sets::detail_terms_witness::half_after_shift = (π_1 + 1) * 3 == π_2
constexpr auto	dedekind::sets::detail_terms_witness::on_naturals = π_1 + 1 == π_2
constexpr Projection< 0 >	dedekind::sets::π
	The unary projection, the identity: the variable of a comprehension over one carrier.
template<std::size_t K>
constexpr Projection< K >	dedekind::sets::π_
	The family: π_<k> is the k-th projection of a flat product.
constexpr Projection< 1 >	dedekind::sets::π_1
	The projections of a pair (and the first three of a tuple).
constexpr Projection< 2 >	dedekind::sets::π_2
constexpr Projection< 3 >	dedekind::sets::π_3

Detailed Description

The term grammar of comprehensions: projections, constants carried as values, arithmetic, arrows applied to terms, conditionals; the comparison atom over two terms; the pointwise connectives of relational predicates.

@partition :terms

Copyright

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

terms__Grammar

term ::= π_i | const(v) | term op term | ap(arrow, term)
       | cond(pred, term, term)
op   ::= '+' | '-' | '*' | '/' | '%'
atom ::= term rel term
rel  ::= '==' | '!=' | '<' | '<=' | '>' | '>='

A term's structure is its type: the slots it mentions (slots_v, a bit mask), its operators, the comparison an atom makes. Its constants are values, spelled as the literals themselves (π_1 + 1 == π_2), so a term built at run time — from Python — is the same term. A constant meets the sort of the term it is combined with: on a pair of Cardinality the 1 above is the cardinal 1, converted when the term is evaluated and checked to be representable. Facts about a constant's value (a divisor is not zero) are checked when the term is built: in constexpr code a violation is a compile error.

Certificates read the structure: an atom π_2 == T with slots_v<T> ⊆ {1} is the graph of a function of the first coordinate, whatever T is.

Every reading of a term is an algebra folded by category::cata, the one engine: each node states its legs once, and an algebra states only the nodes it reads specially (Slots, Total, Bind, Value below). A reading whose results are std::integral_constant is a type-level certificate; the same fold with values is the evaluation.

A term built at run time (from Python) is the same grammar with its shape a value: Term<K> and Pred<K> below, read by the same algebras through their steer rule, and checked against the carrier when the former binds them (bind_check): an operator admitted there or refused (not_admitted), a constant meeting the carrier or refused.

terms__Signature_And_Free_Algebra

The laws decide the syntax. A carrier's certified varieties supply the signature a term may use (admits below: + on a commutative monoid, - on an abelian group, * on a monoid, / on a field, // and % on a dividable chain, the order comparisons on a poset, == and != on any set) and the free algebra on the variables its normal form lives in; equality of terms is equality in that free algebra. The catalogue of free algebras with a canonical representative:

• a chain: the Boolean algebra the intervals generate, read as run lists (order:runs, steps);
• a commutative rig, ring or field: polynomials over the carrier (algebra:polynomial, canonical). A term whose operators are in the signature but outside the catalogue (a remainder, a division by a term) is well-formed and evaluates, and has no equality: it is refused where a normal form is asked, never rewritten. Type-checking is at the former: at compile time for a typed term bound to a constexpr universe, at construction for a term built at run time.

The carrier and its algebras are different entities (the paper's Figure 1), and a carrier bears several: u64 is a chain, a ring and a Euclidean division at once. The signature is the union over the carrier's registered algebras, each rule speaking for one, each import bringing one more into view. A free algebra, and so a normal form, is per algebra, not per carrier: over one carrier the chain's is read as run lists and the ring's as polynomials, and "equal terms" means a different thing in each. A term spanning two algebras (π + 1 < 5) belongs to their combined theory (the ordered ring, whose laws relate <= and +) and has a normal form only where that theory's is catalogued; the translate of an atom π ± c ⋈ k in order:halfspace is the first piece of it, not a licence to glue run lists and polynomials without laws. A field adds no free algebra: division by a nonzero constant factors through the ring (π / 3 on 𝔽₇ is π * 5), so the field certificate only guarantees the constant a unit.

Wikipedia: Term (logic), Term algebra, Atomic formula, Relational algebra

Note

"Die Zahlen sind freie Schöpfungen des menschlichen Geistes, sie dienen als ein Mittel, um die Verschiedenheit der Dinge leichter und schärfer aufzufassen." – Richard Dedekind, Was sind und was sollen die Zahlen? (1888), Vorwort. [Trans: "Numbers are free creations of the human mind; they serve as a means of grasping the difference of things more easily and more sharply."]