使用伊莎貝爾之間平等方面有一些

Question

我有點驚訝，

value "let x = SOME n. n ∈ {1::int,2} in x = x" 

回報True。 β擴張和α重命名後，該術語與以下內容相同：

value "(SOME na. na ∈ {1::int,2}) = (SOME nb. nb ∈ {1::int,2})" 

我不明白爲什麼這種平等應該成立。爲什麼選擇na的值應該與nb的值相同？

Answer 1

左側的術語與右側的術語（模數阿爾法轉換）完全相同。因此，它們也具有相同的價值。由於它是確定性的，所以在HOL中，相等（或者說相當於α等價）的項總是產生相等的值。

你可以想到SOME x. P x給你一個任意但固定的值，對於這個值P屬性（如果存在這樣的值，否則只是一些你根本不知道的固定值）。特別是，對於具有相同參數的SOME的不同「呼叫」將總是給你相同的價值。 THE，undefined等等也是如此。

如果您想要真正的非確定性選擇，您必須在HOL中使用不同的邏輯或模型非確定性。細化框架提供了一個不確定的monad，其中每個操作可以有零個，一個或多個可能的結果。