Domain Algebra: An Axiomatic Framework for Well-Founded Relational ComputationDomain Algebra：良基关系计算的公理化框架

We present Domain Algebra (DA), an axiomatic framework built around a single semantic operator, @D. In DA, the domain $d$ is not external metadata applied to a relation; it is constitutive of the relation's meaning.我们提出 Domain Algebra（DA），这是一个围绕单一语义算子 @D 建立的公理化框架。在 DA 中，domain $d$ 不是附加在关系上的外部元数据，而是关系意义的构成部分。

The assertion $\langle c, r@d, c' \rangle$ does not mean “$r(c,c')$ holds, annotated with domain $d$”; it means that $r$ under $d$-semantics relates $c$ to $c'$. This operator bridges two mathematical traditions: on the logical side, it induces Heyting semantics in which truth is constructive completion within a domain; on the geometric side, it instantiates Grothendieck-style relativization through a fibered structure $F : D^{op} \to C$, with Lawvere's hyperdoctrine providing the common language of both.断言 $\langle c, r@d, c' \rangle$ 的含义不是“$r(c,c')$ 成立，并带有域 $d$ 的标注”；它的含义是：在 $d$ 语义下的关系 $r$ 将 $c$ 与 $c'$ 联系起来。这个算子连接了两条数学传统：在逻辑侧，它诱导出 Heyting 语义，其中真值是在域内的构造性完成；在几何侧，它通过纤维结构 $F : D^{op} \to C$ 实现 Grothendieck 式相对化，而 Lawvere 的 hyperdoctrine 则提供了统一两侧的共同语言。

We establish ten axioms (A1-A10) and prove four main results: a four-way equivalence between well-foundedness, termination, normalization, and admissibility; precise capture of the self-application-free fragment of $\lambda$-calculus; a categorical characterization of self-application as non-well-founded endomorphism in a CCC; and a proof that the domain lattice forms a Grothendieck fibration with Heyting fibers. Base independence further shows that any structure-preserving realization yields identical computation results.我们建立十条公理（A1-A10），并证明四个主要结果：良基性、终止性、规范化与 admissibility 之间的四重等价；对不含自应用的 $\lambda$ 演算片段的精确刻画；把自应用表述为 CCC 中的非良基端同态的范畴论刻画；以及证明 domain lattice 构成带 Heyting 纤维的 Grothendieck 纤维化。base independence 进一步表明，任何保持结构的实现都会给出相同的计算结果。