## Linear types, anyone?

The following is from von Neumann's early account of self-reproducing automata ("Theory and Organization of Complicated Automata", 1949):

The general constructive automaton A produces only X when a complete description of X is furnished it, and on any reasonable view of what constitutes complexity, this description of X is as complex as X itself. The general copying automaton B produces two copies of \phi(X) [\phi(X) is the chain of â€œrigid elementsâ€ which represents X], but the juxtaposition of two copies of the same thing is in no sense of higher order than the thing itselfâ€¦ Now we can do the following thing. We can add a certain amount of control equipment C to the automaton A + B. The automaton C dominates both A and B, actuating them alternately according to the following pattern. The control C will first cause B to make two copies of \phi(X). The control C will next cause A to construct X at the price of destroying one copy of \phi(X). Finally, the control C will tie X and the remaining copy of \phi(X) together and cut them loose from the complex (A + B + C). At the end the entity X + \phi(X) has been produced. Now choose the aggregate (A + B + C) for X. The automaton (A + B + C) + \phi(A + B +C) will produce (A + B + C) + \phi(A + B +C). Hence auto-reproduction has taken place.

Arthur Burks who brought von Neumann's lectures to print goes on to explain that the final result is two automata (A + B + C) and (A + B + C) + \phi(A + B +C), and that if B were to copy the description thrice, the process would start with one copy of (A + B + C) + \phi(A + B + C) and terminate with two copies of this automaton.

von Neumann himself is quick to note that the procedure he outlines is not circular: "It is true that I argued with a variable X first, describing what C is supposed to do, and then put something which involved C for X. But I defined A and B exactly, before I even mentioned this particular X, and I defined C in terms which apply to any X."

Can you formalize von Neumann's construction so that the two arguments that follow will be derivable (provable) from the description of the construction?

## Comment viewing options

### Sorry, the LICS deadline is

Sorry, the LICS deadline is coming up, and keeping me busy...

### Reading the above, I just do

Reading the above, I just do not understand it :-) What is phi(x)? And what are rigid elements? Do you know already the answer (to a question I don't get)? Or is this an open problem? Do I need to read the book you cite in order to understand it?

### phi(x) is a notation here

phi(x) is a notation here introduced. There is no need to understand what rigid elements are. This not a riddle, the only challenge is to formalize the argument that I quoted. (Of course, if you want to know more about von Neumann's work on self-reproducing automata, you should read up on it, but this is immaterial for what I posted about.)

### Well, I don't get it. I have

Well, I don't get it. I have often made the experience that you first have to understand the whole context, then you get the argument, and then you see what is not so important about the context. THEN you formalize, which most often is pretty easy.

### Suggestion

Let's consider "\phi(X)" as "an automaton that describes X", and "+" as an associative and non-commutative operation that plugs automata together "where they fit" (or where they are intended to be plugged). The control automaton C consits of three parts C1, C2, and C3, where C1 calls B, C2 calls A and C3 ties together A's and B's output and cuts them loose from (A+B+C). That is, (A+B+C) is an abbreviation for (C3+A+C2+B+C1).

The production processes can then be given by rewriting rules:
(A) A+\phi(X) -> X+A
(B) B+\phi(X) -> \phi(X)+\phi(X)+B
(C1) (C3+A+C2+B+C1)+\phi(X) -> C3+A+C2+B+\phi(X)+C1
(C2) A+C2+\phi(X)+\phi(X) -> \phi(X)+A+\phi(X)+C2
(C3) C3+\phi(X)+X+A+C2+B+C1 -> (C3+A+C2+B+C1),X+\phi(X)

The automaton (C3+A+C2+B+C1)+\phi(X) results in (C3+A+C2+B+C1),X+\phi(X) by the obvious rule sequence (C1)-(B)-(C2)-(A)-(C3). If we substitute (C3+A+C2+B+C1) for X we get:

(C3+A+C2+B+C1)+phi(C3+A+C2+B+C1) -> (C3+A+C2+B+C1),(C3+A+C2+B+C1)+\phi(C3+A+C2+B+C1).

This is what the first argument states.

For the second argument we change rule (B) and therfore have to adapt the rules for C, too:

(B') B+\phi(X) -> \phi(X)+\phi(X)+\phi(X)+B
(C2') A+C2+\phi(X)+\phi(X)+\phi(X) -> \phi(X)+\phi(X)+A+\phi(X)+C2
(C3') C3+\phi(X)+\phi(X)+X+A+C2+B+C1 -> (C3+A+C2+B+C1)+\phi(X),X+\phi(X)

Now we get (C3+A+C2+B+C1)+phi(C3+A+C2+B+C1) ->
(C3+A+C2+B+C1)+phi(C3+A+C2+B+C1),(C3+A+C2+B+C1)+phi(C3+A+C2+B+C1).

### Just some quick notes. I

Just some quick notes. I don't have the time now (sick baby).

phi(X) is a a description, not an automaton. That's part of the idea. Not crucial perhaps for the exercise though.

Using rewrite rules is a nice idea.