编程语言/语义规范

编程语言的语义

语义，大致而言，是指赋予符号组的含义：ab+c，“ab”+“c”，mult(5,4)。

例如，为了表达用 5 加 4 的语法，我们可以说：在 5 和 4 之间放置一个“+”号，得到“5 + 4”。但是，我们还必须定义 5+4 的语义。如果我们使用算术语义，那么 5+4 将表示/等价于 (=) 9。

在计算机科学中，编程语言的作者“可以”使用或创建“+”的新定义。例如，“+”可以定义为算术减法 (-)。然而，更常见的是，“+”被定义为复数的函数（接收一个值以输出另一个值），甚至字符串（一个有序的符号集合），如“123a”、“aFsd”和“./etc”。

语义绝非仅仅是理论或哲学。编程语言的许多特性只有通过严格分析才能确定。例如，我们希望能够做出诸如“这种编程语言是安全的”之类的陈述。但要证明一种编程语言是安全的，仅仅讨论该语言的语法是不够的。如果没有正式的安全证明，系统可能容易受到许多相互作用的独立问题的意外后果的影响。一种进行此类证明的方法是使用数学模型。

有了某种编程语言的语义，我们可以选择用这种基础语言来描述其他编程语言。因此，一种指定编程语言语义的方法是将其与另一种语言相关联。然而，这会产生一个自举问题：最初的基础语言应该用什么？编程语言研究人员通过使用最初为逻辑而发明的数学模型解决了这个问题，该模型具有广泛的计算应用：Lambda 演算。

Lambda 演算是由 Church、Kleene 和其他人于 1920 年代和 1930 年代发明的，是最简单的图灵完备语言之一。它只有一种值：函数；并且只有两种操作：定义函数和调用函数。为了更简单起见，函数只允许有一个参数。

在接下来的讨论中，请将您的思维调整为思考接受函数作为参数并返回其他函数作为值的函数。这是一个非常抽象的概念，但正如我们将要发现的那样，很快我们就可以通过巧妙的定义来构建这种语言，使其看起来更像我们习惯使用的编程语言。例如，我们将探索的第一个技巧是如何在每个函数只能接收一个参数的情况下，实现允许接收多个参数的效果。

构建操作

在我们开始使用 Lambda 演算之前，让我们先用更标准的编程语言来解决一个难题。假设 Java 只有二元“<”运算符，我们需要定义函数来提供“>”、“>=”和“<=”运算符。我们也没有一元运算符，但我们仍然有 if 语句。

首先，让我们看看我们得到了什么

 // < - Returns true if a is less than b
 public static boolean lessThan(int a, int b) { ... }

我们的任务是定义 greaterThan、greaterThanOrEqualTo 和 lessThanOrEqualTo。请记住，对于这个难题，我们只能调用 lessThan，使用 if 语句，并返回布尔值。请在继续阅读之前想想如何做到这一点。

第一个函数并不太复杂

 // > - Returns true if a is greater than b
 public static boolean greaterThan(int a, int b) {
   return lessThan(b, a);
 }

这是有效的，因为每当我们有 $b<a$ 时，我们已经知道 $a>b$。我们可以使用类似的推理来编写 greaterThanOrEqualTo 和 lessThanOrEqualTo 的实现

 // >= - Returns true if a is greater than or equal to b
 public static boolean greaterThanOrEqualTo(int a, int b) {
   return not(lessThan(a, b));
 }
 
 // <= - Returns true if a is less than or equal to b
 public static boolean lessThanOrEqualTo(int a, int b) {
   return greaterThanOrEqualTo(b, a);
 }
 
 // ! - Returns the negation of b
 public static boolean not(boolean b) {
   if (b)
     return false;
   else
     return true;
 }

在 greaterThanOrEqualTo 的定义中，我们实际上是在否定 lessThan 的结果。因此，当 $a\not <b$ 时，我们返回 true，而当 $a<b$ 时，我们返回 false。但是，当 $a\not <b$ 时，我们知道 $a\geq b$；在这种情况下，我们必须返回 true，并且我们确实返回了。类似地，当 $a<b$ 时，我们知道不可能出现 $a\geq b$ 的情况，因此我们正确地返回了 false。

有了这些定义，我们可以定义 equalTo 和 notEqualTo

 // == - Returns true if a equals b
 public static boolean equalTo(int a, int b) {
   if (greaterThanOrEqualTo(a, b))
     return greaterThanOrEqualTo(b, a);
   else
     return false;
 }
 
 // != - Returns true if a does not equal b
 public static boolean notEqualTo(int a, int b) {
   return not(equalTo(a, b));
 }

现在我们开始以能够让我们在 Lambda 演算中构建操作的方式思考。我们不仅需要发明 < 和 ==，还需要发明数字、布尔值、所有数字运算、所有关系运算、链表、if 表达式、循环结构，甚至输出和其他副作用的模型。

Lambda 演算的内置操作

以下是完整 lambda 演算语言的语法

expr ::= "λ" id "." expr         abstraction, anonymous function definition
expr ::= expr expr               application, calling a function
expr ::= id                      variable use
expr ::= "(" expr ")"            grouping

我们还将引入另一种表示法，以便我们可以创建简写。

definition ::= "let" id "=" expr

在进行这样的“let”声明后，应该将标识符扩展为等式右侧的表达式。我们还将包含另一种形式的括号，它们与已经定义的圆括号没有区别。

expr ::= "[" expr "]"

由于该语言没有太多标点符号，因此将使用大量的括号，因此通过允许两种不同类型的括号，可读性得到提高（因为您可以更好地直观地匹配分组的开始和结束位置）。

最后，标识符可以是任何字符序列，只要它们不是已经具有其他含义的标记。

id ::= $\langle$any printable, non-whitespace characters except ()[]=.;, "let", and "λ"$\rangle$

因此，与大多数编程语言不同，在 lambda 演算中，“0”、“+”、“%”和“15”都是有效的标识符，就像“i”、“x”、“y1”、“remainder”和“theReturnValue”在更常见的编程语言中都是标识符一样。

我们将使用“;”作为行注释。

抽象：定义函数

我们将通过与假设的类似 Java 的语言进行比较来开始指定 lambda 演算规则。抽象规则，

expr ::= "λ" id "." expr

允许我们创建新函数。lambda 符号“λ”标记正在定义一个新函数，其后的标识符是其参数的名称。点“.”之后的表达式是一个表达式，它可能引用参数和作用域内的任何其他变量。请注意，函数在 lambda 演算中没有名称。如果我们想命名它们，我们需要使用“let”形式来创建简写。

看起来我们到目前为止无法定义任何东西。您可能想到的第一个函数是恒等函数

λx. x

也就是说，对于您提供的任何 x，您都会得到 x。为了避免每次想要使用恒等函数时都不断编写λx. x，我们可以创建一个简写

let identity = λx. x

然后引用identity，这与引用语法更重的λx. x相同。

在 Java 中，相同的定义看起来更像这样

public static Function identity(Function x) {
  return x;
}

由于 lambda 演算中唯一的数值或类型是函数，因此参数和返回值都是假设的“Function”类型。

应用：调用函数

应用规则

expr ::= expr expr

允许我们应用（或“调用”）函数。假设“f”是一个函数，“a”是它的参数。要将 f 应用于 a，我们只需将它们并置在一起

f a

由于括号只是提供分组，并且由于f和a已经是终端元素，因此以下所有内容都等效于上述内容

f(a)
(f a)
((f) a)
((f) (a))
(f)a

假设f是我们在假设的类似 Java 的语言中 Function 的一个实例。我们可能会这样编写函数应用

f.apply(a)

这意味着“将f应用于a”。

β-归约

应用的实际语义是替换规则（也称为β-归约规则）。当f是一个 lambda 函数，a是某个值，并且它们并置在一起时，就会发生应用。假设f的参数名为x，并且某个表达式expr使用了x。然后

f a

与以下内容相同

(λx. expr) a

应用表示将所有x的出现都替换为a。我们将这种替换写为

expr [a/x]

鉴于我们之前的恒等函数，我们可以将其应用于元素。所以，

identity a

与以下内容相同

(λx. x) a

这与以下内容相同

x [a/x]

在替换之后，它变为

a

同样，

identity identity

这等效于说

(λx. x) (λx. x)

这与以下内容相同

x [(λx. x)/x]

在替换之后，它变为

(λx. x)

或者，也就是说，恒等函数本身。

优先级顺序

• 从左到右

多个参数和词法作用域

目前，lambda 演算似乎除了创建恒等函数并将其应用于自身之外，不能做更多的事情。为了在该语言中取得进一步进展，我们需要开始将抽象运算视为一个真正意义上的运算。例如，与其定义恒等函数，不如定义一个创建恒等函数的函数

λy. λx. x

这应该被解释为“给定任何 y，返回恒等函数”。

以前在我们的 lambda 函数体中，我们只返回参数。上面的例子表明我们还有另一个选择：返回我们在其中定义的函数的参数。例如，以下内容意味着什么？

λy. λx. y

此函数应被解释为“给定任何 y，返回一个函数，该函数给定任何 x，始终返回 y。”换句话说，它创建一个常数函数，我们在数学中将其表示为图形上的水平线。（图形上的恒等函数将是一条 45 度角的直线，穿过原点。）本节展示了如何使用这种新选项来表达丰富的概念。特别是，本节展示了如何模拟接受多个参数的函数。

您可以考虑通过从只接受单个参数的函数开始来模拟接受多个参数的函数的一种方法是将所有参数组合成一个单元（就像复数包含两个浮点数一样）并传递该单元。这种技术可以描述为元组技术：只要您可以传递一个实际上是多个值的集合的参数，它与首先传递这些多个值实际上没有区别。

您可以使用元组技术，但 lambda 演算中没有元组类型：唯一的类型是接受单个参数的函数。但请回想上面两个使用x和y的函数。因为函数λy创建了λx函数，所以λx函数可以使用x和y中的任何一个。

考虑这个问题的一种方法是关注一个特定的例子。因此，假设您想要定义一个新的函数，该函数接受参数a、b和c，并对这些值进行一些计算。您可以将此函数视为一台机器。限制是，在 lambda 演算中，这些机器只能接受一个值。但是，对于可以返回的内容没有严格的限制。因此，首先考虑一台只能接受a的机器：因为它不知道b或c，所以它无法进行所需的计算。但因为它知道a，所以它可以返回一台也知道a的新机器。因为该机器也接受一个参数，所以我们可以将其设为b。因此，您现在拥有一台知道a和b但不知道c的机器。因此，这台机器应该依次创建一台知道a和b并接受参数c的机器。一旦该机器获得了c，它将能够使用所有三个值进行计算。

为了使这个概念更清晰，假设您想要创建一个可以进行加法的机器。也就是说，某种函数，其含义可能是“给定任何 n 和 m，返回 n + m 的和”。如果我们首先创建一个更原始的函数，即create-adder，我们可以实现这种效果。我们不会立即实现create-adder，但我们将假设它存在，并具有这样的规范

; create-adder: given n, returns a function that adds n to its argument
let create-adder = λn. (details left out for the moment)

假设create-adder存在，定义加法就非常容易了

let + = λn.λm. ((create-adder n) m)

首先，不要被“+”绊倒。它只是一个像其他任何标识符一样的符号。我们完全可以将此函数的简写设为“plus”或“add”，而不是“+”。那么，“+”函数本身是什么？

读取“+”的方式是：“给定任何 n，返回一个函数，该函数给定任何 m，返回 n + m。”假设 5 和 4 被定义为值（我们很快将展示如何做到这一点），那么“+”可以用来将它们相加

((+ 5) 4)

在这里，首先将“+”应用于 5，然后将该结果应用于 4。由于在高级别，“+”被认为是接受两个参数的，因此如果我们删除一些括号，它可能更容易理解

(+ 5 4)

这仍然意味着相同的事情：将“+”应用于 5，然后将该结果应用于 4（如果我们删除所有括号，在这种情况下它仍然会表示相同的意思）。这种调用函数的方式也与前缀表示法相同。

但是，“+”函数究竟是如何返回“n + m”的呢？其主体是

((create-adder n) m)

在这里，将create-adder传递给 n。根据定义，它将返回一个函数，该函数给定任何数字，将返回 n 与该数字的和。然后，我们立即将该函数应用于 m，从而得到 n + m 的和。

这种技巧被称为柯里化，是我们在语言本身只允许单个参数函数的情况下实现多个参数的方式。

创建更丰富的函数

现在我们已经看到了一种在函数只接受单个参数的语言中添加多个参数的方法，我们可以探索其他扩展。为了创建更多编程结构，我们不仅需要创建控制流语句，还需要创建新的值。

我们完全构建的唯一值是：(1) 恒等函数；(2) 返回恒等函数的函数；以及 (3) 返回常数函数的函数。

布尔值和条件语句

我们要创建的第一个值是布尔值 true 和 false。我们一开始可以简单地将 true 定义为恒等函数，然后让 false 为返回恒等函数的函数，但这样可能会发现很难让这些定义变得有用。

相反，在定义 true 和 false 之前，我们应该先问自己，如果我们有了 true 和 false，我们想用它们做什么？

一个理想的特性是我们可以执行 if 操作。我们可以将 if 视为一个三参数函数，它接受一个布尔值，一个“then”值，还有一个“else”值。

if cond A B

注意，if 不是一个关键字，它只是我们使用的符号。我们希望定义它，以便当“cond”为 true 时

if cond A B

简化为

A

当“cond”为 false 时，则

if cond A B

简化为

B

为了达到这一点，我们可以将 true 视为一个有两个参数的函数，一个 t 参数和一个 f 参数，并返回 t。

let true = λt. λf. t

我们可以将 false 视为一个有两个参数的函数，一个 t 参数和一个 f 参数，并返回 f。

let false = λt. λf. f

这样一来，定义 if 就很简单了。

let if = λcond. λA. λB. cond A B

这里，布尔值本身（名为 cond）承担了所有的繁重工作：布尔值同时接受 A 和 B。如果布尔值为真，它应该返回 A，如果布尔值为假，它应该返回 B。根据我们对 true 和 false 的精心定义，这就是将要发生的事情。

[待办事项：修改此内容：目前，我们应该假设某种形式的惰性求值，以便“then”和“else”值不会同时被求值（这可能会导致无限循环）。]

逻辑运算

现在我们已经对 true 和 false 有了合适的定义，甚至有了 if 结构，我们可以非常简单地定义其他布尔运算。这让我们想起之前在 Java 中使用 lessThan 和其他关系函数所做的练习。

not: 布尔值的逻辑非运算。

let not = λb.
  if b
    false
    true

你可能已经注意到，实际上并不需要 "if"，因为我们可以将其删除并直接将值传递给布尔值。

let not = λb. b false true

我们使用 if 只是为了提高可读性。

and: 两个布尔值的逻辑与运算。如果 b 为真，则返回 c，否则返回 false。因此，只有当 b 和 c 都为真时，它才返回 true。

let and = λb. λc.
  if b
    c
    false

or: 逻辑或运算：只有当 b 和 c 都为假时才返回 false。

let or = λb. λc.
  if b
    true
    c

xor: 逻辑异或运算：当 b 和 c 不同时返回 true，否则返回 false。

let xor = λb. λc.
  if b
    (not c)
    c

bool-eq: 布尔值相等性：如果 b 和 c 的值相同，则返回 true。

let bool-eq = λb. λc.
  if b
    c
    (not c)

注意，beq 也可以写成 not (xor b c)。

整数

Church 数 -- 对于所有 n>=0：第 n 个 Church 数接受一个“零”值 z 并对该零值应用给定的“后继”函数 s n 次。用代数术语来说，0 = z（即，不对 z 应用 s），而 1 = s(z)，2 = s(s(z))，3 = s(s(s(z)))，等等。

let 0 = λs. λz. z
let 1 = λs. λz. s z

后继函数：对给定的数字再应用一次后继函数。

let succ = λn.
  λs. λz.
    s (n s z)

is-zero?：如果传入的数字等于零，则返回 true。这是通过将零函数设为“true”，将后继函数设为始终返回“false”的函数来实现的。因此，只有当后继函数应用零次时，结果才会为 true。

let is-zero? = λn. n (λx. false) true

一个使用柯里化的简洁版本是：{ n (and false) true }，这可能更容易理解。

加法：返回 n 和 m 的和。

let + = λn. λm. n succ m

[待办事项：我还见过这种更长的形式，我不确定为什么使用它：]

let + = λs. λz. m s (n s z)

乘法：返回 n 和 m 的积，通过对 0 应用“将 n 加到自身”操作 m 次来实现。

let * = λn. λm. m (+ n) 0

自然数指数：将 n 乘以 m 次方。

let pow = λn. λm. m (* n) 1

列表

减法比较棘手，因此我们需要先定义对。

let pair = λfirst. λsecond. λbool. bool first second

提取对的第一个元素。

let first = λpair. pair true

提取对的第二个元素。

let second = λpair. pair false

cons、car、cdr：将对视为列表。

let cons = pair
let car = first
let cdr = second

减法

现在，回到减法：关键思想是从一个接受一对数字 (a, b) 并返回 (a+1, a) 的操作开始。

let next-pair = λp. pair (succ (first p)) (first p)

现在注意到，如果我们以 (0, 0) 作为零，以 next-pair 作为后继函数，对后继函数应用 n 次将得到以下结果。

times applied   value of pair   value of pair in terms of n
-------------   -------------   ---------------------------
n =         0   (0, 0)          (n, n)
n =         1   (1, 0)          (n, n - 1)
n =         2   (2, 1)          (n, n - 1)
n =         3   (3, 2)          (n, n - 1)
n =         4   (4, 3)          (n, n - 1)

因此，请注意，(n next-pair (pair 0 0)) 对于 n >= 1，会生成对 (n, n - 1)，而对于 n = 0，会生成 (0, 0)。如果我们希望 n 的前驱对于 n >= 1 为 n - 1，对于 n = 0 为 0，我们只需要取这对的第二个元素！这就是我们实现前驱的方式。

let pred = λn. second (n next-pair (pair 0 0))

减法：返回 $n-m$；但如果该值为负，则返回 0。

let - = λn. λm. m pred n

关系运算和除法

现在我们有了减法，就可以比较数字了。

n 是否大于或等于 m？

let >= = λn. λm. is-zero? (- m n)

n 是否小于或等于 m？

let <= = λn. λm. >= m n

n 是否小于 m？

let < = λn. λm. not (>= n m)

n 是否大于 m？

let > = λn. λm. not (>= m n)

equal: n 和 m 是否是相同的数字？

let equal = λn. λm. and (>= n m) (>= m n)

not-equal: n 和 m 是否是不同的数字？

let not-equal = λn. λm. not (equal n m)

div: 给定分子 n 和分母 d，返回商。

let / = λn. λd.
  (if (< n d)
     0          ; -- (n < d)
     (if (equal n d)
        1          ; -- (n == d)
        ; subtract d from n until the value is < d -- (n > d)
        (n
          [λn'.
            (if (< n' d)
               n'
               (- n' d))] n)))

mod: 给定分子 n 和分母 d，返回余数。

let mod = λn. λd. (- n (* (/ n d) d))

Y 组合子

不动点 Y 组合子（按值调用），用于实现递归。

let fix = λf.
  [λx. f (λy. x x y)] [λx. f (λy. x x y)]

Y: fix 的别名。

let Y = fix

用基本类型扩展的 Lambda 演算

[待办事项：讨论这种扩展。通常通过扩展 Lambda 演算，我们可以建立编程语言模型。一个例子是 Feather-weight Java，它被用于证明 Java 是一种安全的语言（理论上；该模型没有考虑实现，而实现可能存在导致安全漏洞的错误）。]