mereology.cppm File Reference

Embryonic Mereology (Part-Whole and Skew Algebraic Core). More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <limits>
#include <optional>
#include <ranges>
#include <type_traits>
import dedekind.category:morphism;

Include dependency graph for mereology.cppm:

Classes
struct	dedekind::category::is_reflexive< T, Rel >
	Trait to mark a relation as reflexive: a ~ a = True. More...
struct	dedekind::category::is_reflexive< T, Rel >
struct	dedekind::category::is_reflexive< T, std::less_equal< T > >
struct	dedekind::category::is_transitive< T, Rel >
struct	dedekind::category::is_transitive< T, Rel >
struct	dedekind::category::is_transitive< T, std::less_equal< T > >
struct	dedekind::category::is_antisymmetric< T, Rel >
struct	dedekind::category::is_antisymmetric< T, Rel >
struct	dedekind::category::is_antisymmetric< T, std::less_equal< T > >
struct	dedekind::category::is_connex< T, Rel >
struct	dedekind::category::is_connex< T, Rel >
struct	dedekind::category::is_connex< T, std::less_equal< T > >
struct	dedekind::category::ChainWalk< T >
	Where a walk from lo ends: the last value reached and how many values it took. reached_hi says whether it stopped at hi (rather than at a saturating top short of it, or at the end of the budget). More...
struct	dedekind::category::ChainStep< T >
	One step of the walk: the next value, or the walk itself once it has ended, which makes an ended walk the fixed point iterate stops at. More...
struct	dedekind::category::Sup
	Value-returning chain lattice ops — the honest T × T → T meet / join. More...
struct	dedekind::category::Inf
	Meet ∧: the greatest lower bound on a chain (min), returned by value. Value-returning sibling of Sup. More...
struct	dedekind::category::unit_trait< bool, Sup >
	bool's ends, the identities of Sup and Inf, declared beside them: every partition that can ask (a chain walk on bool, as :equivalence does) then sees the one definition, before :logic's classifier-answer specialisation could give it a second. More...
struct	dedekind::category::unit_trait< bool, Inf >
struct	dedekind::category::detail_mereology::Dial< N >
	A discrete bounded chain of N values that is no enum: a class with a cover step and two bounds, nothing registered about its relations. More...
struct	dedekind::category::unit_trait< detail_mereology::Dial< N >, Sup >
struct	dedekind::category::unit_trait< detail_mereology::Dial< N >, Inf >
struct	dedekind::category::detail::merc_filtered
struct	dedekind::category::detail::merc_shell

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsTruthObject
	Ω may carry a relation's answer in the laws below: it has a top ⊤, the value a law asserts (reflexivity is rel(a, a) = ⊤). bool (top true) is the default; Ternary names its Ω::True, a value type with a species (Percentage, the bounded chains) finds it on the species. A statement of intent, not a certificate: the laws come before logic, so the truth objects are only certified downstream (:logic, IsΩ).
concept	dedekind::category::IsReflexive
	Formal verification of the identity relation.
concept	dedekind::category::IsTransitive
	Formal verification: (a ≤ b ∧ b ≤ c) ⇒ a ≤ c.
concept	dedekind::category::IsAntisymmetric
	Formal verification: (a ≤ b ∧ b ≤ a) ⇒ a = b.
concept	dedekind::category::IsConnex
	Formal verification: a ≤ b ∨ b ≤ a.
concept	dedekind::category::SupInfOperand
	A carrier on which Sup / Inf (and max / min) are a genuine, usable value op: totally ordered (for <) and copy-constructible (the winner is returned by value). This is the CALL gate: Sup{}(1.0, 2.0) is a valid call that returns a value, so raw floats are not excluded here; only the lattice laws fail on them (see SupInfLattice).
concept	dedekind::category::SupInfLattice
	A carrier on which max / min (and Sup / Inf) are honest lattice ops: usable (SupInfOperand) and carrying a certified order.
concept	dedekind::category::IsWalkableChain
	Rel is a stateless relation on a discrete bounded chain T on which a law of Arity variables can be decided: a step (successor, by argument-dependent lookup, as for HasNNOStep), a least and a greatest value (the identities of Sup and Inf), the top reached from the bottom within chain_walk_budget, and nᴬʳⁱᵗʸ within law_evaluation_budget, all as constant expressions (what cannot be evaluated at compile time is simply not decided here, rather than an error).
concept	dedekind::category::IsChainDecidedReflexive
	Each law, stated once for every relation on a walkable chain: the certificate the concept reads is the law over the whole chain, for ≤, ≥, ==, or any stateless relation, decided and never registered per operator. A carrier that answers through its own member keeps that answer; a law the compiler cannot evaluate is not decided here. Exported conditions, so a rule elsewhere can yield to these.
concept	dedekind::category::IsChainDecidedAntisymmetric
concept	dedekind::category::IsChainDecidedConnex
concept	dedekind::category::IsChainDecidedTransitive
concept	dedekind::category::IsPartRelation
	Verifies that a binary operator satisfies Leśniewski's mereological axioms.
concept	dedekind::category::IsPartialOrder
	Named stage for the partial-order maturity level of parthood.
concept	dedekind::category::IsTotalOrder
	Linear/total refinement of IsPartialOrder.
concept	dedekind::category::IsPartOfRelation
	Minimal core part-whole relation yielding Omega.
concept	dedekind::category::IsMereologicalJoinMagma
	Stage 0 for join-like algebra: closure only.
concept	dedekind::category::IsMereologicalMeetMagma
	Stage 0 for meet-like algebra: closure only.
concept	dedekind::category::IsMereologicalJoinSemigroup
	Stage 1 for join-like algebra: magma + associativity.
concept	dedekind::category::IsMereologicalMeetSemigroup
	Stage 1 for meet-like algebra: magma + associativity.
concept	dedekind::category::IsMereologicalMeetBand
	Non-commutative meet-like operation (associative + idempotent).
concept	dedekind::category::IsMereologicalJoinBand
	Non-commutative join-like operation (associative + idempotent).
concept	dedekind::category::IsAbsorptive
	Mutual absorption and internal idempotency for a pair of operations.
concept	dedekind::category::IsMereologicalSkewLattice
	Non-commutative lattice-style operations (skew lattice fragment).
concept	dedekind::category::IsMereologicalLatticeOperations
	Compatibility lattice alias over the skew core + absorption.
concept	dedekind::category::IsMereologicalDistributiveLatticeOperations
	Mature distributive stage: lattice operations with mutual distribution.
concept	dedekind::category::HasExtrema
	Structural requirement for Dedekind completeness witnesses.
concept	dedekind::category::IsMereologicalCutCandidate
	Transitional bridge contract for the soft-to-hard structural cut.
concept	dedekind::category::Parthood
	Skeletal part-whole contract at the concept level.

Typedefs
using	dedekind::category::detail_mereology::D4 = Dial<4>
using	dedekind::category::detail_mereology::D100 = Dial<100>

Functions
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::reflexive_at (const Rel &rel, const T &a)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::transitive_at (const Rel &rel, const T &a, const T &b, const T &c)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { x == x } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::antisymmetric_at (const Rel &rel, const T &a, const T &b)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; }
constexpr bool	dedekind::category::connex_at (const Rel &rel, const T &a, const T &b)
template<typename T> requires requires(const T& t) { { successor(t) } -> std::convertible_to<T>; { t == t } -> std::convertible_to<bool>; }
constexpr ChainWalk< T >	dedekind::category::walk_chain (const T &lo, const T &hi, std::size_t budget=chain_walk_budget)
	The walk from lo towards hi by the carrier's successor, within chain_walk_budget: the fixed point of one step, reached where the chain ends (at hi, or at a fixpoint of the step), so it stops there.
template<std::size_t Arity, typename Law, typename Rel, typename T, typename... Fixed> requires (sizeof...(Fixed) != Arity) || std::predicate<const Law&, const Rel&, const Fixed&...>
constexpr bool	dedekind::category::holds_on_walk (Law law, const Rel &rel, const T &lo, std::size_t length, const Fixed &... fixed)
	A law of Arity points, at every tuple of points from lo to hi: the one walk every law below reads.
template<std::size_t Arity, typename Law, typename Rel, typename T>
constexpr bool	dedekind::category::holds_on (Law law, const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::reflexive_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::antisymmetric_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::connex_on (const Rel &rel, const T &lo, const T &hi)
template<typename Rel, typename T> requires requires(const Rel& r, const T& x) { { r(x, x) } -> std::convertible_to<bool>; { successor(x) } -> std::convertible_to<T>; }
constexpr bool	dedekind::category::transitive_on (const Rel &rel, const T &lo, const T &hi)
template<typename T>
constexpr std::size_t	dedekind::category::chain_length (const T &lo, const T &hi)
	The number of values from lo to hi by the carrier's successor; 0 when hi is not reached within chain_walk_budget (the top, a fixpoint of the step, short of hi).
constexpr bool	dedekind::category::fits_budget (std::size_t n, std::size_t arity)
	Whether a law of arity variables on a chain of n values fits law_evaluation_budget.
template<typename Whole> requires requires { whole.operator->(); }
constexpr auto	dedekind::category::arrow_drill_down (const Whole &whole)
	Generic opt-in drill-down projector for part-whole wrappers.
template<typename T>
constexpr T	dedekind::category::arrow_drill_down (const T *whole)
	Pointer overload for generic drill-down projection.

Variables
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_reflexive_v = is_reflexive<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_transitive_v = is_transitive<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_antisymmetric_v = is_antisymmetric<T, Rel>::value
template<typename T, typename Rel>
constexpr bool	dedekind::category::is_connex_v = is_connex<T, Rel>::value
constexpr std::size_t	dedekind::category::chain_walk_budget = 1024
	The walk budget of a discrete bounded chain: a chain is decided only when its top is reached from its bottom within this many steps (a machine word is a discrete bounded chain too, but 2⁶⁴ steps is no compile-time decision).
template<std::integral T>
constexpr bool	dedekind::category::is_reflexive_v< T, std::less_equal<> > = true
	Proof: <= on the integral types is a total order (reflexive, transitive, antisymmetric, connex), under the transparent spelling as under the typed one above.
template<std::integral T>
constexpr bool	dedekind::category::is_transitive_v< T, std::less_equal<> > = true
template<std::integral T>
constexpr bool	dedekind::category::is_antisymmetric_v< T, std::less_equal<> > = true
template<std::integral T>
constexpr bool	dedekind::category::is_connex_v< T, std::less_equal<> > = true
constexpr std::size_t	dedekind::category::law_evaluation_budget = std::size_t{1} << 16
	The evaluation budget of a law: a law of k variables on a chain of n values costs nᵏ evaluations, and is decided only within this (reflexivity on a long chain, transitivity only on a short one).
template<typename Rel>
constexpr bool	dedekind::category::detail_mereology::chain_order
template<typename T>
constexpr bool	dedekind::category::is_idempotent_v< T, Sup > = true
template<typename T>
constexpr bool	dedekind::category::is_associative_v< T, Sup > = true
template<typename T>
constexpr bool	dedekind::category::is_commutative_v< T, Sup > = true
template<typename T>
constexpr bool	dedekind::category::is_idempotent_v< T, Inf > = true
template<typename T>
constexpr bool	dedekind::category::is_associative_v< T, Inf > = true
template<typename T>
constexpr bool	dedekind::category::is_commutative_v< T, Inf > = true
template<typename T>
constexpr bool	dedekind::category::is_distributive_v< T, Sup, Inf > = true
template<typename T>
constexpr bool	dedekind::category::is_distributive_v< T, Inf, Sup > = true
template<typename T>
constexpr bool	dedekind::category::is_absorptive_v< T, Sup, Inf > = true
template<typename T>
constexpr bool	dedekind::category::is_absorptive_v< T, Inf, Sup > = true

Detailed Description

Embryonic Mereology (Part-Whole and Skew Algebraic Core).

@partition :mereology

Following the formal axiomatization of Stanisław Leśniewski, this partition introduces the "Part-Whole" relation as a foundational structural primitive. In this stage we define: 1) the primitive part-whole relation (and its order-style axioms), and 2) the non-commutative (skew) maturation ladder for meet/join operations.

Commutative, order-theoretic semilattice/lattice refinements are layered in :posetal to keep order-theory nomenclature and laws localized there.

mereology__Axioms

1. Reflexivity: Everything is a part of itself.
2. Transitivity: A part of a part is a part of the whole.
3. Antisymmetry: Two distinct things cannot be parts of each other.

See also

Leśniewski-style mereology overview: https://plato.stanford.edu/entries/mereology/

Skew lattice background (non-commutative generalization): https://en.wikipedia.org/wiki/Skew_lattice

Copyright

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

Note

"It remains to discuss briefly what general requirements may be justly laid down for the solution of a mathematical problem. I should say first of all, this: that it shall be possible to establish the correctness of the solution by means of a finite number of steps." – David Hilbert, Mathematical Problems (1900)

Variable Documentation

chain_order

template<typename Rel>

bool dedekind::category::detail_mereology::chain_order

inlineconstexpr

Initial value:

=
    IsReflexive<D4, Rel> && IsTransitive<D4, Rel> && IsAntisymmetric<D4, Rel> &&
    IsConnex<D4, Rel>