Ordinary interactive small-step algorithms, I

被引:15
作者
Blass, Andreas [1 ]
Gurevich, Yuri
机构
[1] Univ Michigan, Dept Math, Ann Arbor, MI 48109 USA
[2] Microsoft Res, Redmond, WA 98052 USA
关键词
algorithms; theory; sequential algorithms; interaction; postulates; equivalence of algorithms; abstract state machines;
D O I
10.1145/1131313.1131320
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
This is the first in a series of articles extending the abstract state machine thesis - that arbitrary algorithms are behaviorally equivalent to abstract state machines - to algorithms that can interact with their environments during a step rather than only between steps. In the present work, we describe, by means of suitable postulates, those interactive algorithms that (1) proceed in discrete, global steps; (2) perform only a bounded amount of work in each step; (3) use only such information from the environment as can be regarded as answers to queries; and (4) never complete a step until all queries from that step have been answered. We indicate how a great many sorts of interaction meet these requirements. We also discuss in detail the structure of queries and replies and the appropriate definition of equivalence of algorithms. Finally, motivated by our considerations concerning queries, we discuss a generalization of first-order logic in which the arguments of function and relation symbols are not merely tuples of elements but orbits of such tuples under groups of permutations of the argument places.
引用
收藏
页码:363 / 419
页数:57
相关论文
共 13 条
[1]  
[Anonymous], 2000, ACM T COMPUTATIONAL, DOI DOI 10.1145/343369.343384
[2]  
Blass A., 2003, Bulletin of the European Association for Theoretical Computer Science, P195
[3]  
Blass A., 2003, ACM Transactions on Computational Logic, V4, P578, DOI 10.1145/937555.937561
[4]   Strong extension axioms and Shelah's zero-one law for choiceless polynomial time [J].
Blass, A ;
Gurevich, Y .
JOURNAL OF SYMBOLIC LOGIC, 2003, 68 (01) :65-131
[5]   Choiceless polynomial time [J].
Blass, A ;
Gurevich, Y ;
Shelah, S .
ANNALS OF PURE AND APPLIED LOGIC, 1999, 100 (1-3) :141-187
[6]  
BLASS A, 2000, LNCS, V1862, P1
[7]  
BLASS A, UNPUB GEN INTERACTIV
[8]  
Gurevich Yuri., 1995, Speci fication and Validation Methods
[9]  
MINLNER R, 1999, COMMUNICATING MOBILE
[10]  
Moschovakis Y.N., 2001, MATH UNLIMITED 2001, P919, DOI [DOI 10.1007/978-3-642-56478-9_46, 10.1007/978-3-642-56478-9_46]