Alloy で自動定理証明っぽいやつ
このエントリは Theorem Prover Advent Calendar 2015 - Qiita の 23 日目です。
とは言ってみたものの、内容はいわゆる定理証明器の話ではありません。モデル検査器 Alloy を利用して古典命題論理のシークエント計算をモデル化し、証明図を自動生成させることを目標にします。
なお、以下で部分的に引用しているモデル定義の完全版は alloy_sequent.als · GitHub にアップロードしてあります。
モデル化してみる
命題論理式の実装
まず対象となる論理式を Alloy で記述します。
abstract sig Formula {}
sig Atom extends Formula {}
sig Not extends Formula {
of : one Formula,
}
abstract sig BinaryLogicOperator extends Formula {
left : one Formula,
right : one Formula,
}
sig And, Or, Imply extends BinaryLogicOperator {}
二項演算子たちを定義する際、独立に定義せず間に抽象シグネチャ BinaryLogicOperator を挟んで extends で継承しています。これは Alloy 上の関係には多相性がなく、同じ名前の関係は同じシグネチャ間にしか定義することができないためです。つまり演算子をそれぞれ個別に定義した場合、引数を指す関係名を、例えば andRight : And -> Formula のように演算子ごとにつける必要が生じてしまいます。
そこで、引数を left, right とした BinaryLogicOperator を経由することで、すべての演算子に共通して課したい制約を
fact formulaeAreAcyclic {
all f : Formula | f not in f.^(of + right + left)
}
のように統一的に記述できるというわけです。
シークエントの実装
さて、次にシークエントの定義を記述します。
sig Sequent {
antecedents : set Formula,
succedents : set Formula,
}
通常の記法で言えばシークエント の
が
antecedents, が
succedents です。
本来、これらは「論理式の列」として個数と順番を考えて保持されるべきですが、今回は古典命題論理しか考えないので個数も順番も無視して単なる集合 set として扱います。部分構造論理が好きな人は潔く諦めましょう。
推論規則の実装
シークエントができたら、推論規則も Alloy に載せましょう。
論理式の場合と同じく、もとになる抽象シグネチャを定義します。
abstract sig InferenceRule {
premises : some Sequent,
conclusion : one Sequent,
}
前提 premises は最大 2 個になり得るので some で、結論 conclusion は必ず 1 個なので one で定義しておきました。
なお、公理は前提が空なる推論規則であると考えて premises を set で定義することも考えられますが、この場合、検証の際に証明図を構成する InferenceRule の数が増えてしまいます。ここでは探索空間の最適化を優先することにして、公理は始シークエント InitialSequent として別途定義することにします。
そして、InferenceRule を継承して個々の推論規則を実装します。今回のように継承先によって異なる性質が要求される場合、Alloy ではシグネチャファクトで制約を記述するのが便利です。例えば以下の規則
sig NotRight extends InferenceRule {
} {
one premises
some f : Formula, n : Not {
f in premises.antecedents
f in n.of
n in conclusion.succedents
premises.antecedents - f = conclusion.antecedents
premises.succedents = conclusion.succedents - n
}
}
は否定の導入規則
に対応しています。
同様にして各論理演算子に対応する規則 NotLeft, AndRight, AndLeft, OrRight, OrLeft, ImplyRight, ImplyLeft を定義しておきます。
なお、すでに述べた通りシークエントに登場するコンテクストを集合として実装しているため、構造規則が必要ない（逆に言えば表現できない）ことに留意しましょう。また cut 規則も本質的には必要ないはずなのであらかじめ外しておきます。
証明図の実装
最後に、ここまで登場した要素を積み上げて全体で一つの証明図になるよう制約を加えます。
fact noIsolatedFormulae {
Formula in Sequent.(antecedents + succedents)
}
sig RootSequent in Sequent {
} {
this not in InferenceRule.premises
}
sig InitialSequent in Sequent {
} {
some antecedents & succedents
}
fact rulesFormAProofTree {
one RootSequent
Sequent - InferenceRule.conclusion = InitialSequent
no r : InferenceRule | r in r.^(conclusion.~premises)
all s : Sequent - InitialSequent | one conclusion.s
}
ここでは、シークエントの中で特殊なポジションを持つものが in 記法により定義されています。
証明されるべき最終的な主張が RootSequent, また公理として扱われる始シーケント
が InitialSequent です (2015/12/23 誤植を修正)。
証明図全体は制約 rulesFormAProofTree により、RouteSequent を根とし、InitialSequent を葉とする二分木になります。
検証してみる
無矛盾性の検証
まず、ここまでに定義した Alloy モデルを使って、矛盾を表す前件、後件ともに空なるシークエントが証明されない（であろう）ことを確認してみましょう。
assert consistency {
no s : Sequent | s.antecedents = none && s.succedents = none
}
check consistency for 3
assert に対して check を実行すると、Alloy はアサーションに対する反例を探索します。シークエント計算が正しくモデル化されていれば、ここでは反例が発見されないはずです。
排中律の検証
もう一つ、今度は簡単な定理の例として排中律の証明を Alloy に探索させてみましょう。求めるべき主張は なので以下の
pred を満たす証明図を run で探索させれば OK です。
pred excludedMiddle {
some x : Atom, n : Not, o : Or {
x in o.left
n in o.right
x in n.of
RootSequent.antecedents = none
RootSequent.succedents = o
}
}
run excludedMiddle for 3
以下のような結果が出力されます。
まとめ
とりあえず、今回は試みとして最も単純な古典命題論理のシークエント計算を Alloy でモデル化し、証明を自動探索させてみました。
この他にも例えば、真偽値をシグネチャとして用意し、論理式の評価結果を制約として加えれば、シークエント計算の健全性を示すことができるかもしれません。また、他の体系、例えば直観主義に変更すれば、上で示した排中律の証明は発見できなくなったりするはずです。次なる拡張の方向性はいくつかありそうですが、それはまた別の話。
NGK2015B で AWS + Alloy について話してきました
先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。
www.slideshare.net
当日の動画は [3] NGK2015B（名古屋合同懇親会 2015 忘年会） - YouTube から見ることができます。
TL;DR
- AWS でインフラ運用中
- でも設定が
大人の都合でカオスになりがちだったりして辛い - よろしい、ならば形式手法だ
サンプルコードを動かしてみよう！
まずはインストールしてみる
公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。
java -jar alloy4.2.jar
でウィンドウが起動すれば OK です。
なお、dmg 版も提供されていますが、Mac の人は（少なくとも現状）これをインストールしてはいけません。"Requires Java 6" と宣言している通り、内部のソルバ部分の実装が古い Java ランタイムに依存しているようで、Java 8 では起動できません。ちなみに現在 id:osiire さんが修正版を fork しています。
早速、検査してみる
今回の LT で使用したサンプルコードが Alloy による AWS セキュリティグループのモデリング · GitHub にあるので、手元にダウンロードして Alloy で開いてみましょう。
そしておもむろに Execute をクリック（または command + E）で
条件に合う設定が自動で探索されるはず。おめでとうございます。これであなたも立派な Alloy エンジニア！
ちょっと条件を変えてみる
Next を押すと、条件に合致する例が次々と表示されるのがわかると思います。しかし数が多すぎるし、各々の違いが解りにくいですね？
探索させる条件である run に対して、それぞれの要素（Alloy では atom と呼びます）の個数を制限することができます。以下のように変更して再度実行してみましょう。
run {
some disj i1, i2 : Instance, proto : Protocol, port : Port
| inboundOK[i1, i2, proto, port] &&
outboundOK[i1, i2, proto, port]
} for 2 Instance, 2 IP, 1 CIDR, 1 SecurityGroup, 2 Rule, 1 Port
ちょっとだけ図がすっきりしました。ちなみに、上記を 1 Rule にすると探索が失敗することも確認してみましょう。インスタンス間の通信が成立するためにはインバウンドルールとアウトバウンドルールが少なくとも 1 つずつ必要ですからね。
さて、セキュリティグループのルールに直接 CIDR を指定すると、何のサーバなのかわからないし、後々管理が辛くなりそうですね？「すべてのルールについて、source / destination は（CIDR ではなく）セキュリティグループ名で指定する」という制約を加えるには以下のようにすれば OK。
run {
some disj i1, i2 : Instance, proto : Protocol, port : Port
| inboundOK[i1, i2, proto, port] &&
outboundOK[i1, i2, proto, port]
Rule.(source + destination) in SecurityGroup
}
他にも思いつく制約をいろいろ試してみましょう。
そしてその先へ……
さて、Alloy を少し触ってみてちょっと面白そうだと思ったあなたに、第一にお勧めしたいのがこちら。
Alloy の背景にある関係モデルも含めてしっかり解説されており、密度の高い良書です。サンプルや練習問題も trivial なものから歯ごたえのあるものまで幅広く掲載されており、これを完全にフォローすれば Alloy を使う上でもはや不足はないと言ってよいでしょう。
また、書名に Alloy は入っていないのですが、こちらの書籍も面白いと思います。
Alloy そのものというよりは、実際の仕様や開発ライフサイクルに対してどのように形式手法が関わるのかについて焦点を当てた、より実務者向けの参考書です。
ところで自分はといえば、
例の Alloy 本はとてもよい教科書だと思うのだけれど、如何せん敷居が高い。いつかあのエッセンスを抽出したもっとフレンドリなチュートリアルを書きたい。
— チェシャ猫 (@y_taka_23) 2015, 10月 5みたいな野望があったりなかったりするのですが、それはまた別の話。
第十二回渋谷 Java で Featherweight Java の話をしてきました
8 月 1 日に行われた第十二回渋谷 Java で Java の型システムについて LT をしてきました。以下が使用したスライドです。
ちなみに Featherweight Java を導入した論文はここで読めます。今回の LT では時間の都合上細かい内容をほとんど述べていないので、もし興味があればぜひ元論文に目を通してみると面白いと思います。なお LT で扱ったのは第 2 章で述べられている（ジェネリクスを持たない）FJ の部分です。
スライドの補足
型付け規則と簡約規則について、時間の制限もあり LT の中では例を 1 つずつ挙げるだけに留めました。しかしそのせいでスライド 25 ページ目の主張で "two impolite rules" という表現を用いて規則の詳細から逃げています。
元論文の系 2.4.6 (p.408) を見て頂ければおわかりのように、ここで言っている "two impolite rules" は
- ダウンキャスト式の型付け (p.404, Fig. 2,
T-DCast) - ダウンでもアップでもないキャスト式の型付け (p.404, Fig. 2,
T-SCast)
のことを指しています。FJ において、この 2 つの規則を用いずに型が付く式については正規系まで簡約したときに結果が値である、というのがもともとの主張です。
ジェネリクスの意味論
今回はシンプルな FJ についてのみ触れましたが、元論文ではこの後にジェネリクスを導入した体系 Featherweight GJ が論じられています。というより、分量的にもジェネリクスの方が元論文の「本体」で、今回紹介できた部分はいわばその前哨戦。
もし何か機会があればこのジェネリクスについても話したいと思っているのですが、それはまた別の話。
稼働中の Docker コンテナ内にファイルを転送するツール Docker Inject を作ってみました
ホスト側から run 中の Docker コンテナ内へ、ディレクトリごとコピーします。
背景
Docker を運用している上で、動いているコンテナの中にファイルを送り込みたくなったことはないでしょうか。ないですか？ 残念ながらあるところにはあるのです。とりあえず今回はあるということにして進みます。
docker cp コマンドを使用すれば「コンテナからホストへ」のファイル転送は可能ですが、逆に「ホストからコンテナへ」の転送手段は公式では提供されていないはずです。docker run 時に -v オプションを付けておいて、マウントされたディレクトリをファイルの受け渡し場所として使用することも不可能ではないですが、ご存知の通りすでに稼働しているコンテナに後から -v を設定することはできません。
無論、コンテナにファイルを送り込むと Dockerfile とコンテナの状態とが乖離することになるため、いわゆる immutable infrastructure の観点からは邪道です。公式で提供されていない理由もそのあたりにあるのでしょう。理想を言えばそういう状況は発生しないに越したことはないのですが、現実というやつはいとも簡単に我々を裏切るわけで、まあそういう経緯でこのツールは制作されました。
インストール
今回は Go のクロスコンパイル機能を使ってバイナリ配布にしてみました。解凍して出てきた実行ファイルを PATH が通っている場所に置けばそのまま使えます。
Releases · y-taka-23/docker-inject · GitHub
あるいは Go の処理系が手元にあるなら go get でも使用可能になります。
$ go get https://github.com/y-taka-23/docker-inject
使い方
docker-inject <コピー元> <コンテナ名>:<コピー先> で動作します。
ちなみに Windows の場合、<コピー元> のパスは \ 区切りですが、<コピー先> は Linux なので / 区切りで指定する必要があるのでご注意を。
動作原理
基本的には以下のようなコマンドを実行しているだけです。
$ docker exec -i <コンテナ名> bash -c 'cat > <コピー先ファイル>' < <コピー元ファイル>
これを実行すると
docker execでコンテナ内でコマンドを実行- その際
-iオプションによりホスト側の標準入力がコンテナ内の標準入力に接続される - ホスト側ではコピー元ファイルを標準入力に流し込む
- コンテナ内では
catが標準入力の内容をコピー先ファイルに書き出す
という過程を経て、ホスト側のファイルがコンテナ内に書き出されます。
直したいところ
現状の問題点として、以下がすぐに思いつきます。
- ファイルごとに毎回
docker execを実行しているため動作が遅い - コピー先のファイルは上書きされる。
-fとか-uオプションがない。
可能ならばいずれこの辺も対応したいところではありますが、それはまた別の話。
Dockerfile をパラメータ化するツール VoicePipe を作ってみました
ひとつの Dockerfile から複数の Docker イメージをビルドすることができます。
背景
インフラ環境まわりを Docker 化している場合、しばしば複数の Docker イメージを同時並行的に管理する必要が生じます。例えばミドルウェアのバージョンの組み合わせをいろいろ試したいとか、開発環境と本番環境とで設定を変えたいとか。
一方、一般的にイメージとしてビルドされる情報はすべて Dockerfile に記述されており、docker build コマンドの際にはパラメータを渡すことができないため、いきおい、一部分だけ異なる Dockerfile を複数管理する状況に陥ったりします。
これは面倒だし、Dockerfile に変更を入れるときに漏れが出ないとも限らない。できれば一元化したい。
VoicePipe はこのような状況に対応し、単独の Dockerfile にパラメータを導入して、そこから相異なる複数の Docker イメージをビルドするためのツールです。
インストール
$ go get https://github.com/y-taka-23/voicepipe
使い方
例として、開発環境用と本番環境用に、index.html の内容がそれぞれ異なるふたつの Nginx の Docker イメージを作成する必要があるとしましょう。
最終的な作業用ディレクトリの中身は次のようになります。ちなみに同じものが GitHub リポジトリの example 以下に作成してあります。
+--- Dockerfile +--- index | +--- index_develop.html | +--- index_latest.html | `--- index_production.html `--- voicepipe.yml
まず、Dockerfile の中身は次のようにしましょう。差し替える予定のパラメータとなる部分が、ENV コマンドによって環境変数 INDEX_HTML として定義されていることに注意します。
FROM nginx
ENV INDEX_HTML index_latest.html
COPY index/${INDEX_HTML} /usr/share/nginx/html/index.html
次に、必要なイメージのパラメータを voicepipe.yml に記述します。
repository: user/nginx images: - tag: develop description: "for the development environment" parameters: - name: INDEX_HTML value: index_develop.html - tag: production description: "for the production environment" parameters: - name: INDEX_HTML value: index_production.html
最後に voicepipe.yml と同じディレクトリ内で
$ voicepipe build
を実行すると、ふたつの Docker イメージ user/nginx:develop と user/nginx:production がビルドされるはずです。もちろん、各々のイメージ内の index.html にはそれぞれ対応するものが COPY されています。
動作原理
ls -a などを実行するとわかりますが、ビルドしたあとの作業ディレクトリには次のような隠しディレクトリ .voicepipe が生成されています。
+--- .voicepipe | +--- develop | | +--- Dockerfile | | `--- index | | +--- index_develop.html | | +--- index_latest.html | | `--- index_production.html | `--- production | +--- Dockerfile | `--- index | +--- index_develop.html | +--- index_latest.html | `--- index_production.html +--- Dockerfile +--- index | +--- index_develop.html | +--- index_latest.html | `--- index_production.html `--- voicepipe.yml
また .voicepipe/develop と .voicepipe/production の中にある Dockerfile を見ると、voicepipe.yml の指定に従って ENV 行が書き変わっているのがわかるはずです。実際にビルドされているのはこれら生成された Dockerfile です。
なお、Dockerfile を Git で管理している場合はこの .voicepipe は邪魔なので、.gitignore で無視させるか、あるいはビルド後に voicepipe clean を実行すると削除してくれます。
その他
ちなみに、voicepipe list を実行するとビルドできるイメージとその説明が一覧で表示されたり、voicepipe build -L とするとついでに元の Dockerfile を latest タグでビルドしたりします。
なお、Docker 1.6 から、Dockerfile 中のLABEL 行でイメージにラベルを付与する機能がつきました。VoicePipe でもこのラベルを設定できるようにしようかと思っているのですが、それはまた別の話。
NGK2014B で SPIN について話してきました
名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。
内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。
当日の動画は Youtube から見ることができます。
ちなみに、発表順は乱数で決められているはずなのですが、なぜか去年の NGK と全く同じ 3 番目でした。
リソース共有問題の Promela モデル
LT の冒頭に登場するリソース共有時のデッドロックについて、Promela で記述したモデルが Gist においてあります。
この Promela モデルは、次のようなシステムを想定したものです。
- クライアント
- スキャナもしくはプリンタのどちらかをロックし、その後もう片方をロック
- スキャナもしくはプリンタのどちらかをアンロックし、その後もう片方をアンロック
- リソース (スキャナ、プリンタ)
- ロックするメッセージを待ち、相手のプロセス ID を記憶
- アンロックするメッセージを待ち、相手のプロセス ID とロックしたプロセスを照合
- ロックとアンロックが同じプロセスからのものならば最初に戻る
すぐわかる通り (LT 内でも述べていますが) このシステムには欠陥があり、デッドロックが発生します。スキャナとプリンタにロックを掛ける順番が指定されていない (そして Promela がそういう非決定的な記述を許す) というところがポイントです。
いずれこのモデルを題材にして Promela/SPIN の入門記事でも書くつもりではありますが、それはまた別の話。
Coq で Quine
Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごとく Gist 上 https://gist.github.com/4700318 にも同じものを置いておきました。
Coq の特性あれこれ
Quine なるものを初めて聞いた人は wikipedia:クワイン_(プログラミング) あたりを見てみましょう。「自分自身のソースコードを標準出力する。ただし空ファイルでなく、入力は受け付けない」というのが一般的な Quine のお作法ですが、Coq で書くにはいくつか考えねばならない点があります。
標準出力……。
最大の問題として、Coq 単体では出力ができません。純粋すぎる相手というのは得てして扱いにくいものです。悩んでどうにかなる問題でもないので、コードの最後を Eval compute in として、ここが評価されたときにコード全体と同じ文字列になることを目指しました。
文字列の扱い
大部分の言語と違い、Coq は文字列を扱うのにいちいちライブラリを読み込む必要があります。使うライブラリは Ascii と String。
ascii 型の方はコンストラクタの引数に bool を 8 個取って、8 ビット ASCII コードとして読むものです。
Inductive ascii : Set :=
Ascii : bool ->
bool -> bool -> bool -> bool -> bool -> bool -> bool -> asciiちなみに実験してみるとわかりますが、引数の順番は下位ビットが先です。
Eval compute in Ascii true false false false
false false true false.
= "A"%char
: asciiまた、string 型の方はリストと同じ構造を持っています。
Inductive string : Set :=
EmptyString : string | String : ascii -> string -> stringEmptyString が nil、String が cons 相当のコンストラクタですね。string_scope を開いておくと文字列の結合 append が + でシュガーされるので、見やすくするためにこれを使いました。
クォーテーションの扱い
文字列のデリミタは " です。Quine を書く上で、文字列の中に " が出現するためエスケープを考える訳ですが、ここで若干問題が。どうも Coq では (少なくとも CoqIDE の表示上は) 記号 " を単体で表示させることができないようです。実際、ASCII コード 34 を評価すると
Eval compute in ascii_of_nat 34.
= """"%char
: asciiとなり、"" で一文字分 (つまり "" が " のエスケープ表現) となっていることがわかります。ここは若干不本意ですが、「表示文字列中の " と "" との差には目をつぶる」として逃げることにしましょう。
Quine の実装
以上のことを踏まえて具体的なコードを作っていきましょうか。
まず大まかな構造として、次のような形を考えます。
Definition Q : string := [空欄 A]. Eval compute in [空欄 A'].
この Eval compute in [空欄 A']. でコード自身が表示されればよいわけです。
ステップその 1
Definition と Eval の二つの文がある以上、[空欄 A'] はこの二つの文をつなげた文字列が入るはずです。そこで、次のような形になることがわかります。
Definition Q : string := [空欄 A]. Eval compute in [空欄 B] ++ "." ++ [空欄 C].
非形式的な言い方をすれば、[空欄 B] が「Q にしかるべき文字列を代入せよ」、[空欄 C] が「「このコードを表示せよ」を表示せよ」を表す部分です。
ステップその 2
次に、[空欄 C] について考えます。意味するところが「〜を表示せよ」なので Eval compute in を入れたいところですが、そうすると堂々巡りになってしまいそうですね。回避策として、前半で定義している Q を参照します。
Definition Q : string := [空欄 A]. Eval compute in [空欄 B] ++ "." ++ Q.
そうすると、Q は「〜を表示せよ」でなくてはならないため、Eval compute in で始まることがわかりました。
Definition Q : string := "Eval compute in [空欄 D]". Eval compute in [空欄 B] ++ "." ++ Q.
ステップその 3
次に埋めるべきは [空欄 B] です。ここには前半部に対応する「Q に 「Q の中身」を定義せよ」を意味するコード文字列が入るはずですね。「Q の中身」を文字列として表すのに、冒頭に挙げた参照文献では Q に対して Haskell の show を使っています。Coq に show はないので、手動でデリミタ " を付けましょう。文字列「Q の中身」は """" ++ Q ++ """" です。
Definition Q : string := "Eval compute in [空欄 D]". Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
ステップその 4
これでほとんど完成しました。後は [空欄 D] として、実際に Eval compute in の引数になっている「"Definition Q : string := " ++ """" ++ Q + """" ++ "." ++ Q.」をそのまま持ってきてエスケープすればオッケー。
Definition Q : string := "Eval compute in ""Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.". Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
完成！
ライブラリの読み込みなどを追加し、また見やすくなるように適宜改行を入れたりした完成品が以下になります。はてなブログのベタ打ちだと若干見づらいですが、Gist の方を見てもらうと地の文と文字列との境目が分かりやすいかと。
Require Import Ascii String. Open Scope string_scope. Definition Q : string := " Eval compute in "" Require Import Ascii String. Open Scope string_scope. Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.". Eval compute in " Require Import Ascii String. Open Scope string_scope. Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
その他補足
ここで書いた Quine は当然ですが最短ではありません。改行が無駄ですし、型宣言も省略できます。あるいは、今回は構成手順に重きを置いたためこの形になりましたが、もしかしたらもっと本質的にいい書き方があるかもしれません。しかしまあ、そもそも Coq は短く書くことに向いた言語ではありませんし、無理に追求はしないことにしましょう。なお、どうしても短い Quine が書きたい人は wikipedia:HQ9+ あるいは PHP の利用をおすすめします。
ちなみに今回は深入りはしませんが、「自分自身のコード」に言及する上でキモになっているのが [空欄 C] の中身「「このコードを表示せよ」を表示せよ」という部分です。こういう表現の背後には Kleene の再帰定理があり、またかの有名な不完全性定理の証明と関係があったりして面白い部分ではあるのですが、それはまた別の話。
