イザベルの「商型パターン」とは？
インターネット上で説明を見つけることができませんでした。
2 に答える
8
フレーズを見たところから少し引用すると良いでしょう。「パターンマッチング」は知っているし、「商型」は知っているが、「商型パターン」は知らない。
私は説明を求めてから待つのは好まないので、3 つの単語のうち 2 つ、「商型」を選びます。私が間違った方向に進んでいるとしても、それは価値のある主題であり、Isabelle/HOL の大きく重要な部分です。
というキーワードがあり、同値関係quotient_typeを持つ新しい型を定義できます。
これは、isar-ref.pdf の 248 ページから説明されている商パッケージの一部です。Quotient_typeという Wiki ページがあります。
Brian Hufmann と Ondřej Kunčar による、より複雑な説明があります。Kunčar のWeb ページにアクセスして、 Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOLというタイトルの 2 つの PDF を参照してください。これらはまったく同じではありません。
リフティングと商の型はたまたま関連性が高く、理解するのは容易ではありません。そのため、すべてをよりよく理解するために、今のようにあちこちで少し勉強しようとしています。
HOL の整数と有理数は商型です。例として整数を選びます。
Int.thyを見ることから始めることができます。
商型の場合、セットを定義する同値関係が必要であり、これはintreltype のセットを定義するために使用されますint。
definition intrel :: "(nat * nat) => (nat * nat) => bool" where
"intrel = (%(x, y) (u, v). x + v = u + y)"
これは、自然数に基づく整数の古典的な定義です。整数は自然数 (および以下で説明するセット) の順序付けられたペアであり、その定義により等しいです。
たとえば、非公式に(2,3) = (4,5)、2 + 5 = 4 + 3.
私はあなたを退屈させています、そしてあなたは良いものを待っています。これがその一部です。使用方法は次のquotient_typeとおりです。
quotient_type int = "nat * nat" / "intrel"
morphisms Rep_Integ Abs_Integ
脳に負担をかけ、何が起こっているのかを本当に理解したい場合は、これらの 2 つのモーフィズムが有効になります。生成される関数や単純なルールはたくさんありquotient_type、コマンドなどを使用してすべてを見つけるには多くの作業を行う必要がありますfind_theorems。
関数は順序付きAbsペアを に抽象化しintます。これらをチェックしてください：
lemma "Abs_Integ(1,0) = (1::int)"
by(metis one_int_def)
lemma "Abs_Integ(x,0) + Abs_Integ(y,0) ≥ (0::int)"
by(smt int_def)
それらintは、エンジンのボンネットの下で、 が本当に順序付けられたペアであることを示しています。
ここで、これらの射の明示的な型を と とともに示します。これらはAbs_int、順序対としてだけでなく、順序対の集合としてもRep_int示されます。int
term "Abs_int :: (nat * nat) set => int"
term "Abs_Integ :: (nat * nat) => int"
term "Rep_int :: int => (nat * nat) set"
term "Rep_Integ :: int => (nat * nat)"
また退屈させてしまいましたが、もっと例を示す必要があります。次のように、順序付けられたペアのコンポーネントが 1 だけ異なる場合、2 つの正の整数は等しくなります。
lemma "Abs_Integ(1,0) = Abs_Integ(3,2)"
by(smt nat.abs_eq split_conv)
lemma "Abs_Integ(4,3) = Abs_Integ(3,2)"
by(smt nat.abs_eq split_conv)
と を追加するAbs_Integ(4,3)とどうなりますAbs_Integ(3,2)か? これ：
lemma "Abs_Integ(2,3) + Abs_Integ(3,4) = Abs_Integ(2 + 3, 3 + 4)"
by(metis plus_int.abs_eq plus_int_def split_conv)
このplus_int証明は、Int.thy の44 行目で定義されています。
lift_definition plus_int :: "int => int => int"
is "%(x, y) (u, v). (x + u, y + v)"
このリフトは何ですか？そうすれば、この説明に「数日」かかることになりますが、私はそれを少し理解し始めたばかりです。
私が言ったように、多くのfind_theoremsものが隠されていることを示しています：
thm "plus_int.abs_eq"
find_theorems name: "Int.plus_int*"
より多くの例がありますが、これらは、エンジンのフードの下で、上記を使用してセットを正しく定義しているintセットとして等価クラスに結び付けられることを強調するためのものです。intrel
term "Abs_int::(nat * nat) set => int"
term "Abs_int {(x,y). x + 3 = 2 + y}" (*(2,3)*)
term "Abs_int {(x,y). x + 4 = 3 + y}" (*(3,4)*)
lemma "Abs_int {(x,y). x + 3 = 2 + y} = Abs_int {(x,y). x + 100 = 99 + y}"
by(auto)
そのauto証明は簡単でしたが、次の証明は単純ですが、私には何の魔法も通用しません。
lemma "Abs_int {(x,y). x + 3 = 2 + y} + Abs_int {(x,y). x + 4 = 3 + y}
= Abs_int {(x,y). x + 7 = 5 + y}"
apply(auto simp add: plus_int.abs_eq plus_int_def intrel_def)
oops
私がする必要があるのは、デフォルトで単純なルールではない何かを利用することだけかもしれません.
あなたquotient_typeが話している「商型パターン」でない場合、少なくとも、上記のすべてのfind_theorems戻り値を見て、何かを得ましたInt.plus_int*。
于 2014-05-06T04:32:20.593 に答える
1
商型とは？
商型は、既存の型に関して新しい型を定義する方法です。そうすれば、新しい型を公理化する必要はありません。たとえば、自然数は「自然数 + 負数」と見なすことができるため、整数を構築するために自然数を使用するのが合理的であると考えるかもしれません。次に、整数を使用して有理数を構築することができます。これは、「整数 + 商」と見なすことができるためです。等々。
商型は、「下位の型」で指定された同値関係を使用して、「上位の型」の等価性を決定します。
より正確に言うと、商型は抽象型であり、基礎となる表現の等価関係によって同等性が決定されます。
この定義は最初は抽象的すぎるかもしれないので、基本的な例として整数を使用します。
例: Naturals からの整数
整数を定義したい場合、最も標準的な方法は、直感的に「ab」を表す (a,b) などの自然数の順序付けられたペアを使用することです。たとえば、ペア (2,4) で表される数は、直観的に 2-4 = -2 であるため、-2 です。同じ論理で、(0,2) も '-2' を表し、0-2 = 1-3 = 10-12 = -2 であるため、(1,3) または (10,12) も同様です。
次に、" 2 つのペア (a,b) と (x,y) は、a - b = x - y の場合、同じ整数を表す" と言えます。ただし、マイナス演算は自然数ではおかしくなることがあります (自然数の「2-3」とは何ですか?)。その奇妙さを避けるために、'a - b = x - y' を 'a + y = x + b' に書き直して、足し算だけを使用します。したがって、「a + y = x + b」の場合、2 つのペア (a,b) と (x,y) は同じ整数を表します。たとえば、(7,9) は、'7 + 3 = 1 + 9' であるため、(1,3) と同じ整数を表します。
これは、整数の商定義につながります。整数は、自然数の順序付けられたペアによって表される型です。(a,b) と (x,y) で表される 2 つの整数は、 a+y = x+b の場合にのみ等しくなります。
整数型は、その表現である「自然数の順序付きペア」型から派生します。整数自体をその抽象化と呼ぶことができます。整数の等価性は、基になる表現 '(a,b)' および '(x,y)' が等価関係 'a+y = x+b' に従うときは常に定義されます。
その意味で、整数 '-3' は'(0,3)' と '(2,5)' の両方で表され、0+5 = 3+2 に注目することでこれを示すことができます。一方、'(0,3)' と '(6,10)' は、'0+10 ≠ 3+6' であるため、同じ整数を表していません。これは「-3≠-4」という事実を反映しています。
技術的に言えば、整数「-3」は具体的には「(0,3)」でも「(1,4)」でも「(10,13)」でもなく、等価クラス全体です。つまり、「-3」はその表現のすべてを含むセットです(つまり、-3 = { (0,3), (1,4), (2,5), (3,6), (4, 7), ... } )。「(0,3)」は「-3」の表現と呼ばれ、「-3」は「(0,3)」の抽象化です。
モーフィズム: Isabelle のRepとAbs
RepとAbsは、表現とそれらが表す抽象化の間を移行する方法です。より正確には、等価クラスからその表現の 1 つへのマッピング、およびその逆のマッピングです。それらをモーフィズムと呼びます。
Repは、「-3」などの抽象オブジェクト (等価クラス) を取り、それを「(0,3)」などの表現の 1 つに変換します。Absは反対のことを行い、「(3,10)」などの表現を取り、それを「-7」である抽象オブジェクトにマッピングします。Int.thy(Isabelle の整数の実装) では、これらをRep_Integ整数として定義しAbs_Integています。
ステートメント ' (2,3) = (8,9)' はばかげていることに注意してください。これらは順序付きのペアであるため、「2 = 8」と「3 = 9」を意味します。一方、Abs_Integ(2,3) = Abs_Integ(8,9)「(2,3)」の整数抽象化は整数抽象化「(8,9)」、つまり「-1」と同じであると単に言っているだけなので、ステートメント「 」は非常に真実です。 .
' 'のより正確な言い回しAbs_Integ(2,3) = Abs_Integ(8,9)は次のとおりです。通常、このクラスを「-1」と呼びます。
「-1」は「(0,1) の等価クラス」の便利な省略形であり、「5」は「(5,0) の等価クラス」の省略形であることに注意することが重要です。 '-15' は '(0,15)' の等価クラスの短縮形です。'(0,1)'、'(5,0)'、'(0,15) を正規表現と呼びます。 . したがって、" " と言うのは、" Abs_Integ(2,3) = -1" の単なる省略形ですAbs_Integ(2,3) = Abs_Integ(0,1)。
Repのマッピングが 1 対 1 であることも注目に値します。これは、Rep_Integ(-1)常に同じ表現ペア、通常は正規の '(0,1)' を生成することを意味します。選択された特定のペアはそれほど重要ではありませんが、常に同じペアが選択されます。これは、ステートメントRep_Integ(i) = Rep_Integ(i)が常に真であることを意味するため、知っておくと便利です。
quotient_typeIsabelleのコマンド
' quotient_type' は、指定された型と同値関係を使用して商型を作成します。したがって、関係( )の下の の同値クラスとして、quotient_type int = "nat × nat" / "intrel"商型 が作成されます。マニュアルのセクション 11.9.1 に、コマンドの詳細が記載されています。intnat × natintrelwhere "intrel = (λ(a,b) (x,y). a+y = x+b)"
提供された関係 ( ) が同等であることを実際に証明する必要があることに注意してください。intrel
からの使用例を次に示します。これは、整数を定義し、射であり、同値関係であるInt.thyことを証明します。intrel
(* Definition *)
quotient_type int = "nat × nat" / "intrel"
morphisms Rep_Integ Abs_Integ
(* Proof that 'intrel' is indeed an equivalence *)
proof (rule equivpI)
show "reflp intrel" by (auto simp: reflp_def)
show "symp intrel" by (auto simp: symp_def)
show "transp intrel" by (auto simp: transp_def)
qed
定義と補題: Lifting and Transfer パッケージ
さて、前の説明は、RepとAbsがどこにでも現れるべきであることを示唆していますよね? これらの変換は、商の型に関するプロパティを証明するために重要です。ただし、の 2000 行全体で 10 回未満しかInt.thy表示されません。なんで？
lift_definitionと証明方法transferが答えです。これらは、リフトおよびトランスファーパッケージから提供されます。これらのパッケージは多くのことを行いますが、私たちの目的のために、定義と定理からRepとAbsを隠す役割を果たします。
Isabelle で商型を扱うときの要点は、[1]いくつかの操作を定義し、[2]表現型でいくつかの有用な補題を証明し、[3] これらの表現を完全に忘れて、抽象のみを扱うことです。タイプ。抽象型に関する定理を証明するときは、前に示したプロパティと補題を使用する必要があります。
[1]を取得すると、操作を定義するのにlift_definition役立ちます。具体的には、表現型で関数を定義できるようにし、自動的に抽象型に「リフト」します。
例として、整数の加算を次のように定義できます。
lift_definition int_plus:: "int ⇒ int ⇒ int"
is "λ(a,b)(c,d). (a+c, b+d)"
この定義は の観点から記述されていますnat × nat ⇒ nat × nat ⇒ nat × natが、' lift_definition' は自動的に に「持ち上げ」ますint ⇒ int ⇒ int。
注意すべき重要なことは、関数が適用後も同値関係に従うことを証明する必要があることです(つまり、'x ≃ y' の場合、'fx ≃ f y' の場合)。たとえば、上記の定義では、" if '(a,b) ≃ (x,y)' and '(c,d) ≃ (u,v)', then '(a+c,b +d) ≃ (x+u,y+v)' " (そうでない場合は、 を使用してみてくださいapply clarify)。
優れている点の 1 つはlift_definition、基になる表現のみに関して機能するため、抽象化と表現の間の移行について心配する必要がないことです。Rep_Integしたがって、とAbs_Integinの欠如Int.thy。
transferまた、関数のルールも設定します。[2]を取得する方法: RepとAbsを気にせずにプロパティを証明します。証明方法を使用するtransferと、抽象化に関するレンマを表現レベルに落とし込み、そこで目的のプロパティを証明できます。
例として、加算の可換性を の形int_plus x y = int_plus y xで記述し、メソッドを使用transferしてそのステートメントを表現レベルに落とし込むことができclarifyますintrel (a + c, b + d) (c + a, d + b)。次に、 の定義による単純化によって証明できますintrel。
lemma plus_comm: "int_plus x y = int_plus y x"
apply transfer
apply clarify
by (simp add: intrel_def)
[3]を取得するには、実際の表現を気にせずに、単にこれらの補題と抽象型のプロパティを使用します。
この時点で、必要なのは抽象型とそのプロパティだけなので、商型を使用していることさえ忘れるでしょう。通常、抽象型のレンマはほんの一握りで十分でありInt.thy、一握り以上のものが得られます。
参考資料と参考文献
- 論文「Quotient Types」のセクション 1 では、このトピックの概要を説明しています (他のセクションで詳しく説明しています)。
- 「 Quotients Revisited for Isabelle/HOL 」の紹介でも、「 Rep」と「Abs 」の目的が非常によく説明されています。
- 「Lifting and Transfer」は、これらを隠す方法と、Isabelle の商型の背後にある自動化についてもよく読んでいます。
- Isabelle のリファレンス マニュアル(いくつかのctrl+fを含む) も、特定のコマンドが何をするのか疑問がある場合の優れた情報源です。
于 2021-09-22T15:38:11.103 に答える