Loading...
Searching...
No Matches
expressions.cppm File Reference
module dedekind.sets
Set-builder DSL — comprehension + Boolean connectives. More...
#include <compare>#include <concepts>#include <functional>#include <type_traits>#include <utility>#include <variant>import dedekind.sets:terms;import dedekind.category;
Include dependency graph for expressions.cppm:
Classes | |
| struct | dedekind::sets::SetExpr< Derived, DomainT, L > |
Opt-in CRTP base that supplies the ETCS set surface to a specialized set expression. It provides Member, ι (the subobject inclusion), Codomain, logic_species, and the set-lattice trait members. It keys the classifier χ off the Derived's own operator(). More... | |
| struct | dedekind::sets::SetExpr< Derived, DomainT, L >::Member |
A member is a carrier value; ι projects it back into the ambient (the subobject inclusion the ETCS axioms read). More... | |
| struct | dedekind::sets::answer_logic< L, Answer > |
The species of a predicate's answer, relative to the base's species L: an answer already in L::Ω is in L (so a Chain<int> universe accepts an int-valued predicate), otherwise the answer type names its species (classifier_logic_t; no default). More... | |
| struct | dedekind::sets::answer_logic< L, Answer > |
| struct | dedekind::sets::datum_cardinality< Predicate, Base > |
| struct | dedekind::sets::datum_cardinality< Predicate, Base > |
| struct | dedekind::sets::Comprehension< Base, Predicate > |
| struct | dedekind::sets::UniversalPredicate< T > |
| The universal predicate: accepts every element of T. More... | |
| struct | dedekind::sets::EmptyPredicate< T > |
| The empty predicate: rejects every element of T. More... | |
| struct | dedekind::sets::UnknownPredicate< T > |
The archetypal undecidable predicate: answers Unknown everywhere. More... | |
| struct | dedekind::sets::SetCombine |
The injected leaf-combiner (the reducer's Combine policy) for the subobject lattice: at an order-incomparable residual, hand the two set leaves to the carrier's domain ∧ / ∨ on their runtime data and let the reducer fold the result again. Two plain sets over one universe combine through their predicates (structured_and / structured_or via ADL, elevated back to a set); a value leaf (an Interval) combines directly. Each leg is present only where the carrier actually combines the pair, so elsewhere the residual stays a Meet / Join node. More... | |
| struct | dedekind::sets::set_predicate< S > |
The predicate of a PLAIN set, a Comprehension over the universe 𝔸<T,L> (::type absent otherwise); PlainSet gates the plain-set-only branches (complement pair, predicate negation) so a compound node (Meet / Join) takes the node path. More... | |
| struct | dedekind::sets::set_predicate< Comprehension< 𝔸< T, L, C >, P > > |
| struct | dedekind::sets::Complement< T, L > |
The complement as an arrow on the object \(\mathrm{Sub}(T, L)\) (Subobjects, T in L. It is an involution by the reducer's own law \(\neg\neg A \to A\): operator~ peels the node, so ~~s is s, by type, for every presentation s; the certificate reads that law at the representative. The first arrow on sets category::IsInvolution admits: the concept quantifies over the object, not over one value type (morphism__Objects_And_Their_Presentations). More... | |
| struct | dedekind::category::antimonotone_trait< dedekind::sets::Complement< T, L >, std::less_equal<> > |
| The complement reverses inclusion: \(a \subseteq b \Rightarrow
\neg b \subseteq \neg a\), for every carrier and logic. More... | |
| struct | dedekind::category::is_adjoint< dedekind::sets::Complement< T, L >, dedekind::sets::Complement< T, L >, std::less_equal<> > |
| The complement is its own antitone adjoint, \(a \subseteq \neg b
\iff b \subseteq \neg a\): the De Morgan algebra \(\mathrm{Sub}(T, L)\) as a Galois connection, for every carrier and logic. More... | |
| struct | dedekind::sets::InitialObjectArrow< Init, Target > |
InitialObjectArrow<Init, Target> — the unique arrow from the initial object into any subobject (Init → Target), i.e. the empty function / the ⊥-of-Sub(U) leg. Dual to inclusion_arrow: where that reifies an inclusion into the ambient, this reifies the initiality mediator out of Ø. Gated on category::IsInitialObject<Init> so only a genuine initial object (Ø, tagged) can be the source; the body forwards the (vacuous) Member value and is unreachable in practice (Ø has no members). Canonical span leg for a pushout A ← Ø → B, replacing hand-rolled per-instance span structs. #881. More... | |
| struct | dedekind::sets::SymbolicImagePredicate< U > |
| Symbolic image-of-intensional-Set predicate (#602 layer 1). More... | |
| struct | dedekind::sets::ComposedIsoImagePredicate< SourceSet, FInv > |
Composed predicate for the iso-decidable image(f, Set) specialisation below: y ↦ S(f^{-1}(y)) where S is the source set's characteristic and f^{-1} is the iso's inverse. More... | |
| struct | dedekind::sets::ComposedRetractImagePredicate< SourceSet, RetractFn, L > |
Composed predicate for the retract-decidable image(f, Set) specialisation: y ↦ let mx = retract(f)(y); mx.has_value() S(mx.value()) L::False. More... | |
| struct | dedekind::sets::detail_setexpr_witness::all_in |
Namespaces | |
| namespace | dedekind::sets |
| namespace | dedekind::category |
| namespace | dedekind::sets::detail_complement_involution |
Concepts | |
| concept | dedekind::sets::HasCardinalityType |
| The cardinality bound a comprehension inherits: the datum's when it declares one, else the base's. | |
| concept | dedekind::sets::IsDatum |
A datum over T: a predicate on T (an arrow into a truth object) that is not itself a set. Point, Bounds, LowerCut. | |
| concept | dedekind::sets::PlainSet |
| concept | dedekind::sets::HasStructuredAnd |
| Downstream specialization hook for structured predicate conjunction. | |
| concept | dedekind::sets::HasStructuredOr |
| Downstream specialization hook for structured predicate disjunction. | |
| concept | dedekind::sets::IsLogicalTerm |
A term of the set grammar, the operand sort of && / ||: an arrow (a predicate, a set, a node over arrows) or a point-free relational fragment (π_1 ⋈ π_2, tagged is_rel_predicate, which meets its domain only at the former &). A bare truth value is not a term: bool && bool stays the host language's, and a constant beside a predicate lifts through | |
| concept | dedekind::sets::SetShaped |
A set-shaped carrier: exposes the ambient Domain and the logic_species. The gate constraint for the power-set customization point; the ordered specialisation conjoins it (so it subsumes this gate and wins by partial ordering for the carriers it handles). | |
Typedefs | |
| template<typename Base, typename Predicate> | |
| using | dedekind::sets::comprehension_logic_t |
The logic species of {base pred}: the join (in the species semilattice, category::join_logic_t) of the base's species and the species of the predicate's answer, so a Kleene predicate over a Boole base lifts the base rather than truncating itself, and a Kleene predicate over a Percent base answers in Percent. A pair with no join (a K₃ answer over a Chain<int> base) is refused here. | |
| using | dedekind::sets::detail_complement_involution::UnivSizeSet |
| using | dedekind::sets::detail_setexpr_witness::CompN = Comprehension<𝔸<int>, all_in> |
| using | dedekind::sets::detail_setexpr_witness::SubN = std::remove_cvref_t<decltype(classify<int>(all_in{}))> |
Functions | |
| template<typename T, IsOckhamAlgebra L, IsCardinality C, IsDatum< T > P> | |
| constexpr auto | dedekind::sets::operator& (const 𝔸< T, L, C > &, P p) |
The set former 𝔸<T, L>{} & P = \(\{x \in T \mid P(x)\}\) for a datum P (a point π == v, a cut π > v): the meet with the subobject P classifies (#826; | |
| template<typename T, IsOckhamAlgebra L, IsCardinality C, IsRelPredicate P> requires (only_slot(slots_v<P>, 0)) && (!contains_self_v<P>) && std::convertible_to<std::invoke_result_t<const P&, const T&>, bool> | |
| constexpr auto | dedekind::sets::operator& (const 𝔸< T, L, C > &, P p) |
𝔸<T> & atom for an atom on the unary π (ℕ & % 3 == 0)): the atom evaluated at each element. | |
| template<typename T, IsOckhamAlgebra L, IsCardinality C, typename K> requires (!requires { typename T::first_type; }) | |
| constexpr auto | dedekind::sets::operator& (const 𝔸< T, L, C > &, Pred< K > p) |
𝔸<T> & pred for a predicate built at run time: bound to the carrier now, every operator admitted there or refused (not_admitted), every constant meeting it. Pairs take the product former. | |
| template<typename S, typename P> requires IsSetObject<S> && (!IsSetObject<P>) && (!IsLSet<P>) | |
| void | dedekind::sets::operator| (const S &, const P &)=delete |
S P for a set and a non-set: refused. The filter is the meet, S & P (#826); | |
|
template<typename TargetL, IsSetObject S> requires dedekind::category::LiftsTo<typename S::logic_species, TargetL> | |
| constexpr auto | dedekind::sets::lift_to (const S &s) |
Bring a set object to the species TargetL along the dominance: the identity when it is already there, else the comprehension {x ∈ 𝔸<T, TargetL> | s(x)}. Its species is the join, which is TargetL since s's species embeds into it, and its χ is lift_logic<TargetL>(s(x)) (the universe answers ⊤): the lift is composition with the dominance embedding, no wrapper type. It does not preserve the operand's structural type (interval / halfspace), so a cross-species combine materialises pointwise rather than collapsing structurally. Constrained to a registered inclusion, so a downward or unsupported lift is rejected at the gate. | |
| template<typename T, IsOckhamAlgebra L, typename Reduced> | |
| constexpr auto | dedekind::sets::elevate_meet (Reduced reduced) |
Value-level elevate of a structured_and result to the meet's normal-form value: an empty reduction is the initial object Ø; a finite reduction (a point) is itself a set-like leaf (returned bare); any other reduction is a named predicate wrapped back into a comprehension. (Extracted verbatim from the pre-reducer operator& structured_and branch so SetCombine's type and this value stay in lockstep.). | |
| template<typename T, typename L, typename Reduced> | |
| constexpr auto | dedekind::sets::elevate_join (Reduced reduced) |
Value-level elevate of a structured_or result to the join's normal-form value: a covering pair is the universe 𝔸 (returned bare); any other reduction (a wider halfspace) is wrapped back into a Set. Dual of elevate_meet. | |
| template<typename Base, typename Predicate> | |
| constexpr auto | dedekind::sets::universe (const Comprehension< Base, Predicate > &) |
| template<typename T, IsOckhamAlgebra L, typename P, IsCardinality C> | |
| constexpr P | dedekind::sets::classifier (const Comprehension< 𝔸< T, L, C >, P > &s) |
|
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator& (const LHS &lhs, const RHS &rhs) |
The subobject-lattice meet A & B, over any two IsSubobject operands sharing a carrier and logic. It folds Meet<A,B> through the reducer; SetCombine supplies the domain structured_and at the incomparable residual. The normal form materialises to Ø, 𝔸, an operand, or a structured leaf. An irreducible meet becomes a Meet carrying both operand sets. | |
|
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator| (const LHS &lhs, const RHS &rhs) |
The subobject-lattice join A B, dual to operator&. An irreducible join becomes a Join carrying both operand sets. | |
|
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator& (const LHS &lhs, const RHS &rhs) |
Cross-species meet (#894, step i): two subobjects over the same carrier but different codomains join to the more expressive one (the species semilattice's join, category::join_logic_t; refused when no shipped species is above both); lift both there, then the same-species meet above folds them. This lets a mixed Boole ∩ Kleene combine into the reducer at all. Same-species combines are untouched (this overload requires the species to differ, so it never competes with the meet above). | |
|
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && (!(dedekind::category::builds_lattice_nodes<LHS>::value && dedekind::category::builds_lattice_nodes<RHS>::value)) && std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator| (const LHS &lhs, const RHS &rhs) |
| Cross-species join, dual to the cross-species meet (#894, step i). | |
| template<IsPredicate P> requires IsSetObject<std::remove_cvref_t<P>> | |
| constexpr auto | dedekind::sets::operator~ (const P &p) |
The set complement ~A (#829: ~ is the SET complement; ! is the predicate complement, which category::operator! supplies as a formal Morphism). ~A is the reducer's own Not node — a first-class subobject whose χ is the codomain reflection Ω::RFL of A's, generic over any bounded chain (Boole !, Kleene ¬U=U, and any registered Chain). There is no bespoke wrapper and no is_set_node_v tag: the gate is the structural IsSubobject, and because category defines no operator~ there is nothing to out-prioritise, so the tag that once disambiguated the two operator! overloads is gone (#963). The const reference parameter (matching operator& / operator|) makes this a FALLBACK that loses partial ordering to a type-specific complement, so a Halfspace / Singleton operator~ still wins for its own type (its closed-form collapse, e.g. ~Above<5> = AtMost<5>). | |
|
template<typename LHS, typename RHS> requires IsSetObject<LHS> && IsSetObject<RHS> && std::same_as<typename LHS::Domain, typename RHS::Domain> && std::same_as<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator^ (const LHS &a, const RHS &b) |
Symmetric difference A △ B (set-theoretic XOR; #469), a FREE combinator over IsSubobject (like & / ~), so it composes uniformly whether an operand is a Set, a Meet / Join, or a Not complement node. The textbook identity A XOR predicate — ~ / & / A join-complement law on a complemented codomain. The disjoint fast path (A compile-time collapse. | |
| template<IsSetObject LHS, IsSetObject RHS> requires std::same_as<typename LHS::Domain, typename RHS::Domain> && (!std::same_as<typename LHS::logic_species, typename RHS::logic_species>) && dedekind::category::HaveLogicJoin<typename LHS::logic_species, typename RHS::logic_species> | |
| constexpr auto | dedekind::sets::operator^ (const LHS &a, const RHS &b) |
Cross-species symmetric difference: both operands are lifted into the join of their species and △ is computed there (as for & and | |
| template<typename A, typename B> requires IsSetObject<Meet<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain> | |
| constexpr auto | dedekind::sets::as_pullback (const Meet< A, B > &m) |
The pullback apex of an applied meet: the same set, viewed with the subobject surface and the projection legs π_1 / π_2 (IsPullback), category's view over the node. | |
| template<typename A, typename B> requires IsSetObject<Join<A, B>> && IsSubobject<A, typename A::Domain> && IsSubobject<B, typename B::Domain> | |
| constexpr auto | dedekind::sets::as_pushout (const Join< A, B > &j) |
The pushout apex of an applied join, dual to as_pullback. | |
| template<dedekind::category::IsArrow F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain> | |
| constexpr auto | dedekind::sets::image (F &&, const S &) |
| image(f, {x ∈ 𝔸 | P}) — image of an intensional set under an arrow. Layer 1 of #602. | |
| template<dedekind::category::IsIsomorphism F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain> | |
| constexpr auto | dedekind::sets::image (F &&f, const S &s) |
| image(iso f, {x ∈ 𝔸 | P}) — decidable specialisation for isomorphism arrows (#602 Layer 2 entry). | |
|
template<typename T, typename L, typename C, dedekind::category::IsIsomorphism F> requires (std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, T> && !dedekind::category::IsTerminalMorphism<std::remove_cvref_t<F>>) | |
| constexpr auto | dedekind::sets::image (F &&, const 𝔸< T, L, C > &) |
image of the unbounded universe under an iso F:T→U is the universe of the codomain, 𝔸: an iso is surjective, so it fixes the universe setwise — but onto U, not T. For an endo-iso (U==T) this is 𝔸<T> unchanged; for a heterogeneous iso (e.g. Modular<2> → bool) it correctly returns 𝔸<bool> so callers can query codomain values. | |
| template<dedekind::category::IsRetractableArrow F, IsSetObject S> requires std::same_as<dedekind::category::Dom<std::remove_cvref_t<F>>, typename S::Domain> && (!dedekind::category::IsIsomorphism<std::remove_cvref_t<F>>) | |
| constexpr auto | dedekind::sets::image (F &&f, const S &s) |
image(monic-with-retract f, {x ∈ 𝔸 | P}) — decidable specialisation for monic arrows that ship a retract (a partial inverse via the retract(f) ADL hook). #602 Layer 2 / Case A. | |
| template<typename T, typename L, typename Predicate, typename C, typename LB> | |
| constexpr auto | dedekind::sets::operator^ (const Comprehension< 𝔸< T, L, C >, Predicate > &s, const Ø< T, LB > &) |
Set ^ Ø = Set (symmetric difference with empty is identity). Symmetric of Ø::operator^(S): picks up S ^ Ø when the boundary is on the right, keeping the structural collapse type-level. The boundary's species tag is immaterial (∅ is decided), so it is not matched against the set's. | |
| template<typename T, typename L, typename C, typename Predicate, typename LB, typename CB> | |
| constexpr auto | dedekind::sets::operator^ (const Comprehension< 𝔸< T, L, C >, Predicate > &s, const 𝔸< T, LB, CB > &) |
Set ^ 𝔸 = ¬Set (symmetric difference with the universe is the complement). Symmetric of 𝔸::operator^(S); the universe's species tag is immaterial (⊤ is decided). ~ is the SET complement (a set object); ! would be the predicate complement, an arrow. | |
| template<IsLogicalTerm P1, IsLogicalTerm P2> requires (!IsPredicatePair<P1, P2>) | |
| constexpr auto | dedekind::sets::operator&& (P1 &&p1, P2 &&p2) |
Predicate-level conjunction p1 && p2: structured_and when a domain collapse applies, else the reducer's Meet node, a callable predicate \(\chi_1 \wedge \chi_2\) that also carries its operands via π_1 / π_2. It is the same AST the set-level combinators use, so a set-builder Set{x p1 && p2} shares one representation with A & B. There is no separate AndPredicate. A pair of predicates over one species is IsPredicatePair, which closes on IsPredicate); this one takes every other pair of terms. | |
| template<IsLogicalTerm P1, IsLogicalTerm P2> requires (!IsPredicatePair<P1, P2>) | |
| constexpr auto | dedekind::sets::operator|| (P1 &&p1, P2 &&p2) |
Predicate-level disjunction p1 || p2, dual to operator&&: structured_or when a collapse applies, else the reducer's Join node; a pair of predicates over one species is IsPredicatePair). | |
| template<typename S> requires SetShaped<S> | |
| auto | dedekind::sets::power_set (const S &)=delete |
| Power set \(\mathfrak{P}(S)\) — the default declaration (customization-point gate). | |
|
template<typename S> requires SetShaped<S> | |
| auto | dedekind::sets::𝔓 (const S &)=delete |
Textbook fraktur-P alias for power_set (the deleted default gate). Mirrored on the Python side as dedekind.sets.𝔓. | |
| template<typename T, typename L> | |
| constexpr auto | dedekind::sets::power_set (const Ø< T, L > &) |
\(\mathfrak{P}(\emptyset) = \{\emptyset\}\) — the one power set that needs no subobject normal-form, so it is a closed form here in | |
| template<typename T, typename L> | |
| constexpr auto | dedekind::sets::𝔓 (const Ø< T, L > &) |
|
template<typename A, typename Pred> requires IsSpecies<A> && std::invocable<std::decay_t<Pred>, const A&> && IsΩ<std::invoke_result_t<std::decay_t<Pred>, const A&>> | |
| constexpr auto | dedekind::sets::ambient_set (Pred predicate) |
| Construct a set object over ambient species A from a characteristic predicate. | |
| template<typename S> requires IsSubobject<std::remove_cvref_t<S>, typename std::remove_cvref_t<S>::Domain> | |
| constexpr SubobjectInclusion< std::remove_cvref_t< S > > | dedekind::sets::inclusion_arrow (const S &s) |
Variables | |
| template<typename T, IsOckhamAlgebra L, typename P, dedekind::sets::IsCardinality C> | |
| constexpr bool | dedekind::category::idempotent_leaf_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< T, L, C >, P > > |
| constexpr auto | dedekind::sets::detail_complement_witness::three = 𝔸<int>{} & (π == 3) |
| template<typename A, typename B, typename L, typename C, typename P> | |
| constexpr bool | dedekind::category::is_right_unique_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, C >, P > > = true |
| template<typename A, typename B, typename L, typename C, typename P> | |
| constexpr bool | dedekind::category::is_left_total_v< dedekind::sets::Comprehension< dedekind::sets::𝔸< std::pair< A, B >, L, C >, P > > |
Detailed Description
Set-builder DSL — comprehension + Boolean connectives.
@partition :expressions
- Copyright
- 2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.
expressions__Description
This partition provides the principal "set-builder" abstraction: Comprehension<B, P> – an intensional set whose membership test is a compile-time callable predicate ranging into a subobject classifier L::Omega.
Key constructs exported:
- Comprehension<B,P> – the point-free set-builder node {x in B | P(x)}.
- Boolean connectives &&, ||, ! lifted to predicate combinators.
- operator<= – subset relation (same-predicate -> True; heterogeneous -> Unknown via Kleene).
- the expressions across carriers (A × B, A + B, the ℕ / ℤ widening) are
:heterogeneous. - Relation, SetFunction – subobjects of products.
- relates, is_single_valued_at – point-wise witnesses.
- power_set / 𝔓 – default (deleted) gate here; the ordered/convex specialisation is dedekind.order:powerset (#830).
expressions__Canonical_Examples
const auto xs = ℕ | (χ < 512); // {n in ℕ | n < 512}
const auto grid = cartesian_product(xs, xs); // xs x xs
expressions__References
- Lawvere, F.W. (1964) – ETCS axioms [7]
- Lambek & Scott (1988) – higher-order categorical logic [5]
- Pierce (1991) – basic category theory [10]
@quote "Future users of large data banks must be protected from having to know how the data is organized in the machine." – E. F. Codd, A Relational Model of Data for Large Shared Data Banks (1970)
- Note
- "What is objective must be common to many minds and consequently transmissible from one to the other." – Henri Poincare, The Value of Science (1905)
