На самом деле, если быть достаточно хитрым, то все рассуждения о шагах вычисления можно упрятать в теорему о нормальной форме. Оба этих факта легко доказываются с использованием того, что рекурсивно-перечислимые множества есть проекции рекурсивных.
В совсем простых случаях можно. Но лучше этого не делать.
Нет, серьёзно, вот простое утверждение: если
![$A_0, A_1$ $A_0, A_1$](https://dxdy-04.korotkov.co.uk/f/f/9/c/f9c617d49d7104e4a34934377140480a82.png)
рекурсивно перечислимы и
![$A_0 \cap A_1 = \varnothing$ $A_0 \cap A_1 = \varnothing$](https://dxdy-02.korotkov.co.uk/f/d/4/5/d45b73a9ac27011cf2817ab19130024282.png)
, то
![$A_0 \cup A_1 \equiv_T A_0 \oplus A_1$ $A_0 \cup A_1 \equiv_T A_0 \oplus A_1$](https://dxdy-03.korotkov.co.uk/f/6/c/f/6cf56f1836efc6058aa66b119c54678482.png)
. Для доказательства нужно показать
![$A_i \leqslant_T A_0 \cup A_1$ $A_i \leqslant_T A_0 \cup A_1$](https://dxdy-03.korotkov.co.uk/f/6/0/c/60cf2e9a0ed822ec8f71488ea37e63b882.png)
, остальное совсем очевидно. Сводим так: для каждого
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
сначала проверяем
![$x \in A_0 \cup A_1$ $x \in A_0 \cup A_1$](https://dxdy-02.korotkov.co.uk/f/d/8/f/d8fff3e2f6dd8b1603921fe130083fdf82.png)
, если
![$x \not\in A_0 \cup A_1$ $x \not\in A_0 \cup A_1$](https://dxdy-03.korotkov.co.uk/f/e/4/a/e4a0a3d19e666cc91e9a37115bb3943f82.png)
, то сразу говорим, что
![$x \not\in A_i$ $x \not\in A_i$](https://dxdy-03.korotkov.co.uk/f/e/4/5/e45bd398863f9757c48af8d45541fad182.png)
. Если же
![$x \in A_0 \cup A_1$ $x \in A_0 \cup A_1$](https://dxdy-02.korotkov.co.uk/f/d/8/f/d8fff3e2f6dd8b1603921fe130083fdf82.png)
, то параллельно перечисляем оба множества
![$A_0, A_1$ $A_0, A_1$](https://dxdy-04.korotkov.co.uk/f/f/9/c/f9c617d49d7104e4a34934377140480a82.png)
и смотрим, в какое из них попадёт
![$x$ $x$](https://dxdy-04.korotkov.co.uk/f/3/3/2/332cc365a4987aacce0ead01b8bdcc0b82.png)
...
Совсем простое рассуждение! И как его теперь "без времени" оформить?
![Smile :-)](./images/smilies/icon_smile.gif)
А в теории вычислимости много таких! Вся классика, которая начинается с 1950-ых годов, в основном такая.
Или даже вот совсем простая теорема, из стандартного университетского курса. Доказать, что множество
![$$
K = \{ x : \text{машина с номером }x \text{ останавливается, получив на вход } x \}
$$ $$
K = \{ x : \text{машина с номером }x \text{ останавливается, получив на вход } x \}
$$](https://dxdy-01.korotkov.co.uk/f/0/a/2/0a29da1d162dcc1b932aba5f4f38424d82.png)
не рекурсивно. Я один раз попробовал извратиться и доказать её студентам без каких-либо явных описаний алгоритма, чисто с помощью формального манипулирования функциями. Доказал, конечно, но тут же пожалел, что сделал это! Глупость полнейшая, почёсывание левого уха из-под правого колена!!!
В теории вычислимости лучше наоборот почаще расписывать шаги, заставляя события происходить с ходом времени в определённом порядке. Разные "дескриптивные" определения если и работают, то лишь затуманивают суть происходящего...
P. S. У меня шеф уже который год читает в курсе матлогики теоремы о неполноте без всяких машин и алгоритмов. Чисто через
![$\Sigma$ $\Sigma$](https://dxdy-01.korotkov.co.uk/f/8/1/3/813cd865c037c89fcdc609b25c465a0582.png)
-определимость. И каждый год студенты с круглыми шарами спрашивают: что, почему, как, откуда?
![:shock: :shock:](./images/smilies/icon_eek.gif)
Приходится каждый раз вздыхать и начинать объяснять: ну, давайте рассмотрим машину Тьюринга, которая работает по шагам и, перебирая все возможные формальные доказательства, перечисляет следствия данной разрешимой теории...
P. P. S. Помню, в студенческие годы был у нас один товарисч, который конструктивных рассуждений вообще не признавал. Если ему показывали доказательство, в котором объект с нужными свойствами явно строился, он начинал психовать и кричал: ерунда, это не настоящая математика, не верю я в ваши построения, покажите мне, как утверждение о несуществовании объекта приводит к противоречию!
![Very Happy :D](./images/smilies/icon_biggrin.gif)