部分功能与不足指定的总功能

Question

假设我有一组A ⊆ nat。我想在伊莎贝尔建立一个功能f : A ⇒ Y。我可以使用任一：

1. 部分功能，即nat ⇒ Y option类型的一个，或
2. 总功能，即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最简单的方法是限制您正在推理的域（有界量化）。至于图的例子，图的定理总是对所有的节点表示类似的东西。但正如我所说的，这可能是品味的问题。