На самом деле, если быть достаточно хитрым, то все рассуждения о шагах вычисления можно упрятать в теорему о нормальной форме. Оба этих факта легко доказываются с использованием того, что рекурсивно-перечислимые множества есть проекции рекурсивных.
В совсем простых случаях можно. Но лучше этого не делать.
Нет, серьёзно, вот простое утверждение: если
рекурсивно перечислимы и
, то
. Для доказательства нужно показать
, остальное совсем очевидно. Сводим так: для каждого
сначала проверяем
, если
, то сразу говорим, что
. Если же
, то параллельно перечисляем оба множества
и смотрим, в какое из них попадёт
...
Совсем простое рассуждение! И как его теперь "без времени" оформить?
А в теории вычислимости много таких! Вся классика, которая начинается с 1950-ых годов, в основном такая.
Или даже вот совсем простая теорема, из стандартного университетского курса. Доказать, что множество
не рекурсивно. Я один раз попробовал извратиться и доказать её студентам без каких-либо явных описаний алгоритма, чисто с помощью формального манипулирования функциями. Доказал, конечно, но тут же пожалел, что сделал это! Глупость полнейшая, почёсывание левого уха из-под правого колена!!!
В теории вычислимости лучше наоборот почаще расписывать шаги, заставляя события происходить с ходом времени в определённом порядке. Разные "дескриптивные" определения если и работают, то лишь затуманивают суть происходящего...
P. S. У меня шеф уже который год читает в курсе матлогики теоремы о неполноте без всяких машин и алгоритмов. Чисто через
-определимость. И каждый год студенты с круглыми шарами спрашивают: что, почему, как, откуда?
Приходится каждый раз вздыхать и начинать объяснять: ну, давайте рассмотрим машину Тьюринга, которая работает по шагам и, перебирая все возможные формальные доказательства, перечисляет следствия данной разрешимой теории...
P. P. S. Помню, в студенческие годы был у нас один товарисч, который конструктивных рассуждений вообще не признавал. Если ему показывали доказательство, в котором объект с нужными свойствами явно строился, он начинал психовать и кричал: ерунда, это не настоящая математика, не верю я в ваши построения, покажите мне, как утверждение о несуществовании объекта приводит к противоречию!