isabelle - 偏函数与指定不足的全函数

Question

假设我有一组 A ⊆ nat .我想在 Isabelle 中建模一个函数 f : A ⇒ Y .我可以使用:

一个偏函数，即 nat ⇒ Y option 类型之一, 或

一个总函数，即 nat ⇒ Y 类型之一未指定用于不在 A 中的输入.

我想知道哪个是“更好”的选择。我看到了几个因素:

“偏函数”方法更好，因为比较偏函数的相等性更容易。也就是说，如果我想看看 f等于另一个函数，g : A ⇒ Y ，那我就说f = g .比较未指定的总函数 f和 g ，我不得不说 ∀x ∈ A. f x = g x .

“未指定的总函数”方法更好，因为我不必对构建/解构 option 感到困惑。一直打字。例如，如果 f是一个欠指定的总函数，并且 x ∈ A ，那我只能说 f x ，但如果 f是我不得不说的部分功能 (the ∘ f) x .再比如，对部分函数进行函数组合比对全函数进行组合更棘手。

对于与此问题相关的具体实例，请考虑以下将简单图形形式化的尝试。

type_synonym node = nat
record 'a graph = 
  V :: "node set"
  E :: "(node × node) set"
  label :: "node ⇒ 'a"

一个图包括一组节点、它们之间的边关系和一个 label对于每个节点。我们只关心 V 中的节点的标签.所以，应该 label是偏函数 node ⇒ 'a option与 dom label = V ，或者它应该只是一个在 V 之外未指定的全函数?

Answer 1

这可能是一个品味问题，也可能取决于您想到的用途，所以我只会给您我个人的品味，这将是选项 2。总功能。原因是我认为这两种方法中的有界量化无论如何都是不可避免的。我认为使用方法 1。您会发现这是处理 Option 的最简单方法。是限制您正在推理的域(有界量化)。至于图的例子，图定理总是对 V 中的所有节点说类似的话。但正如我所说，这可能是一个品味问题。