基本介紹
定義,例子,變數約束運算元,形式解釋,
定義
在數學和其他涉及形式語言的學科中，包括數理邏輯和計算機科學，自由變數是在表達式中用於表示一個位置或一些位置的符號，某些明確的代換可以在其中發生，或某些運算（比如總和或量化）可以在其上發生。這個概念有關於占位符（它是以後會被文字串所替換），或表示未指定符號的通配符，但更加深入和複雜。
變數x成為約束變數，比如
'對於所有x，(x+ 1)=x+ 2x+ 1'。
或
'存在x使得x= 2'。
在任何這種命題中，是否使用x或其他什麼字母在邏輯上不重要。但是，在複合命題的其他地方再次使用同一個字母可能導致衝突。就是說，自由變數變成了約束的，並在支持公式的格式化的進一步工作中在某種意義上退休了。
例子
在陳述自由變數和約束變數（或虛變數）的嚴格定義之前，我們會給出一些例子，使這兩個概念比定義看起來更加清楚：
在表達式
中y是自由變數而x是約束變數（或虛變數）；因此這個表達式的值依賴於y的值。
在表達式
中x是自由變數而y是約束變數；因此這個表達式的值依賴於x的值。
在表達式
中y是自由變數而x是約束變數；因此這個表達式的值依賴於y的值。
在表達式
中x是自由變數而h是約束變數；因此這個表達式的值依賴於x的值。
在表達式
中z是自由變數而x和y是約束變數；因此這個表達式的真值依賴於z的值。
變數約束運算元
下列的
都是變數約束運算元，它們都約束變數x。
形式解釋
變數約束機制出現在數學、邏輯和計算機科學中的不同情況中，但是在所有情形下它們是其中的表達式和變數的純粹語法性質。本節中我們用葉子節點是變數、函式常量或謂詞常量，而節點是邏輯運算符的樹，識別表達式來總結語法。變數約束的運算符是幾乎出現在所有形式語言中的邏輯運算符。沒有它們的語言實際上要么是非常缺乏表達能力，要么非常難於使用。約束的運算符 Q 接受兩個參數：變數v和表達式P，把 Q 套用於它的參數時就會生成新表達式 Q(v,P) 。約束運算符的意義由這個語言的語義提供而不是我們現在關心的。
變數約束有關於三個事情：變數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 的自由出現。
在程式頂層的變數約束在技術上在它們所約束的項之內是自由變數，但是經常特殊對待，因為它們可以被編譯為固定地址。類似的，約束於遞歸函式的標識符被稱為在它歸屬的函式體內是自由變數但要特殊對待。
封閉項是不包含自由變數的項。
