2

为什么以下工作：

fun f :: "nat ⇒ bool" where
  "f _ = (True ∨ (∀x. x))"

但这失败了

fun g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a. True))"

和

Additional type variable(s) in specification of "g_graph": 'a 
Specification depends on extra type variables: "'a"
The error(s) above occurred in "test.g_sumC_def"
The error(s) above occurred in definition "g_sumC_def":
  "g_sumC ≡ λx. THE_default undefined (g_graph TYPE('a) x)"

同样，以下成功，

value "True ∨ (∀x. x)"

但这失败了

value "True ∨ (∀x. True)"

和

Wellsortedness error:
Type 'a not of sort enum
Cannot derive subsort relation {} < enum
4

2 回答 2

3

简短的回答是：在您的第一个函数定义中，类型推断很容易推断出x是 type bool，而在您的第二个定义中，绑定变量a不在其他任何地方使用，因此它的类型是任意的（'a）。这就是规范中的附加类型变量 ...所表达的。

如果您a明确限制类型，例如，

fun g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a::bool. True))"

函数定义被接受。

更长的答案：由于 of 的定义g不是递归的，因此您可以将其转换为 usingdefinition而不是fun. 那么你的第一次尝试并没有完全失败，但结果可能会让你大吃一惊。后

definition g :: "nat ⇒ bool" where
  "g _ = (True ∨ (∀a. True))"

的类型g是'a itself => nat => bool而不是预期的nat => bool。原因与之前失败的原因相同fun。由于a是任意类型，因此必须将这个附加类型记录在 的类型中g，这是通过引入一个附加的虚拟参数来完成的，该参数只是明确地说明这个附加类型。这'a itself是一个类型，其构造函数TYPE(...)——将类型作为参数——允许我们在术语级别对类型信息进行编码。例如，

TYPE('a)   :: 'a itself
TYPE(bool) :: bool itself
TYPE(nat)  :: nat itself

然后g TYPE(nat)是gwhere的版本a固定为 type nat。

关于你的value陈述，第二个失败的原因与上述没有真正的关系。在第一个语句中，通用量词绑定一个类型的变量，bool其值可以显式枚举，因此可以通过考虑所有这些值来计算结果。相反，在您的第二个语句中，绑定变量x是任意类型'a，其值无法显式枚举。

于 2013-09-16T03:08:42.640 回答
1

以下失败：

fun f where "f _ = (∀a. True)"

因为 的类型a具有隐藏的多态性（即，函数体内有一个类型变量不存在于函数的类型签名中），这会扰乱函数包的内部证明。

如果你明确地给出a一个类型：

fun f where "f _ = (∀a::bool. True)"

还是您给出a的类型也在函数的类型签名中，如下所示：

fun f where "f _ = (∀a::bool. True)"

函数定义成功。你的例子：

fun f where "f _ = (∀x. x)"

成功，因为x被强制为 type bool。

至于您的value命令，Isabelle 会尝试为您的表达式生成可执行代码，因此不仅需要知道您的 for-all 语句的类型，还需要能够枚举它的所有可能值，以便对其进行测试. 诸如此类的类型可以bool正常工作，但诸如此类的类型变量'a或诸如此类的无限类型nat是不可枚举的，因此 Isabelle 无法为它们生成代码。

于 2013-09-16T03:12:27.180 回答