THE UN IVE RSITY OF MIC H I GAN COLLEGE OF LITERATURE, SCIENCE, AND THE ARTS Department of Mathematics and Logic of Computers Group Technical Report DECISION PROBLEMS OF FINITE AUTOMATA DESIGN AND RELATED ARITHMETICS Calvin C. Elgot administered by June 1959

The work reported and discussed in this thesis has been carried on under the listed grant and contracts with the following agencies: National Science Foundation Washington, D.C. NSF Grant - G-4790 Office of Naval Research Washington, D.C. Contract NONR-1224(21), Project NR 049-114 U.S. Army Office of Ordnance Research through Detroit Ordnance District Detroit, Michigan Contract DA 20-018-ORD-16971 U.S. Army Signal Supply Agency Laboratory Procurement Support Office Fort Monmouth, New Jersey Contract DA-36-039-sc-78057

ACKNOWLEDGMENTS I wish to thank Drs. J. B. Wright and J. R. Buchi for stimulating and helpful discussions, my wife for typing and editing the manuscript of this thesis, and the following Federal agencies for financial support: National Science Foundation, Office of Naval Research, Office of Ordnance Research, and the Signal Corps. -iii

TABLE OF CONTENTS Page ACKNOWLEDGMENTS...o o. * * * o. iii ABSTRACT................, vi Chapter I. BACKGROUND............... 1 1. Motivation 2. Some Basic Notions 3. Two Characterizations of Automata Behavior II. TRUTH ALGORITHMS FOR CERTAIN ARITHMETICS........ 8 4. Truncation Lemma 5. Characterization of Automata Behavior Via a Formal Arithmetic III. SOLVABILITY ALGORITHMS.............,. 27 6. Some Operations which Preserve Regularity 7. Characterizations of A/B-Automata Behavior 8. Solvability-Synthesis Algorithms 9. Remark IV. NON-EXISTENCE OF CERTAIN ALGORITHMS... e 43 BIBLIOGRAPHY................... 48

ABSTRACT Certain formal arithmetics may be employed as design languages for finite automata. In these arithmetics (design) conditions, the notion of automaton, and the notion of an automaton satisfying a condition are all expressible. An automaton satisfies 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 there exists an automaton satisfying a given condition (and if there is one, producing one), (3) whether there exists at most one automaton 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 quasi-finite (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. -vi

CHAPTER I BACKGROUND 1. Motivation. Many variants of the notion of automaton have appeared in the literature. We find it convenient here to adopt the notion of E. F. Moore [7]. Inasmuch as Rabin-Scott [9] adopt this notion, too, it is convenient to refer to (9] for various results presumed here. In particular, Xleene' theorem [5, theorems3,5] is used in the form in which it appears in [9]. It is often perspicacious to view regular expressions, and this notion is used in the sense of 3]. In general, we are concerned with the problems of automatically designing an automaton from a specification of a relation which is to hold between the automaton's input sequences and determined output sequences. These "design requirements" are given via a formula of some kLnd. The problems with which we are concerned have been described in [1]. With respect to particular formalisms for expressing "design requirements" as well as the notion of automaton itself, the problem are briefly and informally these: (1) to produce an algorithm which when it operates on an automaton and a design requirement produces the correct answer to the question "Does this automaton satisfy this design requirement", or else show no such algorithm exists; (2) to produce an algorithm which operates on a design requirement and produces the correct answer to the question "Does there exist an automaton which satisfies this design requireont#", or else show no such algorithm

-2exists; (3) to produce an algorithm which operates on a design requirement and terminates with an automaton which satisfies the requirement when one exists and otherwise fails to termainate, or *l.. show no such algorithm exists. Interrelationships among problems (1), (2), (3) will appear in the paper [1]. This paper will also indicate the close connection between problem (1) and decision problems for truth of sentences of certain arithmetics. The paper (1] will also make use of certain results concerning weak arithmetics already obtained in the literature to obtain answers to problems (1) and (3). Thus [l], in part, concerns applications of logic to automata theory. In the following pages, we shall give some applications of automata theory to logic. More particularly, we hall use automata theory to produce decision procedures for the truth of sentences of certain weak arithmetics. Theorem 5.3 provides a uniform and surprisingly powerful technique for proving that various operations on sets of finite sequences preserve regularity. 2. Some basic notions. Definition: (a) An I-autauton is a quadruplte a <S, f, d, D> where I is a finit non-empty set (the input states or the alphabet), 8 is a finite non-empty set (the internal states), f is a function, f: I x S -- S (the transition unction), d ~ S (the initial internal state), and D C S (D may be called the output of Vt). (b) T(F) is the set of all sequences (io, i1,0.*. in. 1), n > O, such that there i a sequence (sO,.-, sn) satisfying: (x) f(ik,.k) -'k+' 0 < k < n-l, sk' S, ik e I, (2) 5n D, (3) so d.

-3" T(l) is the set of tapes 9] accepted by- or the behavior of Z. The null sequence As T(l) if and only if d s Do (c) T(O) may also be described as the set of all functions i: t0, 1, 2, **2, n-. -~ I, n > 0 (the empty function is included) satisfying the formula: y [(0) d A (n) a D, t(i(x), s(x)) 1 B s(x+l) - f(cx)Q ^ (i(x),,(x)) - 02: *(xel) a f(e2)] ^.- ^ [(i(x), s(x)) *,n (x+l) * f(c)]] where cl, e2,., is enumeration of all the elements of I x S (the complete states of the automaton). 3. Two characterizations of automata behavior, Lot VI be the oset of all finite sequences of elements of I (including the null sequence 10 If ca,P C VI, then.0p is the subset of VI obtained by concateonting a sequence from a with a sequence from p; cs [}jc u c., uv a.. u. *.. A subset of V i I-rsegLr if and only i it is obtainable from and the unit sets, ~4, a a I, by a finite number of applications of vu, *, * Otherwise stated: The class of I-regular osets is the smallest class containing %, {a}, a a I, and closed under U, *, *. An I-regular expression is constructed out of symbols denoting each [a}, a s I, 0 (the empty set), and U% 9, *, [Note that * - IA].] A sat is reula if it is I-regular for some I. (Cf, [3, page 182]and [9, page 17].) 3,1. K1.ene', theorem, If U is an I-automaton, then T(lt) is I-regular and an I-regular expression denoting T(VR) may effectively be obtained. Conversely, if ~ is I-regular, then there exists an I-automaton such thet T(L) -r and, furthermore, 11 may be effectively obtained from an I-regular expression denoting a.

-4The following statement is immediate from the definition of I-regular. 3.2. If a is I-regular and if I C J, then a is also J-regular. 3.3. The class of I-regular sets is closed with respect to union, intersection, complementation (with respect to VI)o (Cf. [9, page 17],) 3.4. The class of regular sets is closed with respect to symmetric difference, intersection. This follows from 3.2 and 3.3. Let p be a mapping of I onto J. There is a unique homomorphism fram the free semi-group FI on I onto the free semi-group F; on J which extends p. This homomorphism in turn induces a mapping P on subsets of FI onto subsets of Fj. If a is a set of I-sequences, then f(c) is a set of J-sequences,? is a projection, and?(ca) is a projection of a. 3.5. If a is regular and p is a projection, then p(a) is regular. Proof. Suppose a is I-regular and p: I -- J. If a a I, then.al a fp(a)) is J-regular. Since p(a.B) - =p().(B) and p(a*) - (P(a))*, the result follows. (Medvedev [6, page 13] gives a construction which, given an I-automaton VL and a p: I — *J, yields a J-automaton p such that T(Lp). (T()). ) From the point of view of regular expressions: the projection of a regular set is obtained by replacing each symbol a (denoting (a) by p(s) (denoting tp(&)3). The following theorem strengthens a result of Medvedev [6, page 11, theorem 2]. 3.6. Theorem. (1) Every regular set is obtainable from a finite number of sets of the types:

-5(a) VA: the set of all finite A-sequences (including the null sequence) where A is any inite set (non-empty), (b) EB(&,b): the set of all sequences uabv where a,b a B and u,v 8 VB and where B ia any finite (non-empty) set, by a finite nuimber of applications of ymetric differences inteorsection, and projection. (2) lach VA, B(a&,b) is regular. Otherwise stated: Given a regular set a there is a Boolean ring polynaoial (in +, r), an assignment of sets chosen fro (a),(b), and a projection p such that if +,A are interpreted as symmetric difference and intersection respectively and if B is the set denoted by this polynomial under this assignmnt, then (B) C-. Furthermore, if a regular expression is given which denotes ra, then the polynomial, the assignment, and the projection may all effectively be determined. Proof. (1) i. If A n B, then VAn VBw Ia. ii. v,.A +,U A(ab)' {A, a1, a2,'",' a where, {a1, 2, "',' A and (Ab.n ~A(ab) is equialent to a polynomial in +,n and the basic sets V, EA(a,b). iii. If A N B a la), then there is a polynomial in the basic sets equal to La), iv. If R is a binary rolation over a finite set A, then a sequence ~a2, ean is an R-sequenc if and only if for each i < a, (ai' ai,l) a R. (Thus the sequences of length loss than or equal to one are R-sequenco.) The set of all R-sequences is equal to VA - [EA(abl) V SA(a2DbR2 U *.. EA(arbr)] where {(labl), (2b2),..., (&rbr)} R - (A x A) - R.

v. Let SA(a) - {au I a c A A u V. Let R be a binary relation on Au {b}, b A, viz., (x,y) e R Q (x - b ^ y A) v (x sA A y a A) y Ae8 A A(x b V x e A). Then the set of R-sequences intersected with {b) u U V Avb (a,b) aecA is the set X of R-sequences (of length> 0) beginning with the letter "b". Now if p: Au {b} -- A takes b into a and is the identity on A, then -() SA(a). vi. Let TA(a) a jua I a a A A u a VAI. Then TA(a) is expressible as the projection of a polynmial in the basic sets. The argument is analogous to v. Now let VI (S, f, d, D> be an I-automaton. Let R hold between complete states (il, *1), (i 2, ) if and only if f(i2, 1) a2. Then the set of R-sequences beginning with (is ) where i e I and s a f(i,d) and terminating with an (i,s) such that a a D when projected by Ap, where p(i,s) - i for all (i,s) a I x S, yields T(Q) - fN. (Cf. the definition of T(t),.) Result (1) now follows from i through vi. (2) VA - A*"; (a,b) - B*.a *. [b2}.B which shows VA and EB(a,b) are regular. (Alternatively one may directly construct automata which accept tapes VA, EB (a,b).) CorollY. If R is a binary relation over a set A, then the set of all R-sequences is regular. Proof. ollows from iv, (2). 3.7. Theorem The class of all T(f), Lan automaton is the

-7smallest class of sets containing VA, ~B(a,b) (for every A, B, a,b a B) and closed under symmetric difference, intersection, and projection. Proof. Immediate from 3.4, 3.5, 3.6. 3.8. Theorem. Every set obtainable from the sets VA, A2(a,b), S3A (a), TA4(a) by a finite number of applications of Boolean ring operations and projections is obtainable from the same sets by Boolean ring operations followed by a single projection (and these sets are exactly the regular sets). Proof Sane as proof of 3.6.

CHAPTER II TRUTH ALGORITHMS FOR CERTAIN ARITHMETICS 4. Truncation lema, Definition. If u is a finite sequence, b is a letter, and, for soae n, u n vbb*b, n > 0, and v does not terminate with b, then ub - v. This is called right truncation of u by b. If a is a set of finite sequences, then ab tub |I u a ) (right truncation of a by b). The meaning of left truncation is analogous. Notice that A a ab if and only if fb)i a f. 4.l. Ia. (a) (,.~)b.a * (b._ I)) uv b. (gb. Lemma. (a. (e 4 - (a) ). (b) (a*)b a *. (b {A1) u { A}. Proof, (a) Let l(u) bo the length of the finite sqUeence u. Let Pb(u) mean u terminates with the letter b...,)b -. Vu:b' e. ^, > 0 ^ -' ('] n am nulu2 1 n > O ul e u2,t p l,\t(2) > n) V (ulu2' ubb.'n > o s o ~Ma2 B, -T;,,(U,2) S<)] -8 -

-9-pa V Icqtuub V u Sr ubf1! j ul a a % u2 e B) v (u' u Iu2I'hu l a a' u2 [ A)] \U2( U2 A U, 9 a 2) V (u- 2b e ( b - b - )),, a, Ou2 B)l] (b) u, AlA u (cL*)b V 4u Vu' b cL* a n>O n n'iTY ^tu.AJ V \n > o \ r > O /ulu2.u.. - n,r,rUlu2...,ur bb" ^ lA< ui A a i \Pb(U) / u iJA] 4 r V _ uc]b b V' > o NU -ulu2 *um- Ohlou. N fl U A \ Ui a] mulu2,~ ~ ~,l<_< r - _ Iu ~ a * (b - IA). 4.2. Lemma. The class of regular sets is closed under right truncation. Moreover, from a regular expression denoting a one can obtain effectively a regular expression denoting ab, Analogous statements hold for left truncation. Proof. If x is a letter, then x)b - {x) if b f x and {x)b - {A) if b - x. The result for right truncation now follows by 4.1. The result for left truncation follows from this and the fact that the class of regular sets is closed under conversion (reversing the order of the sequences). (Cf. [9, page 17].) 5. Characterization of automaata behavior via a formal arithmetic. Let Li be the class of formulas constructed out of (a) xi e Fj' xi e F *.,j,, r)e i,J 1,2,3,F* i (b) x -y, x < y, by meoans of propositional connectives and quantilers V, j. Th xi are individual variables, the Fj set variables, and xi is interpreted a6

-10b the successor of xi. 5.1. Let the individual variables of L1 range over the natural numbers and the set variables range over finite sets of natural numbers. Call the system consisting of the class of formulas L1 and this interpretation L1i. If A[F1, F2,..., F], r > O, is a formula in which at most the variables F1, F2,.-, Fr (the first r set variables in the alphabet of L1) occur free, then associated with A is the class of r-tuples (F1, F2,.*., Fr) of finite sets for which A[F1, F2,.., Fr] is true. Alternatively we may associate with such a formula a function f on the natural numbers with values which are (column) r-tuples of zeros and ones (i.e., an r x co matrix) as follows: f(n) - if and only if n a Fi a ai - 1. If x - max(Flv F2 v. Fr) and y > x, then f(y) is the r-tuple of all zeros. Let ~0 be the restriction of f to the domain (0,1,2,...,x}; % maJr be identified with the r x (x+l) matrix whose ith column is f(i). Moreover ~r is a 1-1 correspondence between all r x co matrices of zeros and ones whose columns are ultimately zero and remain zero and all those r x s matrices of seros and ones, s > 0, whose last (rightmost) column is not the all zero r-tuple. Call these r x s matrices admissible. (The matrix with zero columns is admissible.) Thus with each formula A of is associated a set T (A) of admissible r x s matrices, s > 0, where A is a formula without free individual variables and the number of free set variables is less than or equal to r. [If r - 0, let Tr(A) - IA} if A is true and Tr(A) - 0 if A is false.] Let Ur be the set of all r-tuples of zeros and ones, r > 0 let Ur - Ur r whre r is the all sero r-tuple. (If r - O, let Ur - o0}, U~ - 0. Recall that V~ - 50*'V\ }.

5.2. Notice that in L: xW A 4(x F y F) x-O ~ y' y - x x<y A - D /(z Ia F zs e F) Ax* FAy FI. 5.3. Theorem. (a) If A(F1, F2', ] is a formula of 4, then Tr(A) is Ur-regular and one can effectively find a regular expression which denotes Tr(l). (b) For every regular set a C VUr of admissible sequences there is a formula S(A) of L such that Tr(Z(A)) - a, whore I is a string of existential set quantifiers, A is free of set quantifiers, and the only terms in A are of the form x, x'. Corollary. Let a be an arbitrary I-regular set. Let p be a 1-1 mapping of I into U~. Then p( a) is a U~-regular set ("isomorphic" to a, i.e., the set is a in coded form) and so there is a formula A of L1 such that Tr(A) - p(o)t Remark. It will be convenient to abbreviate formulas of L4 by replacing an r-tuple of finite set variables by a function variable interpreted as having as its domain the natural numbers and range an element of Ur and satisfying (f(x))i' 1 4' x a Fi as well as the property Vf(x) O0r A A/(y > x D f(y) - Or), where Or is the r-tuple X y of all zeros, so that any such function is associated with a finite sequence of elements of Ur. If f abbreviates (F1, F2, ** Fr), then V abbreviates 1 2 r 5.4. Lemma. Ivery formula A[F1, F2, *.., Fr] of 4 is equivalent to a formula B[F1,.., Fr] of 4 in prenex form and such that every individual quantifier occurs to the right of every set quantifier.

Proof. Observe that (1) V A C - V AA C(G(x) D C) V G(z)] x F G F x z VA/NAc G F x and (2) A VC C V Ve V (z) G(x) C] x F G F x z g AVV c1, G F x where G is a set variable not occurring free in C. Assume A[F1, F2, *... Fr] has the property that every set quantifier has as its scope the entire formula to the right of it. Notice that in applying (1) or (2) to A the number of set quantifiers to the right of the x-quantifier is reduced by one. Thus, if V t A is the rightmost individual quantifier which has set quantix X fiers to the right of it, by iterating (1) and (2) a finite number of times one obtains a formula A' in which the x-quantifier appears to the right of all set quantifiers. Moreover, the number of individual quantifiers with set quantifiers to the right is one less in A' than in A. Thus one ultimately obtains a formula B equivalent to A and having the desired properties. 5.5. A formula of the form x (MO) il Fk ^ x 1) 4 Fk A X(mr) 2 Fk ] where each occurrence of 1 is independently c or i, will be called a principal formula where O mo < m1 < ~.. < mr. Call a formula normal if it is a disjunction of conjunctions of

-13(1) principal formulas, (2) atomic formulas, (3) negations of (1) or (2). Lemma 1. Every formula of h is equivalent to a formula of L1 of the form QCM] where Q is a string of set quantifiers and M is a disjunction of conjunctions of principal formulas and negations of principal formulas. (By appropriately permuting F1, F2, 2*,. Fr in the given formula, the variables in Q may be assumed to appear in alphabetical order terminating with Fr.] Proof. In view of 5.2, it may be assumed that the given formula contains atomic parts 5(a) only. Suppose A is normal. (a) Then ~A is equivalent to a normal formula (with the same free variables). (b) Consider VA. V distributes over the disJuncts of A. Let X X D be a disJunct of the form Dl(x) tD2 where x does not occur free in D2 and no variable other than x occurs free in D1. Then Y D & D2 \V Dl(x). Starting with a formula B[F1, F2,..., Fr] of lemna 5.4 one makes use of (a) and (b) until all the individual quantifiers are "moved in". This yields a formula of the ds3ired form. Lenma 2. The set of all admissible sequences in VU is Ur*Ur UnA and is, therefore, regular. 5.6. Proof of 5, 3 (a). Consider a formula of L1 of the form Q[M3 of lemma 1 of 5.5 with free set variables F1, F2,..., Fr. Assume that it is known that if A is a principal formula that T r(A) is regular and that from A a regular expression denoting Tr(A) may be effectively obtained. Then since T(A A B) - Tr(A) n Tr(B), Tr(A V B) - Tr(A) U Tr(B), T (EA) - T(A) iccnplementation is with respect to the set of all admissible sequence in VU (which is regular)] for A and B any formulas of L1 without free

-l,4individual variables, it follows that T r() is regular and a regular expression denoting it is effectively obtainable. Now if A = A[F1 F2, *.., Fr], r > 1, then T r.( VA) is the set obtainable from T (A) by deleting the rth row followed by right truncation of the all zero (r-l)-tuple, i.e., if r > 1 T 1( VA) ( (T (A)))b where Pr maps an r-tuple of zeros and ones onto the (r-l)-tuple obtained by deleting the rth component and b is the all zero (r-l)-tuple. Hence Tr. ( A) is regular and from a regular expression for Tr(A) one may effectively obtain one for Tr i( /A). It remains only to show that Tr(A) is regular for A a principal formula. To simplify the exposition we point out that the principal formulas can, without loss of generality, be taken to be of the form, (1) V (xF AFi AXI 4 F1)JI x l<i<r where each occurrence of q is independently a or 4. This follows from the fact that (assuming m > 1) x FY1 - x'Y2Y Nl o Y2 aY1 F Ymy1 G a G hY'' F] and x IF I (xq F x IF) (x FV (x x' x SF) x, F 0 ( a F <- (xx I F) V(x / F ix' x F) Let A be V Cf(x) - a /nf(x') - b] (cf. remark 5.3), Case I, a a r and b U U Then

T (A)- Uv {a} *b) * (v(UrUo) v tA) Case II. a c Ur and b = Or Then r r Tr(A) (U*{ a) U (Uta~lobe)Ur*UU). Case III. a- Or- b. Then Tr (A) U (u*SUO) v {A)} 5.7. Pooof 523 (b). Leot C VUr be a regular set of admissible sequences. Then a - (A) is regular and is a projection of a regular set B C VU O+, s > O. Specifically: there exists a U -automatonk - <S, f, d, D) such that a - T(f). Without loss of generality, 0 let S be a subset of U5 for a suitable a > O. The complete states Ur x S of may be identified with a subset of Ur+8 as follows: <x,y> s Ur x S is identified with the (r+s)-tuple whose ith member, 1 < i < r, is the ith member of x and whose (r+J)th member, 1 < J S s, is the th member of y. Let B C U~ be the set <x, f(x,d)) Ix e Url. Let - Ur x D. Define RCU U+ x U as follows: <(Xl,yp, <x2,y2 > a R if and only if f(x2,yl) - y2 Then { is the set of finite R-sequences beginning with an element of B and ending with an element of 3 and a " (B) where p is the mapping which takes (<,y> a Ur x S into x. B is the intersection of the three following sets. (a) U S3 (a), B C U~ (those elements of aeB r+8 rr+s beginning with an element of B). (b) a WU (a), E w Uer x D (those elements of VU ~act~l~+8 rI+s r~

-16We now obtain formulas "corresponding" to (a), (b), (c). a) ~Lot B so bl, b2, bi is the kth component of b, For each bi the formula Ai: 0 F re i b 1 ~ lC14;C+r 0 9k FkV where qk is e f bkin and 9k its otherwise, corresponds to Sr (bi), so that (a) corresponds to A1 A V"' VAn. Then A1 A2 V * vAn is an abbreviation of a formula A of Ll and Tr+s(A) U Ur+s(a). b) Let E - {(1, ~ 21.,en}. With each ei associate the formula whr _k<res y where lk ias if ek w 1 and otherwise i Thn V A2 A 1 in an abbreviation of a formula A of Li and Tr (A) U Wu r+(a). c) Let H a R v (Ur+s x {s)) where s is the all zero (r+s)tuple. Let ((eiAl), (.21f2), *.., (.n,fi)} H. With each ei associate A( )s 1< +A x ik Fk where qk is a or J depending on whether K 11 or not. With each fi associate B() ): kQA x' 1k Fk where k is a or j depending on whether If - 1 or not. Then if A is the formula c — abbreviated by A V A(ei) 1 B(fi), then T (A) is the set (c), x a<u r+S If Fis the conjunction of the formulas a), b), c), then Tr+a(~- and TV(V /~ V;)- 1o Tr1 Fr+2 Fr+. Note that {I - T1( A x i F). 5.8. Corollary to 5.3 (a).2 Ehrenfeucht's theorem (unpublished). The set of true sentences of L is effective.

Proof. It may be assumed (5.4) that the given sentence is of the form (a) V A[F F or (b) ~ A[F] F where A is a formula in which at most the set variable F occurs free, Then (a) is true if and only if T1(A[F]) is non-empty, and (b) is true if and only if T1(A[F]) is empty. T1(A[F]) is empty if and only if T(VA[FF]) is empty. Thus, one can effectively find an automatonVtL <(S, f, d, D> with one input state (sometimes called an input-free automaton or autonomous automaton) which represents (a) (or (b)). If the automaton has n internal states, then the (unique) input sequence of length n will determine a sequence of internal states starting with d of length n + 1. At least one internal state must occur more than once in this sequence so that TO(L) is non-empty if and only if an s a D occurs in this sequence. 5.9. For each finite set F of natural numbers let t(F) = 2X. Then t is a 1-1 correspondence between the class of all finite subsets of the natural numbers and the natural numbers. tt() -t(l) + r(F2) 4- C o C N (O i G a O F1 a Oe F2) A)(x ~ C 1 (x e F1 xe 2) v (x a Fr x a C) v(x F2 & xe C) A * x a 0 GI (x a F1 ax a x e C))] where a represents exclusive or. Thus2 Corollary.3 (1) The first order theory of addition of natural numbers is decidable. (2) Furthermore, for any relation

A[xl, x2.., xr] in the first order theory of natural numbers there is a formula B[F1, F2, *", Fr] such that A[xl, x2,..***, r] -l1 -3 -l B[x X1 X20 IC. XI]r Statement (1) with "natural numbers" replaced by "integers" was established by Presburger; statement (1) itself was established by Hilbert and Bernays. The proof of (1) indicated here appears to be simpler than either of the two proofs mentioned, both of which make use of the theory of congruences. 5.10. For each n, n > 1, consider the 22n n-place predicates V Ix 1i F1 ax I F2... / x rl Fn x,. F1 \ xi 4 F2 / @ A^ X' q Fn where each occurrence of q is independently replaced by a or g. Call the class of all these predicates (P. Then every first order formula in 40 is equivalent to one in i4 (without free individual variables) and vice versa. Let't be the class of predicates A[CrF, rF2, **., TFr] defined to hold if and only if A[F1, F2, **.. Fr] holds and A[F1, F2, *.. Fr] is a predicate of P. Then: Corollary. The first order arithmetic theory based upon -~d is decidable and this theory strictly contains the elementary theory of addition of natural numbers in the sense that while addition is definable in the theory of t6', not every predicate in ic is definable in the first order theory of addition. Proof. I{V[x aF Fx' e F /\y A e F (y - vy- x)]) x y is the set 3, 6, 12, 24, *-, i.s., the set [3 x 2n4}>0. This set is not definable in the first order theory based upon + because the sets definable in this latter theory are exactly those whose characteristic function is ultimately periodic while the set f3 x 2nJ,>0

-19does not have this property. (Cf. [4, last paragraph, section 3].) The rest of the argument is contained in 5.9. 5.11. Corolary 1. The first order theory of finite sets of natural numbers based upon n, @ (symmetric difference), 0-, a, and the unary operation F -> Fa defined by x Fs if and only if Vx < y y F y is decidable. Furthermore, the relations on finite sets definable in are exactly the same as those definable in this theory. Proof. The operations An,, and the relations F - G and F - 0 are definable in 1. The principal formula y[x 6 G1 G x't 1 G x G2;Ox' e G2] has as its counterpart in this new theory the formula (i.e. the set of ordered pairs of finite sets defined by this formula is the same as that given by the formula below):''2,pF 1 2 F2 3 3 1 2 3, /\[(G O' ^ F1 C 0.:> F2 ~ G) ^ (0G' ^ 2 c G *0. 3 c 0)] laF3 or@ F1o F3 2 2 c (F2@Fi) fo2 -' Similarlyr for other principal formulas. The unary operation F - F may be replaced by the property F - F without changing the strength of the system. Corollary 2. The first order theory of natural number based upon'(n), (@), -, +, and the property P(n) of being of a power of 2 is decidable where

.20' x t(n) Y 4 - u a —lx n'-ly'-.,-lZ x e(3) Y ~ Z t-lX 0 Z-17 " le. Notice that P(n) T'r ln is a unit set and the property of being a unit seat is definable in L1 Note, too, that we have, in particular, a proper strengthening of Presburger's result, viz., the first order theory of natural numbers based upon addition and the property of being a power of two is decidable and the property of being a power of two is not definable in the Presburger system. 5.12. Let L: be the system consisting of the formulas L with individual variables interpreted as ranging over integers rather than natural numbers and set variables ranging over finite sets of integers. Lemma. For each formula AF1, F2, *.., Fr] of L1 and for each integer jL, A[F!, F2 -., F.L A[9 2l, F'r where x e 4 x-L a Fi, i.e., the class of r-tuples of finite sets defined by a formula of 2 is closed under translation. [Cf. 5.13.] 2 Lemma 1 of 5.5 is valid for L e. Let Rr be the relation botween two r-tuples of finite sets that one is a translate of the other. Each Rr-equivalence class is included in A[F1, F2, ~ *, Frl or in ~A[ F1, F2,..*, Fr] for every formula A for this is true for principal formulas and is preserved by the Boolean operations and projection, Analogous to 5.1 and in view of the lemma one may associate with A[F1, F2,..., Fr] of L a set T2(A[F, F2..., Fr])of admissible-2 matrices, an admissible-2 matrix being a finite sequence of r-tuples of zeros and ones whichneither begins nor terminates with the all zero r-tuple. Analogous to the proof of 5.3 one may establish the following theorem.

Theorem. (a) If A[p1, F2,, Fr] is a formula of L2 then T2(A) is Ur-regular and one can effectively find a regular expression which denotes T (A). (b) For every regular set a of admissibl-2 Ur-sequences there is a formula E(A) of 2 such that Tr(E(k)) a where is a strinl of existential set quantifiers and the only terms in A are of the form x, Z. Corollary to (a). There is a decision procedure for the truth of sentences of L. 5.13. In i: x y /\(x rz asa), x<y 4 / a tts r S ( (-=x..s' s ) y F]. Fps However, x - O is not definable in L2 by virtue of the lema of 5*12* Ccmpare with 5.2. 5.14. Let A be an arbitrary finit set. A sequence of VA i admissible- if and only if (1) it is of length one or (2) it is of length greater than one and the last two elements of the sequence are distinct. Imaa!. The set of all admissible-3 sequences in VA is A-regular., Proof. Identify elements of A with sequences of length one, The set of all admissible-3 sequences is: A U VA' (A - (b)) * b. bcA Definition. If a~ t VA and b a A, then b (modlit ed truncation by b) is defined as tollows:t v ab if and only if (1) v a a and v does not terminate with b, or (2) there exists u s a which terminates with b and if

-22wbb -*b = u and w does not terminate with b, then v a wb. Leana 2. If a C VA is A-regular and b c A, then a b is Aregular. Proof. Cf. corollary 5.3 and remark. Without loss of generality assume that A = Ur for appropriate r. There is a formula y[f] such that Tr3; a. It is sufficient to prove the theorem forA a. Then f(x) - 0~r x > O. LetSg]l be the formula: V f{W[] N f(y') 0r T(y) f Or: ~: f(y) b bD A (x) -(x) A fy x tf(y) - b D lf (x) - b A ( VZ' x Df(z) f b) A (Az > x * f * f(x) - X t Z b f(z) - ) ~ / (g(w) - f()) ^ / g(w) - O }. r,IrK' Then Tb - a b. By theorem 5.3 (a), aCb is regular. 5.15. By a 9uasi-finite set of natural numbers (integers) is meant a set which is finite or whose complement is finite. Let Li be the system consisting of the set of formulas L with individual variables interpreted over the natural numbers and set variables interpreted over quasi-finite sets of natural numbers. Let F1, F2, ~, Fr be quasi-finite sets. Let ck(n) = 1 <u-= n c Fk. Let cl(n) c(n) c2(n) cr(n) Thus, with each r-tuple of finite sets of natural numbers is associated C 6 UNF (N is the set of non-negative integers). Because the Fk are

o23quasi-finite, there exists x. N such that A y> x D c(t) a c(x). e function c restricted to the first x such that this property holds is an element or(PFl, F2,,' Fr) of VUr. Moreover, c is 1-1. Briefys o(Fl F2,...*ce F ) 8 f where domain f {x x _< yr and y (Ps) A Ax >,z x A Fi x% A s > x Fi and if x < y then (f(x))i 1 4 x xe and At > y ff(y) - f(s). The iasg of r is the set of all admissible-3 elements of VUro If A[71, F2, 0o~~ or] is a formula of I, then r(A) is the set of all r(F1, F2o ee, 5) such that A[F1, F2'.., F r holds. Notice that 5.2 holds in L0 Theorem. (a) If A[F1, F2, ~~o F r] i a formula of VL, then T'(A) is U -regular and one can effectively find a regular expression which denotes it. (b) For every regular set a c VU of admissible-3 sequences there is a formula E(A) of I such that -r(E(A)) a G where S is a string of existential set quantifiers, A is free of set gquantifers, and the only terms in A are of the form x, xI, Proof. (a) The proof is analogous to 5.6, ILmma 1 of 5*5 3 1 holds with'I3" in place of 1"n. If A,B are formulas of with at most F1, F2, *, Fr free, then T3r(A B) - T3r(A) T3r(B), $3r(A V B) " T3r(A) U T23(B), sequences of VU (cf. 5.14, lemma 1). r( ) hnr Ii or I'a __ A - _A.6 U -0 _V%.4 -8 1A &-42b) ~~~

where p maps an element of Ur into the element obtained by deleting the rth component and a,b,*** is an enumeration of the elements of Ur1. Since regularity is preserved by projection and modified right truncation (lemma 2, 5.14) it follows that T3 ( V A) is regular. It remains only to show that if A is V[f(x) - a A f(x') - b], X then Tr(A) is regular, where f abbreviates (F1, F2,... Fr) (cf. 5.3). Let m- U (U * {b) * U~ * c} * {d) u Ur * {a * b *'c}. cpd r r c b c,dcUr csUr Then B is regular. if a Z b, then Tr(A) - i U (Ur* ta * {b~ while if a - b, then Tr(A) - u (Ur * Ur - {a}) * a)) {a}. Then T3(A) is regular and the proof is completed. (b) Let a c U* be a regular set of admissible-3 sequences. Thus c - T(l) for some automaton - <S. f, d, D). We may take S as a subset of Ua for some s > O. Identify Ur x Ua with U, the complete states of I. Then a is a projection of a set B C U and 0 is the set of all R-sequences [R C Ur+s x Ur+] beginning with an element of B - (<a, f(a,d)> j a e Ur3 and terminating with an element of Ur x D where (ul1,vj R <u2,' v if and only if ul,u2 e Ur, vl,v2 e U and f(u2, vl) - V2, Notice that the elements of B are admissible-3. Define R and R+ as follows: c Rd aR bAc 1-ld; a R+ b c a A b. Vb b (c - 1 /c - O ) A d - O, c d c d for all a,b s Ur+s Observation. Every finite non-null R-sequence has a unique extension to an infinite R -sequence in which a occurs for some a c Ur+s, and every infinite R -sequence in which appears for some a Ur+ i an extension of some finite non-null A-sequence. If g is an infinite R -sequence such that g(x) - 0, then for all y > x, g(y) - O

Let f abbreviate F1, F2,'*., Fr+s+1. Let -' 4ab1 R' [If(x) - a s f (x') b] A Vy Fr 84i Then sequences in T3r+s+l have the property: (1) if it is of length one, it is of the form; (2) if it is of length two, it is of the form a 0 i (3) if it is of length greater than two, then its last three members are of the form b a a where ab e U and a f b. It follows 110' whereabUr+s that 3r+( V (j)) is the set of all R-sequences. Fr+s+l Lot&lg] be V Let (g] be: Fr+s+l [Ig] 3 g(o) B^\ Vg(x) a Ur x D A A (y > x Dg(y) - g(x)). x y (The second and third conjuncts are abbreviations of disjunctions.) Then T3( V V.. V -). F F F r+l r+2 r+s Corollay i. There is a decision procedure for the truth of 3 sentences of L (and one such procedure is given by the proof of theorem 5.15 (a) together with the last paragraph of 5.8). Corollary 2. The first order theory LO of the Boolean algebra of all quasi-finite sets of natural numbers (based, says upon Us,, ) with operator Fs (cf. 5.11) is decidable. More generally, the relations on quasi-finite sets definable in L3 are exactly the same as those definable in L1. Proof. Similar to 5.11. 5.16. Let 4 be the system consisting of the formulas L1 with individual variables ranging over all the integers and set variables ranging over quasi-finite sets of integers.

-26Theorem. There is a decision procedure for the truth of sentences of L4. Proof. If F1, F2, *, Fr satisfies a formula of L1, then any translate (cf. 5.12) of this r-tuple satisfies the formula. The function f: N -* Ur such that (f(x))i - 1' x a Fi has the property that V A A f(z) = a AA f(z) a and x < y] because of the quasix,y,a z~x - > finite character of the Fi. If f is not constant, let xo - (max x) V A s < x f (z) - a], a z yo " (min y) VA [ >_ y f(z) - a]. a Z Then the finite sequence g- c4(Fl, F2, *-., Fr) if domain g - {x I x yo - xj and A [g(x) - f(x + xO)3 If r is constant and equal to b, then let domain g w- fO and g(O) - b. The mapping dr takes all members of a translation equivalence class into the same element of Ur and distinct equivalence classes go into distinct elements. Moreover, if o(Fl, F2,..., F) - g and domain g - fx I x } y > 0, then y> 1 and g(O) - g(y), g(O) j g(l), g(y-l) f g(y). Via oj, with each formula T[IF, F2, * —, Fr] of is asociatd a set of finite sequences TrG) which may be shown to be regular and a regular expression may effectively be obtained as in the proof of 5.15, theorem (a). This, together with the last paragraph of 5.8, yields a decision procedure for truth.

CHAPTER III SOLVABILITY ALGORITHMS 6. Some operations which preserve regularity. Let (C VAxB A sequence in A x B will sometimes be indicated thus: v, where u a VA and v a VB and u and v have the same length. A sequence a or is A-extendable in o if and only if b v bU e a A sequence in 0r is strongly A-extendable in o if and only if every initial sequent of the sequence is in o and is A-extendable in ac. The set c-is strongly A-extendable if and only if every sequence in c-is strongly A-extendable in a-. If a is strongly A-extendable, every initial segment of an element in r is in 0-. 6.1* Lemma. If ZC VAxB is regular, then there is a A C Y such that (1) rA is regular, (2) A_ is strongly A-extendable, (3) if ~ r and 0 is strongly A-extendable, then e C ~. Furthermore, from an automaton C such that T(G) - 7 one can effectively construct (by the method given in proof) an automaton GA such that T(cA) - a. Proof. Let @ be the AxB-automaton <S, f, d, D~. Then j is p(6), where 6 is the union of {TP and the set of all R-sequence beginning with an element of E- Q<a, f(a,b,d)> I (a,b> a AxBI and terminating with an element of (AxB)xD, and R holds between (<al,bl, ~l and -27

<(a2,b2 ), 82 if and only if f((a2,b2), $1) 2 a2nd p(<a,b>, s) a <a,b>. Let Ro be the restriction of R to A x B x D - Mo, i.e., R0 - R n (Mo x Mo). For n > 0 let Rn+1 be the restriction of R to M,n where <(1, bl' Cj1) Mn+l< ~ <,,1 bl, C1) I Mn A V <1, bl, cl) Rn <(, b, c>. aeA (b,c>sBxD.Inasmuch as MO is finite, there exists m such that R " R- +1 R.2 =- *-. Define RA to be Rm for this a and MA to be Mm for this m. Then <a1,, bl, C) A a A V <a l bl' c> RA <a, b, c). -> - MAaA (b,c> eBxD [Of course, MA may be empty.] Let o be the set of all RA-sequences beginning with an element of El, i.e., beginning with an element of ~ nDRA ()RA is the domain of the binary relation RA). Let -A' pae. 1) YA is regular since it is a projection of a regular set a. 2) We shall show rA is strongly A-extendable. Let vl v2 e *A where ul, u2 U VA and Vl, 2 a VB; then there exists w1, w2 e VS such that ul u2 U1 U1 V,1, and v1 6 VA Sinc thelemen i tho1 Since the elements in the sequence vlare in MA, and, in particular, the

last element of this sequence is in MA, it follows that U1 & A V 1 b a acA <b,c)>BxD ~ w so that A1 V ul a eY aeA beB v1 b 3) Suppose 0 is strongly A-extendable and c_ r. Let u v; then every initial seoient of ua so that if w is the sequence of internal states determined by the automaton @(i.e., if is oa l.. an c A x B, then w is sosl.*. *n where f(ao, d) - so and, U for O < r < n, f(r, %rl) a sr), then every initial segnent of v is an element of 6. Thus, every member of the sequence v is an element of MO U and v is A or is an Ro-sequence beginning with an element of B. Consider an arbitrary initial segment uo a0 U v0 bo of v, w Co where ao a A, bo 0 B, co a D, i.e., <a0, bo, c) M o. Since ro &0 v b A V Uo'o a a alA bleB vo bo b1 Hence

-30uo ao a1 A V Vo bo bl e 6 A<al, bl, C> M aleA (b1,c> BxD Wo Co cl It follows that <a', bo' Co) e M1. Similarly uo ao a1 a2 A V A o v bO bl b2 E6 N,<a2p b2, C2> e MO al&A (blC~ eBxD a2eA (b2,c BxD o 1 2 /A al, bl, Cl1 C M1. It follows that <ao, bo, c )e M2. It should now be clear that (ao, bo, C>o T MA so that U v is.A or is a RA-sequence beginning with an element of E. Thus v a crand u 4.A' We have shown that: if and B is strongly A-extendable, then CA 6.2. If a _ VA, define the interior of a (Int a) to be the set of sequences u e a such that every initial segment of u is in a. A set a is open if and only if a - Int a. We note incidentally that it is immediate from the definition that arbitrary unions and arbitrary intersections of open sets are open so that the class of open sets constitute a topology in the usual sense for VA. Notice that if a is open, then a if 0 4= A. a. Medvedev [6, page 11, theorem 23 proves that if a is regular, then Int a is regular by direct construction of an automaton. The result is established below by means of 5.3. Lemma. If a is regular, then Int a is regular. Proof. Assume A C U~ for an appropriate r. Suppose that Tr[f] - a for an appropriate formulaFof L1. Defin e ~g~ as follows:

-31/A: h<g.< *h] h where h < g abbreviates A(h(x) f Or 3 h(x) " g(x)) x and 0r is the all zero r-tuple. Note that h < g means that the element of VU0 represented by h is an initial segment of the element of Vup represented by g. (Each of the r set variables abbreviated by h are distinct from each of the r set variables abbreviated by g.] 6.3. Lemma. The intersection aL of all open sets containing a given regular set a is regular (and open). Proof. Let a VUO be regular. The intersection of all open set containing a is simply the set of all initial segments of elements in a. Thus if T4tfr] - a and if [g] is defined as follows: V:3 F]3 A. g(x)' or D g(x) a f(x) f X the desired set is Tr1g]. 6.4. a. Let a c VAO, 1 be regular. Suppose Ij a. Let Ki(a), i a 0,1, be the set of sequences ao a1 *** a, aj a A, such that there exists bo, bl,., bn satisfying a aa ~. an (1) bj s O,1), (2) b b1 b b, c, (3) bn - i. Then Ki(a) is regular. If Ae ca, let Ki(a) - Ki(a - {A)) v P1C;{ then Ki(a) is regular. Proof. Let 1 - <S, f, d, D> be an A x t0,1} automaton and suppose T(1) - a. Letl -<S, f, d, D n A x {i>. Let - T(B). Then 0 is the set of all sequences

-32a0a1.*. an b bl b & b such that bn - i. If p(a,b) - a, where a a A, b 6 {O,1}, then Ki(a) - B(s). 6.5. Lemma. Let 0 c_ V be regular. Let _ be the lexicographical ordering of VB induced by a given fixed ordering (~) of B. Define a - ~(D) as follows: u U C A CP V v vC 0 AA ue 3o v: w. Then a is regular (and the set of ordered pairs (u,v> of sequences such that U a is a function). Proof. Suppose (without loss of generality) that AC UrO B C U~ for appropriate r,s. Suppose that Tr+s 7:f i2 f] for an appropriate formula 7of 4. Define )[tgl' g2] as follows: Bg, g221 A /A Ktgl1 f2] A f2(x) 7 g2(x) A A/(y < x f2(y) - g2(y)) f2,x. D. g2(x) j f2(X)' where gl abbreviate 2 l, a, r g2 abbreviates Fr.., Fr+, and f2 abbreviates Fr+s, Fr+s and g2(x) bbreviates a conjunction of conditionals of the form g2(x) - b ~ ) f2(x) - bl v f2(x) - b2 v ** V f(x) - bm where {bl, *-, bn] is the set of all elements bi in B such that b < bi. Then Tr+s - a, and a is regular (cf. theorem 5.3 and remark). 7. Characterizations of A/B-automata behavior. An A/B-automaton is a quadruple V - (S, f, d, g) where ft; A x S - S and g: S -, B. The

-33finite behavior I(J) of t is defined as follows: rv M(1) U u.: A or (2) u Aand V [w vs ^ V VAxB''v u - aal***a A\ v - bobl'**bn w - sosl* ~ -~ a af(a, d) A f(a, sm - sr A /(8m) - b]. O4m<n O~m<n 701. Theorem. A set a C VAxB is the behavior of an A/Bautomaton if and only if (1) a is regular, (2) a is open, (3) ((uv> I " a 3 is a function, (4) tu4V AVsah. Further, if a satisfies the conditions, the proof gives an effective procedure for producing an VL such that J() - a. Proof. Assume a - I(T) for some A/B-automatonV Let - S(, f, d, g>. Define a binary relation R on A x B x S as follows: (al, blp 81> R (a2, b2 82) if and only if f(a2, ) ^ J g(S)' A g(s 2) b2. Let u a 0 if and only if u -A or u is an R-sequence beginning with an element of fa, f(a,d), gf(a,d) | a e A}. Let p(a,b,s) = (a,b> for a E A, b a B, s s S. Then o = a. (Cf. the definition of o (f ).) Hence (1) is satisfied by a.4 Conversely, assume a C VAxB and a satisfies (1), (2), (3), (4)* Without loss of generality assume B C U for an appropriate r. Let ai Pi(a)', 1 < i r, where Pi<a, C1, C2.. ci. a.* Cr) - (a, oi, a a A, and, for all J, cj a {0,1. Let i' <Si i' di,' Di>, 1 <i < r,

-34be A-automata such that T(Wi) - Kl(ai). (Cf. 6.4.) Letlt - (S, f, d, g> be an A/B-autcmaton where B - Ur, S - S1 x S2 x.* x Sr, (f(s))i - fi(si), 1 < i < r, where s a S and the subscript "i" indicates the ith component of an r-tuple, and d - <dl, d2, **, dr) and (g(s))i 1 s Di. Because of condition (3), for all i, 1 < i < r, Kl(ai) n K2(ai) - 0 and because of (4), Kl(ai) V K2(ai) - VA. Now, J(O) satisfies (1), (2), (3), (4) bJr the first part of the theorem. Thus it is sufficient to show that for each u e VA, if vt is the unique element of VB such that a a and v2 is the unique element of VB such that av Z (0), then v1 = v2. V2 It is obvious that A a r nT(Vt). Suppose v $a n'(J) and u b a. Bocause a is open, u a a, and so by (3), w - v. Let bi be the ith component of b and lot wi be the sequence of ith components of its members. Now, b u aa v b <r i ai a [ CLi (b 1 ua e Kl(aci). 1ii~r Vi bi i U a Note that u a c() ~4-0 v c satisfies conditions given in 7 V s above, for some (unique) ws a VS. In particular, g(s) - c. For this s, g(s) - c 4[ci 1 a si a Di] and since (for this s) 4\[i a Di W ua a K1(ai)], it follows that /[ci - 1 ua a Kl(ai)], so that b - c. Remark. Suppose Tr+ [l, f2' AxB' A C Ur BC U~ for appropriate r,s, and is a formula of L. One can seffectively decide whether a is the behavior of an A/B-automaton as follows: (1) a is open if and only if " A Jf] 3^ g _ f. ~.. [g]" g,f

-35is true, where f abbreviates (r+s) set variables, cf. 6.2; (2) 7.1 (4) holds if and onlyr f "is t ruL; (3) 7.1 (3) holds if and only if" 2,: k[fr' f2] A C3f r g2] f2 g2" is true. 7.2. We wish to show that none of the conditions of 7.1 can be dropped without the statement becoming invalid. 7.2.1. Let A - {1) and B = {0,11. Consider the set a: n 111. - 1 1 * O 1 n> 0. 000'a 01' Since o ~ vtA} denotes this set if "0" denotes 4<1, 0>) and "1" denotes {41, 1>), a is regular and 7.1 (1) is satisfied. It is obvious that 7.1 (3), (4) are satisfied and that 7.1 (2) is not satisfied. 7.22.2 Let A, B, a be as in 7.2.1. Then aL (cf. 6.3) satisfies (1), (2), (4) but not (3). 7.2.3. Let A - (0, 1), B - 1), and let a be the set; n> 0 1 1 1... 1 1 1 1 O*. 1 then a satisfies (1), (2), (3), but not (4). 7.2.4. Let A - {a, b) and let B {0, J 1) Let p be the set: n n a a ab a a a. It is known (cf. [9]) that 0 is not regular. Let b b2 bk e a ala2.ak e LBL- bk 1. Since BLis open, it follows that

u ~ ~ = == u "1 U2 v V1 A2 AV1 e V1) A v2 e V0O}. Now a 3atisfies UP,V1 1 u2,v2 7.1 (2), (3), (4). We wish to show a is not regular. If a were regular, then Y M a n VAX{l) is regular. Further, W is isomorphic to L. Hence to show a is not regular, it is sufficient to show L is not regular. Suppose wL were regular, then, assuming a,b E U2, for some T2(3) = L Let [g] be the formula: 3g] A A: g < f A f] *. g f (cf. 6.2). f Then T2(1) = B is regular. Contradiction. Thus a is not regular. 7.3. If A is an arbitrary finite non-empty set, AN is the set of all infinite sequences (functions on natural numbers) of elements of A. If ac VA, then f e lim a 4 {f)L c a, where NL, for B AN, means the set of all finite initial segmnents of elements in 3. Theorem. If a C (A x B)N, then there exists an A/B-automaton such that lim;J($ = a if and only if (1) aL is regular, r1 f (2) & a ^ g a,^rl rn=rn D g "ln= g2 r n where f r n is the restriction of f to the set of natural numbers < n, (3) {f I g P a AN Proof. Assume (1), (2), (3) hold, From (2), it follows that 7.1 (3) holds for a; 7.1 (2) is obvious from the definition of aL;

-37and 7.1 (4) follows from condition (3). Hence, there exists an A/BautomatonVli such that Z(1?) = L. Claim: lira -. If, then f fc aL so that f E lim L a nd a C im. Suppose s lima a L ~gJ g g Because of (3), h a for some h. Consider an arbitrary n, fn - g n for some g, ~ a, Since f r n - f' n, it follows that h n - g' r n - g r n (using condition (2)). Thus, g - h and our claim is established (based only upon conditions (2) and (3)). Let l be an A/B-autaoaton. It is obvious that lim IJ(t) satisfies (2) and (3). Hence, the "claim" of the previous argument establishes that (lira 1(V))L. i(tC) so that (1) is satisfied. 8. Solvability-sthesis algorits. The fundamental solvability-synthesis theorem that we have obtained is given in 8.1. A reformulation is given in 8.3. In 8.6 we obtain a result closely related to results obtained by L. Church [2]. 8.1, Theorem. Suppose Ax. There exists an A/B-automaton t such that J(O) C ~ if and only if 4A (cf. 6.1) is non-empty. If 4A is non-empty, then one may effectively obtain an automaton It such that J(0Z - jr (TA) where j is an arbitrary ordering of B (cf. 6.5). Proof. Suppose 1(fl) c f for some t Then, since J (t is strongly A-extendable, Z1) C_ )A and dA f ~ If ~A f 0' then because it is open, Ae YA and because it is A-extendable, the set u I v e -A VA. By lemma 6.1, YA is regular. Let Wr(~A) - a. From the definition of r&, it follows that us v) | I a is a function and, since {u | v A} - VA, 80, too, u v e a a) = VA. By leamna 6.5, a is regular. It remains only to show that a is open and then the result follows from 7.1.

-38Suppose a2 a2. For some v, s a. Since, I Suppose v2 uu it follows v< vl. Because is A-4xtendable in VA, 2 rA, tfor som w VB' Yr w v w Thus v1v2 ~ vw, so that v: < v (since is a lexicographical ordering), It follows that v - v1 and a is open, and the theorem is proved. 8.2. Corollary. Given r c A x B. One can effectively decide (by the method indicated by the proof) whether: ZI({) C ~ and:(7 ) S0 implies (i111) v 2) Proof. If Y - 0, then the condition is vacuously satisfied (cf. 8.1). Suppose ~A f 0. If L1 is the automaton picked out by 8.1 and 1(12) C ( and 1(i1T)'/ J(2), then there exists e ~ ), a Z (7 ), and v -< w. Hence, if f tis the automaton picked out by 8.1 when the ordering of B is reversed, Z(L) (2). Thus, the conditional of the corollary holds if and only if (1) YA' 0 or (2) tA f 0 and if l is the automaton picked out via 8.1 by an ordering i of B andl/ is the automaton picked out via 8.1 by the reverse ordering k of B, then the symmetric difference of;7(*.) and J(1Z2) is 0. 8.3. An A/B-automaton, A _c U, B U,,may be identified, it will be shown, with a formula of Li of a certain form. Let - <s, f, d, g> be such an automaton. Consider the formula;tb] of LfI V Ct 0:) s(0) - f(a(O), d)A A (s(x') - f(a(x'), a ( x)) N b(x) - s, t x<t gs(X) A a(x) 0 bx ) - b, ), xIt wthre "ta", "b" are function symbols interpreted as taking values

-39respectively in A,B and, respectively, abbreviating finite sequences of set variables. It is obvious that Tm+m,() - 7(I). Thus the formula above may be identified with V. Given an arbitrary formula /Aa,b] of 1 TiLo )' n VAB( Then AJ() C * A.'3,b] z aob h[a,b]* 8.4. If p maps the finite set A onto B, maps elements (and sets of elements)of VA onto elements (and sets of elements) of VB. We wish to extend further the meaning of ^. If f a AN, then (~f)(n) - p(f(n)). If a C AN, then pXa {fpf I f e a. Leoma. (1) If o C_ VA is open, then llm (ac)) - p(lim a), (2) For arbitrary B C VA, liam - lim (Int ). Proof. Let f e lim a. For all n > O, f r n a a and P(f t) a jcL, Now ]pf a p lim a and {f:}L - (~ i n) I n > 0. Hence rf a lf (jpx), Thus, (lim a) c lim (,). We shall now show lim (pa) C j(lim a).5 Suppose g a liU (^). Let a' - c n u f"l(g r n). Note that a' is open because a is. Then n>O a' contains an infinite number of elements, For u a a', let p.,(u) be the number of elements in a' of which u is an initial segment. Now As a' I P,,(A)' oo. We define ag _ a' inductively. Let ag. Suppose u e ag as well as every initial segment of u and suppose p, (U) - co. Let al, a2'... an be an enumeration of the elements of A. If u is an initial segment of v but u f v, then, because a' is open, v is an initial segment of either ual, ua2,..., ua. Since pa,(u) - co, for some i, pC,(uai) = oo. Lot k be the first such i and place uak in g. Thus ag C VA is an infinite set simply ordered by the relation "initial segment of". It is thus unambiguous to define f(n) - u(n), where u a ag has n in its domain. It follows, for all m, f [m a.g c a and p(f P m) a g r m. Thus f c lim a, pf - g and g e p lim a.

-40The proof of (2) is immediate from the definition of lir and Int. 8.5. Lemma. Let 0 C AN be the set of all infinite R-sequenoes f such that f r n is an element of a given set I of sequences of length n, where R is an n-ary relation over A. Then (1) la (pL) * p, and if p i a projection, (2) (P)L (BL), (3) u ((P )L)', (4) L and p(OL) are regular sets and a regular expression denoting them may effectively be obtained. Proof. (1) Let f e B. Then [f}L c L. Hence f 1ls (IL) and B C lim (L). Suppose f 6 m (L). Then i rn e sg tn I Sr 6 CE and, for all m, f f a is an R-sequence. Hence f is an R-oequence and f e O. (2) u (f)L V g ar h(( P8) lr) u g9a V g e ( ^ p(g r m) "U - us (L ). g,m (3) lim (())L) - li (p(1L)) by (2) and by 8.4, lie j(BL) i hJ (1L), since. is open and by (1) the result follows. o(+) K(w)-r A - {]an ~ Ja2}... [an} ~A,.i -a A, is the set of sequences in VA in which the sequence w- a1 a2 o. a occurs and this set is regular. The set R K(w) is regular and is the set of all R-sequences. The set EL is regular, as is any finite set. The set L is:3R K(w) 3 ~L and is, therefore, regular. Since projection preserv regularity, ~(gL) is regular. 8.6. Let L5 be the system consisting of the formulas of L1, with individual variables interpreted over natural numbers and the set variables interpreted over arbitrary sets of natural numbers. With a formula [F1t, F2,.-, Fr] of h we associate a set T~~3Fdefined as follows:

-41f c T: if and only if r i u -and ((zx)) * t'x),, 1: < i r, where fi is the characteristic function of Fi and[lF1, F2, o*.. Fr] holds. Abbreviations introduced for L in remark 5.3 will be used in L as well. 8.6,1. Lett - 8 f, d, g> be an A/Bautomaton. The following formula h4ta,b] of L5 (abbreviated) below may be identified with ls V Is(o)) ^ /(a(O) d)A A (s(x, ) - (a(x'), (x))) b(z) - p(x)3. 8 X If a - T L,(Gt) (assuming range a 5U and range b c.U,), then comparison with 3bCa,b] shows that aL J (JV) * TX3J+413 (of, 83) and by lemma 8.5 (3), lim M(1) - a. 8.6.2. Consider arbitrary formulas of Li of the torm V /\Mta, b, a, x], where range a C A, range b C B, and where Xs is free sX of quantifiers, contains only S, a, b, x free (a, b, *, respectively abbreviate finite sequences of set variables), 3ay contai numerals but not ""m" nor n"". Assume K to be in disjunctive norual form and let n be the maximum of those a's such that x(m) or 0(a) appears in K. Then Tm,,r( /\), range S Ur, is the set of all f (A x B Xz ) which are R-sequences, for some n-ary R, and such that f r n a S for some finite set E (of elements of V of length n). Both R andB are effectively, indeed readily, obtained from N in expandod disjunctive normal form. If B - Tr+, +r( xAx), then;P - T~+( V An) where p T;+mt rII X maps an (m+m'+r)-tuple into the appropriate (m+m')-tuple. 8.6.3. Theore. Given a fomula yA/),, b, a, xz, X as in 8,6.2, of L5. There exists an A/B-automaton L such that lim 7Cl) C I - Tm+m'( V A M) if and only if [A f 0 (ci. 8,1) where 5 X

T = B. Whether or not KA =0 can be effectively decided (by the method given in proof) and if YA 0s, one can effectively produce an automaton satisfying the condition (by the method below), Proof. From 8.6.1 and 8.6.2, it follows that im 7()O (D c L. The set L may be effectively obtained (8.5 (4)), The problem is now reducedito 8.1. 8.6.4. In connection with 8.6.3, it should be noted that: lim J( 8 )A' A.b a. b V / ba, ] x a,b a x where b, 2t are as in 8.6.1. 9. Remark. We give a metamathematical proof that the set n n fb a a b a| n O) is not regular. Let ab 8 U2, 1 If the set were regular, then there would be a formula'[f] of such that T2- B. Then y - 2x V' f(x) -b A f(y) j 0 O\ A(z > y D f(z) - 0)A;[f]. Thus regularity of p implies that z doubling is definable in 1 and by results of R. M. Robinson 10] it would follow that the set of true sentences of is not effective, contradicting 5.8.

CHAPTER IV NCN-EXTISTNCE OF CERTAIN AWO/RITHS 10. Let L2 be the class of well-formed formulas contructed out of individual variables and monadic predicate variables, b meansLL of the succossor operation (), addition (+), * propositional connectives, and first order quantification. Let L2 be the system consisting of L2 with the individual variables ranging over natural numbers and the xonadic predioateo range over properties of natural numbers which are ultimately false and remain false (we could have used finite set variables instead, as in 5) and the unary and binary (non-logical) operations interpreted as indicated and the logical operators and - interpreted in standard fashion, It will be convenient, as a device for abbreviation siailar to 5.3 remark, to employ unary function symbols (we shall uose Oi) in tonrmulas such as i(x) a a where a a A and A is a finite set of symbols, By coding A, i.e., putting A into 1-1 correspondence with a set of r-tuples of zeros and ones, for appropriate r, the function symbol "iw may be replaced by a sequence of r distinct monadic predicate variables. To say i is free means that the associated r monadic predicate variables are free. If aw abc is a word (finite sequence), a,b,o a A, then i(x)i(x+l)i(x+2) -- owill abbreviate i(x) * a \ i(x+l) w b f i(x+2) - o, Notice that in L1: xmO24 * UX+ 43,

-44so that as further abbreviations, we shall employ 0, <. Given a formula G - G[i,m] in which only i, occur free where i is a unary function (interpreted as a function on the natural numbers with values in a finite set B) and a is a monadie predicate. With each i,m such that G[im] is true and m(O) holds associate the finite sequence TG(i,m) of words (in B) whose first n words are i(l)i(2)...i(xl), i(xll)i(x.2)*..i(x2),.. i(x_,. +l)i((x. 2).. (xn where 0 < x1 < x2 < *** < Xn are the first n + 1 numbers for which a holds. Let T(G) be the set of all TG(i,a) such that G[i,]a is true and m(O) holds. 10.1. Lema. For every Post normal system P there is a formula F a F(P) in L2 such that T(F) is the set of all proofs of P. Proof. Let Cm(x,y) abbreviate: M(x) M(Y) (x < y) A (x < S < r -'?), m(x) A m(y) Vx u a y u + u - u With each production of P associate the formula S (w,xy): i(w+l)i(w+2)...i(w+()) Vu + (6) 1' 2- 04"I','U 2 ^i(u+l)i(u+2)...i(u+.t(o)). ok ^AV(s + u,) s+ ) - slx+ ( ) -)u u-1 2 A 4 I i(u +u u - ), i(w + (O I).U ).:(x+u))]

where Q(cr) represents the length of 0. This $ormula expresses the condition that i(w+l)i(w+2)...i(x) - k and i(x+l)i(x2)*.. i(y) - go2 for some 0. Let (cjo2) -, (co2)... (ot.,)P be the productions of P and let a be the axiom of P and define SP(ism) /A [(C.(W,x) Cm(xy) DSO O(wxy)V *es V w,x,y 102 A(w - 0 x- (a) A i(1)i(2)'. i(=)) )]. Then F is [sP(i,m) A m(O), V x O ^A y O Ax y, M(x) t (y)] 1v (0) / x,y y x -Y i(1)i(2).*.i(t(=)) - a]. 10.2. Theorem. The set of satisfiable formulas of L is effectively enumerable but not effective. Indeed, the degree of unsolvability of this set is maximum among all effectively enumerable sets. If P is a Post normal system with 2 letters (see 1. Davis, omputability snd Unsolability, sMcGraw-Hill, Noew York, 1958, page 100, theorem 5.3) which generates the complete (Post, 1944) set of natural numbers and if Fn - F(P) A YcM(x x+n+l) 1 i(x+l) - 1 ^ i(x+2) " 1 A ~*.. i(x+n+l) - 1, then every recursively enumerable set is recursive in the set of G~del numbers of the satisfiable formilas 1n. Proof. n a Sp (see Davis, pag 85, definition l.ii) if and only if iYV F is true, i.e., if and only if Fg is satisfi&ble. The fact that the satisfiable formulas are effectively enuaerable follows readily from the Presburger result.

-4610.3. It is clear that the results of 10.1 and 10.2 hold if the individual variables are intcerpreted over positive integers rather than non-negative integers. Hence, one obtains for either the nonnegative integers or the positive integers: Corollary. If L2 is the system consisting of the formulas L2 but with the interpretation of the predicates unrestricted, then the set of satisfiable formulas of L2 is not effective. Proof. The property of a predicate that it becomes ultimately false and remains so is definable in L2 L2. This (for positive integers) is Putnam's theorem 4 [8, page 50], Putnam's argument can, however, be adapted to give the stronger resultt The set of satisfiable formulas of L2 is not arithmetic. 10.4. Let L be the system consisting of the class of formulas L2 with individual variables interpreted as ranging over all the integers and with the predicates ranging over finite sets of integers. Analogues of the lemma of 10,1 and the theorem of 10.2 hold for L2. T(G) is defined exactly as before. 2J Notice that in L:s x O === Vx + x- x, x 1 ym0X O yA - x, x y x> o V Al p(y) y lp(,-1)] t p(x) p y and p(y-l) V'Yt a ^ p(S). To establish the analogues for L32 we show that "V" can be moved all 2'~ p the way to the left, Let D(p) stand for A [p(y) A y f 1 D p(y-l)]. Notice that y

-47D(p) holds for p if and only if p is a consecutive set of positive integers beginning with 1. Then F - F(i,m) is modified by conjoining Aui(x) D D(p) A p(x) and prefixing the conjunction by V. In the formula F, wherever one p wishes to express x <y, one writes V x + u- y N p(u). U 10.5. Let L2 be the system consisting of the class of formulas L2 with individual variables interpreted over natural numbers and predicates interpreted over ultimately periodic sets (4 set of natural numbers is ultimately periodic if its characteristic function is). Corollary. The set of satisfiable formulas of L4 is effectively enumerable but not effective. The degree of unsolvability of this set is maximum among all recursively enumerable sets. Proof. That the set of satisfiable fornulas is effetively enumerable follows from the Presburger result. The rest of the statement follows from the fact that the property of a predicoate of being finite is definable in L4 and from 10.2. A similar result holds for "integers" in place of "natural numbers". 10.6. Corollary Given an input-free automatonL and a formula B of L2 in which the predicates are interpreted as outputs: the problem of deciding whether VZ satisfies B is effectively decidable while the question "does there exist anfi such that t satisfies B8" is undecidable. See Bfichi, Elgot, and Wright [1] and Elgot and Wright [4, page 68, last paragraph].

BIBLIOGRAPHY 1. J. R. Bflchi, C. C. Elgot, and J. B. Wright, The nonexistence of certain algorithms of finite automata theory. (Abstract), Notices of the American Mathematical Society vol. 5 (1958) p.98. 2. A. Church, Aplication of recursive arithmetic in the theo of computers and automata, Lecture Notes, Summer Conference, University of Michigan, June, 1958. 3. I. M. Copi, C. C. Elgot, and J. B. Wright, Realisation of events by!ogica! nets, Journal of the Association for Computing Machinery vol. 5 (1958) pp. 181-196. 4. C. Elgot and J. Wright, uantifier elimination in a prob!! of logical design, Michigan Mathematical Journal vol. 6 (1959) pp.65469. 5. S. C. Kleene, Representation of events in nerve nets and finite automata, Automata Studies, Princeton University Press, 1956. pp. 3-41. 6, I. T. Medvedev, On a class of events representable in a finite automaton (translated from the Russian by J. Schorr-Kon), M.I.T. Lincoln Lab. Group Report, June 30, 1958, pp. 34-73. 7. E. F. Moore, Gedanken-_ eeriments on sequentisl machineo Automata Studies, Princeton University Press, 1956, pp. 129-153.

-49. 8. H. Putnam, Decidabilit and essential undecdabilitr y Journal of Symbolic Logic vol. 22 (1957) pp, 39-54. 9. M. Rabin and D. Scott, Finite automata and their decision problem, Report, IBN Research Center, LamIb State, Yorktown, Now York, 1958. 10. R. M. Robinson, Restricted sot-theoretical definition in arithmetic, Proceedings of the American Xathamtical Society vol. 9 (1958) pp. 238-242.

FOOTNOTES 1. This was pointed out to me by J. R. Bllchi. 2. This result has been obtained independently by J. R. Bichi. 3. This was suggested by J. fR. BIkchi. 4. This was pointed out to me by J. B. Wright, 5. The proof is closely related to KEnig's infinity le. Theorle der endlichen und unendlichen Graphern Leipsis, Akadeaiache Verlagsgesellschaft M. B. H., 1936, p. 81, Sats 6, -50

DISTRIBUTION LIST (One copy unless otherwise indicated) Assistant Secretary of Defense Office of Technical Services for Research and Engineering 2 Technical Reports Section Information Office Library Branch Department of Commerce Pentagon Building Washington 25, D.C. Washington 25, D.C. Naval Electronics Laboratory Armed Services Technical San Diego 52, California Information Agency 5 Attn: Technical Library Arlington Hall Station Arlington 12, Virginia Naval Ordnance Laboratory Corona, California Chief of Naval Research 2 Attn: Robert Conger, Electrical Department of the Navy and Mag. Division Washington 25, D.C. Attn: Code 437, Information University of Illinois Systems Branch Control Systems Laboratory Urbana, Illinois Chief of Naval Research Attn: D. Alpert Department of the Navy Washington 25, D.C. University of Illinois Attn: Code 923 Digital Computer Laboratory Urbana, Illinois Director 6 Attn: Dr. R. E. Meagher Naval Research Laboratory Technical Information Officer, Air Force Office of Scientific Code 2000 Research Washington 25, D.C. Washington 25, D. C. Commanding Officer 2 Air Force Cambridge Research Office of Naval Research Center Navy No. 100, FPO Laurence C. Hanscom Field New York, New York Bedford, Massachusetts Attn: Electronic Research Commanding Officer Directorate Library ONR Branch Office 346 Broadway Technical Information Officer New York 13, New York U.S. Army Signal Research and Development Laboratory Commanding Officer Fort Monmouth, New Jersey ONR Branch Office Attn: Data Equipment Branch 495 Summer Street Boston 10, Massachusetts

DISTRIBUTION LIST (Continued) Commanding Officer Wayne State University Diamond Ordnance Fuze Laboratories Detroit, Michigan Washington 25, D.C. Attn: Dept. of Slavic Languages, Attn: Tech. Ref. Section, Professor H. H. Josselson ORDTL 06.33 University of California of Los Office of Ordnance Research Angeles Box CM, Duke Station Los Angeles 24, California Durham, North Carolina Attn: Dept. of Engineering, Professor G. Estrin Director National Security Agency Massachusetts Institute of Fort George G. Meade, Maryland Technology Attn: Chief, REMP Cambridge, Massachusetts Burroughs Corporation Naval Proving Ground Research Center Dahlgren, Virginia Paoli, Pennsylvania Attn: Naval Ordnance Computation Attn: A. J. Meyerhoff Center Cornell Aeronautical Laboratory National Bureau of Standards 4455 Genesee Street Washington 25, D.C. Buffalo 21, New York Attn: Dr. S. N. Alexander Attn: Systems Requirements Dept., Dr. Frank Rosenblatt Aberdeen Proving Ground, BEL Aberdeen Proving Ground, Maryland Lockheed Missile Systems Division Attn: Chief, Computation Laboratory Sunnyvale, California Attn: J. P. Nash Office of Naval Research Resident Representative Census Bureau The University of Michigan Washington 25, D.C. 820 E. Washington Street Attn: Office of Assistant Director Ann Arbor, Michigan for Statistical Services, Mr. J. L. McPherson Commanding Officer ONR Branch Office University of Illinois John Crerar Library Building Urbana, Illinois 86 East Randolph Street Attn: Electrical Engineering Dept., Chicago 1, Illinois Professor H. Von Foerster National Bureau of Standards University of California Washington 25, D.C. Institute of Engineering Research Attn: Mr. R. D. Elbourn Berkeley 4, California Attn: Professor A. J. Thomasian

DISTRIBUTION LIST (Continued) Naval Ordnance Laboratory Carnegie Institute of Technology Corona, California Pittsburgh, Pennsylvania Attn: H. H. Weider Attn: Director, Computation Center, Alan J. Perlis George Washington University Washington, D.C. Hunter College Attn: Professor N. Grisamore New York 21, New York Attn: Dean Mina Rees Syracuse University Electrical Engineering Dept. University of Pennsylvania Syracuse 10, New York Institute of Co-Operative Research Attn: Dr. Stanford Goldman Philadelphia, Pennsylvania Attn: Dr. John O'Conner Princeton University Electrical Engineering Dept. University of California Princeton, New Jersey Department of Mathematics Attn: Professor F. S. Acton Berkeley, California Attn: Professor H. J. Bremermann Chief, Bureau of Ships 7 Department of the Navy University of Saskatchewan Washington 25, D.C. Saskatoon, Canada Attn: Code 280 Attn: Dr. Arthur Porter Code 677 Dean of Engineering Code 684 Code 686 Northeastern Unrversity Code 687E 360 Huntington Avenue Code 687F Boston, Massachusetts Code 687G Attn: Professor L. O. Dolansky Naval Ordnance Laboratory IBM Corporation White Oaks, Silver Spring 19, Military Products Division Maryland Owego, New York Attn: Technical Library Attn: Dr. S. Wiirikler David Taylor Model Basin Post Office Department Washington 7, D.C. Office of Research and Engineering Attn: Technical Library 12th and Pennsylvania Avenue Washington 25, D.C. Chief, Bureau of Ordnance A-ttn: Mr. R. Kopp, Research and Department of the Navy Development Division Washington 25, D.C. Air Force Camrb)idge Research Center Air Force Office of Scientific Research L. G. Hansconm Field Washington 25, D.C. Bedford, Massachusetts Attn: Dr. Harold Wooster Attn: Chief, CRE3

DISTRIBUTION LIST (Concluded) Massachusetts Institute of Technology The University of Chicago Cambridge, Massachusetts Institute for Computer Research Attn: Professor W. McCulloch Chicago 37, Illinois Attn: Mr. Nicholas C. Metropolis, Benson-Lehner Corporat ion Director 11930 Olympic Boulevard Los Angeles 64, California Stanford Research Institute Attn: Mr. Bernard Benson Computer Laboratory Menlo Park, Atomic Energy Commission California Washington 25, D.C. Attn: W. H. Kautz, Attn: Division of Research Senior Research Engineer Naval Research Laboratory Commander Washington 25, D.C. Wright Air Development Center Attn: Solid State Electronics, Wright-Patterson Air Force Base, Ohio Code 5210, Mr. G. Abraham Attn: WCLJR, Major L. M. Butsch David Taylor Model Basin Zator Company Washington 7, D.C. 140.5 Mt. Auburn Street Attn: Arthur Shapiro Cambridge 38, Massachusetts Attn: Calvin N. Mooers Diamond Ordnance Fuze Laboratory Library Research Air Development Center Washington 25, D.C. Griffiss Air Force Base, New York Attn: J. E. Rosenberg Attn: RCWID, Captain B. J. Long

UNIVERSITY OF MICHIGAN 3IIIfllll 90 11111111115 III0 2 311 3 9015 02827 3012