假设我有一套A ⊆ nat. 我想在 Isabelle 中建模一个函数f : A ⇒ Y。我可以使用任何一个：
- 偏函数，即 type 之一
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？