Кривая машина
 | Эта статья включает список общих ссылок , но в ней отсутствуют достаточные соответствующие встроенные цитаты . ( январь 2024 г. ) |
В теоретической информатике машина Кривина — это абстрактная машина (иногда называемая виртуальной машиной ). Как абстрактная машина, она имеет общие черты с машинами Тьюринга и SECD-машиной . Машина Кривина объясняет, как вычислить рекурсивную функцию. Более конкретно, он направлен на строгое определение к нормальной форме головы приведения лямбда-терма с использованием сокращения вызова по имени . Благодаря своему формализму он подробно рассказывает, как работает своего рода редукция, и закладывает теоретические основы операционной семантики функциональных языков программирования . С другой стороны, машина Кривина реализует вызов по имени, поскольку она оценивает тело β- редекса, прежде чем применить тело к своему параметру. Другими словами, в выражении ( λ x . t ) u сначала вычисляется λ x . прежде чем применять его к вам . В функциональном программировании это будет означать, что для оценки функции, примененной к параметру, сначала вычисляется функция, а затем применяется ее к параметру.
Машина Кривина была разработана французским логиком Жаном-Луи Кривином в начале 1980-х годов.
Звонок по имени и приведение головы в нормальную форму [ править ]
Машина Кривина основана на двух концепциях, связанных с лямбда-исчислением , а именно: уменьшении головы и вызове по имени.
головы нормальной Уменьшение формы
редекс [1] (говорят также β-редекс) — это термин лямбда-исчисления формы ( λ x . t ) u . Если терм имеет форму ( λ x .t ) ... u 1 , un его называют головным редексом . Головная нормальная форма — это термин лямбда-исчисления, который не является головным редексом. [а] Сокращение головы — это (непустая) последовательность сокращений термина, который сжимает редексы головы. Редукция головы термина t (которая, как предполагается, не находится в нормальной форме головы) — это редукция головы, которая начинается с термина t и заканчивается нормальной формой головы. С абстрактной точки зрения сокращение головы — это способ вычислений программы при вычислении рекурсивной подпрограммы. Важно понять, как такое сокращение может быть реализовано. Одна из целей машины Кривина — предложить процесс приведения термина в головную нормальную форму и формально описать этот процесс. Подобно тому, как Тьюринг использовал абстрактную машину для формального описания понятия алгоритма, Кривин использовал абстрактную машину для формального описания понятия приведения головы к нормальной форме.
Пример [ править ]
Термин (( λ 0) ( λ 0)) ( λ 0) (который соответствует, если использовать явные переменные, термину ( λx . x ) ( λy . y ) ( λz . z )) не является нормальным в голове. форму, потому что ( λ 0) ( λ 0) сжимается в ( λ 0 ), давая головной редекс ( λ 0) ( λ 0), который сжимается в ( λ 0) и который, следовательно, является головной нормальной формой (( λ 0) ( λ 0)) ( λ 0). Другими словами, нормальная форма сокращения головы такова:
- (( λ 0) ( λ 0)) ( λ 0) ➝ ( λ 0) ( λ 0) ➝ λ 0,
что соответствует:
- ( λx . x ) ( λy . y ) ( λz . z ) ➝ ( λy . y ) ( λz . z ) ➝ λz . з .
Далее мы увидим, как машина Кривина сокращает член (( λ 0) ( λ 0)) ( λ 0).
Звонить по имени [ править ]
Чтобы реализовать сокращение головы термина uv , который является приложением, но не является редексом, необходимо уменьшить тело u , чтобы оно отображало абстракцию и, следовательно, создать редекс с v . Когда появляется редекс, его уменьшают. Чтобы всегда сокращать тело приложения, сначала вызывается вызов по имени . Машина Кривина реализует вызов по имени .
Описание [ править ]
Представление машины Кривина, приведенное здесь, основано на обозначениях лямбда-термов, использующих индексы де Брёйна , и предполагает, что члены, для которых она вычисляет головные нормальные формы, замкнуты . [2] Он изменяет текущее состояние до тех пор, пока он больше не сможет этого делать, и в этом случае он получает нормальную форму головы. Эта головная нормальная форма представляет собой результат вычислений или выдает ошибку, означающую, что термин, с которого она началась, неверен. Однако он может вводить бесконечную последовательность переходов, а это означает, что член, который он пытается сократить, не имеет головной нормальной формы и соответствует непрерывным вычислениям.
Доказано, что машина Кривина правильно реализует приведение головы к нормальной форме в лямбда-исчислении. Более того, машина Кривина является детерминированной , поскольку каждому шаблону состояния соответствует не более одного машинного перехода.
Государство [ править ]
Государство состоит из трех компонентов [2]
- термин ,
- стек ,
- среда окружающая .
Термин представляет собой λ-терм с индексами де Брейна. Стек и среда принадлежат одной и той же рекурсивной структуре данных. Точнее, среда и стек — это списки пар <term, Environment> , которые называются замыканиями . Далее вставка в качестве главы списка ℓ (стека или окружения) элемента a записывается a:ℓ , тогда как пустой список записывается □. Стек — это место, где машина хранит замыкания, которые необходимо дополнительно оценить, тогда как среда — это связь между индексами и замыканиями в определенный момент времени во время оценки. Первый элемент среды — это замыкание, связанное с индексом 0 , второй элемент соответствует замыканию, связанному с индексом 1 и т. д. Если машине необходимо оценить индекс, она извлекает туда пару <term, Environment> замыкание, которое дает термин, который нужно оценить, и среду, в которой этот термин должен быть оценен. [б] Интуитивные пояснения позволяют понять правила работы машины. Если написать t для термина, p для стека, [с] и e для окружающей среды, состояния, связанные с этими тремя объектами, будут записываться t , p, e. Правила объясняют, как машина преобразует одно состояние в другое после выявления закономерностей между состояниями.
Начальное состояние направлено на оценку термина t , это состояние t ,□,□, в котором термин равен t , а стек и среда пусты. Конечное состояние (при отсутствии ошибки) имеет вид λ t , □, e, другими словами, результирующий терм представляет собой абстракцию вместе со своим окружением и пустым стеком.
Переходы [ править ]
Кривинская машина [2] имеет четыре перехода: App , Abs , Zero , Succ .
| Имя | До | После |
|---|---|---|
Приложение | ту , п, е | т , < и , е>:p, е |
пресс | λ t , < u ,e'>:p, e | т , р, < и , е'>:е |
Ноль | 0 , p, < t , e'>:e | т , п, е' |
успех | n+1 , p, < t ,e'>:e | н, п, е |
перехода Приложение удаляет параметр приложения и помещает его в стек для дальнейшей оценки. Переход Abs удаляет λ члена, вытаскивает замыкание из вершины стека и помещает его на вершину окружения. Это замыкание соответствует индексу де Брейна 0 в новой среде. Переход Зеро осуществляет первое замыкание среды. Срок этого закрытия становится текущим сроком, а среда этого закрытия становится текущей средой. Переход Succ удаляет первое замыкание списка окружения и уменьшает значение индекса.
Два примера [ править ]
Давайте оценим член ( λ 0 0) ( λ 0), который соответствует члену ( λ x . x x ) ( λ x . x ). Начнем с состояния ( λ 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. Это переводится с переменными в: головная нормальная форма термина ( λ x . x x ) ( λ x . x ) x λ . х .
Давайте оценим член (( λ 0) ( λ 0)) ( λ 0), как показано ниже:
| (( λ 0) ( λ 0)) ( λ 0), □, □ |
| ( λ 0) ( λ 0), [<( λ 0), □>], □ |
| ( λ 0), [<( λ 0), □>,<( λ 0), □>], □ |
| 0, [<( λ 0), □>], [<( λ 0), □>] |
| λ 0, [<( λ 0), □>], □ |
| 0, □, [<( λ 0), □>] |
| ( λ 0), □, □ |
Это подтверждает изложенный выше факт, что нормальная форма слагаемого (( λ 0) ( λ 0)) ( λ 0) равна ( λ 0).
Взаимные производные [ править ]
Машина Кривина, как и машина ЦЕК , не только функционально соответствует метациклическому вычислителю , [3] [4] [5] оно также синтаксически соответствует исчисление — вариант исчисления Пьера-Луи Кюрьена. исчисление явных замен , замкнутое при редукции, со стратегией редукции нормального порядка. [6] [7] [8]
Если исчисление включает в себя обобщенные сокращение (т.е. вложенное редекс сокращается за один шаг вместо двух), то синтаксически соответствующая машина совпадает с исходной машиной Жана-Луи Кривина. [9] [7] (Кроме того, если стратегия сокращения представляет собой вызов справа налево по значению и включает обобщенные сокращения, то синтаксически соответствующая машина — это Ксавье Лероя абстрактная машина ZINC , которая лежит в основе OCaml .) [10] [7]
См. также [ править ]
Примечания [ править ]
- ^ Если иметь дело только с замкнутыми членами, эти члены принимают форму λ x . т .
- ^ Используя концепцию замыкания, можно заменить тройку <term,stack, Environment> , определяющую состояние, парой <closure,stack> , но это изменение носит косметический характер.
- ^ p — это куча , французское слово, обозначающее стек, которое мы не хотим путать с s , обозначающим состояние.
Ссылки [ править ]
- ^ Барендрегт, Хендрик Питер (1984), Лямбда-исчисление: его синтаксис и семантика , Исследования по логике и основам математики, том. 103 (пересмотренная редакция), Северная Голландия, Амстердам, ISBN 0-444-87508-5 , заархивировано из оригинала 23 августа 2004 г. Исправления .
- ^ Jump up to: Перейти обратно: а б с Кюрьен, Пьер-Луи (1993). Категориальные комбинаторы, последовательные алгоритмы и функционалы (2-е изд.). Биркхаузер.
- ^ Шмидт, Дэвид А. (1980). «Машины переходов состояний для выражений лямбда-исчисления». Машины перехода состояний для выражений лямбда-исчисления . Конспекты лекций по информатике. Том. 94. Генерация компилятора, управляемая семантикой, LNCS 94. стр. 415–440. дои : 10.1007/3-540-10250-7_32 . ISBN 978-3-540-10250-2 .
- ^ Шмидт, Дэвид А. (2007). «Машины перехода состояний, еще раз». Вычисления высшего порядка и символьные вычисления . 20 (3): 333–335. дои : 10.1007/s10990-007-9017-x . S2CID 3012667 .
- ^ Агер, Мэдс Сиг; Бернацкий, Дариуш; Дэнви, Оливье ; Мидтгаард, январь (2003). «Функциональное соответствие между вычислителями и абстрактными машинами» . Серия отчетов БРИКС . 10 (13). 5-я Международная конференция ACM SIGPLAN по принципам и практике декларативного программирования (PPDP'03): 8–19. дои : 10.7146/brics.v10i13.21783 .
- ^ Кюрьен, Пьер-Луи (1991). «Абстрактная основа для машин окружающей среды» . Теоретическая информатика . 82 (2): 389–402. дои : 10.1016/0304-3975(91)90230-Y .
- ^ Jump up to: Перейти обратно: а б с Берначка, Малгожата; Дэнви, Оливье (2007). «Бетонная основа для экологических машин» . Транзакции ACM в вычислительной логике . 9 (1). Статья №6: 1–30. дои : 10.7146/brics.v13i3.21909 .
- ^ Свирстра, Воутер (2012). «От математики к абстрактной машине: формальный вывод исполняемой машины Кривина» . Электронные труды по теоретической информатике . 76 . Материалы четвертого семинара по математическо структурированному функциональному программированию (MSFP 2012): 163–177. arXiv : 1202.2924 . дои : 10.4204/EPTCS.76.10 . S2CID 14668530 .
- ^ Кривин, Жан-Луи (2007). «Машина лямбда-исчисления с вызовом по имени». Вычисления высшего порядка и символьные вычисления . 20 (3): 199–207. дои : 10.1007/s10990-007-9018-9 . S2CID 18158499 .
- ^ Лерой , Ксавье (1990). Эксперимент ZINC: экономичная реализация языка ML (Технический отчет). Инрия. 117.
Содержимое этой редакции переведено из существующей статьи французской Википедии по адресу fr:Machine de Krivine ; см. его историю для определения авторства.
Библиография [ править ]
- Жан-Луи Кривин: Машина лямбда-исчисления с вызовом по имени . Высший порядок и символические вычисления 20(3): 199-207 (2007), архив .
- Кюрьен, Пьер-Луи (1993). Категориальные комбинаторы, последовательные алгоритмы и функционалы (2-е изд.). Биркхаузер.
- Фредерик Ланг: Объяснение ленивой машины Кривина с помощью явной подстановки и адресов . Высший порядок и символические вычисления 20(3): 257-270 (2007), архив .
- Оливье Дэнви (ред.): Редакционная статья специального выпуска журнала «Высшие порядки и символические вычисления на машине Кривина», том. 20(3) (2007)
Внешние ссылки [ править ]
СМИ, связанные с машиной Кривина, на Викискладе?
