D
Domain Algebra Official Site
Preprint Overview

Domain Algebra

We formalize Domain Algebra as a fibered $\omega$-CPO equipped with a domain-indexed endofunctor whose least fixed point defines semantics.我们将 Domain Algebra 形式化为一个带有域索引自函子的纤维化 $\omega$-CPO,其最小不动点给出语义。

A representation functor into vector spaces preserves this structure, yielding a strict correspondence between symbolic closure and differentiable fixed-point computation.到向量空间的表示函子保持这一结构,从而在符号闭包与可微不动点计算之间建立严格对应。

Abstract least fixed point semantics最小不动点语义
Base底层 fibered $\omega$-CPO over domains定义在域上的纤维化 $\omega$-CPO
Operator算子 domain-indexed endofunctor $T_d$域索引自函子 $T_d$
Correspondence对应 symbolic closure $\leftrightarrow$ differentiable fixed points符号闭包 $\leftrightarrow$ 可微不动点
Claim

The homepage states the formal core first: semantic locality, structure-preserving representation, and fixed-point identity across symbolic and differentiable substrates.首页首先陈述形式核心:语义局部性、保持结构的表示,以及符号基底与可微基底之间的不动点同一性。

Definition 0.1 Domain Operator域算子

@D

The @ operator binds a relation to a domain, making the domain constitutive of meaning rather than an external label. Truth is always evaluated locally within a fiber $Q_d$ and never in an abstract global space. $(D, \leq)$ forms a complete Heyting algebra, supporting intuitionistic semantics where “true” means “construction completed within this domain.”@ 算子把关系绑定到一个域上,使域成为意义的构成部分,而不是外加标签。真值总是在纤维 $Q_d$ 内局部判定,而不会在抽象的全局空间中求值。$(D, \leq)$ 构成一个完备 Heyting 代数,支撑直觉主义语义,其中“真”意味着“在该域内构造已经完成”。

Definition 0.2 Domain-Bound Relation域绑定关系

r@D

A relation carries no meaning independent of its domain. $r@d_1$ and $r@d_2$ are distinct semantic objects whenever $d_1 \neq d_2$. The symbolic layer writes $\langle c, r@d, c' \rangle$ as an admissible quadruple. The differentiable layer preserves this structure through a representation functor $\hat{\varphi}_d$ satisfying $\hat{\varphi}_d \circ T_d = \widetilde{T}_d \circ \hat{\varphi}_d$ so the closure operator commutes with the mapping. Both compute the same fixed point.关系不携带任何独立于域的意义。只要 $d_1 \neq d_2$,那么 $r@d_1$ 与 $r@d_2$ 就是不同的语义对象。符号层将 $\langle c, r@d, c' \rangle$ 写作一个可容许四元组。可微层通过表示函子 $\hat{\varphi}_d$ 保持这一结构,并满足 $\hat{\varphi}_d \circ T_d = \widetilde{T}_d \circ \hat{\varphi}_d$,也就是闭包算子与映射可交换。两层计算得到同一个不动点。

Definition 0.3 Primitive Quadruple原始四元组
$$\langle c, r, c', d \rangle \in Q$$

The admissible quadruple is the minimal writable unit of the system. All computation, including closure iteration, fixed-point convergence, admissibility checking, and cross-domain reindexing, is built from this single primitive. Under intuitionistic semantics, writing a quadruple is constructing a proof; truth is not assigned after the fact but realized in the act of construction. Four substrates, Prolog, matrix iteration, attention, and memristive crossbar, implement the same algebraic structure without modification.这个可容许四元组是系统中最小的可写单元。所有计算,包括闭包迭代、不动点收敛、可容许性检查和跨域重索引,都由这一原语构成。在直觉主义语义下,写入一个四元组就是在构造一个证明;真值不是事后赋予的,而是在构造行为中实现的。Prolog、矩阵迭代、注意力机制和忆阻交叉阵列这四种基底都可以在不修改代数结构的前提下实现同一个系统。

Structural Summary

Three formal correspondences.三个形式对应。

The homepage is organized around three mathematical commitments: local semantic order in fibers, structure-preserving representation into vector spaces, and exact agreement of symbolic and differentiable fixed points.首页围绕三个数学承诺组织:纤维中的局部语义序、到向量空间的结构保持表示,以及符号不动点与可微不动点之间的精确一致。

fibered $\omega$-CPO representation functor commuting closure fixed-point equivalence
Correspondence I

Fibered $\omega$-CPO纤维化 $\omega$-CPO

Each domain determines a local semantic order and supports monotone iteration toward a least fixed point. Semantics is therefore generated inside fibers rather than projected from a global truth table.每个域决定一个局部语义序,并支持朝向最小不动点的单调迭代。因此语义是在纤维内部生成的,而不是从一个全局真值表投影下来。

Correspondence II

Representation Functor表示函子

The map into vector spaces is not an approximation layer added later. It preserves the same operator structure, so symbolic closure and differentiable update live in strictly corresponding diagrams.到向量空间的映射不是事后附加的近似层。它保持同一算子结构,因此符号闭包和可微更新位于严格对应的交换图中。

Correspondence III

Shared Fixed Point共享不动点

What the symbolic layer reaches by admissible closure is exactly what the differentiable layer reaches by fixed-point convergence. The two substrates differ operationally, but not semantically.符号层通过可容许闭包所达到的结果,正是可微层通过不动点收敛所达到的结果。两种基底在操作上不同,但在语义上并不分离。

Axiomatics

A1–A10 as the formal specification.A1–A10 作为形式规约。

The axiom cards below are styled as a compact specification surface: each statement names one invariant, one semantic role, and one algebraic commitment inside the system.下面的公理卡片被组织成紧凑的形式规约界面:每条陈述都对应一个不变量、一个语义角色和一个代数承诺。

“No domain, no independent meaning.”

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}$$
Reading Paths

Three ways to enter the theory.三种进入这套理论的方式。

From the homepage, readers can continue into the paper line, the interactive demonstrations, or the author and research context.从首页出发,读者可以继续进入论文线、交互演示线,或作者与研究背景部分。

Homepage → Paper → Experience → Author