These ten axioms fix what must be preserved under composition and closure - not how it is stored. The unit $\langle c, r, c', d \rangle$ is a notation, in the way that $\Gamma \vdash e : \tau$ is a notation: no compiler stores triples on account of it. A8 is the axiom that keeps expression and carrier apart.这十条公理规定的是:在合成与闭包之下,什么语义结构必须保持不变,而不是它如何被存储。$\langle c, r, c', d \rangle$ 是一种记法,正如 $\Gamma \vdash e : \tau$ 是一种记法:没有哪个编译器因此在内存里存三元组。A8 正是把表达与载体分开的那条公理。
Axioms as stated in Domain Algebra: An Axiomatic Framework for Well-Founded Relational Computation, version 1.0 (updated 2026-09-09).公理表述依据《Domain Algebra:良基关系计算的公理化框架》第 1.0 版(更新于 2026-09-09)。
A1Concept Category
Concept Category
There exists a Heyting category $\mathcal{C}$ with finite limits, power objects, and internal Heyting structure. Its objects are called concepts.存在一个 Heyting 范畴 $\mathcal{C}$。它有有限极限、幂对象与内部 Heyting 结构,范畴中的对象统一称为 concepts。
$$\mathcal{C}\text{ is a Heyting category}$$
A2Relation Functor
Relation Functor
There is a set $\mathcal{R}$ of relation symbols. Their semantics is given by a functor $\rho : \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{L}$ into a Heyting algebra $\mathcal{L}$, where $\rho(c,c')$ is the truth-value space of relations from $c$ to $c'$. A quadruple carries the symbol; the valuation of A7 reads off the value.存在关系符号集合 $\mathcal{R}$。其语义由函子 $\rho : \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{L}$ 给出,其中 $\mathcal{L}$ 是 Heyting 代数,$\rho(c,c')$ 是从 $c$ 到 $c'$ 的关系真值空间。四元组携带的是符号,A7 的赋值读出的是取值。
$$r \in \mathcal{R},\quad \rho(c,c') \in \mathcal{L}$$
A3Domain Lattice
Domain Lattice
The domains form a frame (complete Heyting algebra) $(D, \leq)$, together with an indexed category $F : D^{op} \to \mathrm{Cat}$ whose value at $d$ is the fiber $Q_d$ of assertions valid in $d$. The fibration is its Grothendieck construction. Joins glue: the fiber over $d_1 \vee d_2$ carries exactly the constraints of both.Domain 构成一个 frame(完备 Heyting 代数)$(D, \leq)$,并配有 indexed category $F : D^{op} \to \mathrm{Cat}$,其在 $d$ 处的取值是 fiber $Q_d$,即在 $d$ 中成立的断言。fibration 是它的 Grothendieck 构造。join 处发生黏合:$d_1 \vee d_2$ 上的 fiber 恰好承载两者的约束。
$$F(d)=Q_d \hookrightarrow \mathcal{C} \times \mathcal{R} \times \mathcal{C},\quad \int F \to D\text{ is a fibration}$$
A4Basic Operation
Basic Operation
The primitive computation unit is the admissible quadruple $\langle c, r, c', d \rangle$. Each domain carries a composability predicate $\mathrm{comp}_d$ specifying which ordered relation pairs may compose. Two head-to-tail paths in the same $Q_d$ compose only if the pair is licensed; otherwise the composite is undefined and no quadruple is derived. $(Q_d, \circ)$ is therefore a partial category.最小计算单位是可容许四元组 $\langle c, r, c', d \rangle$。每个 domain 带有一个可合成性谓词 $\mathrm{comp}_d$,规定哪些有序关系对允许合成。同一 $Q_d$ 内首尾相接的两条路径,只有在该关系对被许可时才合成;未被许可则合成无定义,不产生任何四元组。因此 $(Q_d, \circ)$ 是偏范畴而非范畴。
$$\langle c,r_1,c_1,d\rangle,\langle c_1,r_2,c',d\rangle,\quad (r_1,r_2) \in \mathrm{comp}_d \Rightarrow \langle c,r_1\circ r_2,c',d\rangle$$
A4cClosure Composition
Closure Composition
The Galois closure $\mathrm{cl}_d$ is closed under path composition. Closure preserves not only points, but also the path structure derived from them.Galois 闭包 $\mathrm{cl}_d$ 对路径复合封闭。闭包不仅保存点,还保存由这些点导出的路径结构。
$$\mathrm{cl}_d(S)\text{ is closed under }\circ$$
A5Admissibility
Admissibility
Admissibility is determined by whether the dependency graph of the closure is acyclic. Equivalently, any endomorphic cycle makes the write inadmissible.可容许性由闭包依赖图是否无环决定。等价地,若存在任何端同态循环,则该写入不可容许。
$$\mathrm{Adm}_d(S) \iff G(\mathrm{cl}_d(S))\text{ is acyclic}$$
A6Galois Closure
Galois Closure
For each domain $d$, the family of closed sets $L_d$ forms a complete lattice, and the Galois connection $(\alpha_d, \gamma_d)$ induces the closure operator $\mathrm{cl}_d$.对每个域 $d$,闭合集族 $L_d$ 构成完备格,并由 $(\alpha_d, \gamma_d)$ 给出 Galois 连接,诱导闭包算子 $\mathrm{cl}_d$。
$$\mathrm{cl}_d = \gamma_d \circ \alpha_d$$
A7Intuitionistic Semantics
Intuitionistic Semantics
Each fiber $Q_d$ carries a valuation morphism $\nu_d : Q_d \to \Omega_d$. On every licensed path, composition corresponds to meet, so $\nu_d$ is a homomorphism from the licensed partial path algebra into $(\Omega_d, \wedge)$: derived knowledge is never more certain than its premises.每个 fiber $Q_d$ 带有赋值态射 $\nu_d : Q_d \to \Omega_d$。在每条被许可的路径上,合成对应 meet,因此 $\nu_d$ 是从被许可的偏路径代数到 $(\Omega_d, \wedge)$ 的同态:导出的结论不会比它的前提更确定。
$$\nu_d(r_1\circ \cdots \circ r_k)=\nu_d(r_1)\wedge \cdots \wedge \nu_d(r_k)\quad \text{for licensed paths}$$$$\nu_d(r_1\circ \cdots \circ r_k)=\nu_d(r_1)\wedge \cdots \wedge \nu_d(r_k)\quad \text{仅对被许可路径}$$
A8Base Independence
Base Independence
A realization assigns to each fiber a carrier together with a closure operator and a valuation, such that two squares commute: closure commutes with the carrier map, and valuation factors through a Heyting embedding. Any two realizations agree on every computation term. Symbol tables, matrices, attention, and hardware are carriers, not competing systems.一个 realization 为每个 fiber 指定一个载体,连同其上的闭包算子与赋值,并要求两个方块交换:闭包与载体映射交换,赋值经由一个 Heyting 嵌入分解。任意两个 realization 在每个计算项上一致。符号表、矩阵、attention、硬件都是载体,不是彼此竞争的系统。
$$\Phi \circ \mathrm{cl}_d = \mathrm{cl}_d^\Phi \circ \Phi,\quad \Phi_1(\mathrm{Comp}_d(t)) \cong \Phi_2(\mathrm{Comp}_d(t))$$
Realizations:对应载体:
A9Minimal Invariant
Minimal Invariant
Every computation is a finite composite of basic operations along licensed paths within one domain, so the model keeps its computational invariant at the minimal path level.每个计算都是单个 domain 内沿被许可路径的基本操作的有限合成,因此模型在最小路径层面保持其计算不变量。
$$\mathrm{comp}=\left(c_0 \xrightarrow{r_1@d} c_1\right)\circ \cdots \circ \left(c_{n-1} \xrightarrow{r_n@d} c_n\right)$$
A10Domain Specialization
Domain Specialization
For each domain $d$, $\mathrm{Adm}_d$ is decidable at write-time and compatible with that domain's algebraic structure. Domain-specific rules are instances of A5.对每个域 $d$,$\mathrm{Adm}_d$ 在写入时可判定,并与该域自身的代数结构兼容。域特定规则都是 A5 的实例。
$$\mathrm{Adm}_d\text{ is decidable at write-time}$$