Monadic Table Counter Schemas (MTCSs) are defined as an extension of monadic recursive schemas studied by Ashcroft, Manna, and Pnueli [1]. The extension consists in adding a second parameter with restricted facilities to every function variable; an auxiliary parameter can only be used as (sort of) a counter for the depth of recursion, which, in the framework of program schemas, can only mean that the second parameter in every recursive call is G(Y) where G is a function constant and Y is the formal parameter. Consequently, there are two kinds of predicate symbols: table predicates, which test only the depth of the auxiliary parameter, and factor predicates, which test both parameters. The notions of interpretation, equivalence, halting, and divergence are then defined in the obvious way. The usual notion of freedom, however, does not make too much sense for MTCS; instead, the notion of factor-freedom is introduced, which means that no factor predicate is evaluated twice with the same arguments during a computation. In order to establish a connection between ETOL languages and MTCSs, semicomputations are introduced. These are shown to be closely related to derivations in ETOL systems. A semicomputation is a computation if and only if the MTCS is factor-free. The families of ETOL languages and value languages of MTCS are equal. Using results about regular control sequences of ETOL systems, it is shown that factor-freedom is decidable. The main results of the paper are then the decidability of the halting problem for all MTCS and of the divergence problem for factor-free MTCS. There is no final resolution of the equivalence problem, but it is shown that the equivalence problem of HDOL sequences can be reduced to the equivalence problem of MTCS; hence, this is probably a difficult question.

The author acknowledges his PhD supervisor Professor Eli Shamir for his guidance on this paper, which is very clearly written, contains the necessary proofs, and is (apart from well-known results from formal language theory) self-contained.