伊莎贝尔统一错误

Question

我是 Isabelle 的新手，这是我第一个程序的简化版

theory Scratch
imports Main  
begin

  record  flow = 
    Src :: "nat"
    Dest :: "nat"

  record diagram = 
    DataFlows :: "flow set"
    Transitions :: "nat set"
    Markings :: "flow set"

  fun consume :: "diagram × (nat set) ⇒ (flow set)"
  where
    "(consume dia trans) = {n . n ∈ (Markings dia) ∧ (∃ t ∈ trans . (Dest n) = t)}"
end

函数报错：类型统一失败：类型冲突“_ ⇒ ”和“ 集”

Type error in application: operator not of function type

Operator:  consume dia :: flow set
Operand:   trans :: (??'a × ??'a) set ⇒ bool

编译代码需要做什么？

Answer 1

首先，您为 consume 函数提供了两个参数，但是按照您定义其类型的方式，它需要一个元组。这是不寻常的，而且通常很不方便——改为定义柯里化函数，如下所示：

fun consume :: "diagram ⇒ (nat set) ⇒ (flow set)"

此外，trans是一个常数；关系传递的是属性。可以看到，通过观察trans是黑色的表示它是一个常量，另一个变量是蓝色的，表示它是一个自由变量。

因此我建议使用其他名称，例如 ts:

  where
    "consume dia ts = {n . n ∈ (Markings dia) ∧ (∃ t ∈ ts . (Dest n) = t)}"

伊莎贝尔统一错误

Isabelle unification error

isabelle