4

セットがあるとしますA ⊆ nat。Isabelle a function でモデル化したいと思いますf : A ⇒ Y。次のいずれかを使用できます。

  1. 部分関数、つまり typenat ⇒ Y optionのいずれか、または
  2. 合計関数、つまり にnat ⇒ Yない入力に対して指定されていない型の 1 つ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ますか?

4

1 に答える 1

2

それはおそらく好みの問題であり、あなたが念頭に置いている用途にもよるかもしれないので、私の個人的な好みをお伝えします。これはオプション 2 です。その理由は、いずれにせよ、両方のアプローチで限界のある定量化が避けられないと思うからです。アプローチ 1. を使用すると、最も簡単な方法Optionは、推論しているドメイン (有界定量化) を制限することであることがわかると思います。グラフの例に関して言えば、グラフ定理は常に V のすべてのノードについてのようなことを言っています。しかし、私が言ったように、それはおそらく好みの問題です。

于 2013-03-14T13:48:33.947 に答える