Isabelle HOLCF 不理解 fixrec

Question

这是一个非常简单的理论：

theory Test
  imports HOLCF
begin
  fixrec down :: "'a u → 'a"
    where "down (up x) = x"
end

它给出了以下错误：

Type unification failed: Clash of types "_ ⇒ _" and "_ → _"

Type error in application: operator not of function type

Operator:  up :: ??'a → ??'a⇩⊥
Operand:   x :: ??'b

我尝试过声明不同的函数，但我总是得到类似的错误。有什么问题以及如何解决？

我尝试用 ⇒ 替换 →，但没有用。

Answer 1

单箭头→是连续函数的space，双箭头⇒表示所有总函数的space。 HOLCF 中的所有包仅适用于连续函数。这就是 ⇒ 对大多数 HOLCF 不起作用的原因。但是，连续函数的函数应用程序必须使用 ASCII 中缀运算符 $ 或 \<cdot> 明确编写。所以以下工作：

fixrec down :: "'a u → 'a"
  where "down $ (up $ x) = x"

同样，连续函数的 lambda 抽象使用大写 Λ 而不是小写 λ.

Isabelle HOLCF 不理解 fixrec

Isabelle HOLCF doesn't understand fixrec

isabelle