nanobind_pst.cpp File Reference

Nanobind extension module for Pst: the truth chains (#1001) and the sets over them, per the paper's Lwv grammar (#975). More...

#include <nanobind/nanobind.h>
#include <nanobind/stl/optional.h>
#include <nanobind/stl/string.h>
#include <compare>
#include <concepts>
#include <cstddef>
#include <cstdint>
#include <exception>
#include <functional>
#include <limits>
#include <optional>
#include <string>
#include <string_view>
#include <type_traits>
#include <typeinfo>
#include <utility>
#include <variant>
#include <vector>
import dedekind.category;
import dedekind.algebra;
import dedekind.morphologies;
import dedekind.order;
import dedekind.relational;
import dedekind.sequences;
import dedekind.sets;

Include dependency graph for nanobind_pst.cpp:

Concepts
concept	@156131220235120362223174356105005245200156001166::pst::IsTruthChain
	A truth chain the queries can read: a Pst carrier that is finite by its representation and has the covering step.

Functions
void	bind_readings (nb::module_ m)
	The readings of a term, as free functions: dom(R), classifier(S), codomain(S) …, one spelling, as ap reads _ap. Each class provides the private attribute _name it answers; a value without it is no term the reading applies to (#1054).
	NB_MODULE (_pst, m)

Detailed Description

Nanobind extension module for Pst: the truth chains (#1001) and the sets over them, per the paper's Lwv grammar (#975).

Copyright

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

Description

\(\mathbf{Pst} = \mathbf{Jlt} \cap \mathbf{Chain}\) (paper §3), bound as the private native extension pynzli._pst (re-exported by pynzli.pst). A universe is A(T), the set of every value of a carrier type: B = A(bool) and K3 = A(Ternary), the universes over the two truth chains, carry the chain's order (endpoints, the step in both readings, the order, the classification, the unfold by the cover); U64 = A(u64) and GF_p = A(𝔽ₚ) are the ring's and the field's. The sets over 𝔹 and K₃ are the chain fragment of the Lwv grammar: generators A(T) / Ø(T) / η(v), the former U & (π > v), the lattice & | ^ ~, membership x in S / ap(S, x), the queries == and <= answering in the set's own species (Unknown is a verdict), the quantifiers exists / forall (also any / all), and the normal form runs. Every handle over a truth chain is a run list (order:runs), the library's normal form of these sets, valued in its species; every operator and every query is the library's, on it. Two species of one carrier mix in their join (𝔹 ↪ K₃): a Boolean set beside a K₃-valued one is met, joined and compared in K₃. Different carriers do not mix. The canonical ring and field are bound beside them (#1019): u64 (ℤ/2⁶⁴: + − · wrap, // and % by a nonzero word) and 𝔽ₚ (Fp, Modular<2⁶⁴ − 59>: + − · /, no order), with their universes A(u64) and A(𝔽ₚ); an element equals the int it represents. The term surface (#1006) builds terms over π / π_1 / π_2 that A(carrier) | term and A(carrier) * A(carrier) | term bind, every operator and constant checked then; those sets and relations hold the bound term (a comprehension) and are read pointwise. Reduction stays in C++; Python holds handles.