Cтраница 1
Работа SECD-машины была определена в полуформальном виде в терминах состояний и функции переходов, которая определяет одношаговые переходы из одного состояния в другое. С / - машина обеспечивает корректную реализацию Л, необходимо математически определить операционную семантику и доказать, что она эквивалентна общепринятой ( денотационной) семантике Л, определенной в терминах Р - и б-ре-дукций. Сначала мы дадим формальное определение составных частей SfCD-машины, а затем определим для нее операционную функцию вычисления Eval. При применении к выражению А эта функция возвращает значение, вычисленное для этого выражения SECD-машиной. Доказательство является простым, но имеет множество деталей, и доказательства двух лемм отнесены в конец этого раздела. [1]
Доказательство корректности SECD-машины, данное в разд. Предложите, как можно адаптировать это доказательство, чтобы показать, что реализация, специфицированная для редукции нормального порядка с вызовами по имени, также корректна. [2]
Функцию переходов для энергичной SECD-машины, определенную в разд. [3]
И наш интерпретатор, и SECD-машина являются основанными на контексте, так что фактические параметры функции запоминаются в отдельном контексте, а не подставляются физически в тело функции. Альтернативой этому является использование двумерного графового представления выражений. Вычислитель, редуцирующий выражения в этой форме к их конечным значениям, называется редуктором графов а общая модель вычислений - редукцией графов. [4]
Существуют энергичный и ленивый варианты SECD-машины. Энергичный вариант является наиболее естественным. [5]
Аналогия между МФП - и SECD-машинами, изложенная в гл. МФП соответствуют управляющему стеку в SECD-машине. Однако в нашем случае программа хранится в виде компилированного кода, а не в виде лямбда-выражений. Стек вызовов служит для запоминания состояния вычислений в точке вызова функции и восстановления этого состояния по завершении работы вызванной функции. В этом плане он играет роль, аналогичную работе дампа в SECD-машине. Стек вычислений в МФП в точности соответствует совокупности стека и контекста в SECD-машине. В ней параметры функций сохраняют свои имена, связи между именами и величинами хранятся в контексте. В МФП, однако, все ссылки на параметры функций при компиляции переходят к номера элементов стека, и поэтому возникает необходимость в списке связей имя - величина. И наконец, куча в МФП является лишь местом хранения структур и замыканий. [6]
Ниже мы рассмотрим два метода обработки рекурсии в SECD-машине аппликативного порядка: метод использования У-комбинатора и метод помеченных выражений. Заманчиво использовать У обычным образом для удаления явной рекурсии из выражения, включающего рекурсивную функцию. После этого полученное Х - выражение просто передается для обработки в SECD-машину, которая в конце концов специально построена так, чтобы иметь возможность обрабатывать такие выражения. [7]
На основе приведенной спецификации можно легко написать базовую реализацию энергичной SECD-машины на языке Норе, определив тип данных для представления состояния машины и функцию, реализующую переходы между состояниями. Программа, показанная на рис. 10.1, обеспечивает спецификацию, которая является не только краткий и ясной, но и выполнимой. Заметим, что в этой программе идентификаторы для простоты представляются одним символом. [8]
Модифицируйте Hope-программу, показанную на рис. 10.1, которая реализует энергичную SECD-машину, так, чтобы включить примитивный условный оператор cond и помеченные выражения, определенные в разд. [9]
Подобно другим вычислительным моделям, рассмотренным в этой книге, таким как SECD-машина и редукция графов, функциональная потоковая модель дает представление р-редук-ции и б-правил для поддерживаемых примитивных функций. Эти примитивные функции включают условные выражения, которые, хотя и выражаются с помощью вершин-переключателей и вершин слияния, могли бы точно так же рассматриваться в терминах только двух дополнительных примитивных функций и их дельта-правил. Более того, редекс такого применения можно рассматривать как перезаписываемый в том смысле, что входящие дуги его вершины применения перенаправляются в тело функции. [10]
МОП является примером энергичной абстрактной машины и может рассматриваться как оптимизированная версия SECD-машины. [11]
Общепринятым методом реализации функциональных языков типа LISP является использование четырехстековой машины, за которой закрепилось наименование SECD-машины. [12]
В дальнейшем мы покажем, как эта система может быть обобщена для обеспечения ленивого вычисления Энергичную и ленивую версии SECD-машины часто называют машиной, управляемой данными, и машиной, управляемой запросами, соответственно. [13]
Чтобы сравнить эти функции вычисления, необходимо иметь возможность соотнести значения выражений, выдаваемые семантической функцией eval, с последовательностями переходов SECD-машины из одного состояния в другое. Мы считаем значением замкнутого терма его СЗНФ ( другой, единственный терм) вместе с целым числом, соответствующим числу редукций, необходимых для приведения этого терма к СЗНФ. [14]
Также введем индуктивно понятия и-замыкания и у-контекста, определяющие по существу замыкания и контексты, которые мы использовали в нашем неформальном описании энергичной SECD-машины. [15]