带类型的灵活元数槽化电子图：一种可靠性构造与Alloy案例研究
Typed Flexible-Arity Slotted E-Graphs: A Soundness Construction and an Alloy Case Study
- University of Texas at Arlington（阿灵顿得克萨斯大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
该研究构造带类型的灵活元数槽化电子图，证明其有限展开等式的可靠性，通过Alloy案例研究对比七个管道分支，分析其有界能力与结构合并特性。
AI中文摘要：
槽化电子图表示模一致重命名的开放项，而代数算子可从规范序列、多重集或集合子项中受益。我们在规范层面将两者结合：带类型的槽映射调用驻留于算子声明的端口，其兄弟商与递归扁平化许可分别经过验证。通用有限商表示证明了其最小轨道范式的精确性，而验证记录指定了有效支撑核提取与冲突。对于携带局部端点证书的抽象义务轨迹，我们证明了有限展开等式的可靠性。Alloy案例研究在冻结语料库与受控变换套件上对比了七个相关管道分支，其测量结果表征了有界能力与结构合并；这些结果未确立对Java工件的精化，也未针对形式模型进行实验复现。
英文摘要：
Slotted e-graphs represent open terms modulo consistent renaming, while algebraic operators benefit from canonical sequence, bag, or set children. We compose the two at a specification level: typed slot-mapped invocations inhabit operator-declared ports whose sibling quotient and recursive flattening licenses are certified separately. A generic finite quotient presentation proves exactness of its least-orbit normal form, while certified records specify effective-support kernel extraction and collision. For abstract obligation traces carrying local endpoint certificates, we prove finite-unfolding equational soundness. An Alloy case study compares seven related pipeline arms on a frozen corpus and a controlled transformation suite.
