Turing A-machine and Hoar pit-stop coffee machine

    Anyone who relies on practice without knowing the theory is like a helmsman entering a ship without a helm and compass — he does not know where he is sailing.
    Leonardo da Vinci
    In the Holy Linguistic Wars, the final argument is often cited - since languages ​​are Turing-complete, so far as they are equivalent. Under cat, an attempt to clarify this thesis for those who have already mastered Python and now plans to study Erlang or Haskell by specification. The material is panoramic, not methodical with pictures .

    Alan Turing built his a-car in 1936.
    "... the endless tape is divided into platforms marked with symbols. At each moment exactly one symbol is available to the machine. The state of the machine depends on the available symbol and the machine is free to change this symbol. Inaccessible symbols on the tape do not affect the behavior of the machine. However, the tape can be moved back and forth , it’s an elementary operation for a car. Thus, any symbol has a chance ... "
    1948 essay, Intelligent Machinery Turing.
    image
    We can say that a state machine is hidden inside the machine, so it will be more understandable to practitioners.
    The designer from which you can assemble any a-machine is considered Turing complete. Two machines are considered Turing equivalent if one can assemble the other from the parts.
    Turing prototyped a universal unit capable of replacing an arbitrary a-machine. The Universal Turing Machine achieves this by simply reading from the tape along with the data a description of some kind of private a-machine. Any two UMTs are obviously equivalent. And in 1946, von Neumann built this prototype. It is worth noting here that UMT is a logarithmically slower private a-machine on complex calculations.
    Turing with Church postulated: any function of natural numbers is computable by a person equipped with paper and a pencil if and only if the Universal Turing Machine handles it.
    From the foregoing it follows that nothing can be steeper than the Universal Turing Machine. Whatever the system, the UMT will succeed anyway (if the Church-Turing thesis is correct). Nevertheless, Turing was forced to admit that his car was without brakes. Godel's incompleteness theorem raises the problem of shutdown. You can not be sure that UMT will always reach the Stop state.
    Calculation in UMT is a sequence of steps along the tape and state transitions.
    For example, the integer module abs (int) in assembler can be taken like this
    cdq                      ; Первая инструкция копирует бит знака из регистра eax в edx
                             ;  if eax>=0 then edx:=0 else edx:=0xFFFFFFFF
    xor eax, edx             ; Если операнд XOR равен нулю, то результат равен второму операнду A ⊕ 0 = A
                             ; XOR c -1 зквивалентно побитному NOT       A ⊕ –1 = ¬A
                             ; if eax>=0 then eax:=eax xor 0=eax else eax:=eax xor 0xFFFFFFFF=not eax
    sub eax, edx             ; Последняя инструкция вычитает edx из eax 
                             ; Если eax положительно, edx=0 то ничего и не меняется
                             ; Но если eax отрицательно инструкция добавляет 1 фактически вычисляя -eax 
                             ; ¬A + 1 = –A
                             ; if eax>=0 then eax:=eax xor 0 - 0=eax else eax:=(eax xor -1) - (-1=not eax + 1= -eax
    Imperative programming languages ​​having if and goto implement the Universal Turing Machine.

    In the same 1936, Alonzo Church introduced the world of lambda calculus described by three simple rules about its terms. (In general, Church’s research dates back to 1928-1930, and Turing was a graduate student at Church, and yet his work was published at the same time.)
    • The variables x, y, z ... are terms. (Alphabet)
    • If M and N are terms, then (MN ) –Term. (Application)
    • If x is a variable and M is a term, then (λx.M) is a term. (Abstraction)
    Well, it is also specified that everything else is not a lambda term.
    The abstraction here is a way to describe a function. Application - the ability to apply it to arguments. A lambda expression can be perfectly represented by a tree.
    image
    To revive the meaning of these non-contradictory rules, three types of reduction (simplification) of lambda expressions are introduced.
    • α-conversion: rename the argument (alpha); λx.x → λy.y
    • β-reduction: applying a function to arguments (beta); ((λn.n * 2) 7) → 7 * 2
    • η-conversion: equivalent substitution (eta). λx. (fx) → f
    Note that it is possible to reduce in an arbitrary order and obtain an equivalent result.
    image
    When an expression cannot be reduced, it is considered calculated and in normal form. Computing is a sequence of simplifications.
    In 1958, John McCarthy implements lambda calculus in the Lisp language that can be executed on von Neumann's machine. Lisp is an implementation of lambda calculus and not a Turing machine (it does not have goto), but according to Church-Turing thesis, it is such a machine.A beginner to practice Lisp should first of all realize that the sequence of actions of a program in a functional language is generally unknown to us and is not important, just as the sequence of simplifications applied by the calculator to the lambda expression is not important. The representation of code and data in Lisp is the same - this is a list defined by three operations
    (defun cons (a b)
      (lambda (f) (funcall f a b)))
    (defun car (c)
      (funcall c (lambda (a b) a)))
    (defun cdr (c)
      (funcall c (lambda (a b) b)))

    and the stack can be described like this
    (let (stack)
              (defun push (x)
                (setq stack (cons x stack)))
              (defun pop ()
                ;; note the usefulness of VALUES.
                (values (car stack)
                        (setq stack (cdr stack)))))

    Yes, the lambda calculus of Turing is equivalent, but just not typed. Introducing a restriction on the types of terms, although we generalize the formalism, we reduce the generality of the concept of terms. Typed lambda calculus is generally not Turing complete.

    To achieve completeness, additional abstractions are needed. And in 1942-1945, Eilenberg and MacLane created such an abstraction - the theory of categories. Church calls category theory
    the highest mathematical formalism of all that he had seen

    Category C must contain the
    class ob (X) of objects of the category
    class H (A, B) of morphisms (or arrows f: a-> b)
    two-step operation ∘, composition of morphisms  f∘g, f∊H (B, C) g∊ H (A, B) → f∘g∊H (A, C)
    • associative: h ∘ (g ∘ f) = (h ∘ g) ∘ f
    • and identified id: x → x
      id ∘ f = f = f ∘ id.

    image
    Functors are category mappings that preserve the structure.
    image
    A natural transformation is the ratio of two functors.
    image
    In the early 1970s, Girard and Reynolds independently formulated System-F as a polymorphic lambda calculus (by and large, they allowed the quantifier of universality in lambda notations). Hindley and Milner developed an algorithm-W of complexity O (1) to derive types, that is, linear in size of the expression (for this it was necessary to make the notation prefix). Milner embeds the system in the ML language and by 1990 it appears in Haskell. Thus, in Haskell, you have at your disposal the Hask category containing objects with all data types and morphisms with all possible functions.
    Haskell's concept reflects the idea of ​​mathematician Haskell Curry, who wrote that
    proof is a program, and a formula being proved is a type of program
    Computing in such a formalism is, say, the conclusion of the declared category, and the result of the calculation is regarded as a side effect of the proof.
    For example, for an exponent expanded in a power series,
    image
    we can say
    integral fs = 0 : zipWith (/) fs [1..]      -- тип (Fractional a, Enum a) => [a] -> [a]
    expx = 1 + (integral expx)                  -- код компилируется

    Algorithm-W and an elegant mathematical trick, the monad, as a generalization of structural recursion made it possible to implement the Hask category on von Neumann machines. Haskell is Turing-complete, if only because its type-checker implements W-algorithm. But it should be understood that the language was not designed as a Turing machine, in the theory of categories there is simply no abstraction of state on which finite state machines are built.
    In practice, it is useful for a Haskell student to get used to talking about the types of variables and the morphisms between them, rather than the values ​​(which are immutable).

    Von Neumann's machine is a sequential computer, but the machines have learned to connect in networks. In 1985, Charles Hoare publishes a document, “Communicating Sequential Processes,” in which he develops a new formalism. The preface is written by Dijkstra.
    An object is described in the alphabet of events in which it is involved. The totality of such events form the process.
    Take the queuing machine.
    image
    Let x be an event, and P a process, then:
    (x → P )
    (pronounced “x then P”) describes an object that first fires an event x, and then behaves like P.
    Торгомат = μX • денежка → (шоколадка → X | ириска → X)
    where X is a local variable that can be changed.
    The sequence of events passed by the object makes up the process trace.
    The process environment is also considered a sequential process.
    Two processes can have the same events in the alphabet
    Сладкоежка = μX •(шоколадка → X | ириска → X
    | денежка → шоколадка → X )
    Sweet tooth is not averse to getting a toffee for free, but there are no miracles
    (Торгомат || Сладкоежка ) = μ X • (денежка → шоколадка → X)

    In such a notation, Hoar constructs an algebra capable of effectively solving (at least diagnosing) the “Problem of the dining philosophers” and derives the laws of this algebra.
    L1       P||Q=Q||P
    L2       P ||(Q ||R)=(P ||Q)||R
    L3       (c →P)||(c →Q)=(c →(P ||Q))
     ...

    Formalism is implemented in Erlang, Golang, Ada Haskell libraries and other languages.
    Are two Turing machines planted on the same tape a Turing machine?
    image
    Yes, Hoar answers. It declares its algebra in terms of lambda calculus and implements it in Lisp. Now an agreement has been made that interacting sequential processes can always be trivially represented by one von Neumann running on a machine. The inverse problem, the allocation in the process of two interacting ones is by no means trivial.
    This is what a competitive sieve for the first ten primes in Go might look like
    package main
    // Отсылает 2, 3, 4, ... в канал 'ch'.
    func Generate(ch chan<- int) {
    	for i := 2; ; i++ {
    		ch <- i // Рандеву, посылка возможна только если ее готовы получить.
    	}
    }
    // Копирует из канала in в канал out,
    // исключая делимые на 'prime'.
    func Filter(in <-chan int, out chan<- int, prime int) {
    	for {
    		i := <-in // Получает из 'in'.
    		if i%prime != 0 {
    			out <- i // Посылает 'i' в 'out'.
    		}
    	}
    }
    func main() {
    	ch := make(chan int) // Конструируем канал ch.
    	go Generate(ch)      // Запускаем Generate параллельным процессом.
    	for i := 0; i < 10; i++ {
    		prime := <-ch
    		print(prime, "\n")
    		ch1 := make(chan int)
    		go Filter(ch, ch1, prime) //Запускаем Filter параллельным процессом.
    		ch = ch1
    	}
    }

    From a practical point of view, programming competitively in Erlang, Go, or just for the web, it is important to first determine the common alphabet (shared resources) of the processes. Languages ​​having a toolkit for parallel programming provoke this toolkit to use. It should be remembered that any algorithm can be implemented sequentially and, as a rule, more efficiently.

    So, yes - the described formalisms are Turing equivalent. However, in imitation of Turing, to prove this with each program by reconstructing one paradigm within the framework of another seems counterproductive to me. With their charter, they don’t go to someone else’s monastery. Adopting a language professing a fundamentally different model of computation, one has to revise sustainable skills, metrics, and design patterns.

    Also popular now: