Secd-машина - Большая Энциклопедия Нефти и Газа, статья, страница 3
Спонсор - это человек, которому расстаться с деньгами проще, чем объяснить, откуда они взялись. Законы Мерфи (еще...)

Secd-машина

Cтраница 3


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

После подстановки аргумента при выполнении р-редукции редекс физически заменяется результатом этой редукции - либо атомом, либо корневой вершиной упрощенного ( редуцированного) выражения. Если вершина редекса сама является разделяемой, тогда после замены каждая ссылка на нее соответствует уже вершине в редуцированной форме, и именно поэтому операция замены обеспечивает реализацию семантики вызова по необходимости. Как и в случае преобразования задержки в дампе с присваиванием ленивой SECD-машины, замена вершины редекса является сохраняющей значение в том смысле, что значения заменяемого и заменяющего графов совпадают. Другие вершины редекса не будут затронуты операцией замены, но будут отрезаны от корневой вершины и от графа в целом. Различные типы сборщиков мусора и методы их работы описаны в гл. В примерах на рис. 11.2 и 11.3 эти потенциально мусорные вершины не показаны. На рис. 11.4, а снова показана редукция рис. 11.3, но при этом показаны все отрезанные подграфы, которые могут оказаться мусором.  [32]

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

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

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

Результатом программы в действительности является СЗНФ, а не конечное состояние. Вследствие рекурсивной природы функции Evaluate, однако, тип объекта, возвращаемого этой функцией, полностью зависит от первого из определяющих ее уравнений. Легко изменить это уравнение таким образом, чтобы функция Evaluate возвращала не СЗНФ исходного выражения промежуточного кода, а полное конечное состояние SECD-машины.  [36]

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

Наконец, доказательство ее корректности будет дано в разд. Для установления корректности реализации требуется по меньшей мере формальное доказательство того, что семантика ее модели вычислений эквивалентна семантике языка. В общем случае необходимо также доказать, что формальная спецификация реализации соответствует семантике модели, но это относительно простая задача, если интерпретатор написан на функциональном языке, который сам может отражать семантику модели Следовательно, это доказательство рассматриваться не будет) Доказательство корректности, согласно Плоткину [72], влечет за собой обеспечение формальной семантики работы SECD-машины и затем показывает ее эквивалентность семантике ( 3-редукции Оно дано для энергичной машины, но модификации, требуемые для ленивой версии, достаточно просты.  [38]

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

Принципы работы большинства традиционных компьютеров обычно описывают в виде последовательностей инструкций, которые манипулируют данными и расположены в памяти либо регистрах машины. Последовательность выполнения инструкций контролируется с помощью специального регистра счетчика команд. Говоря более абстрактно, такие архитектуры имеют модель вычислений, определенную в терминах потока управления, и мы уже встречали такую модель для функциональных языков. Например, функция переходов, используемая для описания SECD-машины в гл. Стек, Контекст, Управляющая строка, Дамп), причем управление процессом осуществляется с помощью Управляющей строки, содержимое которой определяет преобразование состояний.  [40]

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

Работа SECD-машины была определена в полуформальном виде в терминах состояний и функции переходов, которая определяет одношаговые переходы из одного состояния в другое. С / - машина обеспечивает корректную реализацию Л, необходимо математически определить операционную семантику и доказать, что она эквивалентна общепринятой ( денотационной) семантике Л, определенной в терминах Р - и б-ре-дукций. Сначала мы дадим формальное определение составных частей SfCD-машины, а затем определим для нее операционную функцию вычисления Eval. При применении к выражению А эта функция возвращает значение, вычисленное для этого выражения SECD-машиной. Доказательство является простым, но имеет множество деталей, и доказательства двух лемм отнесены в конец этого раздела.  [42]

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

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

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



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