THE UNIVER SITY OF MICHIGAN COLLEGE OF LITERATURE, SCIENCE, AND THE ARTS Department of Communication Sciences Technical Report DECISION PROBLEMS FOR MULTIPLE SUCCESSOR ARITHMETICS(1) J. W. Thatcher IBM Watson Research Center Yorktown Heights, New York ORA Projects 03105, 06376, 06689 under contract with: U. S. ARMY RESEARCH OIFFCE (DURHAM) GRANT NO. DA-ARO(D)-31-124-G588, PROJECT NO. 4049-M DURHAM, NORTH CAROLINA and NATIONAL SCIENCE -FOUNDATION GRANT. NO, GP-2359 WASHINGTON, D.C and DEPARTMENT OF THE NAVY OFFICE OF NAVAL RESEARCH CONTRACT'NO. Nonr-1224(21) WASHINGTON, D.C. administered through; OPTFICE OF RESEARCH ADMINISTRATION A AARBOR April 1965

RESEARCH PROGRESS REPORT Title: "Decision Problems for Multiple Successor Arithmetics," J. W. Thatcher, The University of Michigan Technical Report 03105-36-T, April 1965; Nonr 1224 (21), NR 049-114. Background: The Logic of Computers Group of the Communication Sciences Department of The University of Michigan is investigating the application of logic and mathematics to the theory of the design of computing automata, A study of the decision problem for various formal languages is a part of this investigation. Condensed Report Contents: Let Nk denote the set of words over the alphabet Zk = fl,..., k). Nk contains the null word which is denoted X. We consider decision problems for various first-order interpreted predicate languages in which the variables range over Nk(k > 2). Our main result is that there is no decision procedure for truth in the interpreted language which has the subword relation as its only non-logical primitive. This, together with known results summarized in the report, settles the decision problem for any language constructed on the basis of a large number of relations and functions. For further information: The complete report is available in the major Navy technical libraries and can be obtained from the Defense Documenation Center. A few copies are available for distribution by the author.

TABLE OF CONTENTS Page 1. Introduction 1 2. Method of Proof 2 3. Undecidability Results 6 4. Conclusion 15 Acknowledgment 18 Bibliography 19 Footnotes 20 V

1. 1. Introduction. Let N denote the set of words over the 0^0 k alphabet Zk= {1,..., k}. Nk contains the null word which is denoted X. We consider decision problems for various first-order interpreted predicate languages in which the variables range over Nk(k~ 2). Our main result is that there is no decision procedure for truth in the interpreted language which has the subword relation as its only nonlogical primitive. This, together with known results summarized in Section 4, settles the decision problem for any language constructed on the basis of the relations and functions listed below. Concatenation u" v = uv Subword u v v - x 3 y I v = xuy] Pr efix u v — x [ux = v] Suffix v i u 4-'ax [ xu = v] Reflection c(., ) =..,oT ). (o.EZ ) 1e n n 1 i k Right Successors r (u) = uc ((T-E ) a' k Left Successors I (u) = 0u (rEk) Equal length L(u, v) * —u and v have the same number of symbols. N ( ) is the structure <N, S >. The language of N(s ) ), is the first-order applied predicate calculus with equality Lk(c ), is the first-order applied predicate calculus with equality

2. having individual variables u, v, w, x, y, z, u... ranging over N and having a single non-logical constant a interpreted as the corresponding relation on Nk. The theory of Nk( ( )(or of Lk( )), Tk( s), is the set of sentences of Lk(s ) which are true in Nk( ). A relation R, Nk is definable over N ( )(or definable in L( )) if there exists a formula F(x, l.., x ) in Lk( ) such that R(x,...,x ) holds iff <x,...,x > satisfies F(x,...,x ) in r m Ail ^Wm m m N ( ) for every m-tuple <x.., xm> E N A function f: N -N is definable over N ( ) iff its graph (the relation f(xl,..., x ) = y).k, 1. m is definable. By analogy, the meanings of the notations L k(, ), Tk(r l...., r L) (written T,(r, A, L), for convenience) and N (1,..., k,' )(written Nk(, )) should be clear. We will say that L is an interpreted language over Nk if L is the language of some structure with domain Nk. 2. Method of Proof. The schema for defining a function o(on Nk) by primitive recursion from functions 4 and X l'.* Xk is given by: (1) p(x,...,x,X) = 4(x,.. (x ) 1 n n p1,...,x,r (y))=x (x,...,x k. i~~~~~~~~,.,,n),y 1,..., k.

3. The class of k-primitive recursive functions is defined to be the least class of functions containing the constant function, q(x) = X, the right successor functions and the projection functions (ir (x,., x ) = x.) n 1 n 1 and closed under composition and primitive recursion according to the schema above. Generalizing the concept for k = 1, we will define the k-arithmetic relations to be the closure of the k-primitive recursive functions under first-order definability. (2) Our undecidability proofs are based on: Proposition 1. Let L be an interpreted language with theory T. If all arithmetic relations are definable in L then T is undecidable. The most direct argument for Proposition 1 would be Tarski's [7]: under any effective numbering of L in N1, it can be shown that the set of numbers correlated with T is not definable in L. But all recursive subsets of N. are arithmetic and therefore the set of numbers correlated with T is not recursive. Let U, V be arbitrary sets. For a relation B_ Un and w EU, we will write B to denote the (n-l)-ary relation obtained w from B by fixing the first argument. BQ VX Un is universal with respect to V for a class R of relations in Un if {B |w w V}. A relation B' U X U is strongly universal for finite subsets of V' U if there exists a sequence V = V, V1,..., V,.. of subsets of U such that B is universal for finite subsets of V. with respect to 1

4. v. (i- 0 1,...). It is well known that quantification over finite monadic functions permits the conversion of recursive definitions into explicit ones. This second-order quantification can be reduced to first-order quantification if one has available a relation which is universal for finite monadic functions. ) The extension of these ideas to the use of finite binary relations offers no difficulty. Thus, the following proposition provides a method of applying Proposition 1. (All (1-) arithmetic relations are m-arithmetic for any m.) Proposition 2. Let L be an interpreted language over Nk. All m-arithmetic (m < k) relations are definable in L if (i) r ON is definable in L ( = 1,..., m) and (ii) there is a relation Br NkXN which is definable in L and universal for finite binary relations on N with respect to Nk. m k To expand on the comments preceeding the statement of Proposition 2, we observe that the following formula (with quantification over finite binary relations) is an explicit definition of sp(x, y)= z (on N ) defined by primitive recursion from 4 and X1, * )Xm m m according to schema (1). (2) S[vw[ S(, w)4 —w = I(x)] S(y, z) m A /\ Y u yw[ S(r (u), w) - av[ S(u, v) ^ w= X (x, v, u)] ] ]. -r= 1

5. If X and 4 are definable in L and if L satisfies the hypotheses of Proposition 2 then (2) can be expressed in L. Thus the functions on N which are definable in L are closed under primitive recursion m and we can immediately conclude that all m-arithmetic relations are definable in L. To simplify the specific undecidability proofs, we give the following: Lemma 1. If B is strongly universal for finite subsets of VC U then a universal relation for finite relations in V X V is definable over U(B). Proof: Consider the following sequence of definitions: D(z, x, y) = B(z, u) B(z, y) B(z u) u = x u = y] A AA df P A A V AM^aAf ^ -" 4ft T(z, x,;X) = auaw[ D(z, u, w) D(u, x, y) A D(w, y,y)]., ~^4K df ft ^ & A * A & R(z,x,y) =f B( T(v,x,y)] Aft M^ M" dal M # At MA A It is clear that <z,x,y> satisfies D iff B = {x, y}. T defines a z pairing relation on V. For any ordered pair <x, y> there exist u, w (EV1) with B = {x, y} and B = {y}. Also there exists a z (EV ) 1~~ uw2

6. with B = {u, w} and therefore <z, x, y> satisfies T. But for any z x', y' in V, if w, x',y' satisfy T then x' = x and y' = y because, in effect, the definition, {{x, y}, {y}}, of the ordered pair <x, y> is a good one. For any finite binary relation S it is now clear that there exists a w (EV ) such that <w, x, y> satisfies R iff S(x, y). Hence R is a universal relation for finite binary relations on V. The final form for the application of Proposition 1 can now be stated as: Proposition 3. Let L be an interpreted language over N with theory T. If r I N are definable (a= 1,...,m) and if a strongly a' m universal relation for finite subsets of N is definable in L then m all m-arithmetic relations are definable, in L and T is undecidable. 3. Undecidability Results. The following definitions in L. (, c ) will be useful (-=,...,k): T (x)= Vz[ z x-'z S v c z], C At df e^ _* ^ m ^ _w'*% t (x) = =dfT (y)^ ys x V z[ T (z)A zs x —zc- y], o aa A "dfo *' AAtW r*U A" A ot s (x)=y= T (x) AT (y)^ x y^V[x z z y x= z = l o(Tkn 2~ A" 0-f (T ^ zx 3 - Az % ^ % M j T defines the set of c- -tallys {X,cr, cr,.. }; t (x). y is the graph of the maximum -tally function - t (x) is the largest r -tally contained as a subword in x; s (x) = y is the graph of the successor Cr _ ^

7. function on T 0' The concept of maximum tally which Quine [6 ] used to prove the undecidability of T 2(, ^ ) plays the crucial role in defining a (4) strongly universal relation for finite sets. ( Lemma 2. The relation, B(w, u) t2(u) # t2(w)^ t (w)lultz(w) A w, is universal for finite subsets of Nk with respect to Nk and is therefore strongly universal for finite subsets of Nk. Proof: Let S = fu,..., u } be a finite subset of N and take 1I n k v to be any 2-tally larger than every one of the t (u.), i= 1,...,n. Then for w = vlu lvlu lvl.. lvlu Iv, 1 2 n we claim that B = S. Certainly B D S because, by construction, w wt (w) = v * t (u.) and for each i, vlu.lv is a subword of w. But the 2 2i 2 1 occurrences of v in w are uniquely determined (w is uniquely decomposable in the form written above) and thus, for any subword of the form vlulv, either v~ u (and u i B ) or u is one of the u.. w 1 Therefore B = S and B is indeed universal for finite subsets of w Nk.

8. From the definition it is clear that B is definable over Nk(, ). k Since concatenation is k-primitive recursive it follows that all definable relations of L (a, S ) are k-arithmetic. Thus as a consequence of the previous Lemma and Proposition 3 we obtain a slightly modified form of Quine's result: Theorem 1. (Quine) A relation is definable over N (a-. ) k iff it is k-arithmetic and Tk(a, ) is undecidable. k Lemma 3. The relation B as given in Lemma 2 is definable over Nk(r,I, J, Proof: The following formula is claimed to be a definition of B in L (r,, C ).5) The expression lyl is used to abbreviate e r (y). 2 a (3) t (W) t(u,) )A z[ z z w A lul a z A v y[ lyl & z -y - u] A lt2() Z ^A ltz(w)s z-. It is clear that if B(w, u) holds then z can be taken to be t2(w)lult2(w) and <w, u> satisfies (3). On the other hand, if <w, u> satisfies (3) then z = zllulz2 w for some z and z. By the maximality condition on subwords of the form lyl, z1 and z2 must be 2-tallys. z1, z2 must be at least as large as tz(w) by the second line of the definition and no larger than t (w) since z c w. Hence z = t (w)lult (w), z < w and tZ(w) = tZ(u), i.e., B(w, u) holds. 2s 2

9. With Lemmas 2 and 3, we can apply Proposition 3 to obtain: Theorem 2. A relation is definable in Lk(r,,, c ) iff it is k-arithmetic and thus Tk(r,,'. ) is undecidable; L (r,f,' ) and Lk(,' ) are equivalent as to definability. The subword relation is definable in terms of the prefix and suffix relations: x S y -" z [~y A z Ax z] Also it is easy to verify that the left and right successor functions are definable in Lk(ac _,, ). Thus we obtain the following corollary to Theorem 2, the first part of which was conjectured by Buchi in [ 2]. Corollary 1. Tk(.(,, 2 ) is undecidable. The languages Lk(,^ ) and Lk(o-,, _ ) are equivalent as to definability. The reflection function c is an automorphism of the structure Nk(-, ) in the sense that c(cr) = C and u c v - c(u) _ c(v). It is evident that this automorphism property carries over to all relations definable over the structure. Thus, if R(u, v) is a relation definable in L k(-, ), then R(u, v) — R(c(u), c(v)). Because the graph of concatenation does not have this property, it is not definable over Nk(-, s ) and therefore Lk(,' ) is weaker than k,~)adteeoe~,

10. L (r,i, c ) with respect to definability. Any relation on N1, on the other hand, is invariant under c since cj N1 is the identity. Therefore there is no reason to suspect that the arithmetic relations are not definable over Nk(u, c ). We will show in the sequel that these relations are indeed definable. Again we begin by giving a mathematical definition of a relation on N. which has the required universal properties and subsequently show that it is definable over Nk(, c ). k First we describe a set S'N from which will be chosen the odings or finite sets and ultimately, finite binary relations. The codings for finite sets and ultimately, finite binary relations. (6) The definition is given in levels: S = {Znlulnl tz(u) 2n-l and 1S lul}, n 2 and S is taken to be u S. n n> 1 Before defining a universal relation for finite subsets of N (as is required), we observe: Lemma 4. The relation, U'(w, v) 4 —wcS vyES t (w) = r2t2(v) ^ v - w, 2^ 22

11. is strongly universal for finite subsets of S1. Proof: The sequence S1,..., S,... satisfies the definition n of strong universality for the relation U'. To verify this we must show that U' is universal for finite subsets of S with respect to n S. Consider the subset {u,...,u } of S. Each u. is of the n+1 1 m n 1 form 2 v.2n where the uniquely determined v. begins and ends with 1 1 1 and t (vi) S 2. Then taking 2n 2n n Q 21 2 m it is clear that U'(w, u.) for each i and wS +1 But again, the uniqueness of decomposition in the form above insures us that if U'(w, u) then u is indeed one of the u.'s. In effect, what we have in U' is a strongly universal relation for encodings of finite subsets of N1. Any element of S1 is of the form 2v2 where v is a 1-tally of length greater than one. Clearly we can associate with each element of S1 an element of N (21 2 corresponds to 1 m-) to obtain from U' a strongly universal relation for finite subsets of N1. U(w, v) -- z[ U'(w, z)^ tZ(z) = 2 ^rlr(v) = tl(z)] v U'(w, v) A tZ(v) # 2. Lemma 5. U is strongly universal for finite subsets of N1.

12. Proof. Now the sequence N1, S2,...,S,... works in the n definition of strong universality. Lemma 6. The relation U is definable over Nk(, G ) Proof: In consideration of the definitions of T, t, and s C C (and of U and U' it is sufficient for us to show that S is definable over Nk(o-, ). First we introduce the definition: M(zx)= ax c z^y= xc yA yr z -x = yv y= z],%^ 1, C - z^ At Ax A M rx z M(z, x) holds when x is a maximal proper subword of z. Since X has no proper subwords, M(\, x) holds for no x but for z = X, it is easily seen that M is exactly the set consisting of the right and z left predecessors of z. We will prove the following formula is a definition of S. (4) s (l)w ^ Ax1 a x2 x[M(w,x)^ ^ M(w,x )x x M(xl X (x x) A x X^ t (x)= t (x)= t (w)= s t (x) M 22 1 2 2- 2 ^ We must first show that every element of S satisfies the formula above. Let w 2z lul2mES (m > 1). The words x = 2mlulm and m - 1 m-1 m x = 2 lu2 are distinct maximal subwords of w and with m- x = 2 lu12 it is clear that w satisfies (4). For the converse,

13. assume that w = o Icr...r- satisfies (4). We know that n is greater 1 L n than two since x X. Then x= -. n- and x2 a 2. n (possibly interchanging xl, x2). If x were not the "middle" of w then we would have x= 1' cr = r..r = r and this entails 1 n-2 3 n cr 0. and o- = 4r -.. But with 11 w we know 1 3 2 4 6 i = Ci i+l for some i and thus 1= c = C =... which contradicts i +2 3 x lx. Therefore x= a- 2..' n-l as is desired. Let t (w)= 2 and 1 2 n-12 write w= Zmly. If m k then t2(xl) = 2 implies that t (x) = 2 which is impossible. Thus, we must have m = k and with the same argument for the other end of the word we get w = 21w'112k and with 1 1 w we have wES. From Lemmas 5 and 6 we know that a strongly universal relation for finite subsets of N1 is definable in Lk(c, i ). Also, the graph of r, restricted to N is definable as was indicated at the beginning of this section. Therefore, applying Proposition 3 again we have: Theorem 3. All arithmetic relations are definable in Lk(r ) and Tk(c, c ) is undecidable. A Let 6 be any permutation of the symbols Sk and let 6 be the extension of 6 to a concatenation automorphism. Any such mapping is an automorphism of Nk(c ). Thus definability over this structure is K.

14. even weaker than that over Nk(,' ). Of course, it is impossible to define in Nk(s ) any specific symbol (o- E2k) but the following formula defines the set Zk of symbols: vz[ z C x-z = x Vv y[ z S y] ] Az 1 [ x CS Z] 4 m ft M~A %" nA ^ 4^ % The first part of the definition is satisfied by elements of ku {X } whereas the second part excludes X. We will use Yk(X) to abbreviate the formula above. Theorem 4. Tk (c ) is undecidable, Proof: Let A Jbe any formula in Lk(r, < )k We associate with A the following formula of Lk(; ): A( Ad *,..., k)= / 1z() # Azj#z M = 1 i) j J where S2 A is the formula obtained from A by substituting z for Z — 0'.-T0 every occurrence of o (,= 1,..,k). It is assumed that z,, z do not occur in A. If A is a sentence true in Nk (r, - ) then clearly A:'(1,..., k) is true in Nk( ) and, in particular 3z... zkA* is true in Nk(S ). Conversely, if this last sentence is true in Nk ( ), then by the construction of A", A-'(a 1,... k) is true where {a i}=.ke Because permuting the symbols produces an automorphism of Nk( ( ),

15. we also know that A''(l,.., k) is true in Nk( S ) and thus A is true in Nk (, c ). In this way we have a transformation: with the property that AeTk(, G ) if and only if 3 Zl... ZA eT ( ) and a k ^' 1" Ak k decision procedure for the latter theory would yield a procedure for the former. By Theorem 4, Tk( ) is undecidable.. The proof applies equally well to the two other theories with constants which were considered above. Corollary 2. Tk( ) and Tk(, > ) are undecidable. 4. Conclusion. The results of the previous section all apply to Nk for k > 2. The analogous problems for the special case, k = 1, corresponding to the natural numbers, have long been solved. The structure N 1() is simply the natural numbers under addition and T (' ) is known to be decidable (Presburger [5] and Hilbert and Bernays [4] ). Nl(r,f, S ), N1 (C-,, I ) and Nl(_ ) are even weaker being equivalent to the natural numbers under successor and <. Indicative of the power of the additional generator is the fact that only finite and cofinite sets are definable in Ll(r, f, c )(Hilbert and Bernays [ 3] ) whereas all arithmetic sets (in fact 2-arithmetic) are definable in L (r,, s ). Applying the methods of Elgot and Biichi [ 3, 2], J. C. Shepherdson noted that the language Lk(r, <, L) is one in which definability corresponds

16. (7) to acceptance by finite automata, that is, to regularity. As a consequence of this correspondence it follows that the decision problem for this language has a positive solution. Since Nk(r,, L) and Nk(,, L) are isomorphic under c, we also know that Tk(i,, L4 is decidable. In addition, it is easy to verify that Lk(r,e, i, L) and Lk(r, -, L) are equivalent with respect to definability and thus T (r,k,, L) and T (r,,', L) are both decidable. k k By extending an elimination of quantifiers method which the author applied to Lk(r), J. H. Bennett (personal communication) has been able to characterize the definable relations in Lk(ri, c, L) and in particular he has shown that T. (r,, c, L) is decidable. In summary, we now know that the following structures (and all reducts) have decidable theories: (a) (Shepherdson, Elgot and Biuchi) Nk(r,I, I, L) and Nk(r,,>, L) (b) (Bennett) Nk(r,, c,L), and the following structures (and all expansions) have undecidable theories; (c) (Quine) Nk(-) (d) (Theorem 4) Nk(_ ) (e) (Corollary 2) Nk((<, > ).

17. Since every structure based on the objects listed in Section 1 is equivalent to either a reduct of (a) or (b) or an expansion of (c), (d), or (e), it follows that the decision problem for the theory of any such structure can be settled by reference to these cases.

18. ACKNOWLEDGEMENT The author gratefully acknowledges the suggestions and corrections offered by J. H. Bennett, C. C. Elgot and E. G. Wagner. The author is especially grateful to J. B. Wright who has provided so much encouragement through many enlightening and stimulating discussions. This work was supported in part by the following government agencies through contracts and grants administered by the University of Michigan; Office of Naval Research contract Nonr 1224(21); National Science Foundation grant G-22258; U. S. Army Research Office (Durham) grant DA-ARO(D)-31-121-G433; and through U. S. Air Force (Rome Air Development Center) contract AF 30(602)-3340 administered by the IBM Watson Research Center.

19. BIBLIOGRAPHY [1] Asser, G. "Rekursive Wortfunktionen", Fund. Math. 6 (1960)258-278. 2] Biuchi, J. R. "Weak second-order arithmetic and finite automata", Z. Math. Logic. Grundlagen Math. 6 (1960)66-92. [3] Elgot, C. C. "Decision problems of finite automata design and related arithmetics" Doctoral dissertation, The University of Michigan, Ann Arbor, Michigan, 1959. [4] Hilbert, D. and P. Bernays Grundlagen der Mathematik, Berlin, 1939. 5] Presburger, M. "Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritte", Comptes Rendus du I Congress des Mathematiciens des Pays Slavs ( arszawa 1929), pp. 29-101 and 395. [6] Quine, W. V. "Concatenation as a basis of arithmetic", J. Symb. Logic, 11 (1946) 105-114. [7] Tarski, A. "Der Wahreitsbegriff in den formalisierten Sprachen" Studia Philosophica 1 (1930) 361-404. [8] Thatcher, J. W. "Decision problems and definability for generalized arithmetic", Doctoral dissertation, The University of Michigan, Ann Arbor, Michigan, 1964.

20. FOOTNOTES (1) This paper is part of a Ph. D thesis submitted to the Program in Communication Sciences at the University of Michigan and was presented to the American Mathematical Society, NAMS 11, Abstract 64T-359 (1964) 582. (2) Interpreting the set N as the set of k-adic notations for the natural numbers (-... is the notation for So.k ) Asser [ 1] has shown that the k-primitive recursive functions correspond to the (l-)primitive recursive functions and thus, under this interpretation, the k-arithmetic relations are simply notational variants of the arithmetic relations. (3) The author is grateful to J. R. Buichi for pointing out that there is a concise history of this method of converting recursive definitions into explicit ones to be found in Hilbert and Bernays[ 4] (4) J. R. Buchi obtained a universal relation for finite monadic functions using similar techniques (personal communication). This led to hit statement in [ 2] of the undecidability of Tk(o, 4?).(See Corollary 1). (5) We will give the definitions here and below for the case k= 2. For undecidability results this is actually sufficient; for definability it should be clear how to extend the definitions to for arbitrary k > 2. In (3), for example, lylc z is replaced by the disjunction of cr 1ya 2 z for -cr o, 2 2. (6) See footnote 5. (7) In a letter to C. C. Elgot (1959) Shepherdson described the equal length theory and the theorem stated here.

DISTRIBUTION LIST (One copy unless otherwise noted) Technical Library Naval Electronics Laboratory Director Defense Res. & Eng. San Diego 52, California Room 3C-128, The Pentagon Attn: Technical Library Washington, D.C. 20301 Dr. Daniel Alpert, Director Defense Documentation Center 20 Coordinated Science Laboratory Cameron Station University of Illinois Alexandria, Virginia 22314 Urbana, Illinois Chief of Naval Research 2 Air Force Cambridge Research Labs Department of the Navy Laurence C. Hanscom Field Washington 25, D.C. Bedford, Massachusetts Attn: Code 437, Information Attn: Research Library, CRMXL R Systems Branch U. S. Naval Weapons Laboratory Director, Naval Research Laboratory 6 Dahlgren, Virginia 22448 Technical Information Officer Attn: G. H. Gleissner, Code K4 Washington 25, D.C. Asst. Dir. for Computation Attention: Code 2000 National Bureau of Standards Commanding Officer 10 Data Processing Systems Division Office of Naval Research Room 239, Building 10 Navy 100, Fleet Post Office Box 39 Washington 25, D.C. New York, New York 09599 Attn: A. K. Smilow Commanding Officer George C. Francis ONR Branch Office Computing Laboratory, BRL 207 West 24th Street Aberdeen Proving Ground Maryland New York 11, New York Office of Naval Research Office of Naval Research Branch Branch Office Chicago Office 230 N. Michigan Avenue 495 Summer Street Chicago, Illinois 60601 Boston, Massachusetts 02110 Commanding Officer Naval Ordnance Laboratory ONR Branch Office White Oaks, Silver Spring 19 1030 E. Green Street Maryland Pasadena, California Attn: Technical Library Commanding Officer David Taylor Model Basin ONR Branch Office Washington,D.C. 20007 1000 Geary Street Attnt Code 042, Technical Library San Francisco 9, California

DISTRIBUTION LIST (Concluded) The University of Michigan Lincoln Laboratory Department of Philosophy Massachusetts Institute of Technology Attn: Professor A. W. Burks Lexington 73, Massachusetts Attn: Library National Physical Laboratory Teddington, Middlesex, England Office of Naval Research Attn: Dr. A. M. Uttley, Supt. Washington 25, D.C. Autonomies Division Attn: Code 432 Commanding Officer Kenneth Krohn Harry Diamond Laboratories 6001 Dunham Springs Road Washington, D.C. 20438 Nashville, Tennessee Attn: Library Mr. Laurence J. Fogel Commanding Officer and Director General Dynamics/Astronautics U. S. Naval Training Device Center Division of General Dynamics Corp. Port Washington San Diego, California Long Island, New York Attn: Technical Library Department of the Army Office of the Chief of Research and Development Pentagon, Room 3D442 Washington 25, D.C. Attn: Mr. L. H. Geiger National Security Agency Fort George G. Meade, Maryland Attn: Librarian, C-352

UNIVERSITY OF MICHIGAN II11 11111 1111111111111 3 9015 03526 7320