Isabelle：通用数据类型和等价性

Question

我刚开始在 Isabelle 中使我的类型通用，现在一旦我开始使用括号，我就会收到有趣的错误消息。

theory Scratch
imports Main
begin
no_notation plus (infixl "+" 65)

datatype typeA = aa
datatype typeB = bb
datatype ('a, 'b) genericType = cc | 
                                plus 'a 'b (infixr "+" 35)

lemma test1 : "x + y ≡ x + y"
by auto
lemma test2 : "x + y + z ≡ x + y + z"
by auto
lemma test3 : "x + (y + z) ≡ x + y + z"
by auto
lemma test4 : "(x + y) + z ≡ x + y + z"
lemma test5 : "(aa + aa) + aa ≡ aa + aa + aa"
lemma test6 : "(cc + cc) + cc ≡ cc + cc + cc"
lemma test7 : "(cc + aa) + cc ≡ cc + aa + cc"
lemma test8 : "(aa + cc) + cc ≡ cc + aa + cc"

测试 1-3 一切正常，但测试 4 和 5 导致此错误：

Type unification failed: Occurs check!

Type error in application: incompatible operand type

Operator:  op ≡ ((x + y) + z) :: ((??'a, ??'b) genericType, ??'c) genericType ⇒ prop
Operand:   x + y + z :: (??'a, (??'b, ??'c) genericType) genericType

并分别：

Type unification failed: Clash of types "typeA" and "(_, _) genericType"

Type error in application: incompatible operand type

Operator:  op ≡ ((aa + aa) + aa) :: ((typeA, typeA) genericType, typeA) genericType ⇒ prop
Operand:   aa + aa + aa :: (typeA, (typeA, typeA) genericType) genericType

test6 和奇怪的是 test7/8 又好了。将 "cc" 替换为 "aa" 会导致同样的问题。

PS: 我能以某种方式指定类型 'a 和 'b 吗？

Answer 1

Isabelle 中的两种类型只有在句法上真正相等时才相等。 left-hand 边和 right-hand 边具有不同类型的方程不是 well-typed 并且会导致错误消息。

您将 + 定义为 right-associative，因此 x + y + z 只是 x + (y + z) 的缩写。因此，引理 test1 到 test3 是微不足道的，因为等式的两侧在句法上是相等的。

在test4和test5中，left-hand边的类型是((_,_) genericType, _) genericType。另一方面，right-hand 边的类型为 (_, (_,_) genericType) genericType.

为了更好地说明它，我将在中缀中为 genericType 写 +：left-hand 边的类型为 (_ + _) + _； right-hand 边有 _ + (_ + _)。这两种类型在语法上 not 相同，因此是不同的类型。明明是同构的，但还是有区别的

test6 到 test8 是 type-correct 的事实与多态性有关：cc 是具有原理图类型变量 'a 和 'b 可以被实例化为任何东西，而且重要的是，如果 cc 在一个术语中多次出现，则类型变量在每次出现时都可以被实例化为不同的类型。对于前面示例中的 x、y 和 z 等变量，不可能。

但是请注意，虽然 test6 到 test8 可以是 type-checked，但它们显然是错误的，正如 QuickCheck 会告诉您的那样。

至于specifying类型变量：您可以用类型注释术语，例如x + y :: (typeA, typeB) genericType 或 (x :: typeA) + (y :: typeB).

Isabelle：通用数据类型和等价性

Isabelle: generic datatypes and equivalence

generics

types

unification

isabelle