paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Geometry of Computation-Graph Abstraction

计算图抽象的几何
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 4/10 · 论文研究按值λ演算中计算图抽象的类型系统与语义,属于 PL 形式语义,与 TensorFlow 等 ML 系统的语言特性相关,但未涉及静态分析工具、Agentic 程序、浮点或贝叶斯程序分析,也无 LLM 交叉,与用户核心方向仅边缘相关。引用 7 inbox
Koko Muroya, Steven W. T. Cheung, Dan R. Ghica
crossref: 2026-09-12

AI 速览

一句话:用动态交互几何为按值λ演算中的计算图抽象建立类型系统与语义模型,保证垃圾回收和β律安全。

该文研究 TensorFlow 引入的计算图抽象这一语言特性:程序员可以提取并操作计算图的状态,从而方便地定义参数化模型,同时仍能使用通用的搜索与优化算法。作者在按值调用的 λ 演算中形式化该特性,并借助新近提出的动态交互几何(Dynamic Geometry of Interaction)形式化方法建立语义模型。文章给出一个简单的类型系统,以保证计算图抽象的安全性;并证明垃圾回收与 β 律等关键语言性质在该模型下仍然安全。语义模型还表明,该特性有望以合理效率在通用函数式语言中实现。

问题
如何安全地在按值 λ 演算中支持计算图抽象,使程序员能提取和操作计算图状态以定义参数化模型,同时不破坏语言的核心性质。
方法
使用动态交互几何(Dynamic Geometry of Interaction)为按值 λ 演算中的计算图抽象建立语义模型,并设计一个简单类型系统来刻画其安全性。
评估
通过类型系统和语义模型证明垃圾回收与 β 律等关键性质的安全性,并从模型论证该特性可在通用函数式语言中高效实现。
原文摘要(Abstract)

The popular library TENSORFLOW (TF) has familiarised the mainstream of machine-learning community with programming language concepts such as data-flow computing and automatic differentiation. Additionally, it has introduced some genuinely new syntactic and semantic programming concepts. In this paper we study one such new concept, the ability to extract and manipulate the state of a computation graph. This feature allows the convenient specification of parameterised models by freeing the programmer of the bureaucracy of parameter management, while still permitting the use of generic, model-independent, search and optimisation algorithms. We study this new language feature, which we call 'graph abstraction' in the context of the call-by-value lambda calculus, using the recently developed Dynamic Geometry of Interaction formalism. We give a simple type system guaranteeing the safety of graph abstraction, and we also show the safety of critical language properties such as garbage collection and the beta law. The semantic model suggests that the feature could be implemented in a general-purpose functional language reasonably efficiently.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4377,
  title = {The Geometry of Computation-Graph Abstraction},
  author = {Koko Muroya and Steven W. T. Cheung and Dan R. Ghica},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209127}
}