Abstract conjunctive partial deduction for the analysis and compilation of coroutines

详细信息    查看全文

• 作者：Vincent Nys ; Danny De Schreye
• 关键词：Coroutines ; Compiling control ; Abstract conjunctive partial deduction
• 刊名：Formal Aspects of Computing
• 出版年：2017
• 出版时间：January 2017
• 年：2017
• 卷：29
• 期：1
• 页码：125-153
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Math Applications in Computer Science; Theory of Computation; Computational Mathematics and Numerical Analysis;
• 出版者：Springer London
• ISSN：1433-299X
• 卷排序：29

文摘

We provide an approach to formally analyze the computational behavior of coroutines in logic programs and to compile these computations into new programs, not requiring any support for coroutines. The problem was already studied near to 30 years ago, in an analysis and transformation technique called compiling control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also rather ad hoc. We show how abstract conjunctive partial deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine compiling control. We define an abstract domain and all abstract operations required by abstract conjunctive partial deduction. We prove that these concepts satisfy all the correctness conditions imposed by the framework and therefore inherit its main correctness theorem. We also show that there exist more complex coroutining examples which do not fit within abstract conjunctive partial deduction and we propose some further extensions to include them.