Кто-нибудь знает машину Context-Environment (CE) (интерпретатор)?

Question

В настоящее время я изучаю семантику малого шага, используя машину Context-Environment для лямбда-исчисления.

В этом типе машины или, скажем, интерпретаторе, определение замыкания - это открытые лямбда-термины в паре с окружениемкомпонент, который определяет значение свободных переменных в замыкании.

При определении компонента среды в литературе говорится:

ρ ∈ Env = Var ⇀ Clo.

, которая предназначена для отображения переменной в замыкание.

Мой вопрос: почему закрытие?Это непросто понять.

Например, вы можете себе представить: Согласно определению замыкания, каждое выражение имеет свою среду и, следовательно, замыкание, тогда, если текущее выражение для оценки является переменной v,тогда мы можем сослаться на его среду для v, который вернет замыкание?Что это такое?Если значение переменной равно 5, почему бы просто не дать мне 5, а не замыкание ?

Answer 1

Эти примеры часто определяются в контексте λ-исчисления без констант:

terms ::=
        | x       variable
        | t₁ t₂   application
        | λx.t    abstraction

В этом случае только абстракции являются значениями: единственные значения (нормальные формызакрытые условия) имеют вид λx.t;действительно, x не является закрытым членом, и t₁ t₂ может быть дополнительно уменьшен.

При использовании пары (t,ρ) term-environment (идея состоит в том, что ρ сохраняет определения для свободных переменных t, вместо их замены (что является дорогостоящей операцией), значения в ρ сами могут иметь свободные переменные и, следовательно, должны нести свою собственную среду: среда должна быть Var → (Value * Env).Как и в этом ограниченном примере, единственными возможными значениями являются абстракции, мы называем пару лямбда и ее окружение «замыканием», поэтому Var → Clo.

Теперь вы можете захотеть добавить другие вещи в ваш языктакие как константы (5, true и т. д.), пары, определения, продолжения и т. д. Определение терминов будет расширено в каждом случае, и определение значений также может измениться, например 2 + 3 не будет значением, но 5 будет.Значение может захватывать или не захватывать переменные из среды: (λf.f x) делает, но 5 не делает.Однако мы сохраняем единообразное определение Env := Var → (Value * Env), поэтому нам не нужно различать их.

На самом деле вам не нужно, чтобы захваченная среда была точно такой жекак среда, которую вы имели во время создания стоимости.Вам нужно только сохранить привязки для значения, которое фактически зафиксировано в значении, например x в (λf. f x) (это называется «ослабление»).В частности, вы всегда можете выразить «замыкание» для 5 как (5, ∅).