自由變量和約束變量

在數學和其他涉及形式語言的學科中，包括數理邏輯和計算機科學，自由變量是在表達式中用於表示一個位置或一些位置的符號，某些明確的代換（英語：Substitution_(logic)）可以在其中發生，或某些運算（比如總和或量化）可以在其上發生。這個概念有關於佔位符（它是以後會被文字串（英語：String literal）所替換），或表示未指定符號的通配符，但更加深入和複雜。

變量x成為約束變量，比如

對於所有 x，(x + 1)² = x² + 2x + 1。

或

存在x，使得 x² = 2。

在任何這種命題中，是否使用x或其他什麼字母在邏輯上不重要。但是，在複合命題的其他地方再次使用同一個字母可能導致衝突。就是說，自由變量變成了約束的，並在支持公式的格式化的進一步工作中在某種意義上「退休」了。

例子

在陳述自由變量和約束變量（或虛變量）的嚴格定義之前，我們會給出一些例子，使這兩個概念比定義看起來更加清楚：

在表達式

${\displaystyle \sum _{x=1}^{10}f(x,y),}$

中y是自由變量而x是約束變量（或虛變量）；因此這個表達式的值依賴於y的值。

在表達式

${\displaystyle \sum _{y=1}^{10}f(x,y),}$

中x是自由變量而y是約束變量；因此這個表達式的值依賴於x的值。

在表達式

${\displaystyle \int _{0}^{\infty }x^{y-1}e^{-x}\,dx,}$

中y是自由變量而x是約束變量；因此這個表達式的值依賴於y的值。

在表達式

${\displaystyle \lim _{h\rightarrow 0}{\frac {f(x+h)-f(x)}{h}},}$

中x是自由變量而h是約束變量；因此這個表達式的值依賴於x的值。

在表達式

${\displaystyle \forall x\ \exists y\ \varphi (x,y,z),}$

中z是自由變量而x和y是約束變量；因此這個表達式的真值依賴於z的值。

變量約束算子

下列的

${\displaystyle \sum _{x=1}^{10}\qquad \qquad \int _{0}^{\infty }\cdots \,dx\qquad \qquad \lim _{x\to 0}\qquad \qquad \forall x}$

都是變量約束算子，它們都約束變量x。

形式解釋

變量約束機制出現在數學、邏輯和計算機科學中的不同情況中，但是在所有情形下它們是其中的表達式和變量的純粹語法性質。本節中我們用葉子節點是變量、函數常量或謂詞常量，而節點是邏輯運算符的樹，識別表達式來總結語法。變量約束的運算符是幾乎出現在所有形式語言中的邏輯運算符。沒有它們的語言實際上要麼是非常缺乏表達能力，要麼非常難於使用。約束的運算符 Q 接受兩個參數：變量v和表達式P，把 Q 應用於它的參數時就會生成新表達式 Q(v, P) 。約束運算符的意義由這個語言的語義提供而不是我們現在關心的。

${\displaystyle \forall x\,(\exists y\,A(x)\vee B(z))}$

變量約束有關於三個事情：變量v，這個變量在表達式中的位置a，和形成 Q(v, P) 的節點n。注意: 我們定義在表達式中位置為在這個語法樹中的葉子節點。變量約束在這個位置在節點n之下的時候發生。

舉個數學的例子，考慮定義了一個函數的表達式

${\displaystyle (x_{1},\ldots ,x_{n})\mapsto \operatorname {t} }$

這裏的t是一個表達式。t可以包含某些、所有的、或者不包含x₁, ..., x_n的任意一個，並可以包含其他變量。在這種情況下我們稱函數的定義約束了這些變量 x₁, ..., x_n。

在λ演算中，如果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.