有人知道上下文环境（CE）机器（解释器）吗？

发布于 2024-10-19 19:07:02 字数 384 浏览 1 评论 0原文

我目前正在研究使用 Context-Environment 机器进行 lambda 演算的小步语义。

在这种机器中，或者说解释器中，闭包的定义是开放的 lambda 术语与定义闭包中自由变量含义的环境组件配对。

在定义环境组件时，文献中说：

ρ ∈ Env = Var ⇀ Clo.

就是将一个变量映射到一个闭包。

我的问题是：为什么要关闭？这并不容易理解。

例如，你可以想象：根据闭包的定义，每个表达式都有它的环境，因此也是一个闭包，那么如果当前要计算的表达式是一个变量v，那么我们可以为v引用它的环境，这将返回一个闭包？那是什么？如果变量的值为 5，为什么不直接给我 5，而不是一个闭包？

原文

I am currently studying the small-step semantics using Context- Environment machine for lambda calculus.

In this kind of machine, or say interpreter, the definition of the closure is open lambda terms paired with an environment component that defines the meaning of free variables in the closure.

When defining the environment component, the literature says:

ρ ∈ Env = Var ⇀ Clo.

which is to map an variable to a closure.

My question is:
Why closure? It is not straightforward to understand.

For example, you can imagine:
According to the definition of closure, every expression has its environment, and thus a closure, then if the current expression to evaluate is a variable v, then we can reference to its environment for v, which will return a closure? What's that? If the variable's value is 5, why not just give me 5, rather than a closure?

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

把昨日还给我 2024-10-26 19:07:02

这些例子通常是在 λ 演算的背景下定义的，而不需要
常量：

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

在这种情况下，只有抽象是值：唯一的值（正常
封闭项的形式）的形式为λx.t；事实上，x 不是
封闭项和t₁ t2 可以进一步减少。

当使用 (t,ρ) 术语-环境对时（其想法是 ρ
保留 t 自由变量的定义，而不是替换
他们离开这是一个昂贵的操作），ρ 中的值可能有免费的
变量本身，因此需要携带自己的变量
环境：环境应该是Var → (Value * Env)。正如在这个
受限示例，唯一可能的值是抽象，我们命名为
一对 lambda 及其环境是一个“闭包”，因此 Var → Clo。

现在您可能想向您的语言添加其他内容，例如
常量（5、true 等）、对、let 定义、延续、
等等。术语的定义将在每种情况下进行扩展，并且
值的定义也可能会改变，例如 2 + 3 不会改变
一个值，但 5 会。值可能会或可能不会捕获来自
环境：(λf.fx) 可以，但 5 不会。然而，我们保留
Env := Var → (Value * Env) 的统一定义，这样我们就不会
必须区分它们。

您实际上并不需要捕获的环境完全
与您获得该值时的环境相同
建造。您只需要保留以下值的绑定
实际上在值中捕获，例如 (λf.fx) 中的 x （这是
称为“弱化”）。特别是，你总是可以表达
5 的“闭包”为 (5, ∅)。

Those examples are often defined in the context of λ-calculus without
constants :

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

In this case, only abstractions are values : the only values (normal
forms of a closed terms) are of the form λx.t; indeed, x is not
a closed term and t₁ t₂ can be further reduced.

When using an (t,ρ) term-environment pair (the idea is that ρ
keeps definitions for free variables of t, instead of substituting
them away which is a costly operation), the values in ρ may have free
variables themselves, and therefore need to carry their own
environment : environment should be Var → (Value * Env). As in this
restricted example, the only possible values are abstractions, we name
a pair of a lambda and its environment a "closure", hence Var → Clo.

Now you may want to add other things to your language, such as
constants (5, true, etc.), pairs, let-definitions, continuations,
etc. The definition of terms will be extended in each case, and the
definition of values may also change, for example 2 + 3 won't be
a value but 5 will. Value may or may not capture variables from the
environment : (λf.f x) does, but 5 doesn't. However, we keep the
uniform definition of Env := Var → (Value * Env), so that we don't
have to distinguish between those.

You don't actually need the captured environment to be exactly the
same as the environment you had at the time of the value
construction. You only need to keep bindings for the value that are
actually captured in the value, such as x in (λf. f x) (this is
called "weakening"). In particular, you can always express the
"closure" for 5 as (5, ∅).