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