上一页

ⓘ 自由变量和约束变量




自由变量和约束变量
                                     

ⓘ 自由变量和约束变量

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

变量 x 成为 约束变量 ,比如

对于所有 ,x + 1 2 = x 2 + 2 x + 1。

存在 x 使得 x 2 = 2。

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

                                     

1. 例子

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

在表达式

∑ x = 1 10 f x, y, {\displaystyle \sum _{x=1}^{10}fx,y,}

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

在表达式

∑ y = 1 10 f x, y, {\displaystyle \sum _{y=1}^{10}fx,y,}

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

在表达式

∫ 0 ∞ x y − 1 e − x d x, {\displaystyle \int _{0}^{\infty }x^{y-1}e^{-x}\,dx,}

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

在表达式

lim h → 0 f x + h − f x h, {\displaystyle \lim _{h\rightarrow 0}{\frac {fx+h-fx}{h}},}

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

在表达式

∀ x ∃ y φ x, y, z, {\displaystyle \forall x\ \exists y\ \varphi x,y,z,}

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

                                     

1.1. 例子 变量约束算子

下列的

∑ x = 1 10 ∫ 0 ∞ ⋯ d x lim x → 0 ∀ x {\displaystyle \sum _{x=1}^{10}\\qquad \int _{0}^{\infty }\cdots \,dx\\qquad \lim _{x\to 0}\\qquad \forall x}

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

                                     

2. 形式解释

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

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

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

x 1, …, x n ↦ t {\displaystyle x_{1},\ldots,x_{n}\mapsto \operatorname {t} }

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

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

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

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

                                     

3. 参见

  • 开放句子
  • 闭包 计算机科学
  • 闭包 数学
  • lambda 提升
  • 原子句子
  • 句子 数理逻辑
  • 作用域 编程
  • 组合子逻辑