部分功能與不足指定的總功能

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最簡單的方法是限制您正在推理的域（有界量化）。至於圖的例子，圖的定理總是對所有的節點表示類似的東西。但正如我所說的，這可能是品味的問題。