Кривинская машина - Krivine machine

Картинный вид машины Кривина

В теоретическая информатика, то Кривинская машина является абстрактная машина (иногда называют виртуальная машина ). Как абстрактная машина, она разделяет функции с Машины Тьюринга и Машина SECD. Машина Кривина объясняет, как вычислить рекурсивную функцию. Более конкретно, он направлен на строгое определение нормальная форма головы сокращение лямбда-член с помощью вызов по имени снижение. Благодаря формализму он подробно рассказывает, как работает своего рода редукция, и устанавливает теоретические основы операционная семантика из функциональные языки программирования. С другой стороны, машина Кривина реализует вызов по имени, потому что он оценивает тело β-редекс перед этим применяется тело к его параметру. Другими словами, в выражении (λ Икс. т) ты он оценивает сначала λ Икс. т прежде чем применять его к ты. В функциональное программирование, это будет означать, что для оценки функции, примененной к параметру, он сначала оценивает функцию, а затем применяет ее к параметру.

Машина Кривина была разработана французским логиком. Жан-Луи Кривин в начале 1980-х гг.

Вызов по имени и приведение головы к нормальной форме

Машина Кривина основана на двух концепциях, связанных с лямбда-исчисление, а именно уменьшение головы и вызов по имени.

Уменьшение нормальной формы головы

А редекс^[1] (говорят также о β-редексе) - это член лямбда-исчисления вида (λ Икс. т) ты. Если термин имеет форму (λ Икс. т) ты₁ ... ты_п говорят, что это голова редекс. А нормальная форма головы - это член лямбда-исчисления, который не является основным редексом.^[а] А уменьшение головы представляет собой (непустую) последовательность сокращений термина, который сокращает заголовочные редексы. Головное сокращение срока т (который должен быть не в нормальной форме головы) - это уменьшение головы, которое начинается с семестра т и заканчивается на голове нормальной формы. С абстрактной точки зрения, сокращение напора - это способ вычислений программы при оценке рекурсивной подпрограммы. Важно понять, как можно осуществить такое сокращение. Одна из целей машины Кривина - предложить процесс сокращения члена в нормальной форме головы и формально описать этот процесс. Нравиться Тьюринг использовал абстрактную машину для формального описания понятия алгоритма, Кривино использовал абстрактную машину для формального описания понятия редукции нормальной формы головы.

Пример

Период, термин ((λ 0) (λ 0)) (λ 0) (что соответствует, если использовать явные переменные, члену (λx.Икс) (λy.у) (λz.z)) не находится в нормальной форме головы, потому что (λ 0) (λ 0) контракты в (λ 0), что дает редекс головы (λ 0) (λ 0), который сокращается в (λ 0) и, следовательно, является головной нормальной формой ((λ 0) (λ 0)) (λ 0). Иначе говоря, сокращение нормальной формы головы:

((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,

что соответствует:

(λx.Икс) (λy.у) (λz.z) ➝ (λy.у) (λz.z) ➝ λz.z.

Далее мы увидим, как машина Кривина сокращает член ((λ 0) (λ 0)) (λ 0).

Звоните по имени

Осуществить сокращение срока ты который является приложением, но не является редексом, нужно уменьшить тело ты показать абстракцию и, следовательно, создать редекс с v. Когда появляется редекс, его уменьшают. Чтобы всегда сокращать тело приложения, сначала вызывается позвонить по имени.^[b] Станок Кривинье орудует позвонить по имени.

Описание

Представленное здесь представление машины Кривина основано на обозначениях лямбда-терминов, которые используют индексы де Брёйна и предполагает, что члены, по которым вычисляются нормальные формы головы, равны закрыто.^[2] Он изменяет текущий государственный пока он больше не сможет этого делать, и в этом случае он получит нормальную форму головы. Эта нормальная форма заголовка представляет собой результат вычисления или дает ошибку, означающую, что термин, с которого она начиналась, неверен. Однако он может входить в бесконечную последовательность переходов, что означает, что термин, который он пытается уменьшить, не имеет нормальной формы заголовка и соответствует непрерывному вычислению.

Доказано, что машина Кривина корректно реализует приведение нормальной формы вызова по имени головы в лямбда-исчислении. Кроме того, машина Кривина является детерминированный, поскольку каждый шаблон состояния соответствует не более чем одному машинному переходу.

Штат

Состояние состоит из трех компонентов^[2]

а срок,
а куча,
ан среда.

Термин является λ-термом с индексами де Брейна. Стек и окружение принадлежат одной и той же рекурсивной структуре данных. Точнее, окружение и стек - это списки пар <term, environment>, которые называются закрытие. Далее вставка в качестве заголовка списка ℓ (стека или окружения) элемента а написано а: ℓ, а пустой список пишется □. Стек - это место, где машина хранит замыкания, которые должны быть дополнительно оценены, тогда как среда - это связь между индексами и замыканиями в данный момент во время оценки. Первый элемент среды - это замыкание, связанное с индексом 0, второй элемент соответствует замыканию, связанному с индексом 1 и т. д. Если машине нужно оценить индекс, она выбирает там пару <term, environment> закрытие, которое дает термин, который нужно оценить, и среду, в которой этот термин должен быть оценен.^[c] Эти интуитивно понятные объяснения позволяют понять правила эксплуатации машины. Если писать т для срока, p для стека,^[d] и e для среды, состояния, связанные с этими тремя объектами, будут записаны т, п, д. Правила объясняют, как машина преобразует состояние в другое состояние после выявления закономерностей среди состояний.

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

Переходы

Машина Кривина^[2] имеет четыре перехода: Приложение, Abs, Нуль, Succ.

Переходы машины Кривина
Имя	Перед	После
Приложение	т ты, p, e	т, <ты, e>: p, e
Abs	λ t, <ты, e '>: p, e	т, р, <ты, e '>: e
Нуль	0, р, <т, e '>: e	т, p, e '
Succ	п + 1, р, <t, e '>: e	п, п, д

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

Два примера

Оценим член (λ 0 0) (λ 0), что соответствует члену (λ Икс. Икс Икс) (λ Икс. Икс). Начнем с состояния (λ 0 0) (λ 0), □, □.

Оценка срока *(λ 0 0) (λ 0)*
(λ 0 0) (λ 0), □, □
λ 0 0, [<λ 0, □>], □
0 0, □, [<λ 0, □>]
0, [<0, <λ 0, □>>], [<λ 0, □>]
λ 0, [<0, <λ 0, □>>], □
0, □, [<0, <λ 0, □>>]
0, □, [<λ 0, □>]
λ 0, □, □

Напрашивается вывод, что заголовок нормальной формы термина (λ 0 0) (λ 0) является λ 0. Это переводится с переменными в: начальную нормальную форму термина (λ Икс. Икс Икс) (λ Икс. Икс) является λ Икс. Икс.

Оценим член ((λ 0) (λ 0)) (λ 0), как показано ниже:

Оценка ((λ 0) (λ 0)) (λ 0)
((λ 0) (λ 0)) (λ 0), □, □
(λ 0) (λ 0), [<(λ 0), □>], □
(λ 0), [<(λ 0), □>,<(λ 0), □>], □
0, [<(λ 0), □>], [<(λ 0), □>]
λ 0, [<(λ 0), □>], □
0, □, [<(λ 0), □>]
(λ 0), □, □

Это подтверждает отмеченный выше факт, что нормальная форма члена ((λ 0) (λ 0)) (λ 0) равно (λ 0).

Смотрите также

Примечания

^ Если речь идет только о закрытых условиях, эти условия принимают форму λ Икс. т.
^ Эта древняя терминология относится к концепциям 60-х и вряд ли оправдана в 2017 году.
^ Используя концепцию замыкания, можно заменить тройное , который определяет состояние парой <closure,stack>, но это изменение косметическое.
^ p для куча, французское слово "стек", которое мы не хотим путать с s, для гос.

Библиография

Жан-Луи Кривин: Машина лямбда-исчисления по имени. Высшие порядки и символические вычисления 20 (3): 199-207 (2007) архив.
Куриен, Пьер-Луи (1993). Категориальные комбинаторы, последовательные алгоритмы и функциональные (2-е изд.). Birkhaüser.
Фредерик Ланг: Объяснение ленивой машины Кривина с помощью явной подстановки и адресов. Вычисления высшего порядка и символические вычисления 20 (3): 257-270 (2007). архив.
Оливье Данви (Ред.): Редакция спецвыпуска Вычисление высшего порядка и символическое вычисление на машине Кривина, т. 20 (3) (2007)

внешняя ссылка

СМИ, связанные с Кривинская машина в Wikimedia Commons

[2] Если речь идет только о закрытых условиях, эти условия принимают форму λ Икс. т.

[3] Эта древняя терминология относится к концепциям 60-х и вряд ли оправдана в 2017 году.

[5] Используя концепцию замыкания, можно заменить тройное , который определяет состояние парой <closure,stack>, но это изменение косметическое.

[6] для куча, французское слово "стек", которое мы не хотим путать с s, для гос.

[1] Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика, Исследования по логике и основам математики, 103 (Пересмотренное издание), Северная Голландия, Амстердам, ISBN 0-444-87508-5, заархивировано из оригинал на 2004-08-23 Исправления.

[Curien-4] а ^б ^c Куриен, Пьер-Луи (1993). Категориальные комбинаторы, последовательные алгоритмы и функциональные (2-е изд.). Birkhaüser.

[1]

[а]

[b]

[2]

[c]

[d]