程序超图:面向几何代数、空间计算与物理感知编译的多元关系结构
The Program Hypergraph: Multi-Way Relational Structure for Geometric Algebra, Spatial Compute, and Physics-Aware Compilation
https://arxiv.org/pdf/2603.17627


摘要
先前关于维度类型系统与确定性内存管理的工作所引入的程序语义图(PSG),将编译相关属性编码为计算节点之间的二元边关系。该表示法对标量与张量计算是充分的,但对于异构计算中日益成为核心的两类问题,在结构上已显不足。第一类,在面向空间数据流加速器的语境中被认识到,是NPU架构中的瓦片共置与路由约束本质上是多元的:它们共同作用于操作集合,且无法被正确分解为独立的成对约束。第二类,范围更广且影响更深,是几何代数计算(具体而言,是构成克利福德代数神经网络、物理模拟以及基于网格的有限元分析基础的分次多元积)若仅被表示为二元操作序列,则无法在不损失代数恒等性且不累积可避免数值误差的情况下得到忠实表示。
本文引入程序超图(PHG)作为PSG的原则性推广,将二元边提升为任意元数的超边。我们证明,克利福德代数中的阶是现有DTS阿贝尔群框架内的一个自然维度轴;由阶推断导出的几何积稀疏性消除了针对克利福德代数神经网络的主要性能质疑,且无需人工特化;网格拓扑的k-单纯形结构是将超边形式体系应用于几何计算的一个直接实例。我们评估了现有的几何代数库生态系统,识别出当前系统均未解决的一致类型论缺口,并表明PHG在Fidelity编译框架内填补了这一缺口。其实际结果是形成一个编译框架,其中几何正确性、内存放置、数值精度选择与硬件划分均可从单一图结构中联合推导得出,该图结构由语言服务器作为交互式设计时反馈予以提供。
1. 引言
1.1 二元边的边界
文献[10]中引入的程序语义图(Program Semantic Graph)将计算编码为一个有向图,其中节点表示值与计算,边表示数据依赖关系,而边的注解则携带维度、共效应(coeffect)与生命周期信息。该结构对于现有Clef/Fidelity框架所面向的那类计算是充分的:标量算术、张量运算、内存管理的数据结构,以及通过MLIR实现的多目标降级(lowering)。
两类问题暴露了二元边模型的结构局限性。第一类是在异构硬件映射的语境中被认识到的;第二类则是通过与几何代数研究社区的互动而引入的,其范围更广,且其影响远远超出了最初催生该问题的编译问题本身。
第一类是空间数据流架构映射。AMD XDNA 2 NPU将AI引擎瓦片排列成二维网格,并通过DMA与可配置互连实现由程序员显式管理的数据移动[19]。将计算子图映射至该架构,需要将操作集合共置于瓦片上、配置瓦片组之间的路由,并将列划分为空间工作负载上下文。瓦片放置约束并非两个节点之间的约束;它是对必须驻留于同一瓦片或同一列内的节点集合所施加的约束。自然的形式体系是连接共置集合所有成员的超边。二元边团在语义上是不正确的:它断言每一对必须独立地共置,而这并不能推导出所有成员共同共置。
第二类是几何代数计算,且迄今为止是内涵更为丰富的领域。两个多重向量的几何积是双线性的;作为一种二元关系,它似乎契合现有的图模型。问题不在于孤立的乘积,而在于由乘积构建的复合运算。两个子空间的交(meet)、三个点的联结(join)形成平面、四个平面交于一点:这些是具有三个或更多语义上不可分割输入的操作。将三元联结分解为二元联结序列会引入毫无几何意义的中间节点,无法为其分配良类型的阶注解,并在每个中间步骤累积浮点误差。“三个点的联结构成一个平面”这一代数恒等式,是关于三元关系的单一事实;将其编码为两个连续的二元关系会丢失这一恒等性。
这第二类问题的重要性远远超出了眼前的编译问题。几何代数,更广义地说是克利福德代数,为物理模拟、机器人学、流体动力学、相对论电动力学以及基于网格的有限元分析提供了一个与坐标无关的框架。新兴的几何代数神经网络领域利用此结构进行等变学习,并在物理模拟基准测试中展现了最先进的性能[20, 25]。PHG为该领域提供了编译基础设施,开辟了一条从几何代数研究社区的理论进展通向定义科学计算实践前沿的异构硬件目标的道路。
这两个问题指向了相同的结构需求:将二元边推广为任意元数的关系。
1.2 贡献
本文提出四项主张,按所遇驱动问题被识别与确认的顺序依次阐述。
1.3 范围与背景
本文所描述的系统是对文献[10]中引入的 Clef 编程语言与 Fidelity 编译框架的扩展。DTS 与 DMM 系统的所有形式属性均作为已知前提,不再赘述。第 3 节中的几何代数分析假设读者具备研究生入门课程水平的克利福德代数知识;在涉及编译论证的关键处,对特定代数(PGA、CGA)的处理是自包含的。
Fidelity 编译流水线通过一个标准的 MLIR 中间端(Composer)对 Clef 源代码进行编译,该中间端扇出至多条后端路径:面向 CPU、GPU、MCU 及 WebAssembly 目标的 LLVM;面向 FPGA 综合的 CIRCT;以及面向 AI Engine 架构的 MLIR-AIE。图 1 展示了 PHG 在该流水线中的位置,以及三大主要应用领域如何通过它实现连接。

1.4 理论延续性:DCont/Inet 的源头
PHG 的结构动机可追溯至先前 Fidelity 框架工作 [8] 中所确立的 DCont/Inet 对偶性。该工作识别出 Clef 计算表达式在编译过程中分解为两种基本模式:针对顺序带副作用计算的 DCont(定界延续)路径,以及针对纯并行计算的 Inet(交互网)路径,在后者中操作在结构上相互独立并可同时规约。DCont/Inet 对偶性植根于每一类的代数结构。定界延续构成一个单子:它们按顺序组合,其左单位律与结合律允许编译器消除不必要的延续帧并将相邻延续融合。交互网构成一个对称幺半范畴:它们并行组合,其结合律与辫子律(braiding laws)允许编译器自由地对操作进行重组与重排序。MLIR 的 DCont 方言 [11] 与 Inet 方言 [4] 为 Fidelity 流水线中的这两条路径提供了中间表示基础设施。Olivier 模型中的 Actor 在结构上是带有区域(arena)作用域 RAII 的 DCont:每个 Actor 的消息处理器是一个在挂起点捕获的延续,而区域(arena)是该计算从其上下文中所需的共效应(coeffect)资源。Prospero 编排层管理跨 Actor 层次结构的区域生命周期,使 Actor 模型成为 DCont 模式在大规模下的零运行时实现。
PHG 以特定且必要的方向扩展了 Inet 路径。一条交互网规则在二元活跃对(active pair)上触发:即通过其主端口连接的两个代理节点。当独立规约的对象不是标量而是分次多重向量分量时,独立性结构由阶代数决定,且规约单元是一个节点 k 元组,其联合阶约束着输出。一个 p 阶元素与一个 q 阶元素的几何积是二元的,但同时会对多个输出阶产生贡献;k 个 1 阶元素的外积是 k 元的,其结果是所有 k 个输入共同决定的属性。因此,PHG 超边即是 Inet 活跃对在元数 k 上的推广,其中 k 由该领域的代数结构决定。
2. 程序超图:形式结构
2.1 从二元边到超边

2.2 超边注解决策类别

关系种类(Relational kind)。 种类(kind)字段将二元边的依赖种类推广至多元关系:几何积(geometric product)、联结(join)、交(meet)、共置(co-location)、传输(transfer)、同步屏障(synchronization barrier)或用户定义的关系算子。
可达性位向量(Reachability bitvector)。 超边携带一个位向量,每个配置的目标对应一位,指示该超边在哪些目标上是激活的。
2.3 超边的饱和语义

2.4 二元边作为退化超边

3. 几何代数作为 PHG 领域
3.1 克利福德代数入门
克利福德代数(Clifford algebra),在强调其几何解释时也称为几何代数(geometric algebra),是一个统一了几种经典结构的数学框架:向量、复数、四元数以及微分形式的外代数。这种统一不仅仅是符号上的;它揭示了这些看似独立的工具都是同一底层结构的实例,该结构由它们所作用的空间的维度和度规符号(metric signature)参数化。




为何这对编译至关重要。 多重向量的阶不仅仅是一个描述性标签;它是一个结构不变量,决定了哪些代数运算是适用的,哪些积的条目是非零的,以及结果携带何种几何意义。一种计算如果对输入应用了错误阶的积,或者丢失了中间结果的阶追踪,产生的结果要么是零(如果阶超过了代数维度),要么是处于错误阶子空间的结果(这对应于一个几何上无意义的值)。
这些正是 PHG 的阶感知类型系统在设计时(design time)检测到的错误类别。这一区分值得精确界定,因为它与大多数开发者所指的“编译时”不同。在 Fidelity 框架中,Composer 编译器通过 Lattice 作为语言服务器持续运行,PSG 细化(包括阶推断、SMT-LIB2 证明验证以及完整的注解饱和流水线)在编写源代码时执行,而非在显式调用构建时执行。阶违规会在 offending 表达式被键入的那一刻,作为开发环境中的诊断信息浮现出来,这发生在任何构建步骤之前,也发生在任何执行可能之前。习惯于 Python(其中解释器实际上是编译器,错误在运行时被发现)或习惯于传统编译语言(其中“编译时”意味着离散的构建调用)的读者,应将本文通篇的“设计时”理解为:在工程师编写代码时,作为一个无需执行的连续后台服务。正是这种能力使得 PHG 的结构保证具有实用价值,而不仅仅是理论上的可能性。
3.2 克利福德代数的分次结构



3.3 由阶推断导出的几何积稀疏性

具体存在的或缺失的阶由代数的度规符号(metric signature)决定。对于常见情形(PGA, CGA, STA),非零阶贡献完全由代数规范和操作数阶决定。
对 MLIR 生成的实际后果:代码生成遍历观察每个几何积超边上的阶约束,并选择适当的稀疏实现。对于 3D PGA 中的 1 阶乘 2 阶积,生成的 MLIR 计算 8 次乘法和 4 次加法(非零项),而不是 96 次乘法和 80 次加法(稠密凯莱表)。这是一种由 PHG 中的阶注解驱动的编译时选择,在任何 MLIR 优化遍运行之前执行。


3.5 现有几何代数库生态系统的评估
bivector.net 库目录 [26] 提供了生产级几何代数实现的代表性调查。每个库都通过以下三种机制之一来规避“阶”(grade)缺失作为一等类型级属性的问题。

模板驱动的编译时特化(Template-driven compile-time specialization)。 Versor 使用 C++ 模板元编程在编译时推导积的实现。每个多重向量类型的阶被编码在模板参数中,编译器为每个阶组合实例化特化的积实现。相对于 PHG 的局限性在于,Versor 的阶信息存在于 C++ 类型系统中,但对语言服务器不可见,未与内存放置分析集成,未用于异构目标上的表示选择,且无法与物理维度约束组合。
基于优化器的特化(Optimizer-based specialization)。 GAALOP 将符号几何代数表达式转换为针对大量目标语言(包括 C, C++, C#, CUDA, Rust 和 Julia)优化的系数级代码。GAALOP 的架构是现有系统中最接近 PHG 在几何代数方面所做工作的:它执行稀疏性分析并发出针对每个代数和目标的特化代码。关键的区别在于 GAALOP 是一个代码生成工具,而非编译流水线组件。其输出丢失了代数溯源(algebraic provenance);驱动 GAALOP 优化的阶约束并未作为注解保留在发出的代码中。
所有库的共同缺口在于,没有任何一个库将“阶”提供为一种一等类型系统属性,使其能够存活于编译器的语义图中、参与共效应(coeffect)推断、影响内存放置和表示选择,并通过语言服务器协议暴露出来。
Rust 与静态类型语言。 Rust 的类型系统支持常量泛型(const generics),原则上允许将阶编码为类型参数,但现有的工具并未将其构建为一个具备推断、维度多态性或语言服务器集成的完整阶感知类型系统。Rust 的借用检查器(borrow checker)提供了强大的生命周期保证,但没有几何阶的概念,没有维度约束传播的机制,也没有通往文献 [10] 中描述的多目标表示选择的路径。PHG 框架将此扩展至阶层面的几何正确性,两种属性可在同一语义图中联合验证。
4. 空间数据流架构与共置约束
4.1 瓦片映射问题
AMD XDNA 2 NPU 将 AI Engine 瓦片排列成二维网格。每个瓦片包含一个 VLIW(超长指令字)处理器、本地数据内存(通常为 32 KB)以及可配置的流交换互连 [19]。计算被映射到瓦片上;数据通过 DMA 在可配置互连结构上在瓦片间移动。映射问题包含两个耦合的组件:瓦片分配和路由配置。
瓦片分配问题揭示了一个本质上多元(irreducibly multi-way)的约束。考虑一个被划分为四个瓦片的矩阵乘法:瓦片 AA 加载左矩阵的一列,瓦片 BB 和 CC 执行部分点积,瓦片 DD 进行归约并存储结果。瓦片 AA、BB、CC 和 DD 形成一个连贯流水线的约束,无法分解为独立的成对约束。在 PHG 中,该流水线约束是单个超边:

4.2 超边划分:面向 FPGA 的 CIRCT 与面向 NPU 的 MLIR-AIE
共置超边形式体系适用于 Fidelity 框架的两条空间编译路径,但这两条路径在架构上是截然不同的。
CIRCT 降级(lowering)路径面向 FPGA 综合。FPGA 的可编程结构(programmable fabric)是一种空间资源:查找表、DSP 切片、块 RAM 和路由结构分布在固定的芯片拓扑上。一个 PHG 共置超边若编码了一组必须共享 DSP 级联,或者必须适应单个时钟区域以满足时序的操作,那么它正是 VLSI 超图划分算法所原生消费(consume natively)的那种多元放置约束 [12]。Fidelity 框架的 CIRCT 降级遍(pass)可以使用 PHG 共置超边作为划分约束来调用这些算法。输出作为放置指令馈送至厂商综合工具(Xilinx 的 Vivado,Intel 的 Quartus)。
MLIR-AIE 降级路径面向 XDNA 2 NPU 的 AI Engine 瓦片阵列 [1]。与 FPGA 结构不同,AI Engine 瓦片是一种固定架构:以二维网格排列的 VLIW 处理器,具有显式的、由程序员管理的基于 DMA 的数据移动。此处的共置约束是瓦片分配:哪些操作在哪些瓦片上运行,哪些 DMA 通道在它们之间传输数据,以及哪些同步屏障控制流水线。MLIR-AIE 降级遍消费超边注解,并在 AIE 方言中发出相应的瓦片内核代码、DMA 缓冲区描述符和同步原语,随后 aiecc 工具链将其编译为 NPU 二进制文件。
两条路径在编译器的中间端共享相同的 PHG 超边词汇表。区别在于共置约束在目标边界解析为何物:针对 CIRCT 的是 FPGA 结构放置指令,针对 MLIR-AIE 的是结合 DMA 路由的瓦片内核分配。
4.3 GPU 线程束级并行与阶对齐内核
GPU 计算被组织为线程束(warp,32 个同步执行的线程组)和线程块(thread block,共享共享内存的线程束组)。Flash Clifford 实现 [24] 通过将几何积计算构建为融合内核来利用这一特性,其中多重向量维度轴与线程束维度对齐:(MV DIM, BATCH SIZE, NUM FEATURES) 内存布局允许将线性层表达为批次矩阵乘法,且 MV DIM 轴直接映射到线程束通道(warp lanes)。这种布局优化是阶结构的结果:

从带有 PHG 注解的克利福德方言操作到 GPU 的降级路径并非单一的。Triton 路径提供了一种在原始 PTX 或 LLVM IR 之上运行的基于分块(tile-based)的 GPU 编程模型。Flash Clifford 的 Triton 实现表明,融合的 GELU-乘积-RMSNorm 内核很好地映射到 Triton 的分块执行模型,其中阶轴决定内层循环结构,批次轴映射到外层分块循环。面向 NVIDIA 目标的 MLIR GPU 方言到 PTX 的路径提供了一条从 MLIR 操作到 PTX 的结构化路径,而无需经过完整的 LLVM 流水线。面向 AMD 集成 GPU 架构的 MLIR-AIE 路径使 AI Engine 阵列和 RDNA GPU 核心能够在受益于混合执行的工作负载上协同工作。PHG 的每目标可达性位向量处理此划分:注解为 AI Engine 可达的操作路由至 MLIR-AIE 路径;注解为 GPU 可达的操作路由至 MLIR GPU 或 Triton 路径。
5. 物理感知计算
5.1 物理信息神经网络
物理信息神经网络(PINNs)[17] 将物理定律编码为可微损失项。DTS 框架已经提供了在编译时验证损失项维度一致性的机制。PHG 通过两种特定于物理感知计算的方式对此进行了扩展。
首先,PINN 损失函数的梯度既涉及标量神经网络激活值,也涉及物理场量。应用于物理残差项的链式法则产生了具有混合维度特性的梯度:力残差关于位置参数的梯度携带维度 N/m = kg/s²。在 PHG 中,自动微分图是一个超图,因为应用于多输入操作(如纳维-斯托克斯动量方程)的链式法则产生的梯度贡献,是与前向计算相同的操作数上的多元关系。
其次,几何域上的 PINNs 要求物理残差中的空间算子尊重域的几何结构。在 PGA 或 CGA 中,曲面度规被编码在代数的二次型 QQ 中。PHG 的阶感知类型系统可以在编译时验证应用于曲面场量的算子相对于代数的度规是保阶的。
5.2 前向模式自动微分与 Quire
文献 [10] 第 6.9 节确立了前向模式自动微分 [2] 具有特定的共效应(coeffect)签名:无激活带(activation tape),每层

辅助内存,且方向导数中的内积可通过 quire 累加器精确计算。PHG 将此分析扩展至几何代数计算。


对于代数中的多项式函数,该导数具有闭式表达式,其形式与前向计算所使用的代数运算相同。它不需要反向传递;它通过对计算图执行一次前向传递,并使用对偶数(即附加了切线分量的多重向量)进行计算。文献 [10] 第 3.5 节中的 quire 累加器语义适用于切线分量中的内积:方向导数涉及代数基与扰动方向之间的点积,而 quire 为该点积提供了精确累加。
这些特性的结合所产生的影响超出了直接的几何代数语境,值得明确陈述。激活带的消除意味着训练所需的内存不再多于推理:一台能够前向运行模型的设备现在也能对其进行训练,且无需任何与模型深度成比例的额外内存分配。这在训练发生的地点与方式上是一种类别层面的改变,而非渐进式的效率提升。

集群训练中跨工作节点的分布式梯度累加是点积的累加,这正是 quire 使其精确的操作。当前实践使用 bfloat16 或 float32 累加,并依赖跨工作节点的统计平均来管理舍入误差。借助 quire 支持的累加,跨工作节点的梯度归约是精确的,无论工作节点数量如何,仅在累加结束时舍入一次,而非每个工作节点通信步骤舍入一次。对于跨越数千个加速器和数十万步的训练运行,这消除了一个梯度的系统性噪声源,而当前框架将其视为不可约的。DTS 还在设计时验证每个专家的损失关于其参数的梯度携带正确的维度注解:在物理信息 MoE 中,每个专家专攻不同的物理域,与该专家域维度不一致的梯度更新是设计时错误,而非静默的收敛异常。
5.3 网格拓扑与流形约束
文献 [5] 中的“Clean up your Mesh”论文证明了 kk-单纯形和 kk-复形在 PGA 中具有紧凑、无坐标的表示。网格的拓扑一致性,具体而言即面共享边、边共享顶点,且所得复形为有效流形的要求,是针对单纯形集合的约束,而非针对个体对的约束。

5.4 高性能计算与 MFEM 的连接
MFEM 有限元库为在非结构化网格上使用高阶 PDE 求解器提供了一个框架,采用的是标准的基于坐标的方法:顶点是 float64 数组,单元是整数索引数组,且几何运算需要显式的坐标提取和浮点算术。PHG 框架提供了一条通往与 MFEM 兼容的表示的路径,该表示延迟了坐标提取。网格拓扑被表示为带有阶注解 PGA 多重向量的单纯形节点的超图;网格上的几何运算是基于 PGA 代数计算的,无需坐标提取;且坐标仅当求积例程需要时才被提取,此时文献 [10] 中的表示选择函数可以根据值的维度范围选择 IEEE 754、posit 或定点表示。
6. 作为设计时资源的 PHG
6.1 扩展的语言服务器协议
PSG 的语言服务器集成将维度解析、内存放置、逃逸分析诊断和跨目标传输保真度暴露为设计时视图。本文通篇刻意使用“设计时”一词,以将 Fidelity 框架的反馈模型与运行时检测(程序执行期间发现的错误)和传统编译时检测(显式调用构建时发现的错误)区分开来。在 Fidelity 框架中,Lattice 将 Composer 编译器作为持久性语言服务器进程运行。PSG 细化、PHG 饱和以及 SMT-LIB2 证明验证在源代码编辑时增量执行,在工程师编写代码时于开发环境中实时浮现诊断信息。该反馈是连续的,而非受限于构建步骤。
这对于 PHG 的几何代数诊断具有特定意义。克利福德代数计算中的阶违规(例如,在需要 1 阶向量时使用 2 阶二重向量)并非程序针对特定数据执行时发生的运行时故障。它是源代码的一种结构属性,PHG 的饱和语义会无条件地检测到它,无论程序在运行时会处理何种数据。诊断信息在违规表达式被键入的那一刻即可用。PHG 通过以下特定于几何代数的注解扩展了此设计时视图。
阶解析显示(Grade resolution display)。 PHG 中的每个多重向量类型节点都携带其已解析的阶。语言服务器将其渲染为内联注解,显示每个中间结果的阶。对于一系列 PGA 操作,工程师无需手动追踪阶,即可看到哪些操作产生标量、向量、二重向量、三重向量和伪标量。
稀疏性概况(Sparsity profile)。 对于每个几何积超边,语言服务器显示特定阶组合的非零凯莱表条目数量、稀疏实现与稠密实现中的乘法和加法次数,以及缩减百分比。如果工程师在仅需特定阶的地方使用了通用多重向量,语言服务器会显示阶模糊性带来的性能代价。
拓扑一致性诊断(Topological consistency diagnostics)。 对于网格计算,语言服务器验证所有边界一致性约束是否被编码为 PHG 超边。未使用显式边界超边构建的网格会被标记为可能拓扑不一致。
共置兼容性矩阵(Co-location compatibility matrix)。 对于空间数据流目标,语言服务器显示每个超边的每目标共置可行性:哪些目标支持所需的瓦片配置,哪些目标需要分解为更小的子图,以及每个目标上的路由拓扑形态。
6.2 设计时物理验证
对于物理信息计算,PHG 实现了二元 PSG 无法做到的设计时验证。DTS 维度约束与 PHG 阶约束的结合,允许编译器在设计时验证: • 物理损失项在维度上是良构的(DTS 验证,文献 [10] 中已确立)。 • 应用于场量的几何算子保持阶不变(PHG 阶验证)。 • 编码在网格拓扑中的边界条件在拓扑上是一致的(PHG 超边饱和)。 • 为场量选择的数值表示为每个网格单元中的预期值分布提供了足够的精度(表示选择,在文献 [10] 的基础上结合了几何域知识进行扩展)。
每项验证都是可判定的,并在设计时运行:DTS 维度一致性归约为整数环 ZZ 上的线性代数;PHG 阶一致性归约为整数算术;拓扑一致性归约为超边饱和;表示选择是基于维度范围和目标能力的编译时函数。
6.3 工程后果
本文所述的属性解决了一类错误,这类错误是高性能计算、几何机器学习和嵌入式系统工程领域的从业者反复遇到的,且往往缺乏系统性的解决方案。
阶模糊性与过度泛化的代价。 第 3 节报告的稀疏性概况并非边缘情况。在 3D PGA 中,对通用多重向量进行的几何积(在没有任何阶信息可用的情况下)需要评估

凯莱表的所有 256 个条目,其中 95% 在结构上为零。一位工程师如果在始终操作 1 阶输入的计算中使用了通用多重向量类型,就要付出 20 倍的算术开销,而这种开销在源代码层面是不可见的。语言服务器的稀疏性显示使得这一代价在类型声明处即变得可见,而非等到性能分析(profiling)在下游识别出性能回归之后。
作为编译时属性的拓扑一致性。 有限元分析、几何处理和物理模拟中基于网格的计算,常因拓扑不一致而在运行时失败:本应共享边的 T 型接头(T-junctions)、水密模型(watertight model)中缺失的面、导致重合顶点分离的数值漂移。PHG 超边对边界一致性约束的编码,将这些从运行时数值事故提升为编译时结构属性。一个拓扑不一致的网格,是一个 PHG 无法正确饱和的程序。
作为一等设计属性的跨目标保真度。 在硬件目标之间传输数值结果的系统,通常会在边界处以未被追踪或报告的方式丢失精度。扩展至 PHG 语境的 DTS 跨目标传输分析,使这些边界语义显式化:语言服务器报告在每个硬件边界处丢失或转换了何种精度。工程师可以据此做出知情决策,决定在该点是进行重新缩放(rescale)、提升(promote),还是接受该转换。
6.4 PHG 计算图的可证明性边界
一个其结构属性可以在设计时被证明、随着源代码编写持续进行、具有有界运行时间且无需执行即可验证的计算图,属于与那些属性仅在运行时被测试或通过启发式置信度验证的计算图截然不同的工程类别。本节描述的证明由 Lattice 的后台细化过程生成并验证(discharged)。它们不是事后审计;它们运行在工程师之前,随着每个表达式被添加到源代码中即对其进行认证。
习惯于通过测试确立正确性的语言的开发者应注意,这些并非测试:它们是针对所有可能输入的数学证明,是作为生成编辑器中可见类型注解的同一细化遍(elaboration pass)的副产品而产生的。阶不一致、物理损失项中的维度不匹配、超出目标资源的瓦片共置约束:每一个都在违规表达式被键入的那一刻作为诊断信息浮现于开发环境中,而非在调用构建时,也非程序针对数据运行时。Fidelity 框架中“编译时”与“设计时”的区别在于此:编译是产生工件的离散步骤;设计时细化是保持工程师知情的连续服务。两者调用相同的底层约束机制;区别在于结果呈现的时间和方式。

框架通过 SMT 支持的可判定性所验证的内容。 DTS 约束系统扩展为包含内存维度约束(枚举排序)、能力共效应(coeffect)约束(有限域推理)以及目标可达性约束(位向量算术)。这些归约为无量词理论:维度约束对应 QF_LIA,排序约束对应 QF_UF,可达性对应 QF_BV。这三者均是可判定的;在 PHG 细化过程中生成的 SMT 查询保证会终止并给出确定的答案。文献 [10] 第 6.7 节确立了这一双阶段模型:设计时对约束一致性的 SMT 验证,以及编译时的翻译验证,以确保 MLIR 降级在每一遍(pass)中都能保留已验证的属性。
边界所在之处。 上述属性是 PHG 类型与约束结构的一阶属性。该框架不试图证明程序在任意输入下的语义行为属性。一个使用维度一致损失项训练的物理信息神经网络是否会收敛,一个网格操作是否会对退化输入配置产生几何上正确的结果,一个空间数据流流水线是否会在所有可能的调度决策下在给定的延迟预算内完成:这些都是运行时行为的属性,需要运行时验证或概率性保证。这一边界是 Rice 定理的推论。PHG 的贡献并非消除这一边界,而是将尽可能多的相关结构验证推向可判定的一侧,以便剩下的是一组更小、特征更明确的未知量。
其实际后果是,一个面向 XDNA 2 NPU 的、带有 PHG 注解的克利福德代数计算,携带了作为设计时证书(可在任何构建步骤之前在编辑器中获取)的内容:所有涉及物理量的维度一致性、所有几何积与联结的阶正确性、所有网格边界关系的拓扑一致性、相对于目标资源约束的所有瓦片分配的共置可行性,以及相对于其维度范围的所有值的数值表示充分性。工程师无需运行程序即可发现本应传递 1 阶向量的地方却传递了 2 阶二重向量。Lattice 知道这一点,并在代码编写时即予以报告。
7. 相关工作
7.1 编译中的超图表示
编译中的超图表示在 VLSI 布局与布线 [12] 中已得到充分确立,其中超边自然地模拟了连线(net)的多元连接。PHG 将这种表示适配至语义层面,在此超边携带类型与维度注解,而非纯粹的拓扑连通性。
7.2 编译与机器学习中的几何代数
克利福德群等变神经网络(CGENNs)[20] 确立了基于克利福德代数的架构在物理模拟任务中的可行性。可操纵克利福德 CNN 工作 [25] 将其扩展至伪欧几里得群下的等变性,而 Flash Clifford 仓库 [24] 解决了理论与实际效率之间的性能差距。这些先前的工作均未将阶(grade)集成到编译器类型系统中;性能优化是通过手动实现(Flash Clifford, Klein)或运行时特化(GAmphetamine, kingdon)达成的。PHG 提供了从第一性原理推导这些优化的类型论基础。 “Clean up your Mesh”工作 [5] 在几何语境下独立建立了 kk-单纯形的 PHG 编码,但不包含编译框架。网格论文提供了几何学上的正当性;本文提供了编译基础设施。
7.3 DCont/Inet 对偶性与作为其补全的 PHG
DCont/Inet 对偶性 [8] 将计算表达式编译划分为两种机制:针对顺序带副作用计算的 DCont 机制(单子结构,Actor 作为语法糖化的 DCont),以及针对纯并行计算的 Inet 机制(对称幺半结构,结构上独立的规约)。PHG 超边是将 Inet 活跃对(active pair)推广至元数 kk 的结果。
PHG 中的阶注解决定了哪些元组是活跃的:1 阶元素与 2 阶元素的几何积为 1 阶输出(内积)产生一个活跃对,为 3 阶输出(完整积的外积部分)产生一个活跃三元组。这些是在克利福德代数阶格上结构并行的规约,PHG 将它们表示为可同时触发的超边。MLIR 的 Inet 方言 [4] 使用声明式重写规则实现了三种对称交互组合子(擦除 Erase、构造 Construct、复制 Duplicate)。保阶操作是构造子(Constructor)应用;阶湮灭操作(例如对任意 1 阶元素

)是擦除器(Eraser)应用;阶复制操作(quire FMA 累加)是复制器(Duplicator)应用。
7.4 Verse 演算:相邻领域
Verse 为基于通过合一(unification)解析的存在变量的函数式逻辑编程提供了指称语义 [22]。Verse 基于合一的非确定性,与 Fidelity Inet 路径的纯并行规约,操作于相关的数学结构之上,这使得简要的结构比较具有价值。

7.5 源语言语义天花板
异构计算生态系统中一个反复出现的模式,是试图从用 C 或 C++ 编写的程序中恢复语义结构,无论是通过静态分析、程序转换,还是从 C 源代码派生的专用中间表示。这种模式出现在面向空间加速器的数据流图提取中、在 CGRA 映射工具链中,以及在为某些面向 HPC 的处理器架构提供信息的分析遍(analysis passes)中。
这种方法的结构天花板并非对涉及工程工作的批评。它是 C 和 C++ 能表达什么以及不能表达什么的后果。C 编码了数据依赖:计算的结构作为对数组和标量的操作序列,其顺序由控制流决定,大小由类型声明决定。从 C 提取的数据流图忠实地捕获了这些结构依赖。它无法捕获的是从未存在于源代码中的语义信息:正在计算的值的物理维度、几何操作的阶结构、被操作网格的拓扑一致性要求。
C++ 模板可以在 C++ 类型系统内编码阶和维度信息,正如第 3.4 节调查的几何代数库所演示的那样。但 C++ 模板由 C++ 编译器解析,并不被携带至 LLVM 中间表示。Boost.Units 量上的维度注解在 C++ 层面强制执行,随后对下游阶段不再可见;从该代码产生的 LLVM IR 是维度不可知的。从编译时带有维度模板注解的 C++ 代码进行的 C-to-dataflow 提取,接收到的是同样维度不可知的 LLVM IR。注解的生命期终结于 C++ 前端,远早于数据流提取步骤。
PHG 并不从未编写语义结构的程序中提取语义结构;它保留了在源语言类型系统中编码并作为设计承诺贯穿编译过程的语义结构。语义错误的设计时检测成本是有界且系统的;运行时检测成本是无界且偶发的,取决于该错误是产生可见的失败,还是仅仅产生微妙的不正确结果。
8. 未来工作
8.1 超图划分集成
最紧迫的工程任务是将现有的超图划分算法(hMETIS 或 PaToH)集成至 MLIR-AIE 降级路径中,以 PHG 共置超边作为划分约束,并生成瓦片分配与路由配置。
8.2 与 Garamon 和 GAALOP 的兼容性
Garamon 与 GAALOP 均可根据代数规范生成 C 代码。Farscape 已能为 C 库生成 F# 绑定。将 Garamon 的 C++ 库生成与 Farscape 的绑定生成相结合,将为现有 Garamon 生成的代码提供一条导入 Fidelity 框架并附带 PHG 阶注解的路径,而无需在 Clef 中进行完全重写。
8.3 阶可判定性的形式化证明


幺正性保持(要求每个门操作将量子态的 2-范数精确维持在 1.0)是 DTS 意义上的维度不变量,并且可表达为 SMT-LIB2 证明义务,现有验证基础设施可在细化时履行。本节的结构主张是对多量子比特联合测量的超边编码;我们将关于量子振幅 posit 与 IEEE-754 精度的任何主张推迟至专门论述。复单位圆上振幅的相关精度度量是门操作后距单位圆的距离,而非实线上接近 1.0 的相对误差,且在现实门保真度阈值下将 posit 渐缩(posit tapering)连接至该度量的推导超出了本文范围。
Fidelity 编译流水线的量子后端将需要兼容 QIR 的 MLIR 降级路径,其开发取决于容错量子硬件目标的成熟度。用于多量子比特联合操作与综合征测量的 PHG 超边结构,以及用于结构正确性的 PSG 级证明生成,其存在原因独立于量子计算,并在量子-经典语境中自然组合。我们将其认定为未来研究的一个动机充分的方向;本项目先前发表的工作已更详细地考察了这些结构联系 [9]。
8.6 提议的克利福德方言
Fidelity 框架有意避免引入自定义 MLIR 方言,而是依赖已建立的方言生态系统:DCont 与 Inet 用于计算表达式编译,SCF 与 MemRef 用于控制与内存,LLVM 用于本机代码生成,CIRCT 用于 FPGA 综合,MLIR-AIE 用于空间数据流目标。作为一项通用原则,这种克制是正确的。自定义方言会引入维护负担,制造跨框架互操作的障碍,并使关于编译流水线不变量的推理复杂化。

我们预期,如果开发出这样的方言,将在中间端(MiddleEnd)层级实现一个扁平、可处理(tractable)的计算图:带有阶注解的几何操作,既无凯莱表间接寻址,也无运行时特化开销,特定目标的降级路径可由此分化,同时保持阶信息完整。在 CPU 目标上,阶注解将指导 SIMD 内建函数(intrinsic)的选择;在通过 Triton 面向 GPU 目标时,它们将决定线程束对齐(warp-aligned)的内核结构;在通过 CIRCT 面向 FPGA 目标时,它们将约束算术流水线的综合;在通过 MLIR-AIE 面向 NPU 目标时,它们将与 PHG 共置超边交互,将特定阶的计算分配给 AI Engine 瓦片。这种流水线扁平化是否在所有四条目标路径的实际应用中均成立,是一个需要实现与测量的问题;我们在此将其呈现为一个基于第 3.2 节分析与 Flash Clifford [24] 实证结果的、动机充分的假设。
8.7 神经形态目标与时间超边
神经形态处理器,包括 Intel Loihi-2 及更广泛的脉冲神经网络(spiking neural network)硬件家族,呈现出一类计算,PHG 形式体系对其的描述比任何现有的神经形态编程框架都更为自然。当前工具链中的结构性缺口已被精确定位,而填补该缺口的路径直接源于本文所确立的基础。
脉冲神经网络的基本计算原语是符合检测(coincidence detection):当足够多的突触前输入在时间窗口 ττ 内发放(spike)时,神经元即发放。对于一个拥有 NN 个突触前输入的神经元,若其中 kk 个在 ττ 内发放时即触发,则该发放事件是到达脉冲的完整 kk 元组的联合属性,而非任何单个输入的属性。在 PHG 中的自然表示是一个 kk 对 1 的超边:


连续局部适应与 Olivier 星座(Olivier constellation)内的离散认证版本控制是兼容的。经 STDP 训练的权重通过 Loihi-2 的学习引擎在片上连续更新。由于每次权重更新都是局部的,且 DMM 共效应(coeffect)规约限定了每个突触的辅助状态,因此学习过程的内存占用是确定性的,且可在设计时验证。当权重配置有资格注册为新模型版本时,Fidelity 版本控制基础设施会发出相应的 PHG 结构证书和后量子签名记录,从而在保留离散认证版本控制的同时保存连续局部适应。
8.8 面向多切线前向梯度的阶结构化切线选择
第 5.2 节确立了 PHG 对几何代数计算的前向模式自动微分的贡献:quire 为方向导数的内积提供精确累加,且阶注解通过适用于原语(primal)的同一阶推断贯穿切线计算。近期关于多切线前向梯度(multi-tangent forward gradients)[3] 的工作,促使将这一分析扩展至梯度估计器本身的近似质量。



8.9 BAREWire 几何序列化
BAREWire 是 Fidelity 框架针对进程间通信(IPC)与网络交换的 BARE 二进制协议的具体实现,目前负责序列化标量与张量数据。扩展 BAREWire 以处理带有阶注解字段的多重向量序列化,将允许几何计算结果在进程间传输时保留其代数结构,从而实现分布式几何计算流水线,其中每个进程操作特定的阶子空间,而完整的多重向量在边界处组装。
9. 结论
程序超图是对程序语义图的一种有原则且侵入性最小的推广。它保留了所有现有 PSG 属性,为那些若表示为二元关系序列则会导致信息丢失而无法正确表示的计算,添加了元数大于一的超边。
本文的核心技术主张如下:克利福德代数中的阶是 DTS 的自然维度轴,可通过现有推断机制推导得出;由阶推断所隐含的几何积稀疏性,在编译时消除了针对克利福德代数神经网络的主要计算性质疑,且无需手动特化;网格拓扑的 k-单纯形结构是 PHG 超边的直接编码,可提供精确的几何谓词评估,而无需浮点比较;且空间数据流架构映射需要超边共置约束,这些约束无法被正确地表达为二元团(binary cliques)。
对现有几何代数库生态系统的评估揭示了一个一致的缺口:没有任何现有系统将阶作为一等类型级属性进行集成,使其能够保留于编译器的语义图中、参与内存放置与表示选择决策,并通过语言服务器协议暴露出来。PHG 在 Fidelity 编译框架内填补了这一缺口,将文献 [10] 中确立的设计时分析能力扩展至几何正确性、拓扑一致性与空间共置。这些属性汇聚于单一图结构之中,工程师通过呈现维度诊断与逃逸分析的同一语言服务器接口对该结构进行导航,这即是其实际成果。物理信息计算、几何代数神经网络与空间加速器映射是三个截然不同的应用领域,但它们具有共同的结构需求:针对计算节点集合的多元约束。PHG 提供表示;DTS+DMM 推断机制提供分析;Fidelity 编译流水线提供执行路径。
原文链接:https://arxiv.org/pdf/2603.17627