数据流框架中表达式 Herbrand 等价的不动点刻画
计算机科学中的逻辑
2017-10-23 v2 编程语言
摘要
在数据流框架中确定每个程序点处项的 Herbrand 等价是程序分析中的一个核心且被充分研究的问题。大多数用于计算数据流框架中 Herbrand 等价的著名算法，都是通过与给定流图相关的短表达式抽象格上的迭代不动点计算来进行的。然而，Herbrand 等价的数学定义是基于所有可能表达式的（无限）集合上的所有路径交汇刻画。本文的目的是在由程序中变量、常数和算子可构造的所有项的集合上定义的（无限）具体格上，发展 Herbrand 等价的格论不动点公式。本刻画使用了 Herbrand 同余概念的公理化公式，并定义了 Herbrand 同余的（无限）具体格。传递函数和非确定性赋值被公式化为该具体格上的单调函数。Herbrand 等价被定义为上述具体格的适当乘积格上定义的复合传递函数的最大不动点。本文还给出了 Herbrand 等价经典的所有路径交汇定义在上述格论框架中的重新表述，并证明了其与新的格论不动点刻画等价。
关键词
引用
@article{arxiv.1708.04976,
title = {A fix-point characterization of Herbrand equivalence of expressions in data flow frameworks},
author = {Jasine Babu and K. Murali Krishnan and Vineeth Paleri},
journal= {arXiv preprint arXiv:1708.04976},
year = {2017}
}