使用SOME的Isabelle术语之间的平等

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,其中每个操作都可以有零个,一个或许多可能的结果.