例子

在陈述自由变量和约束变量（或虚变量）的严格定义之前，我们会给出一些例子，使这两个概念比定义看起来更加清楚：

在表达式

中 y 是自由变量而 x 是约束变量（或虚变量）；因此这个表达式的值依赖于 y 的值。

在表达式

中 x 是自由变量而 y 是约束变量；因此这个表达式的值依赖于 x 的值。

在表达式

中 y 是自由变量而 x 是约束变量；因此这个表达式的值依赖于 y 的值。

在表达式

中 x 是自由变量而 h 是约束变量；因此这个表达式的值依赖于 x 的值。

在表达式

中 z 是自由变量而 x 和 y 是约束变量；因此这个表达式的真值依赖于 z 的值。

变量约束算子

下列的

都是变量约束算子，它们都约束变量 x。

形式解释

变量约束机制出现在数学、逻辑和计算机科学中的不同情况中，但是在所有情形下它们是其中的表达式和变量的纯粹语法性质。本节中我们用叶子节点是变量、函数常量或谓词常量，而节点是逻辑运算符的树，识别表达式来总结语法。变量约束的运算符是几乎出现在所有形式语言中的逻辑运算符。没有它们的语言实际上要么是非常缺乏表达能力，要么非常难于使用。约束的运算符 Q 接受两个参数：变量 v 和表达式 P，把 Q 应用于它的参数时就会生成新表达式 Q(v, P) 。约束运算符的意义由这个语言的语义提供而不是我们现在关心的。

∀ ∀ -->x(∃ ∃ -->yA(x)∨ ∨ -->B(z)){\displaystyle \forall x\,(\exists y\,A(x)\vee B(z))}

变量约束有关于三个事情：变量 v，这个变量在表达式中的位置 a，和形成 Q(v, P) 的节点 n。注意: 我们定义在表达式中位置为在这个语法树中的叶子节点。变量约束在这个位置在节点 n 之下的时候发生。

举个数学的例子，考虑定义了一个函数的表达式

这里的 t 是一个表达式。t 可以包含某些、所有的、或者不包含 x1, ..., xn的任意一个，并可以包含其他变量。在这种情况下我们称函数的定义约束了这些变量 x1, ..., xn。

在λ演算中，如果x 是项 M = λ x. T 中的约束变量，而且是 T 中的自由变量，则我们称 x 在 M 中是约束的，在 T 中是自由的。如果 T 包含一个子项 λ x . U，则 x 在这个项中是再约束的。这种嵌套的、内层的 x 的约束被称为外层约束的"阴影"。 x 在 U 中的出现是新 x 的自由出现。

在程序顶层的变量约束在技术上在它们所约束的项之内是自由变量，但是经常特殊对待，因为它们可以被编译为固定地址。类似的，约束于递归函数的标识符被称为在它归属的函数体内是自由变量但要特殊对待。

封闭项是不包含自由变量的项。

参见

闭包 (计算机科学)

闭包 (数学)

lambda 提升

作用域 (编程)

组合子逻辑

句子 (数理逻辑)

原子句子

开放句子

引用

A small part of this article was originally based on material from the Free On-line Dictionary of Computing and is used with permission under the GFDL. Most of what now appears here is the result of later editing.

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。