ТЕОРИЯ

ТЕОРИЯ

Сергей Шишкин

Состояние состоит из трех компонентов: термин, стек, окружающая среда.

Терм является λ-термом с индексами де Брейна. Стек и окружение принадлежат одной и той же рекурсивной структуре данных. Точнее, окружение и стек — это списки пар <term, environment>, которые называются замыканиями

Стек — это место, где машина хранит замыкания, которые должны быть оценены в дальнейшем, тогда как среда — это связь между индексами и замыканиями в данный момент времени во время оценки. Первым элементом окружения является замыкание, связанное с индексом 0, второй элемент соответствует замыканию, связанному с индексом 1 и т. д.

Если машина должна оценить индекс, она выбирает там пару <термин, среда> замыкание, которое дает терм для оценки, и среду, в которой этот терм должен быть быть оценены.

Эти интуитивно понятные объяснения позволяют понять правила эксплуатации машины. Если написать t для термина, p для стека, и e для среды, состояния, связанные с этими тремя сущностями, будут записаны как t , p, e. Правила объясняют, как машина преобразует одно состояние в другое состояние после выявления шаблонов среди состояний.

Начальное состояние направлено на оценку терма t, это состояние t,□,□, в котором терм есть t, а стек и окружение пусты. Конечное состояние (при отсутствии ошибки) имеет вид λ t , □, e, другими словами, результирующие термы являются абстракцией вместе со своим окружением и пустым стеком.

Машина Кривина имеет четыре перехода: App (Приложение, Аппликация), Abs, Zero, Succ.

App удаляет параметр приложения и помещает его в стек для дальнейшей оценки. Abs удаляет λ терма, поднимает замыкание с вершины стека и помещает его на вершину среды. Это замыкание соответствует индексу де Брейна 0 в новой среде. Zero занимает первое закрытие среды. Термин этого замыкания становится текущим термином, а среда этого замыкания становится текущей средой. Succ удаляет первое замыкание списка окружения и уменьшает значение индекса.

SECD-машина использует четыре стека: S — стек объектов для вычисления рекурсивных выражений, E (environment) — контекст (отображение идентификаторов в объекты), C (control list) — управляющая строка (список управления), D (dump) — дамп, хранилище предыдущих состояний, используемое для возврата из вызова функций.

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

В самом начале контекст E, стек S и дамп D пусты, а подлежащее вычислению выражение загружается как единственный элемент C, который преобразуется в обратную польскую нотацию в процессе вычислений. Единственной используемой при этом операцией является аппликация, обозначаемая символом ap. Например, выражение f (g x) (единственный элемент списка) заменяется списком [x, g, ap, F, ap].

Вычисление C выполняется в соответствии с обратной польской логикой. Если первый элемент в C является значением, он помещается на стек S. Точнее, если элемент является идентификатором, значение будет привязкой для этого идентификатора в текущем контексте E. Если элемент является λ-абстракцией, для сохранения привязок его свободных переменных которые находятся в E) формируется замыкание, которое помещается в стек S.

Если элементом С является ap (аппликация), из стека извлекаются два значения, и первое применяется ко второму. Если результатом аппликации является значение, оно помещается в стек S.

Однако, если приложение представляет собой λ-абстракцию значения, это приведет к выражению лямбда-исчисления, которое само может быть аппликацией (а не значением) и поэтому не может быть помещено в стек. В этом случае текущее содержимое S, E и C помещается в дамп D (который является стеком этих троек), S делается пустым, а C повторно инициализируется для результата аппликации, а E получает контекст для свободных переменных этого выражения, дополненных привязками, полученными в результате аппликации. Вычисления продолжаются как указано выше.

Признаком завершения промежуточных вычислений является пустой стек C. При этом результат будет находиться в стеке S. В этом случае из стека D извлекается последнее сохраненное состояние вычислений и кладётся на соответствующие стеки. Вычисления продолжается, как указано выше.

Если C и D оба пусты, вычисления завершаются с результатом в стеке S.

Словарь содержит все исполняемые подпрограммы (или слова), которые составляют Форт-систему. Системные процедуры являются предопределенными записями в словаре, который становится доступным при загрузке. Факультативные опционально компилируются после загрузки. Пользователь добавляет user-defined слова.

Базисная форма наиболее распространенного определения слова:

: <name> <words to be executed> ;

Registers in the Forth virtual machine

Cons (construct, точечная пара) - создает объекты памяти, которые содержат два значения или два указателя на значения, конструирует в памяти новый объект из имеющихся двух. Эти объекты также называют cons-ячейками, cons-ами, неатомарными S-выражениями («NATS») или cons-парами. cons-ячейки могут использоваться для того, чтобы хранить упорядоченные пары данных и используются для построения более сложных составных структур данных, в частности списков и двоичных деревьев.

Диаграмма cons-ячеек для списка (42 69 613), созданного при помощи функции cons:(cons 42 (cons 69 (cons 613 nil)))
или записанного как список:(list 42 69 613)

В Лиспе списки реализованы поверх cons-пар. Конкретнее, структура любого списка в Лиспе выглядит следующим образом:

  1. Пустой список, обозначаемый как (), является специальным объектом. Его также обычно называют nil.
  2. Список из одного элемента представляет собой cons-пару, в первой ячейке которой присутствует его единственный элемент, а вторая ссылается на nil.
  3. Список из двух и более элементов представляет собой cons-пару, первый элемент которой является первым элементом списка, а вторая ссылается на список, являющийся хвостом основного списка.

https://telegra.ph/KENTAVR-09-25

Report Page