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 exists a functor $R : \mathcal{C} \times \mathcal{C} \to \mathcal{L}$, where $\mathcal{L}$ is a Heyting algebra. $R(c,c')$ is the truth-value space of relations from $c$ to $c'$.存在函子 $R : \mathcal{C} \times \mathcal{C} \to \mathcal{L}$,其中 $\mathcal{L}$ 为 Heyting 代数。$R(c,c')$ 给出从 $c$ 到 $c'$ 的关系真值空间。
$$R(c,c') \in \mathcal{L}$$
A3Domain Lattice
Domain Lattice
There exists a complete lattice $(D, \leq)$ with a fibration $F : D^{op} \to \mathcal{C}$, where each fiber $Q_d$ is the category of assertions valid in domain $d$.存在一个完备格 $(D, \leq)$,并有纤维化 $F : D^{op} \to \mathcal{C}$,其中每个纤维 $Q_d$ 是在域 $d$ 中成立的断言范畴。
$$F(d)=Q_d,\quad Q_d \hookrightarrow C \times R \times C$$
A4Basic Operation
Basic Operation
The primitive computation unit is the admissible quadruple $\langle c, r, c', d \rangle$. If two paths lie in the same $Q_d$, they compose inside that domain.原始计算单位是可容许四元组 $\langle c, r, c', d \rangle$。若两段路径都位于同一 $Q_d$ 中,则它们可在域内复合。
$$\langle c,r_1,c_1,d\rangle,\langle c_1,r_2,c',d\rangle \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$, and path composition must correspond semantically to meet.每个纤维 $Q_d$ 配备估值态射 $\nu_d : Q_d \to \Omega_d$,并要求路径复合在语义上对应 meet。
$$\nu_d(r_1\circ \cdots \circ r_k)=\nu_d(r_1)\wedge \cdots \wedge \nu_d(r_k)$$
A8Base Independence
Base Independence
Any two realizations preserving Heyting operations, the Galois connection, and valuation must agree on the result of the same computation term.任意两个保持 Heyting 运算、Galois 连接和估值的实现,对同一计算项给出相同结果。
$$\Phi_1(\mathrm{Comp}_d(t)) = \Phi_2(\mathrm{Comp}_d(t))$$
A9Minimal Invariant
Minimal Invariant
Every computation can be expressed as a finite composition of basic operations, so the model keeps its computational invariant at the minimal path level.每个 computation 都能表达为有限个 basic operations 的复合,因此模型的计算不变量保持在最小的路径层级。
$$\mathrm{comp}=\left(c_0 \xrightarrow{r_1@d_1} c_1\right)\circ \cdots \circ \left(c_{n-1} \xrightarrow{r_n@d_n} 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}$$