THE UNIVERSITY OF MI CHI GAN COLTLEGE OF LITERATURE, SCIENCE, AND THE ARTS Department of Philosophy Logic of Computers Group Final Report DESIG ALGORITHMS IN AUTOMATA LANGUAGES A. W. Burks J. R. Bichi C. C. Elgot J. B. Wright UMRI Project 2755 under contract with: DEPARTMENTl OF TBE ARMY OFFICE OF ORDNANCE RESEARCH DETROIT ORDNANCE DISTRICT CONTRACT NO. DA-20-018-ORD-16971 DETROIT, MICHJIGAN administered by: THE UNIVERSITY OF MICHIGAN RESEARCH INSTITUTE ANN ARBOR July 1960

Other agencies of the Federal Government assisted in the support of much of this research. These agencies are the Office of Naval Research, the U. S. Army Signal Corps, and the National Science Foundation.

INTRODUCTION Research under Contract No. Da-20-018-ORD-16971 began in the spring of 1958 and continued, into June, 1960. The details of the principal research are indicated in items 3 through 9 of this report. In particular, attention is directed to the two technical reports, Decision Problems of Finite Automata Design and Related Arithmetics, by Calvin Elgot, and Weak Second-Order Arithmetic sd Finite Automata, by J. R. Buchi, which have already been distributed to the Office of Ordnance Research, and to On a Problem of Tarski by J. R. Buchi, which is a part of this final report. Research has also been conducted in additional areas ancillary to this principal research area. In the technical report Lectures on Switching and Automata Theory by Calvin Elgot (distributed to the Office of Ordnance Research) the automata theory field is reviewed from simple switching theory up through the sequential machine theory of Kleene and $oore. In Sequence Generators and Digital Computers by A. W. Burks and J. B. Wright (included as item 10 of this final report), the theory of a broad class of finite automata is investigated, and numerous algorithms for the analysis and synthesis of these automata are indicated. 1

SUMMARY The principal goal of our research has been to obtain algorithms which would permit the mechanizability of the processes of computer design. Attention was focused on the following design algorithms. 1. Solution algorithm: Given an automaton and given a behavior condition, to determine whether or not the automaton satisfies the condition. 2. Solvability algorithm. Given a behavior condition, to determine whether or not an automaton exists satisfying the condition. 3. Synthesis algorithm: Given a behavior condition, to produce the specifications for an automaton satisfying the condition (providing such an automaton exists). The first goal of research was to ascertain the characteristics of a for-:mal language suitable for setting down of automata structure descriptions, and automata behavior condition descriptions. (The difference between an automaton and a condition is as follows: An automaton expression gives all the relationships existing between every switching and every delay element throughout the machine. A condition expression gives only the input to output relationship, i.e., only the conditions the designer wishes to have satisfied, with no reference to the relationships between the internal junctions by means of which the action is effected.) In the case of the automata structure descriptions, it was apparent that the language to be employed should be a monadic predicate calculus where the predicates would denote junctions of switching or delay elements, and the individuals would denote instants of time. This same language could also be employed to express behavior conditions. For example, A(O) V B(O) D(1) is a condition that possibly is satisfied. by one or more automata. If we arrive at an expression for an automaton which might satisfy this condition, then the Solution algorithm could. be applied, to the automaton and to the condition to see if this is in fact the case. 15

Suppose it is suggested that the automaton pictured (below) satisfies the given behavior conditions: A(O)- V B(O) D D(1) C D This automaton expressed in our formal language is: [A(O) V B(O) - C(O)] and [C(O) - D(1)]. (it should be noted that the condition expression omits mention of internal junction C, while the automaton expression makes explicit the presence and function of internal junction C.) The Solution algorithm will judge the truth or falsity of the assertion that the given automaton implies the given behavior, i.e., the truth of falsity of the following expression: f[A(o) VB(o) = C(o) ] / [C(0) = D(1) ] 3 [A(O) B() CD(1) ]} Now if there is a decision prodecure for the class of sentences of the formal language in which this expression is couched (a decision procedure is a method. of mechanically determining, for any expression of a formal language, whether the expression is true or false),, it then follows that we can mechanically determine whether the automaton satisfies the condition by merely ascertaining the truth or falsehood of this particular assertion by means of the general decision procedure for the language. Thus it is evident that there may be a close connection between the decidability of- the formal language chosen to express automata and conditions, and the existence or lack of it of our three automata design algorithms. We have seen that the existence of a Solution algorithm follows directly from the existence of a general d~ecision procedure for the language employed. The Synthesis algorithm is also readily obtained. It is closely related to the Solution algorithm. In the Synthesis algorithm we are given a condition and asked to find an automaton satisfying the condition, providing such an automaton exists. There are various methods available for generating systematically the. expressions for all automata. Automata expressions are then substituted, one by one, into the Solution algorithm and tested to see whether the automaton satisfies the behavior. This process of generating automaton descriptions, substituting them in the Solution algorithm, and testing whether the conditions are satisfied continues until a suitable automaton satisfying the conditions is obtained.

Since many automata may satisfy the same conditions, additional criteria for choosing the "best" automaton can be brought in (including, of course, minmum number of states, or minimum number of certain elements). For instance, the two automata pictured below both satisfy the condition (A(O) V B(O) 3 D(l) of our earlier example, as does the automaton used in the example. A — D B In setting down conditions for automata, it is advantageous to have a large vocabulary at one's disposal. In the examples so far, the vocabulary has been restricted. to monadic predicates a4d their individuals, and to the connectives of propositional calculus. It would make the application of the design algorithms considerably easier if the designer, in setting down his conditions, could employ such expressions as "all,"t "equals," "less than," "fsome tt""successor of," etc. As we have noted, however, the existence or nonexistence of our design algorithms is closely related to the question of the decidability of the language as a whole, and it seems generally to be the case that the stronger a language is (the larger the number of its primitive operations, etc.), the more likely it is that the language is undecidable. We therefore find our objectives conflicting- the easier it is for a designer to set d.own his conditions, the more likely it is that there can never be a mechanical method of generating the desired. automaton. 5

The second. major goal of our research then became: to test large numbers of formal languages to determine whether the desired automata design algorithms existed in them, seeking to find the strongest useful language for which the algorithms existed. Siince the question of the existence or lack of it of the algorithms seemed to be closely related to the question of the existence or lack of it of a general decision procedure for expressions in the language, the large body of research results3 in formal decidability was thoroughly reviewed. Often it was found that the problem of decidability for a formal language was still open, and a program of examining such languages, and perhaps solving the decision problem for them was undertaken, Both positive and. negative solutions of decision problems were obtained for many languages. In April of 1960, Dr. J. Richard Biichi, Research Mathematician with the Logic of Computers Group, obtained, a positive solution to the decision problem for an extremely useful language. The existence of the Solution and Synthesis algorithms follows immediately in the manner indicated earlier. The question of the existence or not of a Solvability alborithm in this language is still open. (It had been answered in the affirmative for several useful, though weaker, languages,) The language for which Dr. Blichi obtained a decision procedure we shall call the "sequential calculus." It has the following characteristics: it allows all expressions compounded from individual variables ranging over natural numbers, predicate variables ranging over arbitrary sets of natural numbers, quantification (all, some, etc.,) over both individual and predicate variables, the connectives (or, and, not, etc.,) of propositional calculus, equality, less than, and successor. An example of a condition expression in the sequential calculus is given below. (2R) (Vt) S(t) [I(t) &- J(t) &rR(t)] V [I(t) & J(t) & R(t)] V [-I(t) &(t) & R(t) & tR(t) [I(t-) - J(t') &' R(t')] v [-I(t') & J(t2) &,JR(tV) i V [I(t') & Jt') & R(t')] V [I(t) & J(t) & R(t) ]$] & a(Q1 (Vt) i [Q(t) Do I(t)] & (Vx) (at) [t > x & Q(t) ] This is a behavrior conadition for the addition of real numbers less than one, where the sum is also less than one, This condition cannot be realized by a finite automaton. A description of a realizable finite automaton behavior is given on following page. 6

(aR) fR(o) =- S[I(o)] & (vt) [R(t') - [I(t), I(t), R(t) ] & (vt) [U(t) - X[R(t), I(t) I3 This is a finite automaton transformation from infinite input sequences to infinite output sequences. The transformation, successfully expressed here in the sequential calculus, cannot be expressed in many of the formal languages which have been proposed as useful in automata design.

Lectures on Switching and. Automata Theory (2755-2-T, January, 1959) Calvin C. Elgot ABSTRACT These lectures include a study of two-terminal series-parallel relay contact networks, multi-terminal relay contact networks, and sequential networks. General, systematic techniques for the study of series-parallel networks have employed Boolean algebra or propositional calculus. A basic paper on multiterminal relay contact nets makes use of matrices whose entries are elements of a Boolean algebra. More recent work makes use of the algebraic concepts: lattice, semi-group, group. The concept of ring when suitably specialized is intimately connected with Boolean algebras. This indicates the extent to which algebra is invading the mathematical theory of switching. Much recent work has employed more advanced aspects of logic than the propositional calculus. Indeed, the use of logic and its techniques has already produced significant results and promises still more fruitful ones. We begin with some preliminary, simple, algebraic and logical concepts which will lead to a discussion of finite Boolean algebras, propositional calculus, and their application to switching theory. The work of Lunts (which lists results only) is discussed in Section 6. The arguments make use of an important correlation between matrices of zeros and. ones and finite binary relations. This correlation is useful in other work on switching. Automata and sequential circuits are introduced in Section 7 and the connection with Burks-Wright logical nets is pointed out. Moore's theory and related work of Mealy and Ginsburg is expounded. The equivalence, in a certain reasonable sensel of finite automaton, as defined here and as defined in Moore, is indicated. Finite semi-groups are associated with automata in Section 7,9. In the case of permutation automaton (backwards deterministic), the associated seni-group is a group. An application is made of this association. Kleene's theory of regularity is explained. An alternative notion of regularity is defined. and its relation to the primary concept is established. The discussion terminates with an example illustrating several of the main results of the sections on automata theory. [These lectures were prepared as Technical Report 2755-2-T, January, 1959, and were distributed, to the addresses of the official OOR distribution list. ] 9

Decision Problems of Weak Second-Order Aritbmetics and Finite Automata (Preliminary Report, Part I) J. Richard. Biichi and. Calvin C. Elgot ABSTRACT 1. Let L1 be the class of formulas constructed out of atomic formulas xie Fj, Yk = x~ + 1, xi< yj, by means of propositional connectives and quantifiers, axi, aFj. The individual variables range over the natural numbers, N. The second-order variables range over finite sets of natural numbers. Each formula A[F1, F2,..., Fr] in L1 may be interpreted as representing a set (usually infinite) of finite sequences of r-tuples of zeros and ones as well as sets "isomorphic" to that set. Theorem. A set of finite sequences of objects drawn from a finite set is representable by a formula in L1 if and only if it is representable by a finite automaton (cf. Kleene, Automata Studies, or Copi, Elgot, and Wright, J.A.C.M, April, 1958). 2. Corollary. The set of true sentences of L1 is recursive. The corollary has been obtained by A. Ehrenfeucht and R. L. Vaught via Ebrenfeucht's theorem (unpublished), stating that the elementary theory of addition of ordinals is decidable. 3. Corollary. There are solution and synthesis algorithms relative to the class of all automata and L1. (Cf. Buichi, Elgot, and Wright, these Notices, February, 1958, for definitiona.) 4. Each formula A[F1 F2,..., Fr] in L1 defines R Nr via: F > neF 2n Corollary. The elementary theory of R. e.g., x + y = z (Presburger), is decidable. [This paper was presented at the 20-23 January 1959 meeting of the American Mathematical Society, in Philadelphia. The abstract was published in Notices of the American Mathematical Society, Vol 5, No. 7, Dec., 1958, p.834. ] 11

Decision Problems of Weak Second-Order Arithmetics and Finite Automata (Preliminary Report, Part II) Calvin C. Elgot ABSTRACT 1. ILet L2 be the class of formulas constructed out of atomic formulas xic Fj, yk = xi + 1, zk = xi + Yj, by means of propositional connectives and individual quantification (taxi) only. The variables are interpreted as in L1. Theorem. The set of satisfiable formulas of L2 is recursively enumerable but not recursive. 2. If the set variables are interpreted, as ranging over periodic sets (sets whose characteristic function is ultimately periodic), the theorem still holds. 3. Corollary. While there are solution and synthesis algorithms relative to the class of input-free automata and L2, there is no solvability algorithm. 4. If the formulas of L2 are interpreted. over the integers rather than the natural numbers, the theorem still holds. Let EA(a,b) be the set of finite sequences uabv where a e A, b e A, u and v are finite sequences (possibly null) of elements of A, and A is finite. The class of automaton representable sets is the smallest class of sets containing the sets EA(a,b), a unit set consisting of a sequence of length one, and closed under symmetric difference, intersection, and projection. (The mapping induced on sets of finite sequences of elements of A giving a set of finite sequences of elements of B, by an arbitrary mapping from A into B, is called a projection.) This strengthens a result of Medvedev. [This paper was prepared for the American Mathematical Society Meeting in Philadelphia, 20-23 January, 1959. The abstract was published in the Notices of the American Mathematical Society, Vol. 6, No 1, February 1959, p.48.1 13

Decision Problems of Finite Automata Design and Related Arithmetics (Technical Report 2755-6-T, June 1959) Calvin C. Elgot ABSTRACT Certain formal arithmetics may be employed as design languages for finite automata design conditions, the notion of automaton, and the notion of an automaton satisfying a condition are expressible in these arithmetics. An automaton saisfies a condition if a certain formula of the arithmetic is valid. For certain arithmetics, algorithms are produced. which enable one to decide (1) whether a given automaton satisfies a given condition, (2) whether an automaton exists satisfying a given condition (and if there is one, producing one), (3) whether at most one automaton exists satisfying a given condition, (4) whether a given sentence is true. These results make use of a theorem (5.3) which characterizes finite automata behavior by means of formulas of an arithmetic. The following corollary is typical of the side results obtained. If a natural number is identified with the set of natural numbers less than it, then the first-order theory of quasifinite (finite or finite complement) sets of natural numbers based upon the Boolean set operations and the property of being a natural number is decidable. For certain other arithmetics, it is shown that algorithms of the type indicated above fail to exist. [This paper was printed and distributed as Technical Report 2755-6-T, June, 1959. It has been submitted for journal publication. ] 15

Weak Second-Order Arithmetic and Finite Automata (Technical Report 2794-6-T, Sept. 1959) J. Richard Buchi ABSTRACT In essence, this paper states that a certain -ormal language, a weak secondorder arithmetic (designated throughout this paper as W.2.A., and in Elgot, Decision Problems of Finite Automata Design and Related Arithmeticsf as Lt) can be used — in place of the formalism of regular expressions (developed by S. C. Kleene in his paper "Representation of Events in Nerve Nets and Finite Automata," in Automata Studies, Princeton University Press, 1956) in denoting the behavior of finite automata. The important KIeene Synthesis and. Analysis theorems can also.be obtained in this new formulation. (Synthesis: For every formula of W.2.A. one can construct an automaton with special output, such that the behavior of the automaton is just the set of predicates which satisfy the given formulas. Analysis: For every automaton with special output one can obtain a formulas of W.2.A.- such that the formula denotes the behavior of the automaton). This result is of particular value because formulas of W.2.A. seem to be more convenient than regular expressions for formalizing conditions on the behavior of automata. Important additional results in pure logic are also obtained: the synthesis and analysis theorems yield. valuable information on the strength of W.2.A. and related formalisms. [For expositions of CLeene's theory of regularity see Copi, Elgot, and Wright, "Realization of Events by Logical Nets," JACM, 5, 181-196 (1958; Rabin and Scott, "Finite Automata and Their Decision Problems," IBM Journal.114-125 (April, 1959); and rhill, "Finite Automata and Representation of Events," WADC Report TR 57-624, Fundamental Concepts in the Theory of Systems, October, 1957, pp 112-137.] [This paper was printed and distributed, as Technical Report 2794-6-T, September 1959. It is to be published in 1960 in the Zeitschrift f1r Mathematische Logik and Grundlagen der Mathematik. ] 17

On a Hierarchy of Monadic Predicate Quantifiers J. Richard Buchi ABSTRACT Let x, xl, X2o o. be variables ranging over natural numbers, and let il., i2i i3.... be variables ranging over monadic predicate (sets) of natural numbers, let i, j denote k-tuples of i's. The hierarchy [mIm] of predicates P(i)on predicates is defined thus: Zo = a predicates P(i) definable by formulas K[i(o) ] v ($x) H[i(x), i(s+l) ] v (Vx) U[i(x) ], whereby K,H,U are truth functions in the indicated constituents,7rm = {-PIPJPme,, Fm + i = I(EJ) PIPeTCJ. A k-tuple i of monadic predicates may be considered to be an infinite sequence i(0) i(l) i(2),.. whose elements are drawn from the finite alphabet consisting of all k-tuples of truth-values. Let u7v,,.. denote finite words on this alphabet, let u v denote concatenation. Def: P(i) is of finite rank if there is a -congruence relation wuv on words, with finite partition, and such that urvq implies P(tfu2...)- Pv v2...). Theorem: The following are equivalent conditions on P(i): (1) Pe Z2, (2) P is of finite rank, (3) P = Pi.,...Pa kereby each Pc is of the form ifS S S.., R and S being regular sets of finite words. This is established by using basic facts from automata-theory (regularity), the fan theorem (KOnig's infinity lemma), and Ramsey's theorem [Proc. London Math, Soc., (2), 30, 264-286 (1930) ]. Clearly P is of finite rank if and only if P is; therefore Corollary: -7 =72 and therefore n = n = Z2 for n 2. [This paper was prepared for the Missoula, Montana, meeting of the American Mathematical Society in June, 1960, The abstract was published in the Notices of the American Mathematical Society, Vol. 7, No. 3, issue 46, June, 1960, p*381. ] 19

On a Problem of Tarski J. Richard B{chi ABSTRACT Let SC be the interpreted system containing variables x ranging over natural numbers, variables i ranging over monadic predicates on natural numbers, the successor function, propositional connectives, and quantifiers for both types of variables. Using the theorem and definition of the preceeding abstract one obtains: Theorem 1: The predicates P(il, —-,ik) definable in SC are exactly those belonging to Z2. For example: exactly the ultimately periodic sets of natural numbers are definable in SC. Theorem 2: Truth of sentences in SC is decidable. This answers a question of Tarski [see R. M. Robinson, Proc. Am. Math. Soc.,, 9, 238-242 (1958) ], and seems to be a rather strong result since essential assertions about infinity can be stated in SC(parts of the fan-theorem and Ramsey's theorem). By interpreting predicates i as binary expansions of real numbers, theorem 2 may be stated thus: Theorem 2': The flirst-order theory of [Re, +, Nn, Pw] is decidable. Here Re is the set of real numbers > 0, Nn is the set of' natural numbers and Pw is the set of integral powers of 2. (Campare this result with Tarski's decidability of >Re, +,.]). Let SCper be like SC, except that the variables i range over ultimately periodic predicates. Theorem 3: A sentence is true in SCper if and only if it is true in SC. i.e., [Re, +, Nn, Pw] and. [R, +, Nn, Pw] are arithmeticaly.equivalent. Here R stands for the set of rational numbers. [This paper was prepared for the Missoula, Montana, meeting of the American Mathematical Society in June, 1960. The abstract was published in the Notices of the American Mathematical Society, Vol. 17, No. 3, June, 1960, p. 382.] 21

On a problem of Tarski1 by J. Richard BUchi Let SC (sequential calculus) be the interpreted formalism which makes use of individual variables t, x, y, z,... ranging over natural numbers, monadic predicate variables q( ), r( ), s( ), i( ), j( ),... ranging over arbitrary sets of natural numbers, the individual symbol o for zero, the function symbol ) denoting the successor function, propositional connectives, and quantifiers for both types of variables. The purpose of this note is to outline an effective method for deciding truth of sentences in SC. This, according to R. M. Robinson [10], answers a question of Tarski's. In addition, a rather complete understanding of definability in SC will be obtained. 1. Notations. i denotes a n-tuple of predicate variables. Expressions like A [i(o)] B[i(t), i(t')] denote propositional formulas in the indicated constituents. Z1n, Tn, denote the classes of formulas of SC of the following type,: (Er) ~ A[r(o)] A (Vt) B[Ei(t), r(t), r(t')] A (at) C[r(t)] x1': (vr) - A[r(o)] v (at) B[i(t), r(t), r(t')] v (Vt) C[r(t)]' (ar) - F(ir), whereby F E An ~n+l' (Vr) - F(i,r), whereby F 6 The quantifiers (It)y A(t) for (st) [x _ t < y A A(t)], (Vt)Y A(t) for (Vt)[x < t < y DA(t], (et) A(t) for (Vx)(Et) [x< t AA(t)], (VIt) A(t) for (2x)(Vt) [x < t] A(t), (ij) A(j) for (Hj) [(e9t)j(t) A A(j)] can be defined in SC. The classes Lj and i of formulas are defined as follows, (: r) ~ A[r(o)] A (Vt)B[i(t), r(t), r(t')] / (~t) c[r(t)] (Vr) A[r(o)] v(.t) B[i(t), r(t), r(t)] / (vcdt) C[r(t)] 1. The author is much indebted to Dr. J. B. Wright. The work was done under a grant from the National Science Foundation to the Logic of Computers Group, and with additional assistance through contracts with the Office of Naval Research, Office of Ordnance Research, and the Army Signal Corps. 1

Let i be a k-tuple of predicates. The 2 states of i are the k-tuples of truth-values. i may be viewed as an infinite sequence i(o) i(l) i(2)... of states. The variables u, v, w,... will be used for words (i.e., finite sequences) of states. u v denotes the result of juxtaposing u and v. A congruence-relation is an equivalence relation u -iv on words such that u'-v implies u w vo w and w u-' w v. An equivalence relation is of finite rank if it partitions the words into finitely many classes. Also the following classes of formulas will play an essential role, reg: (Hr) - A[r(x)] A (VtY B[i(t), r(t), r(t')] A C[r(y)]'reg' (r)' A[r(x)] v (9tY B[i(t), r(t), r(t')] v C[r(y)]. These may be called regular formulas. Note that for a regular formula, R(i,x,y) depends only on the word iJ(x) i(x+l)... i(y-l). If R is the set of all words i(o) i(l)... i(h) such that R(i,o,h+l), then the formula R(i,x,y) is said to determine the set of words Ro 2. A fundamental lemma on infinite sequences. The working of the decisionmethod for SC is based on induction and a rather more sophisticated property of infinity, namely Theorem A of Ramsey [9].2 Essential parts of this theorem can actually be formulated in SC, in the form of a surprising assertion about the division of infinite sequences into consecutive finite parts. Lemma 1. Let i be any k-tuple of predicates, and let Eo,..., En be a partition of all words on states of i into finitely many classes. Then there exists a division i(o) >(1)... i(xl-1), i(xl) i(xl+l)... i(x2-1), i(X2) i(X2+1)... L(x3-1),... of i such that all words i(xp) i(xp+l)....(xq-l) belong to one and the same of the classes Eo,..., En. Proof: Assume i, En,.o., Ern are as supposed in lemma 1. For o - c - n let Pc consist of all Tyl,Y2) such that yl<Y2 and i(y1) i(yl+l)... i(y2=l) ~ Ec Then Po},'e, Pn clearly is a partition of all 2-element sets of natural numbers. By Ramsey's theorem A it follows that there is an infinite sequence xl < x2 < x3 <... and a o < c - n, such that fxp,xq) E Pc for all xp < xq. By definition of Pc this yields the conclusion of lemma 1. 3. Automata-theory. The following concepts and results are borrowed from the theory of finite automata, and play a very essential role in the study of SC. 2. The usefulness of the "Unendlichkeitslemma" of Kbnig [5 ] (also known as "fan-theorem" in its intuitionistic version) in related problems of automatatheory was first observed by Dr. J. B. Wright. Because of its affinity to K&nig's lemma the present application of Ramsey's theorem was suggested. 2

The reader is referred to Buchi [1], where some of the details are carried out in similar form, and where further references to the mathematical literature on automata are given Lemma 2. The following are equivalent conditions on a set R of words: 1) R is regular. 2) R = E U U nd whereby El,..., En are some of the congruence classes modulo a congruence relation of finite rank on words. 3) R is the set of words determined by a formula F(i,,x,y) belonging to -eg. 4) R is the set of words determined by a formula G(i,x,y) belonging to greg There is an "automata-recursion" r(o) - I, r(t') - J[i(t), r(t)] and an "output" U[r(t)] such that a word i(o) i()... i(x-l) belongs to R just in case the recursion produces an r(x) such that U[r(x)] holds. The reader who is rnot familiar with the concept of regularity of Kleene [4] may take 1-2 of the lemma as its definition (note the analogy to ultimately periodic sets of natural numbers). 35 —5 is shown in essence by Myhill's "subset-construction" [6]; nearly in the present form the details are carried out in BiUchi [1], lemma 7. By dualization one gets 4 —)5. The assertions 5 —.3and 5 -*4 are trivial. A proof of 2 f-3 is contained essentially in Rabin and Scott [8]. Lemma 3-. If the formulas R(i,xy), S(i,x,y) determine regular sets of words, then so do the formulas (at)Y R(ity), (Vt)Y R(i,t,y), R(i,x,y) S(i xy) R(i,x,y) V S(i,x,y), and ~R(i,x,y). This follows by lemma 2 and Skolem's method of replacing bounded quantifiers by recursions. Lemma 4. If the formula R(i,x,y) determines a regular set, then one can find formulas D(i) and E(i) in (in r1) such that D(i) (Vt) R(i,o,t) and E(i) (2t) R(Qil,o,t)). This follows by!(- 5 of lemma 2. The following lemma will provide the basis for the decision method of SC. It was suggested by, and its proof is typical for, automata theory. Lemma 5. There is an effective method for deciding truth of sentences A in Proof: Let C(r) be a formula of form K[r(o)] A (Vt) H[r(t), r(t')] A (eWt) L[(t)]. Suppose r is a k-tuple of predicates such that C(r) holds. Then there are xl < x2 <... such that LW(xl)], L[r(x2)],.... Because r has but a finite number of states, there must be a repetition r(xp) = r(xq) of some state U. 5

Therefore, (2r) C (r) implies the assertion, (1) There are words x = XOX1... Xa and y = Y1Y2... Yb of states and a state U such that L[U], and K[Xo] A H[Xo,X1] A... A H[Xa-l,Xa] A H[Xa,U], and H[U,Y1] A H[Y1,Y2] A... A H[YblYb] A H[Yb,U]. Conversely (1) implies (Sr) C(r), because one has but to let r = xUyUyUy.... Thus, a method I which decides, for given propositional formulas K,H,L and given state U, whether or riot (1) holds, will also be a method for deciding truth of 2j-sentences (2r) C(r). Clearly such a method I can be composed from a method II which, for given propositional formula H[X,y] and given states V and W, decides whether or not, (2) There is a word x = X1X2... Xa such that H[V,X1] A H[X,X2] A...A H[Xa_1,Xa] A H[Xa,W] Let n = 2k be the number of states, and note that in a word x = X1X2... Xa of length a > n there must occur a repetition Xp=Xq, p < q < a. Clearly if x satisfies (2), then so does the shorter word y = XX2... XpXq+lXq+2.. Xa Therefore, to establish whether or not (2) holds it suffices to check among the finitely many words x of length' n. This remark clearly yields a method II for (2), whereby lemma 5 is established. 4. Reduction of formulas of SC. The following lemma is obtained by methods similar to those in BUchi [1], lemma 1. Lemma 6. To every formula A(i) of SC one can obtain an equivalent formula B(i) belonging to some Z (to some en). Based on lemmas 1 to 4 one now can prove the fundamental fact on reduction of formulas in SC. Lemma 7. To every formula A(i) in ~ (in g1) one can obtain an equivalent formula B (i) in gm (in 1). Proof: Suppose A(i) is in Z, say (1) A(i): (r) ~ K[r(o)] A (Vt) H[i(t), r(t), r(t')] A ( t) L[r(t)]. If V,W are states of r and x = XoX1... Xh is a word of states of i then define, [Vx,W]1: H[Xo,,VU] / H[X1,U1,U2] /A H[X2,,UU 3] A... A H[Xh,Uh,W] U1..Uh I[V,x,W]2:. Uh E[X,V,U] A... A H[Xh,Uh,W] A [L[U1] V... V L[Uh]].

(Read [ ]1 as "there is an H-transition through L vrom V by x to W.") Next define the binary relation -'on words of states of i: x V} y VW ([vxW]l - [VVY.9, /VW\ ([V,_,W]2- [V, _,W]2) 2 2 If m is the number of states of r, then clearly c-is the intersection of m + m dichotomies. Therefore, (2) c-is an equivalence relation of finite rank a - 22m2. Furthermore, using the definitions of [ ]l and [ ]2 one obtains, (3) L. is a congruence relation on words. By (2), (3), and lemma 2 it follows that one can find formulas El(i,x,y),..., Ea(i,x,y) such that (4) El,..., Ea are regular formulas (i.e., belong to Eeg). (5) E,..., Ea determine the congruence classes of Le. Next one applies lemma 1 to the partition E1,..., Ea. If follows that for any %, (6) (2s),(Vy)(Vx)Y[s(x)s(6)DEl(i,x,y)] v...v (Es)W(Vy)(Vx)Y[s(x)s(y)DEa(ijxy)] If one defines for 1 - c,d < a, F~d(i):(3s), - (Rx)[s(x)AE,(colx).]A(V'y)(V.x)Y [s(x)s(y) DEd(i,xy)] then clearly each disjunct of (6) is equivalent to a disjunction of F,d's. Therefore, (7) i F-d(), holds for all i. 1 ~; c,d a -cd Suppose now that Fc d(i) and Fcd(j). Then, by definition of Fcd and by (5) there are x1 < x2 < X3 <... and y1 < Y2 < y3 <.. such that i()... i(xl-) j(o) -- j(yJ-l) i(Xp)..o i(Xp+l-1) (Yp j(Yp+l 1)p 12 xp+1- lV-Ji~y~... j~y~~1-l), = 1,2,5,... Because of the definition of'- and (1) it therefore follows that A(i) = A(j). Thus, if Fc,d(i) A Fc,d(j) then A(i) - A(j). Or restating this result, (8) (Vi) [c, d(B) 3 A(i)] V (Vi)[Fc d(i) ~A( )], for any 1 ~ c,d ~ a. If one now defines the set 0 of pairs 1 =< c,d < a by, (9) ~(c,d) ('j)[A(j) A L d(J)], for 1 _ c,d _ a it follows by (7) and (8) that 5

(1-) -,Ai) a-,d(i) By (4), lemma 3, and lemma 4 it follows that there are formulas D,(i,s) and Gd(is) in E1 which are equivalent respectively to6 (x) [s(x) A EC(,,o,x)] and (Vy)(Vx)Y [s(x)s(y) D Ed(i,x,y)]. Referring to the definition of Fa,d this yields, Fcd(i) (s) (t) s(t) A _(i.s) A G(is) Because Dc and G are in Z1 it follows, (11) Fc,d(i) - ([spq). I(o)A(Vt) J(t)A(St) M(t) A (St) N(t)A(.WDt) s(t), for some matrices Ip(o),q(o)], J[i(t), s(t), q(t), p(t), q(t'), p(t')], M[q(t)], N[p(t)]. Note that (2t)ff(t) A (A )N(t) A (e)s(t) may be replaced by [ix) [(.t)X M(t) A (9t)X N(t) A s(x) ], and this in turn may be replaced by (aJh) [-j(o3 /\ h(o) A(Vt)[j(t j(t) j) V M(t)] A (Vt)[h(t') h(t) V N(t)] A (39~t) [j(t)A h(t) A s(t) ]]. The corresponding substitution in (11) then shows that, for any 1 ~_ c,d _ a, the formula Fc d(i) is equivalent to a formula cd(i) in Z"1. By (10) it follows that ~A(i) is equivalent to a formula in z1, and therefore A(i) is equivalent to a formula B(i) in xl. This ends the proof of lemma 7. Theorem 1. The hierarchy of relations on predicates definable by formulas of j7l jn collapses at n=2. To every formula A(i) of SC one can find a formula B(i) of 1 (of slj, Z, 2 ) which is equivalent to A(. Proof: Let C(i): (Hr)[K(o) A (Vt) H(t) A (st) L(t)] be any formula of Zi. Then C(i) _ (2r) [K(o) A (Vt) H(t) A (Dx)(at)X L(t)]. If the term (St)o L(t) is dealt with as shown at the end of the proof of lemma 7, this yields a formula D(^) in >1 which is equivalent to C(i). Using this remark part one of theorem 1 easily follows by an induction of n and the use of lemma 7. By lemma 6 the other part of theorem 1 follows. Remarks: 1. The set U consisting of all infinite i can be defined by a Z' (a Zp) formula, but not by a iTj (a 1T2) formula. This shows that theorem 1 cannot be much improved. 2. Using theorem 1 one easily shows that also formulas A(i,xl,..., xn) of SC, containing individual variables can be put into a normal form, namely (3) ~ K[r(o)] A (Vt) H[i(t), r(t), r(t')] A (.rt) L[r(t)] A U[r(xl)] A... AU[r(xn)] This yields rather complete information on definability in SC. For example, 3. A conjecture of Robinson [10]: A relation R(xl,..., xn) on natural numbers is definable in SC if and only if it is definable in SCfin, which is like SC except that the variables i, j, r,... range over finite sets of natural numbers. This follows from remark 2 by methods similar to those in the proof of lemma 5. For complete discussion of definability in SCfin see Biichi [1]. 6

4. A relation R(il, o., in) on finite sets of natural numbers is definable in SC if and only if it is definable in SCfin" 5. Analyzing the proof of lemma 7 one obtains: A set R of n-tuples i of predacates is definable in SC if and only if R = S1 U... U Sk whereby each Sc is of the form A B B B.. -, A and B being regular sets of words. Lemmras 2, 3, 4, 6 carn be stated and proved in a strong constructive version. To see that this also holds for lemma 7, it remains to ascertain that the finite set 0 of pairs, defined by (9) in the proof of 7, may be obtained effectively for a given A(i). This follows by lemma 5, if one observes that A(i), Fc,d(i) and therefore (Lrj)[A(j)A F,d(j)] are equivalent to Zj formulas. It now follows that theorem 1 can also be proved in an effective version. In particular, to every sentence A of SC one can effectively construct an equivalent one belonging to Ej. Applying lemma 5 again this yields, Theorem 2. There is an effective method for deciding truth of sentences in SC. The strength of these results is best seen by noting some very special cases which occur in the literature and have been obtained by rather divergent methods: 1. The decidability of ~Z-sentences of SC contains the result of Friedman [31], and implies the existence of various other algorithms of finite automata theory as programmed by Church [2]. It also implies some of the results of Wang [11]. 2. In SC one can define x = y, x < y, x - y (mod k) (for k=1,2,...). The decidability of SC therefore considerably improves a result of Putnam [7]. 3. In SC one can define "i is finite." Theorem 2 therefore implies the decidability of SCfin) which was also proved in Buichi [1], and according to Robinson [10] is due to A. Ehrenfeucht. 4. The decidability of the first order theory of [Nn, +, Pw] follows from theorem 4 and improves the classical result of Presburger. 5. Theorem 2 is closely related to another classical result, namely the decidability of the monadic predicate calculus of second order, proved first by Th. Skolem and later by H. Behmarnn. A modified form of lemma 6 yields a rather simple solution to this problem. 7

BIBLIOGRAPHY 1. J. R. Bichi, "Weak second order arithmetic and finite automata." Zeitschrift fur Math. Log. und Grundl. der Math. (1960), pp. 2. Alonzo Church, "Application of Recursive Arithmetic to the Problem of Circuit Synthesis," Notes of the Summer Institute of Symbolic Logic, Cornell, 1957, pp. 3-50, and'Application of Recursive Arithmetic in the Theory of Computing and Automata," Notes: Advanced Theory of the Logical Design of Digital Computers, U. of Michigan Summer Session, 1959. 3. Joyce Friedman,"Some Results in Church's Restricted Recursive Arithmetic, Journal of Symbolic Logic, 22, pp. 337-342 (1957). 4. S. C. Kleene, "Representation of Events in Nerve Nets and Finite Automata.," Automata Studies, Princeton Univ.Press, 1956, pp. 3-41. 5. Denes Konig, Theorie der endlichen und unendlichen Graphen. Akad. Verlagsges., Leipzig, 1936. 6. John Myhill, "Finite Automata and Representation of Events," WADC Report TR 57-624 Fundamental Concepts in the Theory of Systems, October 1957, PP. 112-137. 7. Hillary Putnam, "Decidability and essential undecidability." Journal of Symbolic Logic, 22 (1957), pp. 39-54. 8. M. Rabin and D. Scott, "Finite Automata and Their Decision Problems." IBM Journal, April, 1959, pp. 114-125. 9. F. P. Ramsey, "On a problem of formal logic." Proc. London Math. Soc. (2) 30 (1929),pp. 264-286. 10. R. M. Robinson, "Restricted set-theoretical definitions in arithmetic." Proco Am. Math. Soc., 9 (1958),pp. 238-242. 11. Hao Wang, "Circuit synthesis by solving sequential Boolean equations." Zeitsch. fur Math. Logik und Grundl. der Math., 5 (1959), pp. 291-322.

SEQUENCE GENERATORS AND DIGITAL COMPUTERS A. Wo Burks J, B. Wright The University of Michigan

This research was supported by Project MICHIGAN (Contract No. DA-36-039sc-52654 of the U. S. Army Signal Corps), the Office of Naval Research (Contract No. Nonr 1224 (21)), and the Office of Ordnance Research (Contract No. DA-20-O18-oRD-16971). This paper grew out of some researches on well-behaved nets (see Sec. 3.1); Hao Wang participated in these early investigations and supplied an essential part of the proof of Lemma 353-1 for the case of well-behaved nets. J. Richard Buchi has made many helpful suggestions during the course of our work. (An early version of this paper was presented at a seminar session of the International Conference on Information Processing, Paris, June, 1959. An abstract of this early version should appear in the Proceedings of that conference.) -f —

INTRODUCTION 1.o Sequence -.enerators The basic concept of this paper-i that of sequence generator, is a generalization of the concepts of digital computer, finite automaton,l, logical net, and other information processing systems. In this subsection, we will define sequence generator and some related concepts and will illustrate them immediately thereafter~ Definitions: A sequence generator r = (S, G, R, P p,) consists of a set S (whose elements are called complete states), a set G (whose elements are called generators), a binary relation R (called the direct transition relation), and functions polo, pn (called projections), for some n = 0, 1, 2, 3,..., satisfying the conditions, (1) S is finite, (2) G is a subset of S, (3) R is defined on Sx, and each Pi (for i = 1, 2,..., n) is also defined on SO The values of the function pF, which may be entities of any kind, are called Pi-stateso A sequence generator may be represented by & finite-directed graph whose vertices denote complete states and whose arrows indicate when the direct transition relation holds between two states, In our diagram>'-we will. use rectanglesllatl. those. vertices -which represent \generatWr' sstates -and circles.at..yerticesscrepresenting complete states which are not also generators; the names of complete states and of P-states are written in the circles and rectangles, see Figures 1.2-1b, 1.2-2b, 1.3-1, etc. Though our diagrams are closely related to the usual state diagrams (transition diagrams) employed to represent automata (see, for example, Moore, 1956, p. 134) there are very significant differences. The vertices (nodes) of our diagrams represent complete states, while in the usual state diagrams the nodes represent internal states. This difference results from the fact that in sequence generators complete states are basic and input and output states are derived from complete states by means of projections, while in the usual approach complete states are derived by compounding internal states and input states. (The latter process is explained in Section 1.2; we will discuss the relation of the two approaches further in Section 2.1.) Some eomments and explanations concerning the definition of sequence generator may be helpful. If n=O then r = (S,, G R) is a sequence generator with no projections, Though our definiton of sequence generator permits any number of projections, in this paper we will be mainly interested in sequence generators with zero, one or two projections.

-2Furthermore, the set of complete states S of a sequence generator may be a null set; in this case the domain of definition of each function pl will be empty. It is worth noting that essentially (but not quite) the same concept of sequence generator can be obtained without using the set S of complete states in the definition and then defining S to be the union of G and the field of Ro We will use [a](j,k) (where j is a non-negative integer, k is a non-negative integer or k = cz; j = k) to denote the sequence <c(j), a(j+l),...,oC(k)> when k is finite and the sequence <a1(j), C(j+l), a(j+2),..0> when k = cu. If P is a projection, P([a](j,k)) abbreviates the sequence <P(a(j)), P(C(j+l)),...,P(C(k))> when k is finite and the sequence<P(ca(j)), P(a(j+l)), P(a(j+2)),...> when k = o. Definitions: Let r = (S,G,R,P,...,Pn) be a sequence generator and let k be a non-negative integer or w. [s](O,k) is r-sequence if (1) s(O)EG and (2) for each j, j<k, R(s(j), s(j+l)). A complete state s is { F-accessible} [r-admissible] if s occurs in some { —-— } [infinite] r-sequence. These concepts may be illustrated,'by reference to the direct transition diagram of Figure 1.3-la. The sequence <s7, s8> is a r-sequence, while the sequence <s,s,s' s6, s4, s6s4, s6,s4,s6,o. is an infinite r-sequence. Complete states s7',s8 and s9 are r-accessible but not r-admissible; complete states s3,s45,s5 and s6 are r-accessible and r-admissible, while states sOsl,s2' and s1O are inaccessible (and hence inadmissible). Definitions: Let p be a binary relation and a a set; we define p(a) = { y (Bx)p(x,y) & xca } A complete state s of r = (S, G, R,.., ) is a terminal state of r if R({s}) is null A terminal state of r is a complete state for which there is no successor by the direct transition relation R. Complete states s8 In Burks and Wright, 1953, p. 1364 we defined the concept of an admissible state of a net. When a net is converted into a sequence generator (see Sec. 1.2 below) these states will be accessible rather than admissible in the senses of these terms defined above.

-3and s10 are the terminal states of Figure l 3-1a.. Note that if r has no terminal states, every F-accessible state is r-admissible and vice-versa. We will sometimes need to combine several projections to make a composite projection of them.. For this we will use the notation p x p2 x... x pn which is defined by [P x P x... x P]() = <P1(s), P2(s),.., n(s)> 1.2 Special cases of sequence generators Many concepts in the theory of information processing turn out to be special cases of the concept of sequence generator or are closely related to this concept,. We will discuss a number of these in the present subsection. Since digital computers (automata) and logical nets are of special interest to us we will show in detail how the concept of sequence generator applies to them. In later sections we will derive both new and old results about automata and nets from our new theory of sequence generators We will begin with well-formed nets, review the method of deriving a finite automaton from a well-formed net, and then show how to derive a sequence generator from a finite automaton. We will use the definition of well-formed net of Burks and Wright, 1953, p. 1361, modified to allow arbitrary switching elements and delay elements whose initial output states are one as well as delays whose initial output states are zero. In net diagrams certain nodes (junctions) are designated as net outputs and are distinguished by stars. See Figure 1.2-la. A well-formed net (w.f.n.) may be analyzed in terms of its input states, delay output states, and net-output states. A digital computer represented by w.fn. operates as follows. The "state" of a net at a given time is determined by its input state i and its delay-output state d at that time; these pairs <i,d> are called the complete states of the net. For each time t (t = 0,1,2,...) the complete state Ki,d> determines the net output state X at the same time (t) in accordance with an output Sequence generators may also be derived from automata containing delays whose initial output states are unspecified; these are called "abstract delays" in Burks and Wang, 1953, po201 and Burks, 19579 seco 3o But we will not complicate the present discussion by considering automata with such delay elements.

-4function X, i.e., e = X(i,d). At time 0 the delay-output state dO is uniquely determined by the initial delay-output states of the delay elements. For each time t the complete state <i,d> determines the delay-output state dl at the next moment of time (t+l) in accordance with a direct transition function T, i.e., d1 = T(i,d). The net of Figure 1.2-la is a well-formed net which represents a binary counter. A is the input node, the starred node C is its net output node, and B its delay output node (the initial state of B is zero). The state of C at t indicates the binary count, i.e., the number modulo 2 of l's which have appeared (during the interval of time 0,...,t) on the input node A. The state analysis is given by the following table, where 0 is the initial delayoutput state. i(t) d(t) d(t+l) e(t) (i,d) = X(id) A B B C 0 0 0 0 0 1 1 1 1 0 1 1 1 1 0 0 Definition: A finite automaton is a sextuple <{i}, {d}, {e}, d0g Ty X> where, {d}, {e are finite non-empty sets (whose elements are called input states, internal states, and output states respectively), dO C {d} (dO is called the initial internal state), T is a function from the Cartesian product {i} x {d} into {d} (called the direct transition function), and X is a function from the Cartesian product {i} x {d} onto {e} (called the output function). (This is essentially the definition of Burks and Wang, 1956, p. 203; see also Moore, 1956, p. 1335) The procedure for analyzing a well-formed net which is described in the preceding paragraph clearly converts a well-formed net into a finite automaton. This procedure is reversible; that is, given a finite automaton, one can construct a well-formed net which realizes it. Thus the concepts of wellformed net and finite automaton are basically equivalent and either can be taken as a formal definition of the concept "finite digital computer" (See Church, 1955, Kleene, 1956, pc 5, and Burks, 1957, Seco 3 for other definitions of these conceptso) A three-projection sequence generator r = (S, G, R, I, 0, D) may be associated with a finite automaton as follows. The elements of S are the complete states <i,d> and the elements of G are the complete states <i,d0>o The direct transition relation is defined by R(<il,dl>1 <i2, d2>) d2 = T(i,dl)] and the input, output, and internal state projections by I(<ld>) = i, 0(<i,d>) = X(i,d), and D(<i,d>) = d respectively. The sequence generator associated with the binary counter

of Figure 1.2-la is represented by Figure 102-1b, As before, the rectangles represent elements of G. The subscripts on the complete states correspond to the nodes of the counter in the order A, Bo "sOOslos llysoo0slolsol> is an example of a finite r-sequence; in it the input sequence iOil1il3io0il9i0 produces the output sequence eO, ~e91 00 eO,e,1,e1 (and thus three "ones" on the input leave the counter recording "one"). Note that though the internal states do,d1 are represented on Figure 1.2-lb, the nodes of the graph correspond to complete states and not to internal states as in the case with the usual state diagrams used to represent automata. We have shown how to transform a well-formed net into a finite automaton and vice-versa. We have also shown how to derive a sequence generator from a finite automaton. The latter process is not in general reversible. Only certain sequence generators (those which are deterministic) may be realized by finite automata (see Section 2.1). Our next application of sequence generators is to arbitrary "nets", including nets that are not well-formed. We will use the concept of Burks and Wright, 1953, P. 13539 modified to allow arbitrary switching elements and both kinds of concrete delays. Each switch element translates into a switch equivalence which gives the state of the switch output as a truth function of the switch input, and each delay element translates into two delay equivalences, called the "initial delay equivalence" and the "recursive delay equivalence". The initial-delay equivalence gives the initial state of the delay output and the recursive-delay equivalence equates the delay output at any time other than O to the delay input at the previous time, Hence, each net translates into a conjunction of equivalences0 If the net is not well-formed this conjunction will not directly correspond to (will not give the structure of) a digital computer, but it may specify a computation or behavior condition on a digital computer, (see Section 4) and on this account is of interest, In a sequel to -this paper we will show how formulas of a much more general. kind can be reduced to conjunctions of net equivalences (see Section 4). Figure 1,2-~2a. shows a net with input node E and output node F. The non-input switch element driving node A represents the contradictory or'always false" truth function. The initial state of the delay AB is "true", which for coding reasons we represent by "1"; the initial state of the delay FC is 0. The switch equivalences for this net are A(t) 0- F(t) s F(t), and C(t) [E(t) &'B(t)]. B(O) 1 and C(O) 0 are the initial delay equivalences, while B(t+l) A(t) and C(t+l) - F(t) are the recursive delay equivalences. The procedure about to be described will, of course, associate a well-formed net with a sequence generator; in fact, this sequence generator will generally be different from either of two sequence generators associated with the wellformed net by the processes described above,

A two-projection sequence generator r = (S, G, R, I, 0) may be associated with an arbitrary net in the following way: A complete state s is an assignment of a truth value to each node of the net which makes the switch equivalences of the net true. An element s of S is a generator (element of G) if s assigns to the delay output nodes truth values which make the initial delay equivalences true. R(sls2), where sls2, e S if and only if the truth values which sl assigns to the delay-input nodes and the truth values which s2 assigns to the delay output nodes satisfy the recursive delay equivalences. For each complete state s {I(s)} [0(s)] is s cut down to the {input} [output] nodes (i.e., {I(s)J [M(s)] is the net {input} [output] state contained in s); the input projection will not exist if there are no input nodes. The sequence generator r (S., G, R, I, 0) associated with Figure 1.2-2a is represented by Figure 1.2-2b. Though there are six nodes in the net there are only eight complete states. The subscripts on the state symbols s1~s37, etc. are the decimal codings of the binary representations of the states of the nodes taken in the order E, A, B, C, F, G; e.g., the subscript on s decodes into 001001 showing that in this state nodes B and G are active while the remaining nodes are inactive. The subscript of the input state i is the state of node E and the subscript on the output state e is the state of node F. <slos537$s2Y S38 s37> is a Fr-sequence which has a derived.input sequence <iOil.,io0 ll i1> and a derived output sequence <e0,el,' e0Oel>. It can be proved that F(t) =:E(t+l); such behavior would not, of course, be possible in a well-formed net. Our process for associating a sequence generator with an arbitrary net is different from our process for associating a sequence generator with a well-formed net in the following basic respect. In the latter case we first defined input states, delay-output states (internal states), and output states for the net, and then compounded complete states from-input states and internal states. On the other hand, in associating a sequencegenerator with an arbitrary net we first defined states (complete states) over every node, and then derived input and output states by means of projections. It turns out that in general not every assignment of truth values to the input nodes of an arbitrary net is an input state. In fact, we know of no way of defining states for parts of a net(input, internal, and output states) without pre-supposing states for the whole net (complete states). Indeed, it was our work with arbitrary nets which led us to consider sequence generators (in which complete states are basic, input, internal, and output states derivative).

-7We will now mention other entities besides nets and well-formed nets (digital computers) which are either sequence generators or are closely related to sequence generators. The concept of a non-deterministic automaton of Rabin and Scott (1959, Definition 9) is quite similar to our concept of a sequence generator. Sequence generators are in a certain sense equivalent to formulas constructed from truth functional connectives, monadic predicates, one individual variable "t" (which ranges over discrete times), the successor function, and zero; we plan to develop this connection in a sequel to the present paper (see Section 4). The following are special cases of sequence generators: a finite state grammer (Chomsky and Miller, 1958, p. 95); sequential circuits representable in combinatory logic (Fitch, 1958, p. 263); incompletely specified automata, i.e., automata in which certain sequences of input states are proscribed (Aufenkamp and Hohn, 1957, Section IV); automata with terminal states (ibid., Section VII); and the flow diagrams used in programming a digital computer. A state diagram may be used to characterize a class of finite sequences defined by a regular expression (Myhill, 1957). Finite graphs may be used to analyze certain games (Konig, 1936; and McKinsey, 1952, Chapter 6). There is an obvious relation between finite graphs and sequence generators, and hence some problems concerning games may be studied by means of sequence generators; we will give an example in the next subsection. We remark finally that Harary and Paper (1957) in applying relational logic to linguistics use ideas closely related to the concept of sequence generator. Though we have noted a number of applications of the concept of sequence generator, we wish to make it clear that we are not attempting in the present paper to solve all the problems that have been considered for these applications. In the next subsection we will establish some results concerning infinite r-sequences for sequence generators without projections. In Section 2 we will treat some concepts in which a single projection plays an essential role, and in Section 3 we will work with concepts in which two projections play a special role. 1.3 Reduced form algorithm Algorithm plays a fundamental role in this paper, so we will make a few informal comments about them. An algorithm presupposes a well-defined set of entities, called "the domain of the algorithm". An algorithm is a finite system of rules which may be mechanically applied to any entity of its domain. An algorithm which terminates in a finite number of steps when applied to any entity of its domain is called a "terminating algorithm". The Reduced Form Algorithm to be described soon

is a terminating algorithm, since when it is applied to any sequence generator it will eventually terminate in a sequence generator. An algorithm with a domain D is called a decision procedure for a class A which is a subset of D if for every element of D which belongs to A the algorithm terminates in "yes" and for every element of D which does not belong to A the algorithm terminates in "no". The truth table procedure is a decision procedure for the class of tautologies of the propositional calculus. Before formulating the Reduced Form Algorithm we will describe informally what it does. Let us call a state s of a sequence generator r = (s, G. R, P,i.,Pn ) "extendable" if there is an infinite sequence of complete states <s(O), s(l), s(2),...> such that s (O) is s and R [s(i), s (i+l)] for i = 0, 1, 2... (Note that s is not necessarily a generator, and so the infinite sequence of complete states is not necessarily a F-sequence.) In Figure 1.3-1 states sO and sl are extendable, while states s7 and s10 are not. The Reduced Form Algorithm may be applied to any sequence generator r. In part 1 of the algorithm the operation of deleting terminal states is iterated until we arrive at a sequence generator r with no terminal states. Since a sequence generator has non-extendable states if and only if it has terminal states, r is essentially the result of deleting all nonextendable states from r. In part 2 of the algorithm one begins with the generators of r (and hence of r), and by a succession of steps obtains the accessible states of Jo A new sequence generator r+, called the reduced form of r, is defined on the basis of the states so obtained. Since a state is admissible if and only if it is both extendable and accessible r+ is just r cut down to its admissible states (see Theorem 1.3-1). Algorithm (Reduced Form Algorithm): Consider any sequence generator r = (S, G, R, pipn) (1) Form a new sequence generator by deleting all the terminal states of F, Iterate this process until you arrive at a sequence generator with no terminal states. Call this final sequence generator r = (S, UG R I1..o. n). (2) Define Al inductively by AO - Ai+1 = R(Ai) Form the sequence AoA1,A29..., stopping when AM+l c A=o Ai. (Note: act" means that a is either included in P or equals.) Let Mi=O Ai G = G, and let [pi] be the relation R [projection Pi] cut down to S. Define r+= = l n

-9We will illustrate the Reduced Form Algorithm. Let r = (S,GR) be the sequence generator represented by Figure 1.3-la, with'those complete states which belong to G being designated by rectangles. In part 1 of the algorithm we delete states s8 and sl0O then state s7, and then state S9. S consists of the remaining complete states, G contains s3 and s6. and R is R cut down to S. We have at the end of part 1 the sequence generator r represented by the result of deleting everything to the right of state 5 in Figure 1o.3-la In part 2 of the algorithm we form the sequence {Ss6} [=AO], {s4} [=Aj, {sIsS [-z2] {s49s6 s [} A3o A] Simultaneously we form the sequence {5 oS =+ 2A. T]h 6S4uSl eost woAi] [=u193A=], {,s1} 0 _0As],{s4, 5Ii C i=0Ai stopping at this point since + LS4,S6 C es35 ssi- 5a s6Y i.e. A Ai. Hence S = {se s and r, the reduced form of, is represente by Figure 1,3- r Theorem 1.3-1: The Reduced Form Algorithm, when applied to any sequence generator r, always terminates in a sequence generator r7a The set of complete states of fr equals the set or r-aldm-ssible complete states. As a step toward proving this theorem we first establish Lemma 1.3-2: let p be a binary relation and 6o a set. Define bi for i = 1,2... inductively by bi+l = P(6i) and let a, = _ for 2 = O,1,2,1.. If, for some j, aj = aj+l then for all aeg C aj the union, a1 +1 a= up(la). We now assume Ax = j+l and prove that a Ca., proving first by induction that for all 2 j, o - aj. The initial step is covered by the hypothesis that aj+l = aj For the general step assume =k aj, where k>j. By the fact noted above ak+l = (ku(ak) and jl = Cl U (a.) Combining the four preceding equalities we get ctk+l =aj. J 3 To conclude the proof we note that it follows directly from the definition of a that for i<jCxaccj. We turn now to the proof of Theorem 1.3-51. We will use freely the notation of the algorithm. (I) We prove first that the Reduced Form Algorithm, when applied to any sequence generator r, always terminates in a sequence generator r+ Since S is a finite set, the first part of the algorithm terminates in a sequence generator r. The criterion for stopping in part 2 of the *algorithm is based on a monotonically increasing sequence of subjects, of S. which is a finite set, so the second part of the algorithm will always terminate. Finally, it is clear that a sequence generator r+ is defined in part 2 of the algorithm. (II) We prove next that the set of complete states of r+ equals the set of r-admissible complete states (IIA) We consider a r-admissible complete state sl and show that s1e S. Since S1 is r-admissible there is an infinite sequence [s](O0,w) of 7-admissible states such that for some k, [s](k) = slo A complete state of r is deleted

-10by part 1 of the algorithm only if it cannot belong to an infinite r-sequence, and so [s](O,k) is a P-sequence. Hence by the definition of Ak in the algorithm, sl E Ak and sl E Ui=0 Ai. We now apply Lemma 1.3-2, letting p = R and 50 = G. By (I) above, part 2 of the algorithm terminates; in the notation of the algorithm Am+l C U A. The result of Lemma 1.3-2, put in this notation, is that for all X, A. C Um A. We have already shown that sl e U_ A., and so S1 E U. A But in the i=0: algorithm S is defined to be UmO Ai and so sl e. (TI) We next consider a complete state sl e S and show that sl is r-admissible. In the notation. m 1 m'of the algorithm S = Umi= Ai and so s E U. O Ai. Hence sl is r-accessible. Part 1 of the algorithm terminates in a sequence generator r with no terminal states. As remarked in Sec. 1.1 every accessible state of a sequence generator with no terminal states is an admissible state. Consequently there exists an infinite r-sequence [s](O,ct) such that for some k, sl = [s](k). By the nature of part 1 of the algorithm [s] (0O,O) is also an infinite r-sequence, and so sl is r-admissible. Corollary 1.3-3: (a) Every complete state of r+ is r+-admissible. (b) The set of infinite r-sequences equals the set of infinite r+ -sequences. (c) Every finitie r+-sequence is an initial segment of an infinite P-sequence. We will next discuss the Reduced Form Algorithm and some alternatives to it. Applied to an arbitrary sequence generator r part 1 of the Reduced Form Algorithm produces the set of extendable states of r. Applied to an arbitrary sequence generator r part 2 of the algorithm produces the set of F-accessible states. Since a complete state is admissible if and only if it is both extendable and accessible the two parts of the Reduced Form Algorithm applied to a sequence generator r in either order produce the same sequence generator r. A sequence generator r derived from a well-formed net in the way indicated in Section 1.2 has no terminal states; consequently when part 2 of the Reduced Form Algorithm is applied to r it produces r+. There is an alternative procedure for finding the r-admissible complete states of a sequence generator. Let x be the number of complete states of r. Form all F-sequences of length x+l.; it can be proved that a state is F-accessible if and only if it occurs in one of these sequences. To find the r-admissible states we operate on each sequence as follows: proceeding through the sequence <s(O), s(l),...,s(x)> check an occurrence of a state whenever that state has occurred earlier in the same sequence; then delete all states which follow the last checked state. It can be shown that a state is r-admissible if and only if it occurs in one of the

- 11resultant sequences. This method of finding the i-admissible states can be made the essence of an alternative reduced form algorithm which is simpler to formulate and easier to prove adequate than our Reduced Form Algorithm. It is less efficient however: in the example given earlier m = 2 while x = 11. These differences seem to result from the following fundamental difference between these two algorithms. In the Reduced Form Algorithm the length of the computation is not specified in advance; rather, parts 1 and 2 each contain an internal "stop criterion": one proceeds until he is stopped by these criteria. In contrast, the alternative algorithm first establishes the length of the computation on the basis of a general property of the sequence generator (the number of complete states); since this length is established a priori it is of course determined by the worst case, even though in most cases far fewer steps would have sufficed. This is analogous to the contrast between asynchronous circuits, in which completion of an operation is sensed and the next operation begun immediately, and synchronous circuits, in which the same amount of time is allowed for a given operation in every case, and this is, of course the time required for the worst case (plus a "safety factor"'.). We have presented the more efficient of these two algorithms, despite the fact that it is more difficult to formulate and prove adequate. We did this because finding the reduced form is basic to so many automata algorithms; see, for example, Section 2.3 and Section 3.4. But though in many later cases we know of morereffiitert algorithms (see for example, the alternative to the h-univalence Decision Procedure in'iSection 3.4), we will not present them because we feel that perspicuity of theory and simplicity of exposition is more important there. We mentioned in Section 1.2 that certain puzzles give rise to sequence generators. The so-called "15 puzzle" is a good example since it may be solved by means of our Reduced Form Algorithm. The puzzle consists of a 4 x 4 array of 15 movable blocks (number 1 through 15) and one empty position. A "move" consists in changing a pattern into any one of the (at most) four patterns obtained by shifting a block into the (neighboring) empty space. The problem is to achieve a stipulated pattern by a succession of moves starting from a given pattern. A sequence generator r = (S,G,R,P) corresponding to the puzzle may be defined as follows. The 4 x 4 matrices whose entries are the numbers 0 through 15 are the complete states of r; there are 16' of these. The starting pattern is the sole generator of r. Two states s1 and s2 stand in the direct transition relation R if there is a move taking the pattern corresponding to gs into the pattern corresponding to s2. The projection P has the value 1 on the single pattern stipulated

-12to be the goal and 0 otherwise. The problem is solved by constructing a finite P-sequence <s(0), s(l), s(2),...,s(t)> such that P[s(t)]= 1 and Pts(i)] = 0 for i<t, if such a sequence exists. Clearly this sequence exists if and only if the complete state with a projection of 1 is r-accessible. Whether or not this is the case can be determined by applying part 2 of the Reduced Form Algorithm to r: if such a sequence exists, it will be found in the course of carrying out the algorithm. It turns out that exactly half of the complete states of F are r-accessible and that each of these r-accessible states is also r-admissible. There is a much simpler algorithm for finding the r-accessible states of this particular sequence generator. See W. W. R. Ball, Mathematical Recreations and Essays, MacMillan, 1940, pp. 299-303~

-13A C (a) Binary Counter So10 1 do d1 (b) Three-projection sequence generator r = (S, G, R, I, Q,D) associated with the binary counter (a). Figure 1.2-1

E (a) Ill-formed net with behavior F(t) i E(t+l) 9 41 42_ S10 s2 38 io0 QO0 iVQ 0 (b) Sequence generator r = (s, G, R, I, G) associated with net (a) Figure 1.2-2

-15(a) Sequence generator r = (S, G, R) I 6 (b) r+, the reduced form of r Figure 1 3-1

2. Sequence Generators with One Projection 2.1 Definitions In the last sub-section we made no particular use of the projections of a sequence generator. In this section we shall define some concepts which apply primarily to sequence generators with one projection and will prove some theorems about these concepts. In most applications this single projection is an input projection, an output projection, or a combined input-output projection. In the next section we will work with sequence generators having two projections. These two projections will usually be an input and an output projection. Definition: The behavior of r = (S, G, R. P1,.., ), where n>O, is the set P ([s](O,k)), where P = P x P2x... pn and [s](O,k) is a FD-sequence (finite or infinite). "B(r)" denotes the behavior of r. The infinite behavior of r, denoted by "B13(r)", is the set of infinite sequences in B(r). Corollary 1.3-3b can now be reformulated as follows. Corollary 201-1: B3W(r ) = =B(r+) It is worth noting that in general it is not true that for a sequence generator r = (S,G,R,P) there exists a seauence generator t such that the set of P-sequence equals the behavior of r. This may be shown by a simple example. Let S = {s0,sls2,l} G = {s R = {<s sl>, <s1,s2>, <s2,s0>}, and P(s0) = P(sl) = P0, P(s2)= P1. There is one infinite r-sequence <sOsl s2,sOsl.s2,so0 slS2.'"> and the behavior of r consists of the sequence <p0,p0,plp0p0,pl,...> and all its initial segments, and does not include the infinite sequence p pp.>. Consider a sequence generator = (, R)such that p0,p C S and such that <P0yp.OPl'p0,p0ypl... > is an infir.-te i'-sequence. It follows from the existence of this sequence that R(po,p0) and p0 c G, and hence that <PO'PO'PO' > is an infinite P-sequence. We will now make some remarks about the application of the concept of behavior to nets. By the methods of Section 1.2 we can associate with every net (well-formed or not) a sequence generator r = (S, G, R, I, 8), where I is the input projection and e is the output projection. The behavior of a digital computer (wof.no) consists of the relationship between its inputs and its outputs, and similarly for an arbitrary net. The behavior of a net may be regarded as the set of sequences (finite and infinite) of pairs <i (O), e(0)>, <i (1), e(l)>, <i (2), e(2)>,... for which there is a r-sequence [s](O,k) such that -16

i(t) = I {s(t)} and e(t) = e{s(t) } for every t. This is clearly B(r), the behavior of the sequence generator r = (S, G, R, I, O). In Section 2.3 we present a Behavior Inclusion Procedure to be applied to a pair <r, r7 to decide whether the behavior of r is included in the behavior of r; when applied to the pair <r, 1'> as well as to the pair <r, 1> this tells us whether the behaviors of r and I are equal. By the remarks just made the Behavior Inclusion Procedure can be used to decide whether the behavior of an arbitrary net N is included in or equal to the behavior of a net No In the case of well-formed nets, however, a much more efficient algorithm for deciding equality of behaviors is known (Burks, Wang, 1956, Section 2.2); a basic part of this algorithm consists essentially of finding the reduced form (Section 1.3) of a sequence generator associated with the combined nets. Actually this algorithm applies to any deterministic sequence generator (this concept is defined below); moreover, if r and r are both deterministic and B(r) C B(r), then B(r' C B(r), so this algorithm also answers the question as to whether B(r) C B(r) for the case of deterministic sequence generators. The following lemma will be needed in subsequent proofs. It is a classical interpretation of Brouwer's Fan theorem (Heyting, 19569 pp. 42-43) and is closely related to Konig's Infinity Lemma concerning infinite graphs (K'nig, 1936, p. 81). Our lemma, however>, is stronger than K'Snig's Infinity Lemma in that it does not require that the a's be pairwise disjoint; because of this difference we present here a proof of it. Lemma 2.1-20 Let <0,al1,cO,..o2 be an acsequence of finite non-empty sets and let fp be a binary relation. If for every x e ai+l there is a y e ai such that p(y,x), then there is an infinite sequence <Zo Zl, Z2,..> such that for each i, zi E Gi and p(zizi+l). Proof: Let Pi consist of all finite sequences <xi,xi+l,..,Xi+k> where k = 0,1y92,yogj for i i+k and p(xj, xj+l) for i 5 j < i+k. It follows from the requirement on p in the hypothesis of the lemma that for each i,k9 and element Yi+k of ai+k there is an element of Pi <Yiy Yi+ly, ~ ~yi+k>~ Since this is so for any k, each Pi is infinite. We will now define by induction the desired sequence <zO9 Z1,9 z2. ~0>0 Initial step: Since P0 is infinite while a0 is finite there will be some element z0 of CG0 such that an infinite number of elements of P0 begin with zoo Let 80 be the subset of P0 all of whose elements begin with zo0

General step: Assume given a sequence <zozl1,. ~.ozi> (where i = 0,1,2,..) which belongs to P0 and satisfies the condition that the set 65 of elements of Pi which begin with zi is infinite. The result bi+l of deleting the first element of each member of Pi is an infinite subset of Pi+l, Since ai+l is finite there will be some element Zi+l of ai+l such that P(zi,zi+l) and an infinite number of elements of 6~i+l begin with zi+l Let 5i+l be the subset of 6i1+l all of whose elements begin with Zi+l;6'i+l is a subset of Pi+l and hence 5i+l is also. Hence <z0,zlooo9Zi Zi+l> belongs to 0 and satisfies the condition that the set 6i+l of elements of Pi+l which begin with zi+l is infinite. Thus the inductive hypothesis has been established for the sequence <Zozl9. Zi, zi+l>o This completes the proof of Lemma 2.1-2. Theorem 21l-3 (Infinity Theorem): Let r = (S, G, R, P) be a sequence generator with behavior B(r) and let [p](O,a) be an infinite sequence of P-states. [p](O, W) e B(r) if and only if for every finite k, [p](0,k) c B(r). Proof: (I) It is obvious that [p](O,w) E B(r) implies that for every finite k, [p](0,k) c B(r)o (II) Suppose that for every k, [p](0,k) c B(r)o We will pr)ove that [p](O0,c) e B(r) by means of Lemma 2.12, We define Ci by sl c a. if there exists a 3-sequence [s](O,i) such that [p](O,i) = P{[s](0,i } and si = s(i). It is clear that each ai is finite and nonempty. We let p = R and show that the hypothesis of Lemma 2.12 is satisfied. Suppose s c i+ By definition of aci there exists a 3-sequence [s ](Oi+l such that [p](0,i+l) = {[s3] 0, i+l)} and S2 = [s3l](i+1~ Let s4 = &i)o By the definition of cais4 ai and by the definition of r-sequence, R(sls2)o By Lemma 2.L2 there is an infinite r-sequence [s5](09OD) and by the definition of aci we have P{[s5](0c)} = [p](0,c). Hence [p]O,(0,) c B(r). The following is a corollary of the Infinity Theorem. Let r = (S, G, R, P) and 3 = (S, G, RY P) be two sequence generators and suppose that for every finite k, if [p](O,k)eB(r) then [p](Ok)eB(r); then B(r)cB(r). For consider any infinite sequence [p] (0,W) B(r3) By the Infinity Theorem, for each k [p](Ok)eB(r) Then by hypothesis, for each k [p](0,k)-B(r3). Finally, by the Infinity Theorem [p](O,M)cB(r.). This result holds for r and r interchanged, of course, so we have: if for every finite k [PI (O,k)CB(r) _ [p](Ok)eB(f) then:(r) = P(37). Thus the Infinity Theorem shows that the "finite" behavior of a sequence generator determines its (complete) behavior. Definitions: Let r = (S, G, R, P) be a sequence generator. r is solvable if every infinite sequence of P-states belongs to its behavior. r is {semi-deterministic} [deterministic] if it satisfies the conditions: (1) For any P-state p, there is Lat most one} [exactly one] complete state s of r such that sI G and P(s) = po (2) For any complete state sl and any P-state p of r, there is {at most one} [exactly one] complete state s2 such that R(sl,s2) and P(s2) = po

It is obvious from the definition of {semi=determinism} [determinism] that there is a decision procedure for the class of {semi-deterministic} [deterministic] sequence generators. The problem of solvability is not so simple, but we will later developa decision procedure for solvability (see Theorem 2 3-2). Let us illustrate these concepts. The sequence generator of Figure 1o2-1b, less its last two projections, is clearly deterministic, The sequence generator of Figure 201-la is semi-deterministic but not solvable, while the sequence generator of Figure 201-lb is neither semi-deterministic nor solvable0 By simple inspection it can be ascertained that the sequence generator (SG,R,P) of Figure 3o2-2a is neither semi-deterministic nor deterministic. It is, however, ssolvable, as the following considerations showo Given any -sequence of P-states divide it into a sequence (finite or infinite) of subsequences (finite or infinite), where each subsequence is either an iteration of V0 or an iteration of Pi and the two types of subsequences alternate. Now a rsequence sO sS 1 produces a Pastate sequence pg, pOg,pOp0O followed by at least one occurrence of p1, while a F-sequence s39s35oooS3S2 produces a P-state sequence PlPl, -o P1 Pl followed by at least one occurrence of po. Hence for any sequence of P-states [p](Ok) one can construct a r-sequence [s](O,k) such that [p](O,k) = p([s](0,k))g and so (S,G,R,P) is solvableo Consider next (S,G,R,I) of Figure 102-2bo (S,G,RI) is not semi-deterministic, since the input sequence <iQ3ioyi > is the projection of both <sgslysl> and <s9,sls2>, But (S,G,RI) is solvable, as may be shown by an analysis like that just given for Figure 32-2a; indeed, except for labeling, the behavior of Figure 102-2b is the same as the behavior of Figure 302-2ao The following lemma may be established by simple mathematical inductions with reference to the appropriate definitions. Lemma 2.1-4~ Let r = (S, GI R, P). (a) If r is {semi-deterministic} [deterministic] (solvable) then r+ is {semi-deterministic} [deterministic] solvable)o (b) If every complete state of r is r-accessible, then rV is semi-deterministic} [deterministic] if and only if for every finite sequence of P-states [p](O,t) there exists {at most one} [exactly one] I-sequence Is](Q,-t) such that iP[s](Ot))} = [p](Ot). (c) If f is deterministic, then r is solvableo Other senses of semi-determinism and of determinism may be obtained by replacing every occurrence of "complete state" in the above defintion of semi-determinism and determinism either by "admissible

-20complete state" or by "accessible complete state". We will call the concepts obtained by making the latter substitution "semi-determinisml" and "determinism. It may be shown that these two concepts are equivalent to the conditions stated in the consequent of part (b) of Lemma 2.1-4, In the case of arbitrary nets determinisml becomes the determinism of Burks and Wright, 1953, p. 1359. The process described in Section 1.2 associates with a finite automaton a sequence generator r = (S, G, R, I, O8 D) such that (S, G, R, I) is deterministic. Conversely, given a sequence generator r = (S, G, R, I, 0), where (S, G. R, I) is deterministic, we can define a corresponding finite automaton. Let the set of input states {i} and the set of output states{0} be the ranges of the projections I and 8 respectively. The set of internal states {d} of the sutomaton is a set of sets of complete states of r defined as follows: a {d}.- a = G.,v' (3s) (a = R(s)), where c ranges over non-null subsets of S. Let the initial internal state do=G. The direct transition function T is given by T(i,d) = R(Is I s E d & I(s) = i), where "is.o." means "the complete state s satisfying the condition"..." Finally, the output function X of the net is defined by X(i,d) = 8(isl s c d & I(s) = i). We will give an example. Figure 2.1-2a is a deterministic sequence generator. The set of input states for the associated automaton is {io,il} and the set of output states is O0SalY a2Ia O49. The set of internal states consists of the sets {s Isl}9 s2.9s. an! Iss 4} which we will call d,dl~ and d2 respectively. d is the initial internal state since {sOsl = G. The direct transition and output functions are given by the table i(t) d(t) d(t+l) e(t) =T(iyd) X.(i da) i0 dO d1 a0 i0 dO d2 01 i0 d1 d 1 dO il dX do 0d n Section 2 we gave a process for converting a finite automaton into a Inthree projectSection sequene process for converting a finite automaton into the three projection sequence generator. When this process is applied to the finite automaton just described the result is the sequence generator = (S, G, R, I,, D) of Figure 2.1-2b. It should be noted that B(r) = B(S, 6, R, I, k ). Hence when the two procedures just described are applied successively to a sequence generator F = (S, G, R, IN, ),

-21where (S, G, R, I) is deterministic, the result is a sequence generator F = (S, G, R, I, A, D) with an internal state projection D and such that the behavior of (S, G, R, i, &) is the same as the behavior of r. Any property of a one-projection sequence generator and any operation applicable to a one-projection sequence generator can be extended to a sequence generator r = (S, G, R) without projections by adjoining to it a constant projection P (i.e., a projection with only one P-state); r is solvable, deterministic, etc. if (S., G, R, P) is solvable, deterministic, etc. For example, a well-formed net without input nodes has associated with it (by either of the techniques of Section 1.2) a sequence generator (S, G, R) with one infinite (periodic) rF-sequence. For constant P, (S, G, R, P) is solvable and semi-deterministic, and hence deterministic, and so is (S., G. R); see, for example, Figure 2.2-la. 2.2 Subset sequence generator operation We will next define an operation, denoted by "*", called "the subset sequence generator operation' This operation may be applied to any sequence generator r to obtain its subset sequence generator F*. The complete states of rF* arte sets of complete states of r. The generators, the direct transition relation, &nd the projections of rF* are defined in terms of r in such a way that rF* has the same behavior as r (Theorem 2.2-3 below) and rF* is always semi-deterministic, even though r may not be (Lemma 2.2-1 below). Definition: The subset sequence generator operation,. denoted by "*" applies to any sequence generator r = ( S, G, R, p, p2,..,pn), where n>o, and produces a sequence generator r* = r = (S, G, R, P, P,... ). Let p = pl p2 X... x pn. (1) A subset x of S is an element of S if and only if x is non-null and P has the same value for all elements of x. This definition can be expressed symbolically as follows, where A is the null set, and the variable x ranges over subsets of S: xe S:_ xi A & (sl's2){[(sl e S) & (s2 E S) & S( E x) & (S x) [P(s) = P(s2 x) (2) The elements of G are maximal subsets of G which are elements of So Formally, s EG oo s S &c G & () [s S & (s C s C G)]D(s = sl) (3) Two complete states sl and s2 of S stand in the direct transition relation.i..if and only if s2 is a maximal set of direct successors (by R) of elements of s1. Formally, R(s1,s2):-: sl e & s2 CR (sl) & (so) {[sA E S & (s2Cs5CR(sl))]D(s2 = o)

-22(4) All the elements of a state s of S have the same pi state (for i = 1,2,...,n), and we take this common-value to be the P'-state of s. Formally, Pi(;) = pi(s) where s e s, s e S. (r* is called "the subset sequence generator" of r. Our concept of a subset sequence generator is similar to concepts used by Myhill, 1957, p. 122, Medvedev, 1958, p. 139 and Rabin and Scott, 1959, Definition 11.) It should be noted that the concepts of behavior (Section 2.1) and subset sequence generator are essentially one-projection concepts in the sense that when many projections pl,p2,..pn are given the composite projection plxp2x...Pn is used in the definitions of the concepts. In subsequent theorems and algorithmswe will, for the sake of simplicity, usually state our results for sequence generators with one projection, since it is obvious how to extend them to the many-projection case. The construction of subset sequence generators is illustrated in Figures 2.2-1, 2.2-2. Note that the generators and complete states of the subset sequence generator r* are determined without reference to the direct transition relation of r. Figure 2o2-1 shows that even though r is in reduced form, r* may not be. Though in fact, if r is in reduced form then r* has no terminal states and so B(r*) = B(r*+). In Figure 2~2-2 we begin with a semi-deterministic sequence generator, add to it in various ways to obtain three sequence generators, r, 1 r' which are not semi-deterministic, and then derive the subset sequence generator of each of these. All the subset sequence generator r1*, *, 17*, * are semi-deterministic, as they must be by the next lemma. None of the sequence generators r, r,, r is solvable; r*, r*9 r1*, and. 1* are not solvable either (cf. corollary 2.2-4). Lemma 2.2-1: For any sequence generator F = (S, G, R, P), r1* is semideterministic. Proof: Let r* = r = (S, G, R, P). It follows from the construction of G that for any sl, s2, if Slc 6~.G2E G and P(Sl) = P(s2)X then sl = s2, and it follows from the definition of R that for any s Sl; s2 if R(ss), R(s,s2), and P(s ) P(s2) then Sl = s2' Given a sequence generator r = (S, G, R, P), by the above lemma its subset sequence generator r* = r = (S, G, R, P) is semi-deterministic. Hence for any given finite sequence of P-states [p](Ot) there is at most one complete state Sl satisfying the condition that there exists a r-sequence [s](Ot-l), sl such that P{[s](O,tl), s} = [p](O,t). Moreover, this state

-23Sl is a set of states of ro We will use the location "the state Sl e s corresponding to [p](O,t)" to refer to this set of states 1l if itsexists, otherwise to the null set. Lemma 2.2-2: Let 1* = r = (S, G, R, P) be the subset sequence generator of r - (S, G, R, P), let [p](O,t) be any finite sequence of P-states, and let be the set of states sl for which there exists a r-sequence Is](O,t-l), sl such that P {fs](Ot-l), sl} = [p](Ot)o Then a is the state s1e 6 corresponding to [p ] (O t). Proof: (I) We first prove by an induction on t that for any finite r-sequence [s](Ot) there is a 1-sequence [s](o,t) satisfying the conditions (a) P {[s](O,t)} = P {[s](O,t)} (b) s(t) ~ s(t)o Initial step- given the r-sequence s(O), it follows by the definition of G that there exists a complete state s(0) such that s(O) e s(0) and s(0) e Go General ste~: The inductive hypothesis is that for every r-sequence ]J(Ok) there is a r-sequence [s](O,k) satisfying the conditions (a) and (b)o Consider ~ny? -sequence [s](O,k+l). By the inductive hypothesis there exists a r-sequence [s](Ok) such that [s](Ok) and [s](O,k) satisfy (a) and (b). Since R(s(k), s(k+l)) it follows by the definition of A that there exists a completb state sl such that s(k+l) E sl and A(s(k), sl)Y Hence P {s(k+.} = S(Sl) and [s']('-i9'k)9 s is a r-sequence, and so [s](Ok+l) and [s](O,k), S1 satisfy conditions (a and (b). (II) We next prove by an induction on t that for any finite T-sequence [s](O,t) and complete state sl e 5 (t) there is a r-sequence [s](O,t) satisfying the conditions (c) P{[s](o,t)} = P {[s](Ot)} (d) s(t) sl Initial step: given a r-sequence s(O) and a state sl E s (O), it follows by the definition of G that s is the desiietF1-eequence, General step: the inductive hypothesis is thlat for every 1r7sequence [](O0,k) and state sl e s(k) there is a r-sequence [s](O0k) satisfying conditions (c) and (d) Consider any r-sequence [s](Ok+l) and a state s2 e s(k+l). By the definition of A there exists a state sl satisfying the conditions sI e s(k) and R(sls2). By the inductive hypothesis there is a r-sequence [s](0 k) such that P {[s](0,k)} = P {[s](Ok)} and s(k) = sl. [s](0,k), s2 is the desired r-sequence- This completes the proof of Lemma 2.2-2~

-24Theorem 2.2-3: For any sequence generator r = (S, G, R, P) with behavior B(r), B(r) = B(r)*. Proof: By the preceding Lemma 2.2-2, for every finite t [p](Oyt) e B(r) if and only if [p](O,t) e B(r*). The theorem to be proved now follows by the Infinity Theorem (2.1-3). It should be noted in this connection that the proof of the Infinity Theorem makes implicit use of r*, the subset sequence generator of r. In fact, the sequence <aO9a19la2...> employed in the proof is an infinite r*- sequence. Lemma 2.2-4: For any sequence generator r = (S, G, R, P), r is solvable if and only if r* is solvable. (This follows easily from part 2 of Lemma 2.1-4, Lemma 2.2-1, and Theorem 2.2-3.) 2.3 Decision Procedures Behavior Inclusion Procedure: Consider two sequence generators r = (s, G, R P) and r = (s, G, R, I), and let {a} [a] be the number of states in {Sf [S]o Form all {I-sequences} [I-sequences] of length 1 + a2 or less and form the set {Qa} [a] of their {P-projections} [P-projections]. Write "yes" or "no" as acO or not. Theorem 2.3-1: Let A be the class of pairs of one-projection sequence generators <r,1> such that B(r) c B(r), i.e,, such that the behavior of r is included in that of r. The Behavior Inclusion Procedure is a decision procedure for A. Proof: (I) It is obvious that if B(r) c B(1) then Oac, i.e., that the algorithm yields "yes". (II) We assume that Oac&. ioe., that the algorithm yields "yes", and prove that B(r) c B(r). Let = (s G, R, P) = r* and let a be the set of P-projections of'-sequences of length 1 + a2- or less. By Theorem 2.223 =- a and B(r) = B(r), so we will assume that cca and prove that B(F) c B(f). (IIA) Let {at}[UIt] be the subset of sequences of {B(r)} [B(r)] of length t+l or lesso We will now establish by induction that for every t, at c ato Initial Step: Since by assumption cot: and by definition c = aao2a and =a - aaa so akClOk for k = a.2a. General step: we assume that cakcak for k > a.2a and prove that ak+lC ak+l. Consider an arbitrary r-sequence [s](O,k+l) for k = ao2ao Let [p](O,k+l) = P{[s]0, k+l)]}o By the inductive hypothesis there exists a r-sequence [s](Ok) such that i{[s](Ok)) = [p](0,k),

-25We will show that there exists a complete state "O satisfying the conditions (2) P(sO) = p(k+l), i.e., that there exists a r-sequence <[s](O,k),so> such that'j[s](O0k),s' = [p](O,k+l). It follows from the nature of the subset sequence generator construction that P has no more than 2 complete states,, and hence the number of pairs of complete states <s,s> is no more than a.2 Since k 2 a.2a there exist tl,t2; such that 0 - tl< t2 - a2a 5 k, s(t1) = s(t2) and s(tl) = s(t2). Let (3) [Sl](0,J+l) = {[s](, t1), [s](t2+l,k+l)} (4) [sl](o,a) = {['](o,t9), [s](t2+l,k)} (5) [Pl](O,2+l) = {[p](O,tl), [P](t2+1, k+l)} where 1 = k - (t2 - tl). Note that (6) P{[sl](o,e+l)} = [pl](o,1+l) (7) P['l"](OY)} = [pl](Oi,) Because s(t1) s(t2)} [s(tl) s(t2)] we have that {[sl1(O,e+l) (8) [s2] (0o, +l)} = [p1](o,2+i). It follows from (7) and (8) and (8) that (9) {[s2](o,e)} = i{[s1](o,)} = [p1](o, ) and since r is semi-deterministic (Lemmas 2.1-4 and 2.2-1) we have that (10) [2](1(o,) = [sl](o,=)o It follows from (4) that (11) s1 (=) =; (k)

-26and hence by (10) (12) 4"2() = S(k). Since [s2] (0$,+l) is a r-sequence we have that R{s2(G), s2(2+1)} and hence by (12) that (13) R{s(kX9 s2G(+l)}. Now by (8) and (5) (14) s2(2+l)} = p(k+l). Conditions 13 and 14 show that s2(i+1) satisfies conditions (1) and (2) and hence that s2(e+1) is the desired state s0o (IIB) We have shown that if Gaca then for every t, atC'6t. It follows by the Infinity Theorem (Theorem 2.1-3) that if aOca then B(r) cB(r') As remarked earlier this is equivalent to: if acc then B(r) cB(Fr). This completes the proof of Theorem 2.3-1. In formulating the Behavior Inclusion Procedure we have not attempted to minimize the computation required. Many simplifications will occur to anyone who uses this algorithm. For example, since any two elements of a complete state s c S must have the same projection the bound 1 + ao2 may be greatly reduced. Note also that if r is already semi-deterministic, it i not necessary to make use of r* in the proof, and the bound 1 + ao2 may be replaced by 1 + a&o The Behavior Inclusion Procedure may be used as the basis of a decision procedure for solvabilityo Let r = (S, G, R, P) be giveno By definition r is solvable if every infinite sequence of P-states belongs to its behavior (Section 2.1). r = (S, S, R, P), where R(sls2) for all sl's2 e S, has as its behavior the set of all sequences of Pstates. Hence the behavior of r includes all infinite sequences of Pstates, so r is solvable if and only if B(g) c B(r). By Theorem 2o3-1 the Behavior Inclusion Procedure is a decision procedure for behavior inclusion, so we have proved the following theorem. Theorem 2.3-2: Let r = (S, G, R, P) be a sequence generator and let R(sl'S2) for all sls2 e S. The Behavior Inclusion Procedure applied to the pair <(S, S, R, P), r> is a decision procedure for the solvability of Fo

-27When the Behavior Inclusion Procedure is applied first to the pair <rP r> and then to the pair <F, (> the result is "yes" in both cases if and only if B(r) = B(r). This "behavior equivalence procedure" may be used to reduce the number of complete states of a sequence generator so as to obtain a behaviorally equivalent sequence generator with fewer states. Consider r = (s, GI -R, P). We will say that two complete states sI and s are "behaviorally equivalent" if BI(S,{sl}s R,,)] =B[(S{s2} R P)].1 Let r be the result of identifying all behaviorally equivalent states of r. P will in general have fewer states than r and yet B(P) = B(r). Moore's concept of two sequential machines being indistinguishable by any experiment is a special case of our concept of behavioral equivalence, and the above process of identifying behaviorally equivalent states is analogous to the "reduction procedure" of Moore, 1956 and Mealy, 1955. We have examples to show that the procedure we described does not always lead to a behaviorally equivalent sequence generator with a minimal number of complete states and that the procedure of Moore and Mealy does not always lead to a behaviorally equivalent sequential machine with a minimum number of internal states.

-28so P0 (a) Semi-deterministic non-solvable sequence generator 0 e a-, (b) Sequence generator neither solvable nor semi-deterministic Figure 2.1-1

-29di s2 S1 i45 (a) Deterministic sequence generator r - (s, G, R, I, G) Figure 2.1-2 (part)

-30iO, 02 ioj do> />/<i1 dl io, Q01 i," // <i1' d2> il. dO> \\il, Q3 0 d2 <i~do> jQ <iO 12> io,"4 d2 (b) Internal state sequence generator (s, G. R, ), D ) corresponding to (a) Figure 2.1-2 (part)

-31~, r I S Is Si~' (a) r = (S, G, R, P) (b) r*, the subset sequence generator of r Figure 2.2-1 The construction of a subset sequence generator

PO p-~ l PO (P 1 —- (1 (a) Sequence generator (a,) r*, the subset r = (SI GI R, P). sequence generator of r. r is semi-deterministic I,* is semi-deterministic 0 ljO L o Po ~ ~~~~~ Po ~~~~~~~~O 0 ~~~~~~~~~~~~~~~~~~~~~~~~~~~p0 \ (b) Sequence generator (b') r*, the subset sequence generator of 1'. P is not semi-deterministic r* is semi-deterministic Figure 2.2-2 (part) Examples which illustrate Lemma 2.2-1: For any sequence generator 1 = (5, G, R, P) r* is semi-deterministic.

-3352 (c) f'= (s, 6G,, P).,S1 S P is not semi-deterministic (c * the subset sequence (cl) f*, the subset sequence generator of r. f* is semi-deterministic (d0 r{5 (S. G. R'P) (d) r= (.; "Re') r is not semi-deterministic (d) r*, the subset sequence.enerator of r. r* is semi-deterministic Figure 2.2-2 (continued)

3. Sequence Generators with Two Projections 3.1 Definitions The results of the last section concern primarily one projection of a sequence generator. In the present section we will work mainly with two-projection sequence generators. Definition: r = (S, G, R, P, Q) is h-univalent (h = 0, 1, 2,.~,,;3) if for every two infinite r-sequences [sl](O,w), [s2](O,U) and any time t, if P([sl](O,t+h)) = P([s2](O,t+h)) then Q(sl(t)) = Q(s2(t))o (By definition, t+C = a.) Note that h-univalence is essentially a property of a set of infinite sequences of pairs <pjq>, and hence a property of B"(r), the infinite behavior of To As a consequence the following lemma holds. Lemma 3.1-1: Let r = (S, G, R, P, Q) and = (S, G, R, iP Q)P If B~(r) = 7('F) then r is h-univalent if and only if r is h-univalento This lemma, together with Corollary 2.1-1 and Theorem 2.2-3, immediately yields Lemma 3.1-2: Let r = (s, G, R, P, Q). The following three conditions are equivalent: (1) r is h-univalent, (2) r* is h-univalent, (3) r+ is h-univalent. There is a close connection between zero-univalence and semideterminism which is brought out by the following lemma. Lemma 3.1-30 (a) Let r = (S, G, R, P, Q) and r = r+o r is 0-univalent if and only if for any two finite r-sequences:[sl](03t) and [s2](0,t), if P([sl](O0,t)) = P([s2](0,t)) then Q([sl](O,t)) Q([s2](0,t)). (b) Let r = (S, G, R, P) and r = -r+. r is semi-deterministic if and only if for any two finite r-sequences, [sl](0,t) and [s2](0,t), if P([s1](0,t)=Pk[s2](0.,t)) then [sl](O,t) = [s2](0,t)o Note that the sequence generator of part (a) of the lemma has two projections, while that of part (b) has one projection. Part (a) may be established by using Corollary 1.3-3 and the definition of univalence; part (b) follows from Corollary 1o3-3 and Lemma 2,1-4b. It follows from Lemma 3b1-3 that for any projection Q, if (S, G, R, P) is semi-deterministic then (S, G, R, P, Q) is 0-univalent. The converse is not in general true, but the following lemma asserts a connection between the 0univalence of a sequence generator and the semi-determinism of a related sequence generator.

Lemma 3.1-4: Let F = (S Gg R, P, Q) and let r'*+ = (S, Gg R, P, Q)o r is zero-univalent if and only if (S, G, R, P) is semi-deterministic. It might seem that since r is the reduced form of the subset sequence generator of', it would follow immediately by Lemma 2.2-1 that if F is 0-univalent then (S, G, R, P) is semi-deterministic. This is by no means the case. It can be shown from Lemma 2.2-1 by means of the definition of the subset sequence generator operation that (S, G, R, PxQ) is semi-deterministic, while the conclusion of Lemma 3.1-4 is that (S, G, R, P), which is a different sequence generator, is semi-deterministic. For any projection Q, if a sequence generator, (S, G, R, P) is semi-deterministic then (S, G, R, PxQ) is semi-deterministic, but the converse is not in general true. Proof of Lemma 3.1-4: ("Only if" part) We assume that r is 0-univalent and prove that (S, O 9, P) is semi-deterministic, (I) We will use three sequence generators in the proof besides F. These are: = (S, GQ R, P, ); r = (, G, R, PxQ); and = (s, G, R, P)o We will first establish some results that will enable us to use Lemma 3.1-3a on r and Lemma 3o1-3h on r and r. (A) By construction r = F+ and by Lemma 3.1-2 r is semi-deterministic. (B) By construction r = + and by Lemma 2.1-1 r is semi-deterministic. (C) By construction F' ='+ Our task is to prove that F is semi-deterministic. (II) Since F, r, and r have S, G, RG in common, the sets of F-sequences, V-sequences, and'-sequences are identical with one another. Consider now any two finite F-sequences [sl](0,t) and ['2](0,t); these are also arbitrary F-_sequences and arbitrary F-sequences. Using (IA) and applying Lemma 3o1-3a to F we obtain (1) If P([il3(0,t)) = P([S2](0ot)) then Q([~l](O,t)) = Q([12](Ot)) Using (IB) and applying Lemma 3.1-3b to F we obtain (2) If P([Sl](o0t)) = P([ t2](0,t)) and Q([sl](0t)) = Q([S2](0,t)) then [Sl](0,t) = [2](0, t). Combining (1) and (2) and noting that [sl](O,t) and [s2](0,t) are arbitrary'-sequences, we get (3) For any two finite r-sequences [l1](0,t) and [s2](0,t), if P([Sl](0=t)) = P([2]](0,t)) then [1s](0,t) = [s2](0,t).

-36I.. Using (3) and (IC) and applying Lemma 3.1-3b to r we obtain (4) r is semi-deterministic, which completes the proof of the "only if" part of the Lemma. ("If" part)~ We assume that (S, G, R, F) is semi-deterministic and prove that r is O-univalento Since every complete state of V is raccessible, by Lemma 2,1-4b we have that for every finite sequence of Pstates [p](Ot) there exists at most one V-sequence [s](O,t) such that [s~](O~t)) = [p](0,t). Hence for any two V-sequences [SlA](0,), [s2](0,0) and any time t, if P([sl](Ot)) = P([~2](Ott)) then sl(t) = s2(t). Since a projection is a (single-valued) function we have that if P([~S](O,t+O)) = P([s2](O,t+O)) then Q(Sl(t)) = Q('2(t)), so r is O-univalento V r*+, and by Lemma 3.1-2 r is O-univalento This completes the proof of Lemma 3.1-40 We next apply this lemma to an example. Consider r = (S, G, R, P, Q) of Figure 3.-l.ao Note that the complete states s2 and s4 have the same projections (pO and qo) and stand in the same relation to state so. Thus the two rFsequences so, S49 so SOY sS2g so have the same sequence of P-projections PO' Po, PO and hence (S, G, R, P) is not semi-deterministic. These two r-sequences do have the same sequence of Q-Projections q0o q2, q0 and in fact r is 0-univalento By Lemma 3.1-4 (S, G, R, P) of Figure 3.1-lb must be semi-deterministic. An examination of the states of (S, G, R, P) shows that it is deterministicy so a fortiori it is semi-deterministic. (The determinism of (S, G, Rg P) will be discussed after Lemma 3.2-3 below.) Note that the main difference between r and r*+ in Figure 3.1-1 is that the two states s2, s4 of r have become a single state {s2' s} of r*+o

Definition: I' = (S, G, R, P, Q) is uniquely solvable if (1) (S, G, R, P) is solvable and (2) (S, G, R, P, Q) is >-univalent. We remarked earlier that h-univalence is essentially a property of the infinite behavior of a sequence generator, and this remark applies to unique solvability as wello Thus r is uniquely solvable if and only if for any infinite sequence of Pstates [p](O,o) there is exactly one sequence of Q-states [q](O,w) such that the sequence Kp(O), q(O)>, <p(1), q(l)>,ooo belongs to B(r). T6 put the point in another way: a sequence generator r = (S, G, R, P, Q) is uniquely solvable if and only if its behavior defines a single-valued function (transformation) from the set of all infinite sequences of Pstates into the set of all infinite sequences of Q-states. Various consequences follow from this facto The result of replacing "h-univalence" by "uniquely solvable" in Lemma 3o1-1 is also a Lemmao A similar remark holds for Lemma 3ol-2 except that r+ may have fewer P-states (values of p) than r. It was shown in Section 2o1 that well-formed nets and deterministic sequence generators are equivalent m a certain sense- for every w~f~n. there is a corresponding deterministic sequence generator and viceversa. The wOf.n. gives the structure of an automaton while the associated deterministic sequence generator gives the corresponding complete state diagram. An analogous relation holds between the well-behaved nets of Burks and Wright, 19539 Po 1358 and uniquely solvable sequence generators. Consider any net and label all its non-input nodes as output nodes. The procedure of Section 102 will associate with this net a sequence generator which is uniquely solvable if and only if the original net is well-behavedo 3.2 The Displacement Operator and the I-Shift Operation We will first define a displacement operation Dk which applies to sets composed of finite sequences of pairs and/or wadsequences of pairs. Roughly speaking Dk has the effect of leaving the first element of each pair where it is and displacing the second element of each pair k places to the right. Displacing the second element of the first pair k places to the right will leave k gaps, since the first pair is not preceded by any pair. It will be convenient always to fill these gaps with the same element; we will use the fixed state q0 for this purpose. Definition: Let the universe of discourse V consist of all finite sequences of pairs and all a-sequences of pairs and let A be the null set. The operator D (without superscript) is defined to apply to any sequence of V as follows:

D(<xo, Yo>, <xl, Y>, <x2, Y2>, <x3, y3>,...) (<xo, A>, <xl, YO>, <x29 Yl>, <x3, Y2>,..) D(<xx0, YO>, <xl Yl>, o o-<xnl Yni>9 <xn, Yn>) = (<x0o A>, <.xl~ YO>yooo <Xn-l, Yn_2> <Xny Yn-l>) The operator D is extended to apply to an arbitrary set a of V by D(a) = {vI(u) [u e a & V = D(U) where v and u range over elements of Vo Finally, we define Dk, k = 0,1,2y,., to apply to an arbitrary set a of V by.the induction Do (a) a Di+l (a) = D(Di(a)) DR is called the displacement operator. We next define a shifting operation which may be applied to an arbitrary sequence generator r = (S, G, R, P, Q) to produce the I-shifted sequence generator r (S, G, R, P, Q). The effect of this operation is to displace the behavior of r, so that the behavior of Fa2, i.e., B(1ry), equals the displaced behavior of r1, ieO, D2[B(r)], as is shown in Lemma 3.2-1 below. To help make clear the definition of Fr, we will make some remarks about rl. Extend Q to apply to A, so that Q(A) = A. The generators of F2 are the pairs <A, s>. where s belongs to G. Suppose so, Sl9 s2~ s3, s4 is a f-sequence with the resulting behavior element <Po, qo>s <Pis l1>, <P2, q2>, <P3, q3>, <P4, q4>o Then <, A so>, <s, s1> y <bsn "2>9 2 3 A, 0>, <So, S>, <S1, s2> <s2, s3>> <s3, s4> is the corresponding rl-sequence with the resulting behavior element <pO, A >, <Pl, qo>, <P2, q1>, <P3, q3>, <P4, q3>o rF may be obtained by shifting r ~ times in this way.

-59Definition: The unit-shift operation, denoted by "<?", applies to any sequence generator r = (S, G, R, P, Q) and produces a sequence generator r< = i = (~, 9, R, fP, Q) defined as followso (1) The elements of G are all the pairs <A, s> where s belongs to G: <A, s> e G - sEG (2) The elements of S are all the pairs <sl, s2> which either belong to G or are connected by the direct transition relation R: = {<S1 s2> t <sl, s2> e G v R(s1s2)} (3) Two complete states <Sl1 s2> and <s3, s4> of S stand in the direct transition relation R if and only if s2 = s3~ R (<slp s2>, <s3, s4>) [<sl, s2>, <s3, s4> e S & s2 = S3io (4) The P-projection of a complete state <sl s2> of S is the P-projection of its second element s2: A(<sl, $2>) = P(s2), where <sl, s2> e S. (5) Extend Q to apply to A, stipulating that Q(A) = A. The Q-projection of the complete state <Sl, s2> of S is the Q-projection of it, first element: Q(<sl, s2>) = Q(sl), where <sl, s2> C So The i-shift operation, denoted by "1"' applies to any sequence generator r = (S, G, R, P, Q) and produces a sequence generator rP it is defined in terms of the unit-shift operation by means of an induction: rF = F r+l - (rJ)<> The i-shift construction is illustrated in Figure 3.2-1. Part (a) shows a sequence generator r with two projections, while part (b) shows r1, the result of shifting r one unit of time. It should be noted that the generator <A, so> can only occur as the first state of a P-sequence; an examination of the definition of the i-shift operation shows that the generators of any r2 can only occur as the first states of r -sequences.

(We are assuming throughout that A is not an element of S; if it is, S should be redefined so it is not.) Note also that both r and F1 are in reduced form; this is a special case of the general fact that if r is in reduced form then rh is in reduced form. We will discuss next the behaviors of r and Fl. The behavior element [ and the element of B(r)] (1) <Pgo, qo0> <PO" q0>, <Pl, ql>l <PO, qo> is derived from the r-sequence SO0 S0Y Sly S1, SO The corresponding Fl-sequence is <A, So>, <s0o S0>u <s0o Sl>g <S1y S.>1 <e l So> which gives rise to the behavior element [an element of B(r1)] (2) <po0 A>, <p0o q0>, <Pl qo0>, <Pl ql>> <Po' ql>. Note that this last sequence (2) is the result of displacing sequence (1) by one unit. This is an example of the general fact that B(Fl) = Dl[B(r)], which is a special case of the following lemma. Lemma 3.2-1: Let r = (S, G, R. P, Q). Then (a) D2[B(r)] = B(rI) (b) D [Bw(r)] = 3(r ) Proof: (IA) We prove first that D[BW(F)] = 3P(r<C>). Let <> = p = (S,G,R,P,Q). It follows from the definition of the unit shift operation that there is a one-one correspondence between the set of infinite r-sequences and the set of infinite F-sequences with corresponding sequences being of the form (1) so, sly s2 S3, (2) <A, so>, <sO, l1>, <sly s2>, <s2, 53>... When P x Q is applied to (1) we get (3) <PO' q0>' <Pl,9ql> <P2, q2>9 <P3s q3>, "

_41as an element of Be(F) and when P x Q is applied to (2) we get (4) <Po, A>~ <P1i qO>, <P2, ql>, <P39 12>, 0 0 as an element of B'(Fr). By definition of D, D[(3)] = (4). Hence D[B'0(r) ] = BM(Fr ). (IB) Applying mathematical induction to result (IA) we get D [B'l(r)] = BW(F)1]. (IIA) An argment similar to that of (IA) may be given for finite r-sequences and finite r -sequences. When the result is combined with result (IA) we get D[B(r)] = B(r~)o (IIB) Applying mathematical induction to (IIA) we get D [B(r)] = B(rI) Corollary 3,2-2~ Let r = (S, G, R, P, Q) and P - = (s G, R, P9 Q). [r is (i + h)-univalent] {(S, G, R, P) is solvable} (r' is uniquely solvable) if and only if [rI is h-univalent] {(S, G, R, P) is solvable} (rP is uniquely solvable). This corollary is illustrated by Figure 3.2-2. Consider r of this figure. It was shown in Section 2.1 (in the paragraph preceding Lemma 2.1-4) that (S, G, R, P) is solvable. Also, r is unit-univalent. To see this observe that every immediate successor (by the direct transition relation R) of a given complete state s has the same P-projection; e.g., R(sO) = {SO, Sl} and P(sO) = P(s1) = P0 Since (S, G, R, P) is solvable and r is unitunivalent, r is uniquely solvable.. Turn now to r1, the unit-shifted sequence generator of r. Since (S, G, R, P) is solvable and r is unit-univalent and uniquely solvable, by Corollary 3.2-2, Fl (less its last projection) must be solvable, and rl must be zero-univalent and also uniquely solvable. Lemma 3.2-3: Let r = (SGR,PQ) satisfy the conditions (1) r is h-univalent for some finite h (2) (S,G,R,P) is solvable. Let rh*+ = = (S,G,R,P,Q). Then (a) (S, G, R, P) is deterministic (b) Dh[Br(r)] = B)(R).

=42~ Proof~ (IA) We will prove first that (S, G, R, P) is solvable. It is given that (S, G, R. P) is solvable. By Corollary 3.2-2, Lemma 2.2-4, and Lemma 2.1-4a, (S, G, R, P) is solvable. (IB) We prove next that (l, G, R, P) is semi-deterministic. It is given that r is h-univalent. By Corollary 3.2-29 rh is O-univalent. By Lemma 3.1-4, (S, G, R, P) is semi-deterministic. (IC) It follows from Lemma 2.1-4b and the definition of solvable that if every complete state of any sequence generator r = (S, G, R, P) is raccessible, than r is deterministic if and only if r is both semi-deterministic and solvableo Applying this principle to (S, G, R, P) and using (IA) and (IB) we conclude that (S, G, R, P) is deterministic. This proves part (a) of the lemma. (II) By Lemma 3.2-lb h crh (I) D [Bw(r)] = B (h ). By Theorem 2o2-3 B(rh) B(rh* ) and hence (2) 3(rh) = B~ (r h*)o But by Corollary 2.1-1 (3) Be(rh*) Be(rh+). Combining (1), (2), and (3) gives part (b) of Lemma 352-3 and completes the proof of the present lemma. We may apply this lemma to Figure 3.1-1. As noted in Section 3.1 (S,G,R,P) is not semi-deterministic but (S, G, R, P,Q) is O-univalento It is easy to see that (S, G, R, P) is solvable. Applying Lemma 3.2-3 with h = 0 we conclude that (S,G,1,P) is deterministic and that Be(r) = BEP(). These two facts may be confirmed by inspection of Figure 3.1-b. Actually B( ) = B() in Figure 3.1-1, i.e, the finite behaviors of r and r are equal as well as the infinite behaviors. There is a variant of Lemma 3.2-3 which covers this point. Since our main interest in the present section is in infinite behavior we will merely state this result without proof. Let r = (S,G,R,P,Q) be h-univalent and (S,G,R,P) solvable; Then rh* less its Q-projection is deterministic, h[B(r)] = B(rh*) and if r is in reduced form then B(rh*) = B(Ph*+)B

1453 Figure 3.2-3 also illustrates Lemma 3.2-3. We begin with r = (S, G, R, P, Q), where r is unit-univalent and (S, G, R, P) is solvable. Lemma 3.2-3 tells us that rl*+ (less its last projection) is deterministic, and also that Dl[BW(r)] = Bw(rf2x+). (rl is shown in Figure 3.2-2b; it has 12 complete states. rl1 has 28 states, but only 6 of these are rl*-admissible, so Fl*+ has only 6 states.) 3.3 Time-Shift Theorem We will prove now a lemma which is used in proving one of our main theorems (the Time-shift theorem) and in validating a procedure for h-univalence. Lemma 3..3-1 (Fixed Bound Lemma): Let r = (S,G,R,P,Q) be a sequence generator with k r-admissible complete states. Then r is'-univalent if and only if it is k2-univalent. Proof: The proof is one direction is obvious. To prove that if r is iunivalent it is k2-univalent we consider any two r-sequences [sl](Ow), s2](0,w) and any time t such that P([sl](O,t+k2)) P([s2](0,t+k2)). Since there are k2 distinct pairs of complete states, there are two times tl, t2 such that t tl< t2= t + k2, s(t) = s1(t2), and s2(tl) = s2(t2) Form the sequences [s ](Oc)= [Sl](O,t2-l), [Sl](tl,t2-l), [sl](tl, t2-l),... [s4](0,w) = [s2](0,t2-1), [s2](tl,t2-l), [s2](tl,t2-l)... These are both F-sequences since they are composed of segments of r-sequences linked by the direct transition relation. Since P([sl](O,t+k2)) = P)[s2](0,t+k2)) we have by construction P([s3](0,a)) = P([s4)(O0,o)). Because r is Aounivalent, Q([s3](0,w)) = Q ([s4](0,c)). Then by construction Q(sl(t)) = Q(s1(t)) and Q(s2(t)) = Q(s4(t)), and so Q(sl(t)) = Q(s2(t)). Hence F is k -univalent. Consider a sequence generator F=(S,GR,P,Q). If (S,G,R,P) is deterministic then (SG,RP,Q) is uniquely solvable, but the converse does not in general hold (see Figure 3.1-la). We noted earlier (Section 3.1) that unique solvability is essentially a property of the infinite behavior of a sequence generator. This suggests the question: What is the relation of the behaviors of uniquely solvable sequence generators to the behaviors of deterministic ones? This question is answered by the following theorem,

[44which shows that for every uniquely solvable sequence generator there is a deterministic sequence generator whose infinite behavior is a displacement of the infinite behavior of the given sequence generator. In Section 4 we will introduce a concept of "computation". Using this concept the result may be expressed: the behavior of every uniquely solvable sequence generator can be computed by a finite automaton. Theorem 3.3-2 (Time-shift Theorem):, Let r d (S,G,R,P,Q) be a uniquely solvable sequence generator with k r-admissible complete states and let lk2*+ = r = (S,G,R,P,Q). Then (a) (SGgRP) is deterministic (b) Dk2[B(r)] = B= (r)o Proof: This follows immediately from the definition of uniquely solvable (Section 3.1)9 Lemma 3.2-3, and the Fixed Bound Lemma (353-3. Consider the Time-shift theorem in relation to r of Figure 3.2-2a and the derived Fl*+ of Figure 3o2-3. r is uniquely solvable and has 4 radmissible complete states. Then the time-shift theorem tells us that F16+, less its last projection, is deterministic. This is clearly so, for F*+ less its last projection, is deterministic, and further applications of the I-shift operation will obviously not destroy this property. We pause to note an analogue of the Time-shift Theorem in which the shifting takes place in the opposite direction. The displacement operator DI was defined to produce a right-shift of the Q-projections of a F-sequence; that is9 it shifts the Q-projections ~ steps later in time, leaving the P-projections as they were. One could easily extend this operator to cover shifts in the opposite direction (i.e., with the Q-projections moved earlier in time); this could be symbolized by using the same operator DI, allowing negative as well as positive integer values for I. Similarly the I-shift operator can be extended to produce shifts of the Q-projections to the left; again, we can use the same symbolism r and signify left-shifts by negative values of 9o We then get the following partial analogue to the time-shift theorem. Let r = (S GR,P,Q) be a sequence generator, with (S,G,RyP) deterministic, Let r = r, where I is negative. Then r is uniquely solvable, and D.(r)] = BW(F). Combining this with the Time-shift Theorem we obtain the following result~ the set of infinite behaviors of uniquely solvable sequence generators is exactly the set of displaced infinite behaviors of deterministic sequence generatorso

It is not obvious from the definition that the class of hunivalent sequence generators is decidable. However, this is in fact the case, as we will. now show. h-univalence Procedure (where h is any non-negative integer or w): Let r = (SG,R,PQ) be the given sequence generator. Find k, the number of admissible complete states, by the Reduced Form Algorithmo Let i = min (hk2) Form r = (S Answer "yes" or "no" as (S G.R P) is semi-deterministic or not. Theorem.3-3:3 The h-univalence procedure is a decision procedure for the class of h-univalent sequence generators. Proofo We will use the notation of the algorithm. By the Fixed Bound Lemma r is h-univalent if and only if r is ~-univalent. By Corollary 3.2-2 r is Y-univalent if and only if r is 0-univalent By Lemma 3.1-4'P is 0univalent if and only if (SGRP) is semi-deterministic. As noted in Section 201, it is obvious from the definition of semi-determinism that there is a decision procedure for the class of semi-deterministic sequence generators. This completes the proof of the theorem. It can be shown that the following is a characterization of hunivalence. Let r = (SG,RP,Q), k the number of r-admissible complete states, and = mi.n (hk2). Then r is h-univalent, if and only if, for any two r-sequences [Sl](O,c) and [s2](0,wu) and any time t k, if P([sl](Ot+')) = P([s2](0,t+e)) then Q(sl(t)) = Q(s2(t)). This characterization can be made the basis of a decision procedure for hunivalence which is more efficient than the one we have given. Since unique solvability is defined in terms of solvability and a-univalence (Section 31), by combining the ac-univalence procedure with the decision procedure for solvability of Theorem 2 3-2, we obtain a decision procedure for unique solvability.

-46s4 So s2 PO' q2 POj qO pgj q2 sI s3 (a) r = (s, G. R P, Q). r is zero-univalent and uniquely solvable, but (S,G,R,P) is not semideterm inisticc. (b) r'*+ - =(i, 6, R, %, &). (S, GI R~ P) is deterministic, and a fortiori semi-deterministic (S, G~ R, P) is semi-deterministic.

-47so L S1 (a) r = (S, G, R, P, Q) <Aj so> Os S Os> <s1, So> <SO, Sl> S<s, Sl> Pl,9 CO Pl, ql (b) rl (1 unit-shifted sequence generator of r) Figure 3.2-1 Illustration of the 4-shift construction, for ~ = 1. In accordance with Lemma 3.2-1, D'[B(r)] - B(r').

-48< <s2,, SOe <ss32> Po, ql P, qOi 11.1A isoe so> Sl s2i z lvable. <nl s3q lr is 1-univalent] {',l less its last projection, is solvable} if and only if [rLis O-univalent] {r', less its last projection, is solvable} (rl is uniquely solvable)

-49So s2 _' POIo I_- P9ClO P (a) r I (S, G. R. P. I) (S, G, R, P) is solvable but not deterministic. r is unit-univalent and uniquely solvable. Figure 3.2-2a

<s, s2> / P~wts POA 1', where <s is Figure.-a (ess> it<s 3> last projection) is deterministic Tsllus t rae PLem' T<siOlste a so sls2> Figure 3.2-3 r, where r is Figure 3.2-2a r and rl (less their last projectiorr) are not deterministic, but rl + (less its last projection) is deterministic D [BP(r)] = Be(rl ) This illustrates Lemma 3.2-3.

BIBLIOGRAPHY Aufenkamp, Do 0, and Hohn, Fo E., "TAnalysi s of Sequential Machines, Institute of Radio Engineers Transactions on Electronic Computers EC-6 (1957), 276-285, Burks, Ao W.,'"The Logic of Fixed and Growing Automata," in. Proceedings of an International Symposium on the Theory of -Switching_, 2-5 April, 1957, Cambridge- Harvard University Press, 1959, Part I, ppo 147-188. Burks, A, W. and Wang, Ho "The Logic of' Automata,' Journal of the Association for Computing Machinery 4 (1957), 193-218, 279-297. Burks, A. Wo and Wright, J. B. "Theory of Logical Nets," Proceedings of the Institute of Radio Engineers 41 (1953), 1357-1365o Chomsky, N, and Miller, G. Ao "Finite State Languages," Information and Control 1 (1958), 91-112. Church, A., The Journal of Symbolic Logic 20 (1955), 286-287. Copi, I. M.o Elgot, C. C. and Wright, J. B,,'Realization of Events by Logical Nets " Journal of the Association for Computing Machines 5 (1958), 1.81196, Fitch, F. B., "Representation of Sequential Circuits in Combinatory Logic." Philosophy of Science 25 (1958), 263-279. Harary, F. and Papery H. HI. "Toward a General Calculus of Phonemic Distribution, Language 33 (1957), 143'-169. Heyting, A., Intuitionism_ an Introduction Amsterdam, North Holland Publishing Co., 1956. Kleene, S. C.,'Representationof Events in Nerve Nets and Finite Automata " Automata Studies ed. C. E, Shannon and J, McCarthy, Princeton, Princeton University Press, (1956), 3-21. Konig, D., Theorie der endlichen und unendlichen Graphen, Leipzig, Akademische Verlagsgesellschaft M. B, H., 1936.

-52-,dvedev, I, T. "On a Class of Events Representable in a Finite Automaton," translated by J, J. Schorr-Kon from a supplement to the Russian translation of Automata Studies (edited by Co Shannon and J. McCarthy), Group report 34-73, 1958, Lincoln Laboratory, Lexington, Massachusetts. Moore, E. F,, "Gedanken Experiments on Sequential Machines," Automata Studies, edited by Co E Shannon and J. McCarthy, Princeton, Princeton University Press, 1956, 129-1534 Moore, E, F, and Shannon, Co E,, "Reliable Circuits using Less Reliable Relays," Journal of the Frankl.in Institute 262 (1956), 191-208, 281-287. McKinsey, J, C. C,, Introduction to the Theory of Games, New York, McGraw-Hill, 19520 Mealy, Go Ho, "A Method for Synthesizing Sequential Circuits, The Bell System Technical Journal 94 (1955), 1045-10790 Myhill, J~, "Fundamental Concepts in the Theory of Systems " WADC Technical Report 57-624, ASTIA Document Noo AD 155741, 1957, Putnam Ho. "Decidability and Essential Undecidability," The Journal of Symbolic Logic 22 (1957), 39-54, Rabin, M, 0, and Scott, D,, "Finite Automata and their Decision Problems, " IBM Journal of Research and Development 3 (1959), 114-125. Shannon, Co E., "A Mathematical Theory of Communication," Be'll System Technical Journal 27 (1948), 379-423, 623-656. Turing, A, Mo, "On Computable Numbers, with an Application to the Entscheidungsproblem," Proceedings of the London Mathematical Society Series 2, 42 (1936), 230-265 and 43 (1937)9 544-546, Von Neumann, J, "Propabilistic Logics and the Synthesis of Reliable Organisms from Unreliable Components," Automata Studies, edited by Shannon and McCarthy, Prince.ton, Princeton University Press, 1956, 43-980.Von Neumann, J., "The General and Logical Theory of Automata," Cerebral Mechanisms in Behavior, New York, John Wiley and Sons, 1951, 1-41 O

UNIVERSITY OF MICHIGAN 3 90 11111111115 02656 6490 3 0502656 6490