THE U NIVE R S I T Y O F M I C H I GAN COLLEGE OF LITERATURE, SCI:ENCE, AND THE ARTS Department of Philosophy Technical Report SEQUENCE GENERATORS AND FORMAL LANGUAGES Arthur W. Burks Jesse B. Wright ORA Project 03105 under contract with. DEPARTMENT OF THE NAVY OFFICE OF NAVAL RESEARCH CONTRACT NO, Nonr 1224(21) WASHINGTON, D, C, administered through: OFFICE OF RESEARCH ADMINISTRATION ANN ARBOR September 1961

I9XVn 1w4 7$

Most of the results presented herein are drawn from our much longer paper which is to be published in the Proceedings of the Symposium on Recursive Function Theory held in New York City, April 6-7, 19615 and sponsored by the American Mathematical Society, the Association for Computing Machinery, and the Association for Symbolic Logic. The terminology and mode of development in the present paper differ considerably from that of the longer paper. The fundamental concept is that of a sequence generator. An sequence generator is a finite, directed, labeled graph. Each node may or may not be labeled as a root R. Each node is labeled with a pair of truth values. We are particularly interested in what we call the "behavior" of a sequence generator (see Fig. 2). The behavior of a sequence generator is a set of matrices of truth values. The pairs of truth values taken from the nodes along an infinite path of the graph constitute a two-by-omega matrix. Such a twoby-omega matrix belongs to the behavior of a sequence generator if and only if it is taken from a path of the graph which begins with a root. For example, the first element of Fig. 2 is taken from the path that starts with the root and always stays in the root, while the second element is taken from the path that starts with the root and oscillates back and forth between it and the other node. This concept of behavior may be connected to the ordinary one by calling the upper truth value of a node an input and calling the lower truth value of a node an output. A sequence generator then determines a relation between infinite input sequences and infinite output sequences, which relation constitutes its behavior. The inputs and outputs labeling nodes may be vectors of truth values rather than single truth values, Our results all apply to this more general case, but in the interest of simplicity we will present them in terms of the case where the input and output vectors are of length one, Digital computers or finite automata are closely related to a special type of sequence generator called a deterministic sequence generator. Figure 3 is deterministic. A sequence generator is deterministic when it satisfies these two conditions: (1) For each truth value, there is exactly one root having that as its input truth value. (2) For each node and each truth value. there is exactly one node following the given node and having the given truth value as its input The deterministic sequence generator of Fig, 3 corresponds, in fact, to a binary counter. 1

Consider a graph derived from a digital computer or finite automaton in the following way. Each pair consisting of an input state and an internal state is a complete state. A node of the graph is provided for each complete state. The labels on a node give the input state and output state associated with the corresponding complete state of the automaton. Directed arrows of the graph indicate direct transitions between complete states. Any graph derived from a digital computer in this way is a deterministic sequence generator, and each deterministic sequence generator corresponds to a digital computer, The rows of truth values in the infinite matrices introduced earlier define predicates on the natural numbers. This suggests the use of logical formulas to represent sequence generators. We do this in an interpreted system called the sequential calculus, A formula of the sequential calculus is given in Fig. 4. The symbols of the sequential calculus are: individual variables,, interpreted as ranging over the natural numbers; monadic predicate variables, interpreted as ranging over predicates of natural numbers; the individual constant zero; the successor function; truth-functional connectives; and quantifiers on both individual and predicate variables. To each sequence generator there corresponds a formula of the sequential calculus, as illustrated in Fig. 4. The existential predicate quantifier "there is an s" asserts the existence of an infinite sequence of nodes satisfying four conditions: s(o) says that this infinite sequence of nodes begins with the root R, (VT) [S(T) V s(mT) ] that it is indeed a path of the graph; i(T) - S(T) and o(-X) s(T) define the input and output predicates for the path. This correspondence between formulas and sequence generators is such that a pair of predicates of natural numbers <i,o> satisfies the formula if and only if the corresponding two-by-omega matrix of truth values belongs to the behavior of the given sequence generator. See next the normal form of Fig. 5. Every formula derived from a sequence generator can be put in the normal form (Es) [R&((VT)P) ], where R and P are both truth functions, the root condition R being a truth function of s(o), P being a truth function of s(), s(T'), i(-r), and o(T). Conversely, one can derive from any normal form formula a corresponding sequence generator. Thus formulas of the sequential calculus can be studied by means of sequence generators, to which combinatorial methods can be easily applied. We will next present a theorem which was arrived at by working with sequence generators but is more easily stated here as a theorem about formulas of the sequential calculus, We introduce the following definition for a formula ~(i,o) containing i and o as the only free variables. {1(i,o) is uniquely solvable if and only if for each predicate i there is exactly one predicate o such that the pair

<i,o> satisfies (i,o) in the intended interpretation. It is clear that when a formula (i,o) is uniquely solvable, it implicitly defines a function such that o = i) if and only if'(i,o). o is a function which maps the set of all predicates of natural numbers into the set of all predicates of natural numbers. We are interested in a recursive definition of the type Church calls an unrestricted singulary recursion. As Fig. 6 shows, such a recursion gives: s(o) as a truth function of i(o),..., i(h) S(T') as a truth function of S(T); i(T'),..., i(T'+h) o(T) as a truth function of S(T), where h is a constant. Our first theorem is a definability theorem for uniquely solvable normal form formulas. The theorem is: for every uniquely solvable normal form formula Pe(i,o), there exists an equivalent formula (S)(T)2J(s,i,o,T), where 2)(s,i, o,T) is an unrestricted singulary recursion. Furthermore, the formula (HS)(T)V(S,i,o,T) can be constructed effectively from the given formula i,o). The proof of the definability theorem has three steps. The first can be expressed if we think of the natural numbers as discrete times with T being a time variable. Consider now a uniquely solvable normal form formula ~(i,o) and the corresponding sequence generator with input i and output o. The output o at time T may, contrary to physical reality, depend on input states which occur at a time later than T. Let k be the number of nodes of the sequence generator. It turns out that the amount of anticipation is bounded by k2, that is, the parameter h of the unrestricted singulary recursion is in fact k2. Thus the first step of the proof of the definability theorem establishes the fact that for a uniquely solvable sequence generator with k nodes, the output o at time T is independent of input states after T+k2. The second step of the proof of the definability theorem involves a function or operation on the class of sequence generators, called the subset sequence generator operation, and used by LMyhill, Medvedev, Rabin, and Scott. Let r be a sequence generator and let rF be the subset sequence generator of r. The nodes of r* are sets of nodes o-' P. The arcrows of r* are placed according to the arrows of r in such a way as to take account of the fact that a binary relation induces on the subsets of its domain a function which is single-valued. There are two important facts about r*. First, if r is uniquely solvable, then for each predicate i there is exactly one path of r* giving rise to i. Second, r* has the same behavior as F. Previous users of the subset sequence generator operation have shown this second fact to be so when behavior is based on finite sequences. Thfs behavioral equivalence may be ex35

tended to our concept of behavior, which is based on infinite sequences, by means of Kdnig's infinity lemma. As a consequence of steps one and two, our consideration of the normal form formula 6(i,o) is reduced to a sequence generator r* and a number k2 having these two properties: first, for each predicate i there is a unique path in r* giving rise to i; second, k2 is a bound on the time dependence of the predicates s and o on the predicate i, since S(T) and hence o(T) are independent of the input states after T+k2. To obtain the unrestricted singulary recursion for C(i,o) we must express S(T') as a truth function of s(T) and i(T),...,i(T'+h). For any given i we use the predicate s defined by the corresponding path through r* as the s of the recursion, and we take h to be k2. A simple argument based on the uniqueness of the path will show that S(T') is a time-independent truth function of s(T) and i(T'),...,i(T'+h). To write o as a restricted singulary recursion of i and s is now essentially a matter of an elaborate truth table. Our definability result may be generalized to arbitrary formulas of the sequential calculus by means of some theorems about the sequential calculus established by J. R. Buichi. Bfichi's main result is that there is a decision procedure for whether or not an arbitrary sentence of the sequential calculus is true in the intended interpretation. An immediate corollary of this result is that there is a decision procedure for unique solvability, since an arbitrary formula C(i,o) is uniquely solvable if and only if the following formula of the sequential calculus is true: (i) (H o) o)&(o)[ e(i, o)(T) (O(T) - O 1(T))]~. The generalization of our definability result involves the concept of a finitely anticipatory formula. A formula e(i,o) is finitely anticipatory if for each time T there is a integer h such that the input states from time zero up to time T+h determine the output state at time T. It should be noted that in an unrestricted singulary recursion h is a constant, whereas in the definition of finitely anticipatory, h is a function of T. Since' can be defined in the sequential calculus, the statement that g(i.o) is finitely anticipatory can be expressed by a sentence of the sequential calculus. Therefore, the decidability of truth of sentences of the sequential calculus implies that the class of finitely anticipatory formulas is effectively decidable. We can now state our general definability theorem. Let c (i,o) be any formula of the sequential calculus. The theorem states that the relationship between i and o can be expressed by an unrestricted singulary recursion if and only if C(i,o) is both uniquely solvable and finitely anticipatory. More

precisely, let,(io) be any foriula of the sequential calculus having i and o as the only free variables. There is an unrestricted singulary recursion s(s,io,?) such that. (i,o) - s)(T)s —si.,oT) if and only if (i,o) is both uniquely solvable and finitely anticipatory. Moreover, there is an algorithm applicable to6 (i,o) which yields an equivalent formula, (s) (T)2 (S,i,oT), if one exists.* TIhe proof of the generalized definability theorem is too involved to be presented here, but we will make some remarks about it. The proof uses a normal form involving an infinite existential quantifier (PZ ) (see Fig. 7). "(I3t)G" means that there exist infinitely many natural numbers satisfying G. The infinite existential quantifier -f AX) is definable in the sequential calculus. Bfuchi has shown that, for any formula e(i,o) of the sequential calculus having the predicates i and o as t;he only free variables, there is an equivalent normal form formula. As show-n in the top line of Fig. 7, this normal form is (.s) [R&(:'T) G)&((VT)P), where R is a truth function of s(o), G is a truth function of s(T), and P is a truth functmionl of S(T), S(T'), i(T), and (T)-r) This normal form is tihe sam),e as t.h orLe we had before except for the addition of the conjanoCt (r T i-G. The generalized normal formr of Fig, 7 c.aorresponds to an extension of the idea of sequence generator in which each node may or may not be labeled as a goal G f see Fig. 8). The effect of the infinite quantifier (,1) of the formula is obtained in a sequence generator rith goals by considering only paths which pass through the goals infinitely many times. There is then a one-one correspondence bet-weeen generalized nornal form formulas and sequence generators with goal1s, whizh. correspondence preserves behavior. Figure 8 gives an example of a sequence genlerattor with, goals and the equivalent generaalized norma.l.or fform fczula.:It will be recalled that in the r case of an ordinary uniquely solvable sequence generator vwitth. k nodegs, the outnput; o at. time T is determined by the input states from time zero up to time T-+k, The same lemma holds for those sequence generators with goals w-lich are both uniquely solvable and finitely anticipatory. so that, as before, the amoun-t of anticipation is independent of time. A om.nplete presentation of thie proo"f of the general definability theorem requires going inside iBUchi s proof of decidabiity for the sequential calculus and making -use of regular sets as defined by KLeene. We will not here present this proof but wilns cJoncl ude by s=nmmarizing the main result of this paper: there is an algorit}.n app icable to any formula of the sequential calculus with free input and output predicates. This algorithm produces an equivalent unrestricted singclary recursion2 if one exists, and otherwise indicates that none exist+s. *This theorem is not in the paper to be puiJ.ished in the Proceeding of the Symrnposium on Recursive Fun.tion Theilory. 5

t f f t R = root t = true f = false Fig. 1. Sequence Generator. Finite, directed, labeled graph. R t ttttt.. f f ffff... R t ftftf.. f ft ft ft.. Fig. 2. Two elements of the behavior of Fig. 1. t t f J | t Fig.. Deterministic sequence generator for a binary counter.

t f f I - t (3s) {s (o) (VT) [S(T) V S(T')] a [i (T) - S(T)] a [O(T) e S(T)] Fig. 4. Sequence generator and formula of the sequential calculus. (3 s) [R a((vT)P)] R [s(o)] P [s (T), S (T'), i (T), o (T)] are truth functions Fig. 5. Normal form. s(o) A [i (o),.... i (h)] a s (T') B [s (T); i (T'),.... i(T-+ h)] a o(T) D [s(T)] A, B, D, are trut-h functions Fig. 6. Unrestricted singulary recursion.

(3s) [R a ((3T ) G) a ((VT) P)J R[s(o)] G[s(T)] P [s (T), s (T'), i (T), o (T)] are truth functions Fig. 7. Generalized normal form. R G t f f. _- t (3s) s (o) & (3 T)S(T) ('T) [S (T) V S (')] & ( i (T) - s (T))a (O (T) S (T))] } Fig. 8. Sequence generator with goals and equivalent generalized normal form formula.

BIBLIOGRAPHY 1. Bichi, J.R., "On a Decision Procedure in Restricted Second-Order Arithmetic," to appear in the Proceedings of the 1960 International Symposium on Logic, Methodology and Philosophy of Science, Stanford University Press. 2. Church, Alonzo, "Application of Recursive Arithmetic to the Problem of Circuit Synthesis." Summaries of talks presented at the Summer Institute for Symbolic Logic, Cornell Univ., 1957, Institute for Defense Analysis, Princeton, 1960. 3. Kleene, S.C., "Representation of Events in Nerve Nets and Finite Automata," in C.E. Shannon and J. McCarthy (eds.), Automata Studies, Princeton University Press, Princeton, N.J.3 1956, pp. 3-41. 4. KEnig, D., Theorie der Endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft M.B.H., Leipzig, 1936. 5. Medvedev, 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, C.E. Shannon and J. McCarthy (eds.), Group Report 34-73, Lincoln Laboratory, Lexington, Mass., 1958. 6. Myhill, J., "Finite Automata and Representation of Events," in Fundamental Concepts in the Theory of Systems, WADC Technical Report 57-624, ASTIA Document No. AD 1557 41, 1957. 7. Rabin, M.O., and D. Scott, "Finite Automata and Their Decision Problems," IBM Journal of Research and Development, 1959 3, 114-125.

DIS TRIBUTION LIST (One copy unless otherwise noted) Asst. Seco of Defo for Res0 2 Bureau of Ships and Engo Department of the Navy Information Office Library Br. Washington 25, DoCo Pentagon Bldgo Attn Code 671 NTDS Washington 25, Do C. Chief, Bureau of Ships Armed Services Tech. Inforo Agcyo 10 Department of the Nary Arling Hall Stao Washington 25, D oC0 Arlington 12, Virginia Attn Code 280 Chief of Naval Research 2 Chief, Bureau of Ships Department of the Navy Department of the Navy Washington 25, DoCo Washington 25, D.C. Attn Code 437, Inf. Syst. Br. Attn Code 687E Chief of Naval Operations Naval Ordnance Laboratory OP-071-12 White Oaks Navy Depto Silver Spring 19, Maryland Washington 25, Do C. Attn Technical Library Director, Naval Res. Lab, 6 David Taylor Model Basin Tech. Inf. Officer/Code 2000 Washington 7, D. Co Washington 25, D.oC Attn Technical Library Commanding Officer, Officer of 10 Naval Electronics Laboratory Naval Research SanY Diego 52, California Navy No. 100, Fleet PO 0. Attn Technical Library New York, New York University of Illinois Commanding Officer, ONR Br. Office Control Systems Laboratory 346 Broadway Urbana, Illinois New York 13, New York Attn Do Alpert Commanding Officer, ONR Br. Office University of Illinois 495 Summer St. Digital Computer Laboratory Boston 10, Massachusetts Urbana, Illinois Attno Cr. JoEo Robertson Office of Technical Services Technical Reports Section Technical Irmcfrmation Officer Department of Commerce U.So Army Signal Research and Dev. Lab. Washington 25, D oC Fort Monmouth, New Jersey Attno Data Equipment Branch

DISTRIBUTION LIST (Continued) Director 3 Naval Ordnance Laboratory National Security Agency Corona, California Fort Geoo Go Meade, Maryland Attno HoHo Weider Attn0 Chief, REAMP George Washington University Naval Proving Ground Washington, DoC0o Dahblgren, Virginia Attno Profo No Grisamore Attno Naval Ordmn Computation Center Dynamic Anal and Control Lab. National Bureau of Standards Massachusetts Institute of Tech. Washington 25, DoC o Cambridge, Massachusetts Attno Dro SoNo Alexander Attno DoWo Baumann Aberdeen Proving Ground, BRL Burroughs Corporation Aberdeen Proving Ground, Maryland Research Center Attno Chiefs Computation Labo Paoli, Pennsylvania Attno AoJ0 Meyerhoff Office of Naval Research Resident Representative Hermes Incorporated University of Michigan 75 Cambridge Parkway 820 E. Washington Street Cambridge 42, Massachusetts Ann Arbor, Michigan Attn0 Mr. Reuben Wasserman Commanding Officer Lockheed Missiles and Space Div. OR., Branch Office 3251 Hanover Street John Crerar Library Bldg. Palo Alto, California 86 East Randloph Street Attn0 D.oG Willis Chicago 1, Illinois Univo of Michigan Commanding Officer Ann Arbor, Michigan ONR Bralnch Office Attno Depto of Philosophy, 1030 Eo Green Street Profo Ao Wo Burks Pasadena, California Census Bureau Commanding Officer Washington 25, Do C. ONR Branch Office Attnr Office of Asst. Director for 1000 Geary Street Statistical Services, San Francisco 9, California MrE Jo Lo McPherson National Bureau of Standards National Science Foundation Washington 25, D.C. Program Dir. for Documentation Reso Attn. Mr4 RoDo Elbourn Washington 25, D0 Co Attno Helen Lo Brownson

DISTRIBUTION LIST (Continued) Univ. of California - LA Diamnond Ordnance Fuze Laboratory Los Angeles 24, California Attn. Library Attn Depto of Engineering, Washington 25, D. Co Profo Gerald Estrin U.S. Army Signal Research and Dev. Lab, Columbia University Fort Monmouth, New Jersey New York 27, New York Attno M. Tenzer Attn. Depto of Physics, Profo Lo Brilloutin Harvard University Cambridge, Massachusetts Hebrew University Attn School of Applied Science, Jerusalem, Israel Dean Harvey Brook Attn. Prof. Y. Bar-Hillel The University of Chicago Massachusetts Inst. of Technology Institute for Computer Research Cambridge, Massachusetts Chicago 37, Illinois Attno Profo W. McCulloch Attn, Mr. Nicholas C. Metropolis, Dir, Benson-Lehner Corporation Commander 1860 Franklin Street Wright Air Development Diis:-ion Santa Monica, California Wright Patterson Air Force Base, Ohio Attn Mr. Bernard Benson Attno WCLJR, Maj* L. M. Butsch Atomic Energy Commission Laboratory for Electronics, Inc. Washington 25, D. C. 1079 Commonwealth Ave. Attn. Division of Research Boston 15, Massachusetts Attno Cro H. Fuller Naval Research Laboratory Washington 25, D. C. Stanford Research Institute Attno Security Systems Computer Laboratory Code 5266, Mr. G. Abraham Menlo Park, California Attno H. D. Crane Cornell University Department of Mathematics General Electric Co. Ithaca, New York Schnectady 5, New York Attn. Profo Mark Kac Attn. Library, LoM.Eo Dept., Bldg. 28-501 Dr. A. M. Uttley National Physical Laboratory The Rand Corporation Teddington, Middlesex 1700 Main Street England Santa Monica, California Attn.- Numerical Analysis Dept. Willis Ho Ware

DISTRIBUTION LIST (Continued) Hunter College Post Office Department New York 21, New York Office of Research and Engineering Attno Dean Mina Rees 12th and Pennsylvania Ave. Washington 25, D. C. General Elestric Research Laboratory Attno Mro Ro Kopp, Res. and Dev. Div. Po.o Box 1088 Schenectady, New York Air Force Cambridge Res. Center Attno Information Studies Section Lo Go Hanscom Field, Bedford, Mass. Ro Lo Shuey, Manager Attno Chief, CRRB Radio Corporation of America Office of Chief Signal Officer Moorestown, New Jersey Department of the Army Attno Missile and Surface Radar Divo Washington, Do C. Sidney Kaplan Attn. Res, and Dev. Div. SIGRO-6D Mr. L. H. Geiger University of Pennsylvania Institute of Co-Operative Research Bell Telephone Laboratories Philadelphia, Pennsylvania Murray Hill Laboratory Attn. Dr. John O'Conner Murray Hill, New Jersey Attno Dr, Edward F. Moore Stanford Research Institute Menlo Park, California National Biomedical Research Inst. Attn Dro Charles Rosen 9301 19th Avenue Applied Physics Group Hyattsville, Maryland Attn. Dr R. S Ledley, Northeastern University 360 Huntington Avenue National Bureau of Standards Boston, Massachusetts Washington 25, D. C. Attn. Prof. L. 0. Dolansky Attn. Mrs. Frances Neeland Marquardt Aircraft Company University of Pennsylvania 16555 Saticoy Street Moore School of Electrical Eng. P. 0o Box 2013 - South Annex 200 South 33rd Street Van Nuys, California Philadelphia 4, Pennsylvania Attn. Dr. Basun Chang, Res. Scientist Attn, Miss Anna Louise Campion Texas Technological College Varo Manufacturing Company Lubbock, Texas 2201 Walnut Street Attn Paul G. Griffith Garland, Texas Dept. of Electrical Engineering Attno Fred P. Granger, Jr. IBM Corporation Data Processing Systems Staff Military Products Division Department of State Owego, New York Washington 25, D. C. Attrno Dro So Winkler Attn. Fo Po Diblasi

DISTRIBUTION LIST (Continued) Dro Saul Gorn, Director Federal Aviation Agency Computer Center Bureau of Research and Development University of Pennsylvania Washington 25, Do Co Philadelphia 4, Pennsylvania Attn. RD-375 / Mr. Harry Hayman Applied Physics Laboratory Mro Donald F. Wilson Johns Hopkins University Code 5144 8621 Georgia Avenue Naval Research Laboratory Silver Spring, Maryland Washington 25, D. Co Attno Supervisor of Technical Reports David Taylor Model Basin Bureau of Supplied and Accounts, Chief Washington 7, D. CO Navy Department Attno Aerodynamics Lab., Code 628 Washington, Do CO Miss Cravens Attno Cdro JoCo Busby, Code W3 Chief, Bureau of Ships Auerbach Electronic Corporation Code 671A2 1634 Arch Street Washington, D. C. Philadelphia 3, Pennsylvania Attno Lcdro Eo Bo Mahinske, USN National Aeronautics and Space Admin. Lincoln Laboratory Goddard Space Flight Center Massachusettes Insto of Technology Greenbelt, Maryland Lexington 73, Massachusettes Attn. Chief, Data Systems Division Attno Library

UNIVERSITY OF MICHIGAN 3 9015 02846 7366lll II I I 3 9015 02846 7366