程式語言/語義規範

程式語言的語義

語義，大致而言，是指賦予符號組的含義：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 是一種安全的語言（理論上；該模型沒有考慮實現，而實現可能存在導致安全漏洞的錯誤）。]