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

单箭头→是连续函数的空间，而双箭头⇒表示所有全函数的空间。HOLCF中的所有包都只能使用连续函数。这就是为什么⇒不能在大多数HOLCF上工作的原因。然而，连续函数的函数应用程序必须使用ASCII型中缀运算符$或\<cdot>显式编写。因此，下面的方法是可行的：

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

类似地，连续函数的lambda抽象使用大写的Λ而不是小的λ。