Correctness of effect-based program transformations
Correctness of effect-based program transformations
复制标题
基于效果的程序转换的正确性
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
M. Hofmann
中科院分区：
文献类型：
--
作者：
M. Hofmann
我们考虑一个类型系统能够跟踪阅读，写和分配在一个高阶语言的动态分配引用。我们给这个类型系统，使我们能够验证一些效果依赖的程序等价的意义上的观察等价的指称语义。例如：x = e; y = e; e′（x，y）等价于x = e; e′（x，x），前提是e不从它写入的存储器区域读取，而且不分配封装在x和y值中的存储器。这里，x可以是高阶函数或引用，也可以是两者的组合。上述等价的两边在指称语义中是相关的，这意味着它们在观察上是等价的，即可以在任何（良好类型的）程序中相互替换。在学习过程中，我们学习了一些流行的技术，如参数化逻辑关系、区域、可容许关系等，属于程序设计语言原理研究人员的工具箱。
We consider a type system capable of tracking reading, writing and allocation in a higher-order language with dynamically allocated references. We give a denotational semantics to this type system which allows us to validate a number of effect-dependent program equivalences in the sense of observational equivalence. An example is the following: x = e; y = e; e′(x, y) is equivalent to x = e; e′(x, x) provided that e does not read from memory regions that it writes to and moreover does not allocate memory that is encapsulated in the values of x and y. Here x can be a higher-order function or a reference or a combination of both. The two sides of the above equivalence turn out to be related in the denotational semantics which implies that they are observationally equivalent, ie can be replaced by one another in any (well-typed) program. On the way we learn popular techniques such as parametrised logical relations, regions, admissible relations, etc., which belong to the toolbox of researchers in principles of programming languages.