lattice.cppm File Reference

Order-theoretic meet / join / lattice structures. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <type_traits>
import dedekind.category;

Include dependency graph for lattice.cppm:

Classes
struct	dedekind::order::bit_subset_eq< T >
	Integral carriers under the bitwise Boolean algebra (#710). More...
struct	dedekind::category::is_reflexive< T, dedekind::order::bit_subset_eq< T > >
struct	dedekind::category::is_transitive< T, dedekind::order::bit_subset_eq< T > >
struct	dedekind::category::is_antisymmetric< T, dedekind::order::bit_subset_eq< T > >
struct	dedekind::category::is_directed< T, dedekind::order::bit_subset_eq< T > >
struct	dedekind::category::is_codirected< T, dedekind::order::bit_subset_eq< T > >
struct	dedekind::category::HeytingExponential< T, dedekind::order::bit_subset_eq< T >, std::bit_and< T > >
	HeytingExponential specialisation for the bitwise Boolean lattice (#710): on integral T (excluding bool — see caveat below) under bit_subset_eq with std::bit_and as meet, the relative complement a → b = ~a | b (Boolean Heyting), and the eval morphism e(x) = e & x (meet). Required so IsHeytingLatticeCategory fires at row 6 of the Form-chain for this Rel / Meet pairing. More...
struct	dedekind::category::LatticeBottom< T, dedekind::order::bit_subset_eq< T > >
	Bitwise-lattice bottom: the all-zeros bitmask. More...
struct	dedekind::category::LatticeTop< T, dedekind::order::bit_subset_eq< T > >
	Bitwise-lattice top: the all-ones bitmask. More...
struct	dedekind::category::is_complement< std::bit_not< T >, T, dedekind::order::bit_subset_eq< T >, std::bit_or< T >, std::bit_and< T > >
	Canonical specialisation: std::bit_not<T> is the complement for the bitwise Boolean lattice on integral T (excluding bool — see caveat). Complement laws hold structurally: a & ~a = 0 (bottom) and a | ~a = ~T(0) (top). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::order::HasLatticeOperators
	Pure syntactic shape: T supports the bitwise / lattice operators &, |, ^, ~ with results convertible to T.
concept	dedekind::order::IsOrderMeetSemilattice
	Re-export the certified meet-semilattice stage from :posetal.
concept	dedekind::order::IsOrderJoinSemilattice
	Re-export the certified join-semilattice stage from :posetal.
concept	dedekind::order::IsOrderLattice
	Bundled lattice witness: the strict commutative-ring proof under (std::bit_xor<T>, std::bit_and<T>) AND the bitwise/lattice operator surface on T, by definition.
concept	dedekind::order::IsOrderDistributiveLattice
	Re-export the certified distributive lattice stage from :posetal.

Functions
template<typename T, typename Step> requires std::is_integral_v<T>
constexpr T	dedekind::order::bit_closure (T seed, Step step)
	Reachability / the universal-algebra "generated by", over the power-set lattice: the reflexive-transitive closure of a bitmask seed under a one-step adjacency step — the least bitmask ⊒ seed (in bit_subset_eq) that is closed under step, i.e. ⨆ₙ stepⁿ(seed) with join the lattice's own bit_or. It is the Boolean instance of the generic closure (category:functor) over this lattice; decidable because the finite bit-carrier stabilises. Reusing it: reachability of a graph whose nodes are bit positions and step is the adjacency.

Variables
constexpr auto	dedekind::order::detail_bit_closure::edge_step
template<typename T>
constexpr bool	dedekind::category::is_absorptive_v< T, std::bit_or< T >, std::bit_and< T > >
	Algebra-trait specialisations for std::bit_or<T> / std::bit_and<T> on specific integral T (#710).
template<typename T>
constexpr bool	dedekind::category::is_absorptive_v< T, std::bit_and< T >, std::bit_or< T > >

Detailed Description

Order-theoretic meet / join / lattice structures.

@partition :lattice

Copyright

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

order_lattice__Scope

Species carrying binary meet and/or join operations that respect the underlying order, reaching up to distributive lattices. The actual axiomatic certification (associativity, commutativity, idempotence, absorption, distributivity) lives in dedekind.category:posetal as IsCertifiedOrder{Meet,Join}Semilattice etc.; this partition re-exports those witnesses under the order-theoretic names a mathematician expects to find alongside posets and chains.

Wikipedia: Semilattice, Lattice (order), Distributive lattice.

Note

"Lattice theory provides the appropriate generality for the algebraic study of order, just as group theory does for symmetries." [Trans: original is English; the gloss is that meet (∧) and join (∨) play the same role for partial orders that the group operation plays for symmetry groups.] — Garrett Birkhoff, Lattice Theory (3rd ed., AMS Colloquium Publications vol. 25, 1967), Preface. Birkhoff's monograph is the canonical reference for the meet/join axiomatics this partition re-exports under the names mathematicians expect to find next to chains and posets.

Variable Documentation

edge_step

auto dedekind::order::detail_bit_closure::edge_step

inlineconstexpr

Initial value:

= [](unsigned s) -> unsigned {
  unsigned out = 0;
  if (s & 0b0001u) out |= 0b0010u;  
  if (s & 0b0010u) out |= 0b0100u;  
  if (s & 0b0100u) out |= 0b1000u;  
  return out;
}