会话类型状态空间构成格
Session Type State Spaces Form Lattices
查看机构详情
- Independent Researcher, Berlin, Germany
机构由 AI 辅助整理，请以论文原文为准。
浏览论文内容
中文总结 AI 辅助
本研究证明良构会话类型的状态空间经强连通分量商化后构成有界格，推导得到对偶性与子类型的格理论对应关系，并在108个基准协议上完成验证，同时实现了Lean 4机械化证明。
中文摘要 AI 辅助
我们证明，每个良构会话类型的状态空间经强连通分量商化后构成有界格；n元并行组合可生成乘积格。由此得到两个推论：对偶性在同构意义下保持格结构，且Gay-Hole宽度子类型对应非递归类型的格嵌入。我们在来自网络、数据库、分布式系统、AI及容错领域的108个基准协议上验证了该结论：所有协议均构成格，其中93个为分配格，15个为非分配格。该结果已在Lean 4中实现机械化验证，配套有两个独立开发的工具实现。
英文摘要
We prove that the state space of every well-formed session type, quotiented by strongly connected components, forms a bounded lattice; n-ary parallel composition yields product lattices. Two consequences follow: duality preserves the lattice up to isomorphism, and Gay-Hole width subtyping corresponds to lattice embedding for non-recursive types. We validate this on 108 benchmark protocols across networking, databases, distributed systems, AI, and fault tolerance: all form lattices, 93 distributive, 15 non-distributive. Mechanised in Lean 4 with two independently developed tool implementations.
