Secd-машина

Cтраница 2

Выбор именно этих двух примеров обусловлен тем, что они представляют две крайности в области приложения функциональных языков, а именно - использование строгих языков, основанных на оптимизированной SECD-машине, и использование ленивых языков на основе оптимизированной редукции графов. Обсуждение этих вопросов содержится в разд. [16]

Мы будем использовать порядок, устанавливаемый параметром t предиката М имеет значение N за время в приведенных ниже индуктивных доказательствах лемм и теоремы, в которых последовательности редукций соотносятся с переходами SECD-машины из одного состояния в другое. Поскольку имена переменных не меняются в определении этого предиката, ясно, что если М аМ, то М имеет значение N за время t, если и только если для некоторого N a. Ясно также, что если eval ( M) существует, то это замкнутая величина. [17]

В случае вызова по необходимости, если мы имеем дамп для задержки, так что величина в вершине S будет результатом вычисления задержки, местоположение, сохраненное в дампе, при восстановлении заменяется этим результатом. Затем из дампа восстанавливается состояние SECD-машины, и примитивная функция применяется к вычисленному значению задержки. [18]

Механизм, представленный в этом разделе, вычисляет записанные в нотации де Брейна выражения, используя категорий-ные комбинаторы в качестве примитивов, ККЛ как основу для правил переписывания и явный контекст. Читатель может почувствовать здесь привкус SECD-машины. [19]

Аналогия между МФП - и SECD-машинами, изложенная в гл. МФП соответствуют управляющему стеку в SECD-машине. Однако в нашем случае программа хранится в виде компилированного кода, а не в виде лямбда-выражений. Стек вызовов служит для запоминания состояния вычислений в точке вызова функции и восстановления этого состояния по завершении работы вызванной функции. В этом плане он играет роль, аналогичную работе дампа в SECD-машине. Стек вычислений в МФП в точности соответствует совокупности стека и контекста в SECD-машине. В ней параметры функций сохраняют свои имена, связи между именами и величинами хранятся в контексте. В МФП, однако, все ссылки на параметры функций при компиляции переходят к номера элементов стека, и поэтому возникает необходимость в списке связей имя - величина. И наконец, куча в МФП является лишь местом хранения структур и замыканий. [20]

Лэндина использует для вычисления К-вы-ражений четыре стека. Ее работу очень легко описать неформально Строгое описание работы SECD-машины основано на представлении ее состояния в зависимости от содержимого ее четырех стеков и заключается в описании переходов машины из одного состояния в другое. Важность SECD-машины состоит в том, что она лежит в основе многих методов практической реализации. Ясно, однако, что без оптимизации SECD-машина является далеко не самым эффективным средством реализации функционального языка. [21]

Затем расширим способности нашей машины, научив ее обрабатывать другие примитивные конструкции, необходимые в практических функциональных языках программирования, - условные выражения и рекурсию. Однако мы увидим, что в этом случае для энергичной SECD-машины имеют место определенные трудности. [22]

Слова состояния и указатели кучи. [23]

Для определения того, какие ячейки активны, необходимо проанилизировать состояние процесса вычислений. Это состояние может быть представлено как стеком вычислений ( как в SECD-машине), так и единственным указателем на высокоуровневую ячейку графа вычислений ( как при использовании редукции графов) либо каким-нибудь иным образом. [24]

МФП является аббревиатурой термина машина функционального программирования. Абстрактная МФП-машина основана на использовании стеков и может рассматриваться как оптимизированный вариант SECD-машины. Исходная программа транслируется в FC-форму путем удаления сопоставления с образцом ( см. гл. [25]

ПГ выражения ( XY) Z эквивалентен исходному ПГ для Bf, где входящие дуги X, Y и Z присоединены к вершинам-значениям, содержащим величины X, Y и Z. Должно быть ясно, что используемые здесь замыкания являются просто обобщением замыканий, используемых в SECD-машине, поскольку они моделируют частичные применения комбинаторов, имеющих несколько аргументов, вместо карринговых функций от одного аргумента. Короче, подстановки конкретных значений вместо переменных в Bf не выполняются до тех пор, пока все значения аргументов не будут в наличии. [26]

В самом деле, необходимые расширения аналогичны тем, которые были предложены с той же целью для SECD-машины в гл. [27]

Вся совокупность вопросов получила окончательное разрешение после того, как Лэндин ( Landin 1964) формализовал программные аспекты лямбда-исчисления, специально учитывая факторы, связанные с функционалами и контекстом вычислений. Построенный Лэндином формализм основывался на четырех структурах данных в виде списков: стек ( stack), контекст environment), управление ( control) и дамп ( dump), из которых происходит и имя его формализма - SECD-машина. Для решения проблемы контекста он предложил понятие замыкания, которое с тех пор занимает важное место в программировании, особенно в управлении параллельными процессами. [28]

Строгие примитивные функции с одним аргументом не составляют проблемы, а примитивные функции с большим числом аргументов считаются обладающими свойством карринга. Частичное применение функции от п аргументов ( п 1) к m n объектам дает в результате замыкание; тело применяемой функции не вычисляется, пока все аргументы не будут в наличии Все эти механизмы присутствуют в только что описанной SECD-машине, не считая соответствующих примитивных операций, и для ленивой машины это все, что нам необходимо. Однако в энергичной реализации возникают некоторые проблемы, связанные с условными выражениями и рекурсией. Их мы сейчас и рассмотрим. [29]

Страницы: 1 2 3 4