Подумалось, что эти, казалось бы никак не связанные вещи, имеют нечто общее. В проблеме останова, есть некоторое ограничение концептуального плана. Мы можем немного перефразировать ее и выдать нечто вроде: «Если бы был всеведующий проблема бы не существовала».
В LC существует некая подковерная возня. Все мы знаем, что в реализации лексического скопа есть волшебный лукап, который знает, что где искать и куда подставлять. В реализации оптимизатора тоже есть всеведующий, который сначала делает подстановки. Во всех случаях происходят подковерные волшебные штучки, которые «просто работают». Юзеру его не показывают. Это и есть всеведающий.
Если бы мы спросили, а как происходит подстановка, нам бы могли ответить: это вопрос реализации, не забивай голову. В разрешении проблемы останова, мы тоже могли бы реализовать анализатор, который тупо, по синтаксису, может определить, завершиться ли алгоритм. Разумеется, это невозможно определить для рантайма, когда неизвестно что поступит, в общем случае, но в ограниченных семантиках можно это сделать. А можно на этапе компиляции тупо запускать прогу, и ждать. Если она не завершиться в течении, скажем, получаса, падать с ошибкой. У нас появляется всеведающий. Только к реальной проблеме останова это не имеет отношения. Точно также, LC не имеет отношения к реальным вычислениям, это сахар, по большому счету, а не концепция. Человеку в здравом рассудке, понять ее невозможно. Мы могли бы абстрагироваться не только от подстановок, но и от самих вычислений. Нажми на кнопку — получи результат. Это тоже «исчисление» в этом смысле. Такими исчислениями активно пользуются секретарши и бухгалтера, давя клопов на своей клаве. 1С-UI-calculus. Звучит неплохо.
