Abstract conjunctive partial deduction for the analysis and compilation of coroutines

作者：Nys Vincent^*; De Schreye Danny

来源：Formal Aspects of Computing, 2017, 29(1): 125-153.

DOI：10.1007/s00165-016-0389-8

• Coroutines
• Compiling control
• Abstract conjunctive partial deduction

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.

• 出版日期2017-1