Synchronous Schemes and Their Decision Problems

Abstract

A class of schemes called synchronous schemes is defined. A synchronous scheme can have several variables, but all the active ones are required to keep a synchronized rate of computation as measured by the height of their respective Herbrand values. A "reset" statement, which causes all the variables to restart a new computation, is admitted. It is shown that equivalence, convergence, and other properties are decidable for schemes in this class. The class of synchronous schemes contains, as special cases, the known decidable classes of Ianov schemes, one-variable schemes with resets, and progressive schemes.