我有点惊讶
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 选择的值相同？
最佳答案
左侧的项与右侧的项完全相同(模 alpha 转换)。因此，它们也具有相同的值(value)。在 HOL 中，相等(或者更确切地说 alpha 等价)项总是产生相等的值，因为它是确定性的。
你可以想到一些x。 P x 为您提供属性 P 所持有的任意但固定的值(如果存在这样的值，否则只是一些您对此一无所知的任意但固定的值)。特别是，具有相同参数的 SOME 的不同“调用”将始终给出相同的值。 THE、undefined 等也是如此。
如果您想要真正的非确定性选择，则必须在 HOL 中使用不同的逻辑或建模非确定性。细化框架提供了一种非确定性单子(monad)，其中每个操作都可以有零个、一个或多个可能的结果。
关于isabelle - 使用 SOME 的 Isabelle 术语之间的相等性，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22749091/