时态并发约束程序设计语言及其表达能力

理论计算机科学www.elsevier.com/locate/entcs时态并发约束程序设计语言的表达能力（特邀演讲）帕拉米代西卡图夏摘要tcc范式是一种时间并发约束程序设计的形式主义。在文献中已经提出了几种在表达无限行为的方式上不同的TCC语言。在这项工作中，我们研究了这些语言的表达能力特别是，我们表明：(1)带有参数的递归过程可以被编码为带有动态范围的无参数递归过程，反之亦然。（2）复制可以被编码为具有静态作用域的无参数递归过程，反之亦然。（3）（1）中的语言比（2）中的语言严格地更有表现力此外，我们还证明了行为等价对于（1）中的语言是即使过程变量从固定的有限域中取值，不可判定性结果也成立（与Mogens Nielsen和Frank D. 巴伦西亚）1571-0661cElsevierLtdO pe nacccessunderC CB Y-NC-NDlicens e.10.1016/S1571-0661（05）01357-5