函數式編程：等價性和價值評估

Question

我正在閱讀關於SML的一些註釋，並且對作者的評論有點困惑。讓e ==> v指示評價值和e ~ e' 表明e是外延上等價於e'

作者寫道：

如果e ~ e'（包括t型），並有t類型的SML價值v ST e ~ v，則存在SML值v'（同樣是t），s.t. e' ==> v'和v ~ v'。

確保您注意到（和理解我們爲什麼不在這裏說，如果e ~ e'和e ~ v然後e' ==> v。

爲什麼不呢？

Answer 1

如果你開始e和e'是值v和v'已經，那麼第二個語句會說

如果v ~ v'和v ~ v，然後v' ==> v

這可以簡化爲

如果v ~ v'，然後v' ==> v

是外延性的完全相反的，因爲可以有例如

v = fn x => x + 0 
v' = fn x => x 

它們不是相同的值，而是延伸相等。

Answer 2

因爲那意味着兩者的語法值減少到相同的。但是，外延平等與句法平等不一樣。這意味着，粗略地說，程序沒有辦法將值分開。

特別注意，函數表達式本身就是值。但是具有不同主體的不同函數值可能仍然是相等的，因爲它們在應用於相同參數時會計算相同的結果。簡單的例子：

fun x => x 

和

fun x => let y = x in y 

兩個值是語法上不同但外延上相等。