Перефокусировка (семантика)

В информатике используемое перефокусировка — это преобразование программы, для более эффективной реализации семантики сокращения — то есть небольшой операционной семантики с явным представлением контекста сокращения. Это шаг к реализации детерминированной семантики как детерминированной абстрактной машины .

Небольшая операционная семантика определяет смысл данной программы. $p_{0}$ как последовательность одношаговых сокращений, которая начинается с $p_{0}$ и продолжается последовательностью сокращений $p_{i}$ , где $i>0$ :

$p_{0}\rightarrow p_{1}\rightarrow p_{2}\rightarrow \cdots$

Сокращение на один шаг от $p_{n}$ к $p_{n+1}$ достигается за счет

нахождение наименьшего потенциально сокращаемого термина ( потенциального редекса ) с использованием заданной стратегии сокращения , если этот потенциальный редекс существует в $p_{n}$ (в противном случае $p_{n}$ является неприводимым); и
сокращение этого потенциального редекса с использованием заданных правил сжатия, если оно действительно (в противном случае $p_{n}$ застрял).

Семантика редукции — это операционная семантика небольших шагов с явным представлением контекста каждого потенциального редекса.

Письмо $C$ для такого контекста приведенная выше последовательность одношаговых сокращений гласит:

$p_{0}=C_{0}[{\mathit {pr}}_{0}]\rightarrow C_{0}[c_{0}]=C_{1}[{\mathit {pr}}_{1}]\rightarrow C_{1}[c_{1}]=C_{2}[{\mathit {pr}}_{2}]\rightarrow C_{2}[c_{2}]\rightarrow \cdots$

где

$p_{0}$ сначала разлагается на контекст $C_{0}$ и потенциальный редекс ${\mathit {pr}}_{0}$ ,
${\mathit {pr}}_{0}$ это прописано в контракте $c_{0}$ ,
$C_{0}$ затем перестраивается вокруг $c_{0}$ а затем разлагается на контекст $C_{1}$ и потенциальный редекс ${\mathit {pr}}_{1}$ ,
и т. д.

Эта последовательность разложений, сжатий и рекомпозиций изображается следующим образом:

         contract               contract               contract        
       o--------->o           o--------->o           o--------->o      
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o--------------------->o--------------------->o--------------------->o
          reduce                 reduce                 reduce

Перефокусировка — это вырубка последовательных редукций: ^[1]^[2]

         contract    refocus    contract    refocus    contract        
       o--------->o---------->o--------->o---------->o--------->o------
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o                      o                      o                      o

После первоначальной декомпозиции последовательность сокращений и перефокусировок имеет структуру детерминированной абстрактной машины .

Фон

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

Пример

Рассмотрим следующий детерминированный язык арифметических выражений над целыми числами со сложениями и частными наподобие бритвы Хаттона. ^[3]^[4]

В OCaml :

type operator = Add | Quo;;

type expression = Lit of int | Opr of expression * operator * expression;;

Так $1+10$ анализируется как Opr (Lit 1, Add, Lit 10) и $11/2$ анализируется как Opr (Lit 11, Quo, Lit 2).

type value = Int of int;;

let expression_of_value (v : value) : expression = match v with Int n -> Lit n;;

Наименьшие потенциально сокращаемые выражения ( потенциальные редексы ) представляют собой операции над значениями, и они выполняются с помощью функции сжатия, которая отображает фактический редекс в выражение и в противном случае выдает сообщение об ошибке:

type potential_redex = PR of value * operator * value;;

type contractum_or_error = Contractum of expression | Error of string;;

let contract (pr : potential_redex) : contractum_or_error =
  match pr with
    PR (Int n1, Add, Int n2) ->
     Contractum (Lit (n1 + n2))
  | PR (Int n1, Quo, Int n2) ->
     if n2 = 0
     then Error (string_of_int n1 ^ " / 0")
     else Contractum (Lit (n1 / n2));;

Сложение двух целых чисел представляет собой настоящий редекс, как и частное целого числа и ненулевого целого числа. Так, например, выражение Opr (Opr (Lit 1, Add, Lit 10), Add, Lit 100), то есть $(1+10)+100$ , сводится к Opr (Lit 11, Add, Lit 100), то есть $11+100$ , выражение Opr (Lit 11, Quo, Lit 2), то есть $11/2$ , сводится к Lit 5, то есть $5$ с $11=5\cdot 2+1$ , и выражение Opr (Opr (Lit 1, Quo, Lit 0), Add, Lit 100), то есть $(1/0)+100$ , сводится к Error "1 / 0".

Предположим, что стратегия сокращения — самая левая-внутренняя (т. е. сначала глубина и слева направо), как это фиксируется следующими правилами сравнения:

                    e1 -> e1'
     ---------------------------------------
     Opr (e1, opr, e2) -> Opr (e1', opr, e2)
 
                    e2 -> e2'
 -----------------------------------------------
 Opr (Lit n1, opr, e2) -> Opr (Lit n1, opr, e2')

Следующая функция одношагового сокращения реализует эту стратегию:

let rec reduce_d (e : expression) : value_or_expression_or_stuck =
  match e with
    Lit n ->
     Value (Int n)
  | Opr (e1, opr, e2) ->
     match reduce_d e1 with
       Value v1 ->
        (match reduce_d e2 with
           Value v2 ->
            (match contract (PR (v1, opr, v2)) with
               Contractum e ->
                Expression e
             | Error s ->
                Stuck s)
         | Expression e2' ->
            Expression (Opr (expression_of_value v1, opr, e2'))
         | Stuck s ->
            Stuck s)
     | Expression e1' ->
        Expression (Opr (e1', opr, e2))
     | Stuck s ->
        Stuck s;;

Словами:

литерал сводится к значению;
если выражение e1 застрял, то и выражение тоже Opr (e1, opr, e2), для любого выражения e2;
если выражение e1 сводится к выражению e1', то для любого выражения e2, Opr (e1, opr, e2) сводится к Opr (e1', opr, e2);
если выражение e1 сводится к значению v1, затем
- если выражение e2 застрял, то и выражение тоже Opr (e1, opr, e2);
- если выражение e2 сводится к выражению e2', затем Opr (e1, opr, e2) сводится к Opr (e1, opr, e2');
- если выражение e2 сводится к значению v2, затем Opr (e1, opr, e2) это потенциальный редекс:
  - если этот потенциальный редекс является действительным, то его сжатие дает выражение; Opr (e1, opr, e2) сводится к этому выражению;
  - если этот потенциальный редекс не является реальным, то Opr (e1, opr, e2) застрял.

Оценка достигается путем итерационной редукции. Он возвращает либо значение, либо сообщение об ошибке:

type result = Normal_form of value | Wrong of string;;

let rec normalize_d (e : expression) : result =
  match reduce_d e with
    Value v ->
     Normal_form v
  | Expression e' ->
     normalize_d e'
  | Stuck s ->
     Wrong s;;

Эта одношаговая функция сокращения является структурно рекурсивной . Он реализует структурную операционную семантику для этого минималистичного языка арифметических выражений с ошибками.

Например, функция редукции неявно строит следующее дерево доказательства для выполнения шага редукции: $(1-(5+5))-(2-20)\rightarrow (1-10)-(2-20)$ :

                   ------------
                   5 + 5  -> 10
              ---------------------
              1 - (5 + 5) -> 1 - 10
 -----------------------------------------------
 (1 - (5 + 5)) - (2 - 20) -> (1 - 10) - (2 - 20)

Переформатирование этого дерева доказательств, чтобы подчеркнуть неявное разложение, дает:

                  -------------------------------------------------->
                ^                 contraction                         |
                |         -----------------------------               |
                |         5 + 5              ->      10               |
    implicit    |    ----------------------------------               | implicit
  decomposition |    1 - (5 + 5)             ->  1 - 10               | recomposition
                |   -----------------------------------------------   |
                |   (1 - (5 + 5)) - (2 - 20) -> (1 - 10) - (2 - 20)   v

Семантика редукции — это операционная семантика небольших шагов, в которой неявный контекст потенциального редекса становится явным. Таким образом, один шаг сокращения приводит к

построение контекста редекса,
стягивание этого редекса, и
перекомпоновка контекста вокруг контракта для получения сокращения:

  (1 - (5 + 5)) - (2 - 20)  \
 [(1 - (5 + 5)) - (2 - 20)] | explicit
 [[1 - (5 + 5)] - (2 - 20)] | decomposition
 [[1 - [5 + 5]] - (2 - 20)] /
                              contraction
 [[1 - [ 10  ]] - (2 - 20)] \
 [[1 -   10   ] - (2 - 20)] | explicit
 [(1 -   10   ) - (2 - 20)] | recomposition
  (1 -   10   ) - (2 - 20)  /

Наглядно арифметическое выражение вычисляется поэтапно:

         contract               contract               contract        
       o--------->o           o--------->o           o--------->o      
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o--------------------->o--------------------->o--------------------->o
          reduce                 reduce                 reduce

Преобразование функции одношагового сокращения в Continuation-Passing Style , разграничивающее продолжение от типа value_or_expression_or_stuck -> 'a печатать value_or_expression_or_stuck -> value_or_expression_or_stuck, и разбить это ограниченное продолжение на два (один для продолжения декомпозиции и один для повторного составления, используя изоморфизм типов между $A+B\rightarrow C$ и $(A\rightarrow C)\times (B\rightarrow C)$ ) упрощает реализацию соответствующей функции нормализации:

type value_or_decomposition_cc =
  Val_cc of value
| Dec_cc of potential_redex * (value -> value_or_decomposition_cc) * (expression -> expression);;

let rec decompose_expression_cc (e : expression) (kd : value -> value_or_decomposition_cc) (kr : expression -> expression) : value_or_decomposition_cc =
  match e with
    Lit n ->
     kd (Int n)
  | Opr (e1, opr, e2) ->
     decompose_expression_cc
       e1
       (fun v1 ->
         decompose_expression_cc
           e2
           (fun v2 ->
             Dec_cc (PR (v1, opr, v2), kd, kr))
           (fun e2' ->
             kr (Opr (expression_of_value v1, opr, e2'))))
       (fun e1' ->
         kr (Opr (e1', opr, e2)));;

let decompose_cc (e : expression) : value_or_decomposition_cc =
  decompose_expression_cc e (fun v -> Val_cc v) (fun e' -> e');;

let rec iterate_cc_rb (vod : value_or_decomposition_cc) : result =
  match vod with
    Val_cc v ->
     Normal_form v
  | Dec_cc (pr, kd, kr) ->
     (match contract pr with
        Contractum e ->
         iterate_cc_rb (decompose_cc (kr e))
      | Error s ->     (*^^^^^^^^^^^^^^^^^*)
         Wrong s);;

let normalize_cc_rb (e : expression) : result =
  iterate_cc_rb (decompose_cc e);;

В подчеркнутом коде контракт перекомпонуется, а результат декомпозируется. Говорят, что эта функция нормализации основана на редукции , поскольку она перечисляет все редукции в последовательности редукции.

Перефокусировка

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

Наглядно:

         contract    refocus    contract    refocus    contract        
       o--------->o---------->o--------->o---------->o--------->o------
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o                      o                      o                      o

Интенционально , тезис перефокусировки заключается в том, что вырубка лесов достигается за счет продолжения разложения контрактума в текущем контексте. ^[1] ^[2]

let rec iterate_cc_rf (vod : value_or_decomposition_cc) : result =
  match vod with
    Val_cc v ->
     Normal_form v
  | Dec_cc (pr, kd, kr) ->
     (match contract pr with
        Contractum e ->
         iterate_cc_rf (decompose_expression_cc e kd kr)
      | Error s ->     (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
         Wrong s);;

let normalize_cc_rf (e : expression) : result =
  iterate_cc_rf (decompose_cc e);;

В подчеркнутом коде декомпозиция продолжается. Говорят, что эта функция нормализации не содержит редукций , поскольку она не перечисляет ни одного из редуктов в последовательности редукции.

На практике два продолжения дефункциональны в традиционных контекстах первого порядка, вывернутых наизнанку, что дает реализацию Феляйзена и Хиба семантики редукции : ^[5] семантика малых шагов, разработанная независимо от продолжений и дефункционализации, но чье представление — как показано здесь — может быть получено путем CPS-преобразования и дефункционализации представления Структурной Операционной Семантики.

Набросанная выше конструкция полностью формализуется с помощью Coq Proof Assistant . ^[4]

Приложения

На протяжении многих лет перефокусировка использовалась для взаимосвязи исчислений и абстрактных машин. ^[6]^[7] Помимо машины CEK , машины Кривина и машины SECD , примеры также включают химическую абстрактную машину и абстрактные машины для JavaScript. ^[8]^[9]^[10] Бах Поулсен и Моссес также использовали перефокусировку для реализации структурной операционной семантики и модульной структурной операционной семантики. ^[11]

В более широком смысле, перефокусировка использовалась для создания систем типов и реализаций сопрограмм. ^[12] для перехода от проверки типа через сокращение к проверке типа через оценку, ^[13] для вывода классического секвентивного исчисления вызова по необходимости, ^[14] для получения интерпретаций постепенно типизированного лямбда-исчисления, ^[15] и для полного сокращения. ^[16]^[17]

Корректность

Дэнви и Нильсен сформулировали условия переориентации и неофициально доказали их. ^[2] Сечковский, Бернака и Бернацкий формализовали переориентацию с помощью Coq Proof Assistant . ^[18] Бах Поульсен доказал правильность перефокусировки для XSOS с помощью индукции правил. ^[19] Бернака, Харатоник и Зелинска обобщили перефокусировку с помощью Coq Proof Assistant . ^[20] Используя Agda , Свиестра доказал шаг перефокусировки как часть формализации синтаксического соответствия между $\lambda {\widehat {\rho }}$ исчисление со стратегией приведения нормального порядка и машиной Кривина . ^[21] Также используя Agda , Розовский доказал шаг перефокусировки как часть формализации синтаксического соответствия между $\lambda {\widehat {\rho }}$ исчисление с использованием стратегии сокращения аппликативного порядка и машины CEK . ^[22]

Ссылки

^ Jump up to: ^а ^б Дэнви, Оливье ; Нильсен, Лассе Р. (2001). Синтаксические теории на практике . Второй международный семинар по программированию на основе правил (RULE 2001). Том. 59. Электронные заметки по теоретической информатике. дои : 10.7146/brics.v9i4.21721 .
^ Jump up to: ^а ^б ^с Дэнви , Оливье; Нильсен, Лассе Р. (2004). Перефокусировка в семантике редукции (Технический отчет). БРИКС. дои : 10.7146/brics.v11i26.21851 . РС-04-26.
^ https://delimited-continuation.github.io/refocusing-arithmetic-expressions.ml
^ Jump up to: ^а ^б Дэнви , Оливье (2023). Вырубка лесов: переориентация (Технический отчет).
^ Феллизен, Матиас ; Хиб, Роберт (1992). «Пересмотренный отчет о синтаксических теориях последовательного управления и состояния». Теоретическая информатика . 103 (2): 235–271. дои : 10.1016/0304-3975(92)90014-7 .
^ Берначка, Малгожата; Дэнви, Оливье (2007). «Бетонная основа для экологических машин» . Транзакции ACM в вычислительной логике . 9 (1). Статья №6: 1–30. дои : 10.7146/brics.v13i3.21909 .
^ Берначка, Малгожата; Дэнви, Оливье (2007). «Синтаксическое соответствие между контекстно-зависимыми исчислениями и абстрактными машинами» . Теоретическая информатика . 375 (1–3): 76–108. дои : 10.7146/brics.v12i22.21888 .
^ Дэнви, Оливье ; Милликин, Кевин (2008). «Рациональная деконструкция машины SECD Ландина с оператором J». Логические методы в информатике . 4 (4): 1–67. arXiv : 0811.3231 . дои : 10.2168/LMCS-4(4:12)2008 . S2CID 7926360 .
^ Шербануц, Траян Флорин; Рошу, Григоре ; Месегер, Хосе (2009). «Переписывание логического подхода к операционной семантике» . Информация и вычисления . 207 (2): 305–340. дои : 10.1016/j.ic.2008.03.026 . hdl : 2142/11265 .
^ Ван Хорн, Дэвид; Возможно , Мэтью (2018). Аналитическая платформа для JavaScript (технический отчет).
^ Бах Поульсен, Каспер; Моссес, Питер Д. (2013). «Создание специализированных интерпретаторов модульной структурной операционной семантики». Логический синтез и преобразование программ . Конспекты лекций по информатике. Том. 8901. Синтез и преобразование логических программ, 23-й международный симпозиум, LOPSTR 2013. стр. 220–236. дои : 10.1007/978-3-319-14125-1_13 . ISBN 978-3-319-14124-4 .
^ Антон, Конрад; Тиманн, Питер (2010). Ввод сопрограмм . Том. 6546. Тенденции функционального программирования - 11-й Международный симпозиум (TFP). стр. 16–30.
^ Сергей, Илья (2012). Эксплуатационные аспекты систем типов: взаимовыводная семантика проверки типов и постепенные типы для владения объектом (Диссертация). КУ Левен.
^ Ариола, Зена М.; Даунен, Пол; Наката, Кейко; Саурин, Алексис; Хьюго, Гербелен (2012). Классические секвенциальные исчисления по требованию: единство семантических артефактов . Функциональное и логическое программирование, 11-й международный симпозиум, FLOPS 2012. Springer. стр. 32–46. дои : 10.1007/978-3-642-29822-6_6 .
^ Гарсиа-Перес, Альваро; Ногейра, Пабло; Сергей, Илья (2014). «Вывод интерпретаций постепенно типизированного лямбда-исчисления» . Материалы семинара ACM SIGPLAN 2014 по частичной оценке и управлению программами . Частичная оценка и манипулирование программами на основе семантики (PEPM 2014). стр. 157–168. дои : 10.1145/2543728.2543742 . ISBN 9781450326193 .
^ Мунк, Йохан (2007). Исследование синтаксических и семантических артефактов и его применение для определения лямбда-выражений, сильной нормализации и слабой нормализации при наличии состояния (Диссертация). Орхусский университет. дои : 10.7146/brics.v15i3.21938 .
^ Гарсиа-Перес, Альваро; Ногейра, Пабло (2014). «О синтаксическом и функциональном соответствии между гибридными (или многослойными) нормализаторами и абстрактными машинами» . Наука компьютерного программирования . 95 (2): 176–199. дои : 10.1016/j.scico.2014.05.011 .
^ Сечковский, Филип; Берначка, Малгожата; Бернацкий, Дариуш (2011). «Автоматизация вывода абстрактных машин из семантики редукции:: Общая формализация перефокусировки в Coq». Автоматизация вывода абстрактных машин из семантики редукции . Конспекты лекций по информатике. Том. 6647. Реализация и применение функциональных языков. стр. 72–88. дои : 10.1007/978-3-642-24276-2_5 . ISBN 978-3-642-24275-5 .
^ Бах Поульсен, Каспер (2015). Семантика расширяемой системы переходов (Диссертация). Университет Суонси.
^ Берначка, Малгожата; Харатоник, Витольд; Зелинская, Клара (2017). Генерализованная перефокусировка: от гибридных стратегий к абстрактным машинам . Том. 84. 2-я Международная конференция по формальным структурам вычислений и дедукции (FSCD 2017). стр. 1–17.
^ Свирстра, Воутер (2012). «От математики к абстрактной машине: формальный вывод исполняемой машины Кривина» . Электронные труды по теоретической информатике . 76 . Материалы четвертого семинара по математическо структурированному функциональному программированию (MSFP 2012): 163–177. arXiv : 1202.2924 . дои : 10.4204/EPTCS.76.10 . S2CID 14668530 .
^ Розовский, Войцех (2021). Формально проверенный вывод исполняемой и завершающей машины CEK из лямбда-p-hat-исчисления с вызовом по значению (PDF) (Диссертация). Университет Саутгемптона.

[danvy_nielsen_brics-01-1] Jump up to: ^а ^б Дэнви, Оливье ; Нильсен, Лассе Р. (2001). Синтаксические теории на практике . Второй международный семинар по программированию на основе правил (RULE 2001). Том. 59. Электронные заметки по теоретической информатике. дои : 10.7146/brics.v9i4.21721 .

[danvy_nielsen_brics-04-2] Jump up to: ^а ^б ^с Дэнви , Оливье; Нильсен, Лассе Р. (2004). Перефокусировка в семантике редукции (Технический отчет). БРИКС. дои : 10.7146/brics.v11i26.21851 . РС-04-26.

[3] ttps://delimited-continuation.github.io/refocusing-arithmetic-expressions.ml

[danvy_23-4] Jump up to: ^а ^б Дэнви , Оливье (2023). Вырубка лесов: переориентация (Технический отчет).

[felleisen_hieb_92-5] Феллизен, Матиас ; Хиб, Роберт (1992). «Пересмотренный отчет о синтаксических теориях последовательного управления и состояния». Теоретическая информатика . 103 (2): 235–271. дои : 10.1016/0304-3975(92)90014-7 .

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

[2biernacka_danvy_brics-07-7] Берначка, Малгожата; Дэнви, Оливье (2007). «Синтаксическое соответствие между контекстно-зависимыми исчислениями и абстрактными машинами» . Теоретическая информатика . 375 (1–3): 76–108. дои : 10.7146/brics.v12i22.21888 .

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

[şerbǎnuţǎ_et_al_ic-09-9] Шербануц, Траян Флорин; Рошу, Григоре ; Месегер, Хосе (2009). «Переписывание логического подхода к операционной семантике» . Информация и вычисления . 207 (2): 305–340. дои : 10.1016/j.ic.2008.03.026 . hdl : 2142/11265 .

[van_horn_might_18-10] Ван Хорн, Дэвид; Возможно , Мэтью (2018). Аналитическая платформа для JavaScript (технический отчет).

[bach-poulsen_mosses_lopstr-13-11] Бах Поульсен, Каспер; Моссес, Питер Д. (2013). «Создание специализированных интерпретаторов модульной структурной операционной семантики». Логический синтез и преобразование программ . Конспекты лекций по информатике. Том. 8901. Синтез и преобразование логических программ, 23-й международный симпозиум, LOPSTR 2013. стр. 220–236. дои : 10.1007/978-3-319-14125-1_13 . ISBN 978-3-319-14124-4 .

[anton_thiemann_tfp-10-12] Антон, Конрад; Тиманн, Питер (2010). Ввод сопрограмм . Том. 6546. Тенденции функционального программирования - 11-й Международный симпозиум (TFP). стр. 16–30.

[sergey_thesis_12-13] Сергей, Илья (2012). Эксплуатационные аспекты систем типов: взаимовыводная семантика проверки типов и постепенные типы для владения объектом (Диссертация). КУ Левен.

[ariola_et_al_flops-12-14] Ариола, Зена М.; Даунен, Пол; Наката, Кейко; Саурин, Алексис; Хьюго, Гербелен (2012). Классические секвенциальные исчисления по требованию: единство семантических артефактов . Функциональное и логическое программирование, 11-й международный симпозиум, FLOPS 2012. Springer. стр. 32–46. дои : 10.1007/978-3-642-29822-6_6 .

[garcía-pérez_et_al_pepm-14-15] Гарсиа-Перес, Альваро; Ногейра, Пабло; Сергей, Илья (2014). «Вывод интерпретаций постепенно типизированного лямбда-исчисления» . Материалы семинара ACM SIGPLAN 2014 по частичной оценке и управлению программами . Частичная оценка и манипулирование программами на основе семантики (PEPM 2014). стр. 157–168. дои : 10.1145/2543728.2543742 . ISBN 9781450326193 .

[munk_thesis_07-16] Мунк, Йохан (2007). Исследование синтаксических и семантических артефактов и его применение для определения лямбда-выражений, сильной нормализации и слабой нормализации при наличии состояния (Диссертация). Орхусский университет. дои : 10.7146/brics.v15i3.21938 .

[garcía-pérez_nogueira_scp-14-17] Гарсиа-Перес, Альваро; Ногейра, Пабло (2014). «О синтаксическом и функциональном соответствии между гибридными (или многослойными) нормализаторами и абстрактными машинами» . Наука компьютерного программирования . 95 (2): 176–199. дои : 10.1016/j.scico.2014.05.011 .

[sieczkowski_et_al_ifl-11-18] Сечковский, Филип; Берначка, Малгожата; Бернацкий, Дариуш (2011). «Автоматизация вывода абстрактных машин из семантики редукции:: Общая формализация перефокусировки в Coq». Автоматизация вывода абстрактных машин из семантики редукции . Конспекты лекций по информатике. Том. 6647. Реализация и применение функциональных языков. стр. 72–88. дои : 10.1007/978-3-642-24276-2_5 . ISBN 978-3-642-24275-5 .

[bach_poulsen_thesis_15-19] Бах Поульсен, Каспер (2015). Семантика расширяемой системы переходов (Диссертация). Университет Суонси.

[biernacka_et_al_fscd-17-20] Берначка, Малгожата; Харатоник, Витольд; Зелинская, Клара (2017). Генерализованная перефокусировка: от гибридных стратегий к абстрактным машинам . Том. 84. 2-я Международная конференция по формальным структурам вычислений и дедукции (FSCD 2017). стр. 1–17.

[swierstra_msfp-12-21] Свирстра, Воутер (2012). «От математики к абстрактной машине: формальный вывод исполняемой машины Кривина» . Электронные труды по теоретической информатике . 76 . Материалы четвертого семинара по математическо структурированному функциональному программированию (MSFP 2012): 163–177. arXiv : 1202.2924 . дои : 10.4204/EPTCS.76.10 . S2CID 14668530 .

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]