多元χ演算运行时错误的不可判定性

多元χ演算运行时错误的不可判定性 On the Undecidability of Run Time Error in Polyadic χ-Calculus 陈韬略 1 first-author 韩婷婷 1 颜锋 1 吕建 1 南京大学计算机软件新技术国家重点实验室,江苏,南京,210093 南京大学计算机软件新技术国家重点实验室,江苏,南京,210093 针对多元χ演算运行时刻通信安全的判定性问题进行了研究.通过从Lazyλ项到χ项的编码,将判定一个Lazyλ项是否有范式的问题归约为进程是否有通信错误的问题.证明了在多元χ演算中,通讯错误也是不可判定的.结论说明不存在算法直接来检测进程的通信安全性,而只有通过其他间接的手段（如构造类型系统）才能部分达到预防运行时错误的目的. This paper deals with a significant mobile process calculus, that is, polyadic χ calculus which exploits name exchange as its communication mechanism and can exchange several information in one communication process. This work investigates the problem whether one can design some algorithms to detect the run time error directly. Following the general pattern of undecidability proofs, this paper reduces the problem of deciding whether a Lazy λ term has a normal form to the decidability of run time error by constructing a encoding from the λ terms to the χ process and thus show that the problem to check communication errors in the polyadic χ calculus is undecidable, which illuminates that only by some indirect means （e.g. type system）, can one detect possible run-time errors in concurrent programs and unfortunately, such approach is inherently incomplete. 并发理论 进程代数 χ演算 运行时错误 不可判定性 concurrent theory process algebra χ calculus runtime error undecidablity TP301 国家重点基础研究发展规划973项目资助（2002CB312002）;国家自然科学基金资助项目（60273034）;国家863高科技项目资助项目（2002AA116010） 2004-05-01 2021-04-01 5