Isabelle Tutorial その23
8.3 Type Classes
型クラスの概念はHaskellによって広まりました。型クラスは型とインタフェースの集合を定義し、そのクラスに属する型はインタフェースを実装しなければなりません。Isabelleが提供する型クラスも同様ですが、さらにプロパティ(型公理)を定めることができ、クラスに属する型はプロパティを満たさなければなりません。型tがクラスCに属することをt :: Cと書きます。また型クラスは継承することができ、DがCのサブクラスであることをD < Cと書きます。
8.3.1 Overloading
型クラスによって関数のオーバーロードが可能になります。従って定数をそれぞれの型に対して多重定義できます。
Overloading.
型クラスを使い、任意の型に対する加算演算子[+]を導入してみます。
class plus = fixes plus :: "'a => 'a => 'a" (infixl "[+]" 70)
これは、新しいクラスplusと同時に、定数plusの構文を定義します。またplusはクラス演算子でもあります。plusに属する型はその型変数に対して"'a :: plus"を制約として持ち、これはクラスplusに属する型は"'a"をインスタンス化した結果でなければならないことを意味します。インスタンス化の例を見てみます。
instantiation nat :: plus begin
コマンドinstantiationはローカルスコープを開きます。ここでは、plusをnatでインスタンス化します。まず、natに対する関数plusを定義しなければなりません。
primrec plus_nat :: "nat => nat => nat" where "(0::nat) [+] n = n" | "Suc m [+] n = Suc (m [+] n)"
デフォルトでは、型tに対するクラス演算子fのローカル名はf_tとします。次に、型natがクラスplusのプロパティを満たしていることを証明しなければなりません。クラスplusにはプロパティがないので、証明は".."と書くだけで終わります。
instance ..
最後に、endで閉じて終わります。
end
以上で、Suc (m [+] 2)といった記述ができるようになりました。
次に、plusをplusのペアでインスタンス化してみます。
instantiation * :: (plus, plus) plus begin fun plus_prod :: "'a * 'b => 'a * 'b => 'a * 'b" where "(x, y) [+] (w, z) = (x [+] w, y [+] z)" instance .. end
8.3.2 Axioms
クラスにプロパティを付けると、そのクラスに属する型の制約となります。
Semigroups.
plusのサブクラスとしてsemigroupsを定めます。
class semigroup = plus + assumes assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
semigroupに属する型は[+]について結合律を満たさなければなりません。このクラスプロパティを使って、semigroupに属する型に対する定理を導出することができます。*1
lemma assoc_left: "(x::'a::semigroup) [+] (y [+] z) = (x [+] y) [+] z" by (rule assoc[THEN sym])
このように証明された定理は、このクラスに属する型に対して自由に使うことができます。
インスタンス化の時には、クラスプロパティを満たすことを証明しなければなりません。
instantiation nat :: semigroup begin instance
証明はメソッドintro_classesで始めます。
apply(intro_classes) apply(induct_tac x) by simp_all end
ペアについても同様に証明してみます。
instantiation * :: (semigroup, semigroup) semigroup begin instance apply(intro_classes) apply(case_tac x, case_tac y, case_tac z) by (simp add: assoc) end
ペアを構成するそれぞれの型がassocを満たすことから、ペアもまたassocを満たすことを証明できます。
Monoids.
semigroupを拡張してサブクラスmonoidlを定義します。monoidlは定数neutralを持ち、これは[+]に対する左単位元です。
class monoidl = semigroup +
fixes neutral :: "'a" ("O")
assumes neutl: "O [+] x = x"
上と同じく、natでインスタンス化します。natの[+]に対する単位元は0です。
instantiation nat :: monoidl begin definition neutral_nat_def: "O = (0::nat)" instance apply(intro_classes) apply(subst neutral_nat_def) by simp end
ペアも同様にインスタンス化できます。
instantiation * :: (monoidl, monoidl) monoidl begin definition neutral_prod_def: "O = (O, O)" instance apply(intro_classes) apply(case_tac x) by (simp add: neutral_prod_def neutl) end
完全なモノイドをモデル化するには、neutralが右単位元である必要があります。
class monoid = monoidl + assumes neutr : "x [+] O = x"
nat及びペアでのインスタンス化は省略します。
Groups.
最後にクラスgroupを作成します。
class group = monoidl +
fixes inv :: "'a => 'a" (":- _" [81] 80)
assumes invl: ":- x [+] x = O"
さらに、次の補題も証明しておきます。
lemma left_cancel: "((x::'a::group) [+] y = x [+] z) = (y = z)" apply(rule iffI) apply(subgoal_tac "(:- x [+] x) [+] y = (:- x [+] x) [+] z") apply(simp add: invl neutl) apply(simp add: assoc) apply(simp) done
このように定義したクラスgroupはmonoidでもあります。これを、groupがmonoidのサブクラスであることを証明して導入します。
instance group < monoid apply(intro_classes) apply(subgoal_tac "(:- x [+] x) [+] O = (:- x [+] x)") apply(simp add: assoc left_cancel) apply(simp add: invl neutl) done
この証明結果がIsabelleの型システムにも伝わり、groupがmonoidのサブクラスであることが型クラスの継承関係に追加されます。
Inconsistencies.
互いに矛盾するプロパティをクラスに付加することもできます。しかし、既に見たようにインスタンス化するためにはその型変数がプロパティを満たすことを証明する必要があり、矛盾するプロパティは証明できません。
Syntactic Classes and Predefined Overloading.
上の例では最初に構文クラスであるplusを定義しましたが、操作とプロパティを同時に定めるsemigroupから始めることもできました。一般的には操作とそのプロパティを同時に定義する方が良いでしょう。しかし操作の構文が汎用的な場合は、上の例のように構文とそのプロパティを別のクラスで定義することによって、構文を使い回すことができます。
逆に構文を持たず、プロパティのみを定義するクラスも考えられます。例えば理論Finite_Setで定義されているクラスfiniteがあります。このクラスは有限集合"finite (UNIV :: 'a::finite set)"を定義しています。
8.4 Numbers
これまでは数値型に自然数型のnatを使用してきましたが、HOLには整数型intもあります。intは帰納法が使えませんが、所謂減算が使えます。よって減算を含む複雑な計算を解くにはnatよりもintの方が有利です。更には、有理数型rat、実数型real、複素数型complexもあります。Isabelleにサブタイプはなく、よって型は全て異なります。多くの算術演算子は多重定義されており、代数的な性質は型クラスを使って体系化されています。
多くの算術式はメソッドarithで証明することができます。また、算術式に関する多くの定理も用意されています。以下ではそれらの定理の一部を見ていきます。
8.4.1 Numeric Literals
定数0と1は全ての数値型に対して多重定義されています。他の値は数値リテラル、例えば2、-3、441223334678などで表わします。またIsabelleは加算や減算、乗算、整数型の除算や剰余算などは実際に計算します。
算術演算子が多重定義されているため、式の型に注意する必要があります。例えば次の証明はうまくいきません。
lemma "2 * m = m + m"
型を見てみると、'aとなっていることがわかると思います。型が定まらないため、証明が失敗します。例えば2::intのように型を指定すると、もちろん証明できます。
数値リテラルはパターンとして使うことができません。例えば次のような定義はエラーが返ります。
function h where "h 3 = 2" | "h i = i"
これを定義したい場合は、例えば次のようにします。
"h i = (if i = 3 then 2 else i)"
8.4.2 The Type of Natural Numbers, nat
natはこれまでに何度も使ってきました。natに関する多くの定理は理論NatとDividesで用意されています。
Literals.
1はnatでは次のように定義されています。
1 = Suc 0 (One_nat_def)
これは単純化ルールなので、simpを使用すると自動的に置き換えられます。特に大きな値はリテラルで書いた方が明らかに読みやすいですが、多くの定理はSuc nの形にのみ適用できます。
次の二つの定理も単純化ルールです。
2 + ?n = Suc (Suc ?n) (add_2_eq_Suc) ?n + 2 = Suc (Suc ?n) (add_2_eq_Suc')
証明の中で例えば100をSuc 99に変形するのは簡単ではありません。よって予め0とSucのみで表わした方が良いでしょう。
Division.
natに対してdivとmodも定義されており、次の定理があります。
?m mod ?n = (if ?m < ?n then ?m else (?m - ?n) mod ?n) (mod_if) ?a div ?b * ?b + ?a mod ?b = ?a (mod_div_equality)
さらにいくつかの定理を紹介します。
?a * ?b div ?c = ?a * (?b div ?c) + ?a * (?b mod ?c) div ?c (div_mult1_eq) ?a * ?b mod ?c = ?a * (?b mod ?c) mod ?c (mod_mult_right_eq) ?a div (?b * ?c) = ?a div ?b div ?c (div_mult2_eq) ?a mod (?b * ?c) = ?b * (?a div ?b mod ?c) + ?a mod ?b (mod_mult2_eq) ?c ~= 0 ==> ?c * ?a div (?c * ?b) = ?a div ?b (div_mult_mult1) ?m mod ?n * ?k = ?m * ?k mod (?n * ?k) (mod_mult_distrib) ?m <= ?n ==> ?m div ?k <= ?n div ?k (div_le_mono)
いくつかの定理は除数が0以外という制限が付いています。natにおける0による除算の結果は0です。
?a div 0 = 0 (div_by_0) ?a mod 0 = ?a (mod_by_0)
整除関係は標準的な形で、すべての数値型に対して多重定義されています。
(?b dvd ?a) = (EX k. ?a = ?b * k) (dvd_def)
さらに整除性について次の定理もあります。
[| ?m dvd ?n; ?n dvd ?m |] ==> ?m = ?n (dvd_antisym) [| ?a dvd ?b; ?a dvd ?c |] ==> ?a dvd ?b + ?c (dvd_add)
Subtraction.
natではnがmより大きいならば、m - nは0になります。次の定理はn <= mという条件なしに成り立ちます。
(?m - ?n) * ?k = ?m * ?k - ?n * ?k (diff_mult_distrib)
減算は次の場合分けルールで除去することができます。
?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) (nat_diff_split)
例えばこの定理を次のように使用できます。
lemma "(n - 2) * (n + 2) = n * n - (4::nat)" apply(simp split: nat_diff_split, clarify)
1. !!d. [| n < 2; n * n = 4 + d |] ==> d = 0
n < 2から0か1のどちらかです。
apply(subgoal_tac "n = 0 | n = 1", force, arith) done
8.4.3 The Type of Integers, int
帰納法はありませんが、intを含む証明はnatに似ており、多くの定理が用意されています。
絶対値を返す関数absは、intを始め負数を持つ全ての型に対して多重定義されています。absを含む式はメソッドarithで証明できます。
lemma "abs (x + y) <= abs x + abs (y::int)" by arith
剰余の正負は除数に依存します。
0 < ?b ==> 0 <= ?a mod ?b (pos_mod_sign) 0 < ?b ==> ?a mod ?b < ?b (pos_mod_bound) ?b < 0 ==> ?a mod ?b <= 0 (neg_mod_sign) ?b < 0 ==> ?b < ?a mod ?b (neg_mod_bound)
更に次の定理が用意されています。
(?a + ?b) div ?c = ?a div ?c + ?b div ?c + (?a mod ?c + ?b mod ?c) div ?c (zdiv_zadd1_eq) (?a + ?b) mod ?c = (?a mod ?c + ?b mod ?c) mod ?c (mod_add_eq) ?a * ?b div ?c = ?a * (?b div ?c) + ?a * (?b mod ?c) div ?c (zdiv_zmult1_eq) ?a * ?b mod ?c = ?a * (?b mod ?c) mod ?c (zmod_zmult1_eq) 0 < ?c ==> ?a div (?b * ?c) = ?a div ?b div ?c (zdiv_zmult2_eq) 0 < ?c ==> ?a mod (?b * ?c) = ?b * (?a div ?b mod ?c) + ?a mod ?b (zmod_zmult2_eq)
最後の二つはnatの場合とは異なり、cが正数でなければなりません。また、定理名に現れるzは整数の集合を表わす記号からきています。
もし値域に上限あるいは下限があるならば、整数に対しても帰納法が使えます。値域の範囲によって、次の四つの帰納ルールがあります。
[| ?k <= ?i; ?P ?k; !!i. [| ?k <= i; ?P i |] ==> ?P (i + 1) |] ==> ?P ?i (int_ge_induct) [| ?k < ?i; ?P (?k + 1); !!i. [| ?k < i; ?P i |] ==> ?P (i + 1) |] ==> ?P ?i (int_gr_induct) [| ?i <= ?k; ?P ?k; !!i. [| i <= ?k; ?P i |] ==> ?P (i - 1) |] ==> ?P ?i (int_le_induct) [| ?i < ?k; ?P (?k - 1); !!i. [| i < ?k; ?P i |] ==> ?P (i - 1) |] ==> ?P ?i (int_less_induct)
8.4.4 The Types of Rational, Real and Complex Numbers
rat、real、complexは理論HOL-Complesに定義されており、これを使用するためにはMainではなくComplex_Mainをimportsする必要があります。
これらの型にはdivではなく、除算演算子/が定義されています。有理数と実数は稠密性を持っており、二つの異なる値の間には別の値が存在します。
?x < ?y ==> EX z>?x. z < ?y (dense)
また実数は完備性を持ちますが、有理数は持ちません。完備性の形式化は理論RCompleteに書かれています。
分数を/で表わすことができ、単純化で自動的に約分されます。
1. P ((3 / 4) * (8 / 15))
apply simp
1. P (2 / 5)
2 * 10^6のように指数表現で表わすこともでき、これも単純化で実数に変換されます。
8.4.5 The Numeric Type Classes
Isabelle/HOLは型クラスを使用して数値に関する理論を体系付けています。いくつかの型クラスと定理を紹介します。
- semiringとordered_semiring: 半環は演算子+と*、それらの結合律、さらにそれぞれの単位元となる0と1を与えます。演算子はまた一般的な分配則を満たし、さらに加算(+)は交換律を満たします。順序半環は半環を継承し、更に線形順序を与えます。natは順序半環に属します。
- ringとordered_ring: 環は半環を継承し、単項のマイナス(加法に対する逆元)と減算(-)を与えます。順序環には関数absが定義されています。intは順序環に属します。
- fieldとordered_field: 体は環を継承し、逆数を与えます。順序体は順序環を元にします。complexは体に、realは順序体に属します。
- division_by_zeroはinverse 0 = 0とa / 0 = 0を満たすすべての型を含みます。このクラスはIsabelleの標準的な数値型をすべて含みますが、体の基本的な定理はこの性質に依存することなく証明されています。
0除算を含まない環であるクラスring_no_zero_divisorsは吸収律を満たし、次の定理があります。
(?a * ?b = (0::?'a)) = (?a = (0::?'a) | ?b = (0::?'a)) (mult_eq_0_iff) (?a * ?c = ?b * ?c) = (?c = (0::?'a) | ?a = ?b) (mult_cancel_right)
ProofGeneralのメニュー Isabelle > Settings > Show Sorts で型クラスを表示することができます。定理mult_cancel_leftを型クラスを付けて示してみます。
((?c::?'a::ring_no_zero_divisors) * (?a::?'a::ring_no_zero_divisors) = ?c * (?b::?'a::ring_no_zero_divisors)) = (?c = (0::?'a::ring_no_zero_divisors) | ?a = ?b) (mult_cancel_left)
Simplifying with the AC-Laws.
加算に関する交換則と結合則を示します。
?a + ?b + ?c = ?a + (?b + ?c) (add_assoc) ?a + ?b = ?b + ?a (add_commute) ?a + (?b + ?c) = ?b + (?a + ?c) (add_left_commute)
add_acでこれらすべての定理を参照することができます。乗算に関しては同様にmult_acがあります。これらは半環で証明されており、よってすべての数値型がこの性質を持ちます。
Division Laws for Fields.
次に除算演算子に関するルールを見てみます。次の定理は、乗算と除算を使って表わされた有理式の単純化ルールです。
?a * (?b / ?c) = ?a * ?b / ?c (times_divide_eq_right) ?b / ?c * ?a = ?b * ?a / ?c (times_divide_eq_left) ?a / (?b / ?c) = ?a * ?c / ?b (divide_divide_eq_right) ?a / ?b / ?c = ?a / (?b * ?c) (divide_divide_eq_left)
次の定理を使用し、符号を商から取り出すことができます。
- (?a / ?b) = - ?a / ?b (minus_divide_left) - (?a / ?b) = ?a / - ?b (minus_divide_right)
分配則もありますが、これは単純化ルールではありません。
(?a + ?b) / ?c = ?a / ?c + ?b / ?c (add_divide_distrib)
Absolute Value.
関数absはint、rat、realを含むすべての順序環に定義されています。いくつかの定理を示します。
abs (?a * ?b) = abs ?a * abs ?b (abs_mult) (abs ?a <= ?b) = (?a <= ?b & - ?a <= ?b) (abs_le_iff) abs (?a + ?b) <= abs ?a + abs ?b (abs_triangle_ineq)
Raising to a Power.
クラスordered_idomは環を元にし、さらに指数表現を原始帰納を使用して定義しています。理論Powerに含まれるいくつかの定理を示します。
?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n (power_add) ?a ^ (?m * ?n) = (?a ^ ?m) ^ ?n (power_mult) abs (?a ^ ?n) = abs ?a ^ ?n (power_abs)
