Абстрактные машины и категориальная комбинаторная логика
Рассмотрим особенности моделирования абстрактных машин средствами формальной системы категориальной комбинаторной логики.
Абстрактной машиной (abstract machine) в рамках данного курса будем называть математическую формализацию, которая моделирует правила выполнения программы (или, иначе, алгоритмы) для реальной вычислительной машины (компьютера).
В настоящее время при практической реализации различных классов языков программирования, в частности функциональных и объектно-ориентированных языков, широко используются аналоги абстрактных машин в форме так называемых виртуальных машин (virtual machine).
Виртуальные машины представляют собой средство создания промежуточного (следующего за текстом программы на высокоуровневом языке программирования) кода (именуемого в различных реализациях Java-кодом, MSIL-кодом и т.д.), который затем транслируется в машинный код. Заметим, что последний пример промежуточного кода, а именно, MSIL (Microsoft Intermediate Language), представляет собой ни что иное, как код виртуальной машины, реализованной корпорацией Microsoft для технологической платформы .NET.
Отметим также то обстоятельство, что абстрактные машины позволяют адекватно моделировать различные подходы и стратегии вычислений, включая ранее рассмотренные рекурсивные вычисления, а также вычисления по необходимости (иначе известные как "ленивые"), которые будут рассматриваться в ходе курса.
Уточнив понятия об абстрактных и виртуальных машинах, перейдем к исследованию особенностей различных классов рассматриваемых формализаций, проиллюстрировав выделенные классы необходимыми примерами из математической теории и практики программирования.
Прежде всего, следует отметить то обстоятельство, что практически все без исключения абстрактные модели вычислительных машин оперируют понятием состояния, изменения которого и отражают ход выполнения программы.
При этом следует, во-первых, выделить ранние, "наивные" формализации на состояниях, которые не были практически поддержаны ни языками программирования, ни собственно компьютерами.
К ранним абстрактным машинам можно отнести известные из истории математики машины Тьюринга и Поста. Первая абстрактная машина характеризовалась бесконечной лентой для хранения "инструкций", а также считывающей и записывающей головкой, передвигающейся по ней; вторая машина действовала подобно первой.
Несмотря на объективные трудности практической реализации, ранние абстрактные машины, безусловно, были весьма значимыми для развития computer science, т.к. предвосхитили появление и обозначили ряд этапов развития реальных компьютеров и языков программирования для них.
Кроме того, следует отдельно рассмотреть более поздние, зрелые формализации машин, основанные на состояниях. К ним в первую очередь относятся упомянутая ранее SECD-машина П. Лендина, а также категориальная абстрактная машина.
Как уже отмечалось, в 60-х годах, уже в эпоху высокоуровневых языков программирования, П. Лендином (Peter J. Landin) была разработана так называемая SECD-машина, а именно, математическая формализация для вычисления ламбда-выражений.
При этом SECD-машина была предназначена для редукции ламбда-выражений и использовала механизм передачи параметров при вызове функции по значению (call-by-value), в отличие от других типов передачи параметра (например, по имени или call-by-name).
Свое название SECD-машина получила от аббревиатур имен своих основных четырех элементов, а именно:
Stack - стек, т.е. последовательность атомарных ламбда-выражений (переменных и констант), а также ламбда-абстракций;
Environment - среда, т.е. хранилище значений, которые связываются с переменными в ходе вычислений;- Control - управление, т.е. последовательность "инструкций", управляющих работой SECD-машины;
Dump - дамп, т.е. хранилище состояния SECD-машины (обычно пуст либо содержит прежнее состояние).
Именно перечисленная четверка элементов в полной мере характеризует состояние SECD-машины в произвольный момент вычислений.
Заметим, что именно SECD-машина стала прообразом для более поздних формализаций, на которых реализованы ML-машины, в частности категориальная абстрактная машина (КАМ).
