ПРОВЕРИТЬ машину

Машина CEK — это абстрактная машина, изобретенная Матиасом Феллейзеном и Дэниелом П. Фридманом слева направо , которая реализует вызов по значению . ^[1] Обычно он реализуется как интерпретатор функциональных языков программирования , но может также использоваться для реализации простых императивных языков программирования . Состояние в машине CEK включает оператор управления, среду и продолжение . Оператор управления — это термин, который оценивается в этот момент, среда (обычно) представляет собой карту имен переменных со значениями, а продолжение сохраняет другое состояние или особый случай остановки. Это упрощенная форма другой абстрактной машины, называемой SECD-машиной . ^[2]^[3]^[4]

Машина CEK построена на машине SECD, заменяя дамп (стек вызовов) более продвинутым продолжением и помещая параметры непосредственно в среду, а не помещая их сначала в стек параметров. Могут быть внесены и другие модификации, в результате чего создается целое семейство родственных машин. Например, машина CESK имеет переменные карты среды для указателя на хранилище, которое фактически представляет собой кучу. Это позволяет моделировать изменяемое состояние лучше, чем обычная машина CEK. Машина CK не имеет среды и может использоваться для простых вычислений без переменных. ^[5]

Описание

Машина CEK может быть создана для любого языка программирования, поэтому этот термин часто используется расплывчато. Например, можно создать машину CEK для интерпретации лямбда-исчисления . Его среда сопоставляет переменные с замыканиями, а продолжения представляют собой либо остановку, либо продолжение для оценки аргумента (ar), либо продолжение для оценки приложения после оценки функции (ap): ^[4]^[6]


Переход	От	К
Переменная	х , Е, К	t , E', K где замыкание(t,E') = E[x]
Приложение	(fe) , Е, К	f , E, ar(e, E, K)
Абстракция при оценке функции	Абс, Е, ар(т, Е', К)	t, E', ap(Abs, E, K)
Абстракция при оценке аргумента	Abs, E, ap(λx.Exp, E', K)	Exp, E'[x=замыкание(Abs,E)], K

Представление компонентов

Каждый компонент машины CEK имеет различные представления. Управляющая строка обычно представляет собой вычисляемый термин или иногда номер строки. Например, машина CEK, оценивающая лямбда-исчисление, будет использовать лямбда-выражение в качестве управляющей строки. Среда почти всегда представляет собой карту переменных и значений или, в случае машин CESK, переменных и адресов в хранилище. Представление продолжения варьируется. Он часто содержит другое окружение, а также тип продолжения, например аргумент или приложение . Иногда это стек вызовов, где каждый кадр представляет собой остальную часть состояния, то есть оператор управления и среду.

Сопутствующие машины

Есть еще несколько машин, тесно связанных с машиной CEK.

машина ЦЭСК

Машина CESK — еще одна машина, тесно связанная с машиной CEK. Среда машины CESK сопоставляет переменные с указателями в «хранилище» (куче), отсюда и название «CESK». Его можно использовать для моделирования изменяемого состояния, например, исчисление Λ _σ, описанное в оригинальной статье . Это делает его гораздо более полезным для интерпретации императивных языков программирования, а не функциональных. ^[5]

машина CS

Машина CS содержит только оператор управления и хранилище. Это также описано в оригинальной статье. В приложении вместо помещения переменных в среду оно заменяет их адресом в хранилище и помещает значение переменной в этот адрес. Продолжение не требуется, поскольку оно лениво вычисляется ; не нужно помнить об оценке аргумента. ^[5]

SECD-машина

Машина SECD была машиной, на которой была основана машина CEK. Он имеет стек, среду, управляющий оператор и дамп. Дамп представляет собой стек вызовов и используется вместо продолжения. Стек используется для передачи параметров функциям. Управляющий оператор был написан в постфиксной нотации , и машина имела собственный «язык программирования». Утверждение лямбда-исчисления, подобное этому:

(Миннесота)

будет написано так:

Н: М: будет

где ap — функция, которая объединяет две абстракции. ^[7]^[8]

Происхождение

На странице 196 книги «Операторы управления, машина SECD и $\lambda$ -Исчисление", ^[9] и на странице 4 одноименного технического отчета, ^[10] Матиас Феллизен и Дэниел П. Фридман написали «[CEK] машина является производной от расширенного интерпретатора Рейнольдса IV.", имея в виду Джона Рейнольдса Интерпретатор III в «Определённых интерпретаторах языков программирования высшего порядка». ^[11] ^[12]

А именно, вот реализация машины CEK в OCaml: представление лямбда-членов с индексами де Брёйна:

type term = IND of int    (* de Bruijn index *)
          | ABS of term
          | APP of term * term

Значения — это замыкания , как это Питер придумал Ландин :

type value = CLO of term * value list

type cont = C2 of term * value list * cont
          | C1 of value * cont
          | C0

let rec continue (c : cont) (v : value) : value =
  match c, v with
    C2 (t1, e, k), v0 ->
     eval t1 e (C1 (v0, k))
  | C1 (v0, k), v1 ->
     apply v0 v1 k
  | C0, v ->
     v
and eval (t : term) (e : value list) (k : cont) : value =
  match t with
    IND n ->
     continue k (List.nth e n)
  | ABS t' ->
     continue k (CLO (t', e))
  | APP (t0, t1) ->
     eval t0 e (C2 (t1, e, k))
and apply (v0 : value) (v1 : value) (k : cont) =
  let (CLO (t, e)) = v0
  in eval t (v1 :: e) k

let main (t : term) : value =
  eval t [] C0

Эта реализация находится в дефункциональной форме , с cont и continue как представление продолжения первого порядка. Вот его переработанный аналог:

let rec eval (t : term) (e : value list) (k : value -> 'a) : 'a =
  match t with
    IND n ->
     k (List.nth e n)
  | ABS t' ->
     k (CLO (t', e))
  | APP (t0, t1) ->
     eval t0 e (fun v0 ->
                  eval t1 e (fun v1 ->
                               apply v0 v1 k))
and apply (v0 : value) (v1 : value) (k : value -> 'a) : 'a =
  let (CLO (t, e)) = v0
  in eval t (v1 :: e) k

let main (t : term) : value =
  eval t [] (fun v -> v)

слева направо Эта реализация выполнена в стиле передачи продолжения , где область ответов полиморфна, т. е. реализуется с помощью переменной типа. ^[13] Эта реализация передачи продолжения отображается обратно в прямой стиль следующим образом:

let rec eval (t : term) (e : value list) : value =
  match t with
    IND n ->
     List.nth e n
  | ABS t' ->
     CLO (t', e)
  | APP (t0, t1) ->
     let v0 = eval t0 e
     and v1 = eval t1 e
     in apply v0 v1
and apply (v0 : value) (v1 : value) : value =
  let (CLO (t, e)) = v0
  in eval t (v1 :: e)

let main (t : term) : value =
  eval t []

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

type value = FUN of (value -> value)

let rec eval (t : term) (e : value list) : value =
  match t with
    IND n ->
     List.nth e n
  | ABS t' ->
     FUN (fun v -> eval t' (v :: e))
  | APP (t0, t1) ->
     let v0 = eval t0 e
     and v1 = eval t1 e
     in apply v0 v1
and apply (v0 : value) (v1 : value) : value =
  let (FUN f) = v0
  in f v1

let main (t : term) : value =
  eval t []

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

Этот вывод имитирует Дэнви рациональную деконструкцию Лэндина машины SECD . ^[14] Обратный вывод (преобразование замыкания, преобразование CPS и дефункционализация) описано в статье Джона Рейнольдса «Определительные интерпретаторы языков программирования высшего порядка». который является источником машины CEK и впоследствии был идентифицирован как образец преобразования композиционных оценщиков в абстрактные машины и наоборот. ^[11]^[15]

Новое время

Машина CEK, как и машина Кривина , не только функционально соответствует метациклическому вычислителю (посредством преобразования CPS вызова по значению слева направо), ^[15] оно также синтаксически соответствует $\lambda {\widehat {\rho }}$ исчисление - исчисление, использующее явную замену - со стратегией уменьшения аппликативного порядка слева направо, ^[16] ^[17] и то же самое для машины SECD (посредством преобразования CPS с вызовом справа налево). ^[18]

Ссылки

^ Аккаттоли, Бениамино; Баренбаум, Пабло; Мацца, Дамиано (19 августа 2014 г.), «Дистилляция абстрактных машин», Труды 19-й международной конференции ACM SIGPLAN по функциональному программированию , ACM, стр. 363–376, doi : 10.1145/2628136.2628154 , ISBN 9781450328739 Они различаются тем, как ведут себя по отношению к приложениям: CEK реализует вызов по значению слева направо, т. е. сначала оценивает функциональную часть, а LAM вместо этого отдает приоритет аргументам, реализуя вызов справа налево. по стоимости.
^ Йенс Палсберг (28 августа 2009 г.). Семантика и алгебраическая спецификация: очерки, посвященные Питеру Д. Моссесу по случаю его 60-летия . Springer Science & Business Media. стр. 162–. ISBN 978-3-642-04163-1 .
^ Феллизен, Матиас ; Финдлер, Роберт Брюс ; Флэтт, Мэтью (10 июля 2009 г.). Семантическая инженерия с помощью PLT Redex . МТИ Пресс. стр. 113–. ISBN 978-0-262-25817-3 .
^ Перейти обратно: ^а ^б Тилеке, Хайо (9 декабря 2015 г.). «Реализация функциональных языков с помощью абстрактных машин» (PDF) . Архивировано из оригинала (PDF) 17 июля 2021 г. Проверено 9 сентября 2020 г.
^ Перейти обратно: ^а ^б ^с Феллизен, Матиас ; Фридман, Дэниел П. (октябрь 1986 г.). «Исчисление заданий на языках высшего порядка» (PDF) .
^ «Повышение квалификации на машине CEK» . CMSC 330, лето 2015 г. Проверено 19 сентября 2020 г.
^ «Виртуальная машина SECD» (PDF) .
^ "секунда" . www.cs.bath.ac.uk. Проверено 23 сентября 2020 г.
^ Феллизен, Матиас ; Фридман, Дэниел (1986). Операторы управления, машина SECD и $\lambda$ -Расчёт . Формальное описание концепций программирования III, Elsevier Science Publishers BV (Северная Голландия). стр. 193–217. дои : 10.1007/978-3-319-14125-1_13 .
^ Феллизен , Матиас; Фридман , Дэниел П. (1986). Операторы управления, машина SECD и $\lambda$ -Расчет (PDF) (Технический отчет). Департамент компьютерных наук Университета Индианы. 197.
^ Перейти обратно: ^а ^б Рейнольдс, Джон К. (1972). «Определенные интерпретаторы языков программирования высшего порядка». Материалы ежегодной конференции ACM-ACM '72 . Том. 2. Материалы 25-й Национальной конференции ACM. стр. 717–740. дои : 10.1145/800194.805852 .
^ Рейнольдс, Джон К. (1998). «Возвращение к дефинициональным интерпретаторам». Вычисления высшего порядка и символьные вычисления . 11 (4): 355–361. дои : 10.1023/А:1010075320153 . S2CID 34126862 .
^ Тилеке, Хайо (2004). «Полиморфизм типов ответов при передаче продолжения вызова по имени». Языки и системы программирования . Конспекты лекций по информатике. Том. 2986. Языки и системы программирования, 13-й Европейский симпозиум по программированию, ESOP 2004, LNCS 2986, Springer. стр. 279–293. дои : 10.1007/978-3-540-24725-8_20 . ISBN 978-3-540-21313-0 .
^ Дэнви , Оливье (2004). Рациональная деконструкция машины SECD Ландина (PDF) . Реализация и применение функциональных языков, 16-й международный семинар, IFL 2004, Пересмотренные избранные статьи, Конспекты лекций по информатике 3474, Springer. стр. 52–71. ISSN 0909-0878 .
^ Перейти обратно: ^а ^б Агер, Мэдс Сиг; Бернацкий, Дариуш; Дэнви, Оливье ; Мидтгаард, январь (2003). «Функциональное соответствие между вычислителями и абстрактными машинами» . Серия отчетов БРИКС . 10 (13). 5-я Международная конференция ACM SIGPLAN по принципам и практике декларативного программирования (PPDP'03): 8–19. дои : 10.7146/brics.v10i13.21783 .
^ Берначка, Малгожата; Дэнви, Оливье (2007). «Бетонная основа для экологических машин» . Транзакции ACM в вычислительной логике . 9 (1). Статья №6: 1–30. дои : 10.7146/brics.v13i3.21909 .
^ Розовский, Войцех (2021). Формально проверенный вывод исполняемой и завершающей машины CEK из лямбда-p-hat-исчисления с вызовом по значению (PDF) (Диссертация). Университет Саутгемптона.
^ Дэнви, Оливье ; Милликин, Кевин (2008). «Рациональная деконструкция машины SECD Ландина с оператором J». Логические методы в информатике . 4 (4): 1–67. arXiv : 0811.3231 . дои : 10.2168/LMCS-4(4:12)2008 . S2CID 7926360 .

[AccattoliBarenbaumMazza2014-1] Аккаттоли, Бениамино; Баренбаум, Пабло; Мацца, Дамиано (19 августа 2014 г.), «Дистилляция абстрактных машин», Труды 19-й международной конференции ACM SIGPLAN по функциональному программированию , ACM, стр. 363–376, doi : 10.1145/2628136.2628154 , ISBN 9781450328739 Они различаются тем, как ведут себя по отношению к приложениям: CEK реализует вызов по значению слева направо, т. е. сначала оценивает функциональную часть, а LAM вместо этого отдает приоритет аргументам, реализуя вызов справа налево. по стоимости.

[Palsberg2009-2] Йенс Палсберг (28 августа 2009 г.). Семантика и алгебраическая спецификация: очерки, посвященные Питеру Д. Моссесу по случаю его 60-летия . Springer Science & Business Media. стр. 162–. ISBN 978-3-642-04163-1 .

[FelleisenFindler2009-3] Феллизен, Матиас ; Финдлер, Роберт Брюс ; Флэтт, Мэтью (10 июля 2009 г.). Семантическая инженерия с помощью PLT Redex . МТИ Пресс. стр. 113–. ISBN 978-0-262-25817-3 .

[:1-4] Перейти обратно: ^а ^б Тилеке, Хайо (9 декабря 2015 г.). «Реализация функциональных языков с помощью абстрактных машин» (PDF) . Архивировано из оригинала (PDF) 17 июля 2021 г. Проверено 9 сентября 2020 г.

[:0-5] Перейти обратно: ^а ^б ^с Феллизен, Матиас ; Фридман, Дэниел П. (октябрь 1986 г.). «Исчисление заданий на языках высшего порядка» (PDF) .

[6] «Повышение квалификации на машине CEK» . CMSC 330, лето 2015 г. Проверено 19 сентября 2020 г.

[7] «Виртуальная машина SECD» (PDF) .

[8] "секунда" . www.cs.bath.ac.uk. Проверено 23 сентября 2020 г.

[felleisen_friedman_fdpc3-9] Феллизен, Матиас ; Фридман, Дэниел (1986). Операторы управления, машина SECD и $\lambda$ -Расчёт . Формальное описание концепций программирования III, Elsevier Science Publishers BV (Северная Голландия). стр. 193–217. дои : 10.1007/978-3-319-14125-1_13 .

[felleisen_friedman_87-10] Феллизен , Матиас; Фридман , Дэниел П. (1986). Операторы управления, машина SECD и $\lambda$ -Расчет (PDF) (Технический отчет). Департамент компьютерных наук Университета Индианы. 197.

[reynolds_72-11] Перейти обратно: ^а ^б Рейнольдс, Джон К. (1972). «Определенные интерпретаторы языков программирования высшего порядка». Материалы ежегодной конференции ACM-ACM '72 . Том. 2. Материалы 25-й Национальной конференции ACM. стр. 717–740. дои : 10.1145/800194.805852 .

[reynolds_98-12] Рейнольдс, Джон К. (1998). «Возвращение к дефинициональным интерпретаторам». Вычисления высшего порядка и символьные вычисления . 11 (4): 355–361. дои : 10.1023/А:1010075320153 . S2CID 34126862 .

[thielecke_esop04-13] Тилеке, Хайо (2004). «Полиморфизм типов ответов при передаче продолжения вызова по имени». Языки и системы программирования . Конспекты лекций по информатике. Том. 2986. Языки и системы программирования, 13-й Европейский симпозиум по программированию, ESOP 2004, LNCS 2986, Springer. стр. 279–293. дои : 10.1007/978-3-540-24725-8_20 . ISBN 978-3-540-21313-0 .

[danvy_ifl-04-14] Дэнви , Оливье (2004). Рациональная деконструкция машины SECD Ландина (PDF) . Реализация и применение функциональных языков, 16-й международный семинар, IFL 2004, Пересмотренные избранные статьи, Конспекты лекций по информатике 3474, Springer. стр. 52–71. ISSN 0909-0878 .

[ager_et_al_03-15] Перейти обратно: ^а ^б Агер, Мэдс Сиг; Бернацкий, Дариуш; Дэнви, Оливье ; Мидтгаард, январь (2003). «Функциональное соответствие между вычислителями и абстрактными машинами» . Серия отчетов БРИКС . 10 (13). 5-я Международная конференция ACM SIGPLAN по принципам и практике декларативного программирования (PPDP'03): 8–19. дои : 10.7146/brics.v10i13.21783 .

[1biernacka_danvy_brics-07-16] Берначка, Малгожата; Дэнви, Оливье (2007). «Бетонная основа для экологических машин» . Транзакции ACM в вычислительной логике . 9 (1). Статья №6: 1–30. дои : 10.7146/brics.v13i3.21909 .

[rozowski_thesis_21-17] Розовский, Войцех (2021). Формально проверенный вывод исполняемой и завершающей машины CEK из лямбда-p-hat-исчисления с вызовом по значению (PDF) (Диссертация). Университет Саутгемптона.

[danvy_millikin_lmcs-08-18] Дэнви, Оливье ; Милликин, Кевин (2008). «Рациональная деконструкция машины SECD Ландина с оператором J». Логические методы в информатике . 4 (4): 1–67. arXiv : 0811.3231 . дои : 10.2168/LMCS-4(4:12)2008 . S2CID 7926360 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]