查看“自由变量和约束变量”的源代码

在[[数学]]和其他涉及[[形式语言]]的学科中，包括[[数理逻辑]]和[[计算机科学]]，'''自由变量'''是在[[表达式]]中用于表示一个位置或一些位置的[[符号]]，某些明确的[[代换]]可以在其中发生，或某些运算（比如[[总和]]或[[量化]]）可以在其上发生。这个概念有关于'''占位符'''（它是以后会被{{tsl|en|String literal|文字串}}所替换），或表示未指定符号的[[通配符]]，但更加深入和复杂。

变量 ''x'' 成为'''约束变量'''，比如

:'对于所有 ''x''，(''x'' + 1)<sup>2</sup> = ''x''<sup>2</sup> + 2''x'' + 1'。

或

:'存在 ''x'' 使得 ''x''<sup>2</sup> = 2'。

在任何这种命题中，是否使用 ''x'' 或其他什么字母在逻辑上不重要。但是，在复合[[命题]]的其他地方再次使用同一个字母可能导致冲突。就是说，自由变量变成了约束的，并在支持公式的格式化的进一步工作中在某种意义上''退休''了。

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

在表达式
:<math>\sum_{x=1}^{10} f(x,y),</math>
中 ''y'' 是自由变量而 ''x'' 是约束变量（或虚变量）；因此这个表达式的值依赖于 ''y'' 的值。

在表达式
:<math>\sum_{y=1}^{10} f(x,y),</math>
中 ''x'' 是自由变量而 ''y'' 是约束变量；因此这个表达式的值依赖于 ''x'' 的值。

在表达式
:<math>\int_0^\infty x^{y-1} e^{-x}\,dx,</math>
中 ''y'' 是自由变量而 ''x'' 是约束变量；因此这个表达式的值依赖于 ''y'' 的值。

在表达式
:<math>\lim_{h\rightarrow 0}\frac{f(x+h)-f(x)}{h},</math>
中 ''x'' 是自由变量而 ''h'' 是约束变量；因此这个表达式的值依赖于 ''x'' 的值。

在表达式
:<math>\forall x\ \exists y\ \varphi(x,y,z),</math>
中 ''z'' 是自由变量而 ''x'' 和 ''y'' 是约束变量；因此这个表达式的[[真值]]依赖于 ''z'' 的值。

===变量约束算子===
下列的

:<math>\sum_{x=1}^{10}\qquad\qquad \int_0^\infty\cdots\,dx\qquad\qquad \lim_{x\to 0}\qquad\qquad \forall x</math>

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

==形式解释==

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

<div style="float:left; width:251px; border:1px; border-style:solid; padding:2px; margin-right:10px; text-align:center; font-size:smaller">
[[File:IMG_binding.gif]]
<br><math>\forall x\, (\exists y\, A(x) \vee B(z)) </math>
</div>
变量约束有关于三个事情：变量 ''v''，这个变量在表达式中的位置 ''a''，和形成 Q(''v'', ''P'') 的节点 ''n''。注意: 我们定义在表达式中位置为在这个语法树中的叶子节点。变量约束在这个位置在节点 ''n'' 之下的时候发生。

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

::<math> (x_1, \ldots , x_n) \mapsto \operatorname{t}</math>

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

在[[λ演算]]中，如果x 是项 M = &lambda; x. T 中的约束变量，而且是 T 中的自由变量，则我们称 x 在 M 中是约束的，在 T 中是自由的。如果 T 包含一个子项 &lambda; 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.''

[[Category:數理邏輯|Z]]
[[Category:數學表示法]]