一句话:为 π-演算进程结合多项式终止类型与因果语义,建立外部消息因果触发的多项式消息复杂度界。
本文研究 π-演算分布式进程的计算复杂度,关注由外部输入消息因果引发的迁移数量。作者将 Bellantoni 与 Cook 的多项式递归函数刻画融入 Deng 与 Sangiorgi 的终止类型系统,并基于 Degano 与 Priami 的因果语义定义分布式消息复杂度,以识别交错迁移间的依赖。随后对可类型化进程进行语法流分析,以保证消息计算界。结果证明该分析对给定进程可判定;在可靠性意义上,它保证从外部收到的输入请求因果依赖的消息总数受该请求内容的多项式界定;在完备性意义上,每个多项式递归函数都可由可类型化进程计算。
This paper studies the complexity of π-calculus processes with respect to the quantity of transitions caused by an incoming message. First we propose a typing system for integrating Bellantoni and Cook's characterisation of polynomially-bound recursive functions into Deng and Sangiorgi's typing system for termination. We then define computational complexity of distributed messages based on Degano and Priami's causal semantics, which identifies the dependency between interleaved transitions. Next we apply a syntactic flow analysis to typable processes to ensure the computational bound of distributed messages. We prove that our analysis is decidable for a given process; sound in the sense that it guarantees that the total number of messages causally dependent of an input request received from the outside is bounded by a polynomial of the content of this request; and complete which means that each polynomial recursive function can be computed by a typable process.