bonotakeの日記

ソフトウェア工学系研究者 → AIエンジニア → スクラムマスター・アジャイルコーチ

ディープラーニングをやる人向け『仕事ではじめる機械学習』のオススメと注意点

ディープラーニング 機械学習 書籍

はじめに

明けましておめでとうございます。今年もよろしくお願いします。

たまたま昨年末に、Facebookの謎な対応により始めてしまったはてなブログ、「次書くかどうかわからない」とは書きましたが、次も書いてみることにしました。

なぜそう思ったか、理由は2つあります。1つは、日頃はTwitterかFacebookばっかりやっている自分ですが、そっちだとどうしても書いたものが流れてしまって、あとから自分で見返したくても見返せないこと（特にFacebook。TwitterはTwilog使ってるのでまだマシ）。

もう1つは、とある本について、どこかに書き留めておきたいなぁ、と思ったこと。

その本の名前は、『仕事ではじめる機械学習』です。

仕事ではじめる機械学習

仕事ではじめる機械学習

経緯

この本、最初は同人誌だったものが、オライリーから昨年10月に電子書籍として発売されたところ、ベストセラーとなって、今月1/16に紙の本（ソフトカバー本）が改めて発売するとのこと。

僕はこの本、電子書籍が出た割と直後くらいに買いまして、非常に感銘を受けました。

早速、機械学習（ディープラーニングですが）でメシを食っている勤務先にも布教しました。会社でも電子書籍を購入しまして*1、エンジニアだけではなく、ビジネス開発やセールスのメンバーにも読んでほしい、と、社内Slackで宣伝しまくりました。

ただ、一方で。

「機械学習」でなく「ディープラーニング」を飯の種にしている人間からすると、多少気になる点があり、ついこんなツイートを。

そしたらその後、著者の1人である有賀さんに初めてお会いしたとき、いきなり「ディープラーニングだとどこが違うんですか？」などと質問され、（わーおしっかりチェックされとるやんかーい！）と冷や汗をかいたり……

そんなこんながありましたんで、（たぶん沢山有るので今更ですが）簡単ながらこの本の紹介と、普通の機械学習（ML）でなくディープラーニング（DL）を使う人の場合、どういう点に注意して読めばいいのか、という辺りを書きたいと思います*2。

『仕事ではじめる機械学習』のススメ

この本、何がいいかといいますと、あくまで「ビジネスで機械学習システムを組む人のための本」、になっているということです。

「機械学習」ではなく、「機械学習システム」*3であることがポイント。機械学習をすることが主目的ではなく、あくまで、実現したい製品／サービスのために機械学習を用いる、というスタンスが首尾一貫している、ところがいいのです。

ですので、機械学習そのもののテクニカルな説明は、要点は押さえつつも最低限に抑えられています。それよりも、機械学習をどう使うか、機械学習プロジェクトをどうマネジメントするか、機械学習製品・サービスをどう構築するか、のノウハウ解説に力点が置かれています。こういう本は、洋書を含めて他にないのではないでしょうか。

特に1章『機械学習プロジェクトのはじめ方』には「機械学習をしなくて良い方法を考える」という項目があります。そこでは機械学習をシステムに組み込むデメリットもしっかり書かれています。一般企業の中で機械学習を使おうか、と考えるときには、当然こうした、メリット・デメリットを天秤にかけた冷徹な視点が必要です。

まぁ私のいるディープラーニング専業の会社では「ディープラーニングを使わない」＝失注、なわけですが（汗）、ただ、お客さんに「ディープラーニングならなんでもできるに違いない」といった過度な期待とともに依頼されて「何だよできねーのか」と失望される、よりは、冷静にこうした視点で臨んで頂いたほうが、僕らも助かりますし、いま過熱気味のAI/DL業界にとっても、その後のハイプの暴落度合いが小さくなるんじゃないか、と思っています。

ディープラーニングの人向け注意点

一方で、MLでなくDL視点で読んだ場合、この本がどういう点で「違う」のか、を、僕なりにさらっとまとめてみます。

主要なアプリケーションの違い

この本の後半（第7～9章）、応用事例として挙げられているのは、「映画の推薦システム」「Kickstartarの分析」「マーケティング資源の効率化」です。いずれも、データ分析とその応用、の話です。MLを用いるのは殆どの場合データ分析なので、これは当然です。

一方DLに興味がある人がやりたいのは、ある種のデータ分析もあるとは思いますが、多くは「画像認識・生成」「音声認識」「自然言語処理」といったものへの応用じゃないかと思います。 データ分析、といえばその通りなのですが、恐らくピンと来ない人も多いのではないかな、と思います。 なのでDLに関しては、もっと違った応用事例を読みたいな、と思ってしまいます。

あと敢えて述べるなら、この本では主にWebがフロントエンド、DBがバックエンドにあるシステムが想定されていて、MLは確かにWebシステム・Webサービスで用いることも多いのですが、DLの場合はどうなんだろう？とは思います。これは僕の会社が主に組み込み系を主体にやっているせいもあるんですが、相対的にWebシステムへの応用度合いは、MLより低いのでは？と思います（この辺はあくまで僕の肌感覚で、実際のところはわかりません）。

適用の仕方の違い

MLにおいては、特徴量の設計（feature engineering）が、品質の良いシステムを構築するための重要なファクターになります。特徴量とは、「機械学習の予測モデルに 入力をする情報のこと」（同書より引用）です。どの特徴量を選ぶか、どう機械学習に組み入れるかで、機械学習の精度がガラッと変わってしまいます。

一方DLでは、どの特徴量を用いるかも学習されるため、DLシステムの開発者が気にする必要はほとんどありません。よって、DLではこの工程は事実上省かれることになります。

DLでは、MLの「アルゴリズムの選定」に相当する「ネットワークの選定」が最初のポイントになってきます*4。多くは、これまで様々な大学・企業が色々なアプリケーション向けに設計した既知のネットワーク（画像からの物体検出なら「YOLOv2」、とか）のうち良さそうなものを選定することになります。場合によってはオリジナルのネットワークを組む人もいるかもですが、「実際に性能が出るのか」の評価から行わないといけないので、ごく稀です。【1/9追記】ここ、同僚からツッコミがありました。ベースラインとしては既知のネットワークを使うけど、そこに色々手を加えてカスタマイズすることはよくあるとのこと。なので訂正しときます。【追記おわり】

あとは、教師データの準備がML以上に大きな比重を占めます。特徴量などを人手で設計する必要がなくなった分、DLでは大量の教師データが必要で、これをどこからどうやって調達するか、が実は一番大変だったりします。

その後は、ひたすら計算機をぶん回して学習させます（バッチ学習の場合）。ここが極めて時間がかかる（場合によっては数日とか）ので、DLを専業にしている会社は学習時間をいかに短縮するかのノウハウが色々あったりするようです。

……ん？ ウチ？ あれ、どうだったかな（汗）

とはいえ

やはりDLもMLの一種ですし、共通点は多いです。教師データをどう準備するか、（ハイパー）パラメータのチューニング、実システムにおける問題点への対処方法、などなど。

過学習や汎化性能などの問題も当然ありますし、恐らく気にしている人は気にしているかもですが、DLは一般的な傾向として汎化性能が高いこともあって、普通のMLほど敏感になる必要はないかもしれません。ただし、「トレンドの変化などで入力の傾向が変化する」（同書より引用）可能性は、アプリケーションによってはDLでも発生し得て、なのでやはりDLシステムでも気をつけなければなりません。

最後に

ということで『仕事ではじめる機械学習』、極めて面白いしオススメなのですが、僕の感想は究極的には、次の一言に尽きます。

いやホント、誰か書いて。

……と、こういう場合の典型的な切り返しが「言い出しっぺがやれ」だったりするんですが。

実は水面下で、「ディープラーニング版『仕事ではじめる機械学習』になるかもしれない本」の企画を進めています。まったく同じ趣旨になるかどうかはわかりませんが、ディープラーニングで仕事をしたい人向けの本を世に出すべく、画策中です。

そんなすぐには出ないかもしれませんし、企画がポシャるかもしれませんが、まぁ、乞うご期待、ということで。

【1/9追記】かなり反響あったんで、補足を書きました。↓ bonotake.hatenablog.com 【追記おわり】

*1:「紙で読みたい」という人もいたので、ソフトカバー本発売決定にあたり、そちらも予約注文しています。

*2:読み終わってから少し時間が経っているので、詳細に突っ込んだ話はしません。読み終わった当時は色々と思っていたこともあったのですが、今は若干記憶がぼやけ気味なのが残念。もう少し早くにまとめておくべきだった。

*3:この用語が本で用いられているわけではありません。ただ前回の記事でも述べましたが、僕は現在「機械学習工学研究会」（機械学習のためのソフトウェア工学を研究する会）を立ち上げようとしてまして、そのコミュニティの中で僕はこういう用語を使っています。

*4:1/8追記：有賀さん（chezouさん）からブコメ頂いてる通り、この辺は『仕事ではじめる機械学習』でも軽く触れられています。

2017年を振り返って

雑記

はじめに（おことわり）

これは、僕がはてなブログに書く初の記事になります*1。

元々これは、Facebookに友達限定で書いた記事を、一般公開向けに少し改訂したものです。なぜこんなことをしているかというと、FBに書いた記事、FBからスパム認定食らって削除されてしまったもので……なんで？？！！（1/2追記：本日スパム認定は取り消されました。）

長文すぎたのか、とか、マネーフォワード推しすぎたのか、とか、色々想像は膨らむのですが、はっきりした理由はわからず。

で、今回はたまたま他所で下書きしてて、たまたまその下書きが残っていたので、折角なので……とこっちに転載することにあいなった訳です。

なお、僕は元々『たけをの日記＠天竺から帰ってきたよ』なる「はてなダイアリー」を過去に書いていたのですが（今回はてなブログ開設にあたって記事をこちらにインポートしています）、ほとんどtwitterとFacebookに軸足を移したため徐々に更新頻度は落ち、最後の記事から3年以上更新は止まっていました。

そういう意味で、今後も更新するかどうかはわかりませんので、どうかご承知おきを。

2017年を振り返って

さて、新年まであと数時間となったところで、ここに今年の振り返りをしておこうかと。 今年は大きく3つの出来事がありました。

１．転職したこと

何を置いてもまずはこれ。人生の大きな転換期になりました。

きっかけは、まぁ僕の前職をご存じの方は（ネット上に細かい経歴載ってますので、簡単にわかります）お分かりのとおり、勤めていた会社の経営不安にあったのですが。結果としては、会社飛び出して大正解だったな、と。今んとこ。

今から思えばここ何年か、何とも言えない停滞感に苛まれていたというか、色々がんじがらめの会社の中でどこか汲々としていて、自分に対する自信もかなりの部分失っていたように思います。

環境変えて、しかも大企業から急成長しているベンチャーに飛び込んで、新しい空気を吸えたことで、今まで失っていた色々を回復しました。

新しい会社も、もちろん問題はないとは言わないけど、今のところ、皆目標に向かって自律的でアクティブに動いてるし、アットホームな雰囲気もあるし、すごく気に入ってます。

ベンチャー特有の？「自分が頑張らないと潰れるかも……」というプレッシャーも適度なスパイスになってますｗ

２．ML×SEの活動がスタートしたこと

多少転職に絡まなくはないんですが、始まったのは転職前のことです。

前職でも、今まで培ってきたソフトウェア工学の知見を機械学習に活かせないか、といったモチベーションで潜航的に研究をしていたのですが、そこに来て、今年のSESでのパネルが非常に面白く、Facebookに感想エントリーを書いたのでした。

https://www.facebook.com/bonotake/posts/1504893489556668

そしたら、このエントリーがきっかけで、実際に「機械学習×ソフトウェア工学」を考えるコミュニティを作ることに。

そしていくつかの偶然が重なって、結果として、来年度に日本ソフトウェア科学会傘下で、新たに「機械学習工学研究会」（MLSE）を立ち上げようと今動いています。

長らく研究職に携わってましたが、まさか自分が研究会の立ち上げに回るとは思ってもおらず。

前はとにかく、自分が論文を書いてpublishすることが唯一の貢献の手段だと思っていたし、周囲からもそれが求められていたのですが、幸か不幸か、公的には研究職を離れたことでその呪縛からも逃れ、こういう、もっと違うアプローチで貢献するのもアリだな、と、一段俯瞰した視点で考えられるようになりました。

特にこの「機械学習のためのソフトウェア工学」という分野は、特に国内では誰も手を付けられていない研究分野だと思っていて、そういう意味で、国内での研究の萌芽を促していきたいです。自分が論文を書くことはなくても（機会があったら書きたいけど）、他の人が次々に研究をし、論文を書ける土壌を作れればいいな、と。

内向きの仲良しクラブ的な研究会も存在しますが、MLSEはそういう風潮には陥らず、多くの研究者やエンジニアに開かれた、オープンな活動をしていきたいな、と思っています。

３．マネーフォワードを使い始めたこと

moneyforward.com

話はガラッと変わってしまうのですがw 地味にこれが生活を変えました、っていうか非常に助かってます。

使い始めたきっかけは、前職で給料減らされてｗ 色々節約したくて、まずは家計簿つけるか、と考えたのが始まり。

しかしこれが、使い始めてみると非常に便利で。単なる家計簿という枠を越えて、ありとあらゆる手持ち資産を一括管理できるのです。これ使うまで、自分の手持ち総資産がいくらか、ということもまともに把握できてなかったし。各所に散らばった口座を全部まとめて、どこにいくらあるのかわかるし、どこでいつ何をいくら買ったのかとか、全部可視化できるようになりました。Fintech万歳。

そしてこれが地味に影響があったのが、やはり転職のときのドタバタで。前職では企業年金もあれば給与引き去りで財形貯蓄ができたりとかしたところ、そういう制度が一切ないベンチャーに移って、その手の資産運用を自分でやる必要性が出てきました。ほんの僅かですが、退職金も出たし。

今までだったら、そのへん全部とっ散らかって終わってたと思うんですが、マネーフォワードがあるお陰で1円単位で管理できるので、ズボラな自分でもすごくやりやすい。

まぁまだ「運用」なんて大げさなものはやってないし、今年は色々手続きしただけで終わってしまいましたが、来年からは自分でもなんとかなりそう。

そんなこんなで、何かとっ散らかってしまいましたが、今年の3大出来事でした。

*1:これより過去の記事は、僕が「はてなダイアリー」で書いていた記事をインポートしたものです。

Alloyで直積を考える

Alloy

前回の続きです。正確には、前回の続きの後の檜山さんのブログ記事に対する更なる「合いの手」です。

一連の記事を読んでいろいろ考えているうち、実は直和だけでなく直積も問題だということがわかりましたｗ
ということで、前回とほぼ同じノリで直積も考えてみます。今回も使ったAlloy記述全文はGistに貼りました。
あと、上記檜山さんの記事の「関係圏を観察してみる」以降を適時引用します。Alloyは関係をベースにした言語なので、関係圏とは相性がとてもいいのです。

お膳立て

さっき問題あるとは書いたものの、直積は直和と違い、Alloyにはちゃんと言語機能としてあります。集合A に対して A->A と書きます。
なんで直積なのに関数型みたいな書き方すんの？という方にはこちらを。関係圏では（翻ってAlloyも）集合の直積は冪とか関数（関係だけど）とほぼ同一視できるようです。
ということで、このAlloyの直積を議論の対象として扱います。檜山さんの記事に合わせると、テンソル積と呼ぶべきですかね。

単位元（単位対象）

関係圏Relでは、ホムセット Rel(A, {0, 1}) はAのベキ集合にはなりません。Rel(A, {0}) がAのベキ集合なのです。{0}は単元集合1です。1は、関係圏においては始対象でも終対象でもありません（始対象＝終対象＝空集合です）。1は、テンソル積（集合の直積でした）の単位対象として特徴付けられます。

だ、そうなので、単元集合を持ってきましょう。
Alloyには特別特定の単元集合があるわけではないので、1からこさえます。と言っても1行で終了ですが。

one sig Unit {}

冒頭のoneで、必ず1個だけ存在する、すなわち単元集合であるという宣言をしております。

で、これがテンソル積の単位対象になってることを確かめてみます。
……といっても、単純じゃないんですよねこれ。要は、 Unit->A ないし A->Unit が Aと同型になっているって言えばいいんですけど。
同型であることの証明ってAlloyで書きづらい……*1

てなわけで、「集合のサイズが等しい」っていう、間接的な形で確認することにします。
ということで、以下のアサーションを。反例出ないと思います。

check {
  all a: set univ {
    #(Unit -> a) = #a
    #(a -> Unit) = #a
  }
}

対角、余対角

対角ですが、こんな感じで。直和の時とほとんど感覚は同じです。

fun diagP (a: univ): univ -> univ {
  a -> a
}

適当な集合Aに対して、A->Aを作って返してやるだけです。
一方余対角ですが、ないらしいので、

論理積∧は、p, q:A→1 に対して、δA;(p×q);ρ と定義する。ρ:1×1→1 は、テンソル積の単位法則に伴う自然同型。

にあるρ:1×1→1 （ここまでの書き方に沿えば、ρ:(Unit->Unit)->Unit）をこさえましょう。こんな感じです。

fun ro (r: Unit -> Unit): Unit {
  Unit.r
}

rの頭からUnitと結合して、r: Unit->Unitの後ろ側の成分（第二成分）だけを取り出して返します。
え？第一成分は要らないの？これでいいの？？ とお思いになるかもしれませんが……一般的にはダメかもしれません。しかしAlloyの矢印型直積を使う分には、これで構いません。この理由は後で述べます。
で、せっかくなので、上記の論理積 δA;(p×q);ρ を作ってしまいましょう。 まずは δA と (p×q) を結合するために、次のような関数をこさえます。

fun joinL (a: univ->univ, r: (univ->Unit)->(univ->Unit)): Unit->Unit {
  (a.univ).(r.univ.univ) -> (univ.a).(univ.(univ.r))
}

aの第一成分とrの第一成分、第二成分と第二成分を結合して、改めて -> でつなぎなおします。これも、直和のときに考えた結合と、基本的な理屈は同じです。

以上の diagP（δA）とjoinL（結合子 ; ）、ro（ρ）をつないで、さっきの論理積の定義を書き下します。

fun prodL (f,g: univ -> Unit): univ -> Unit {
  {x: univ, u: Unit | u = x.diagP.joinL [f -> g].ro }
}


こうして、論理積 f ∧ g が定義できたんですけども。
これって結局、やっぱり、Alloyでいうところの

f & g

と同じなんですよね。実際、以下のアサーションは反例出ないです。

equiv_product: check {
  all f, g: univ -> Unit | prodL[f, g] = f & g
}

ということで、直和の時とオチもほぼ同じでした。ちゃんちゃん。

ちなみに、以前紹介したドメイン付きクリーネ代数のAlloyモデルですが、命題をPropのべき集合（set Prop）で与え、論理積はその間の集合積 & で書いてました。この辺とややつながった感じ？

直積にもいろいろある

で、上記 ro の定義がなんであんないい加減でいいのか、というお話ですが。
実は、ひとくちに「直積」と言っても、ビミョーな差でいくつか種類があるのです。それで「Alloyの矢印型直積を使う分にはこれで構わない」なんてビミョーな表現をしたのです。


ro の引数 r: Unit -> Unit （＝Unit×Unit）ですが、具体的に何種類の値があるかわかります？
Unitが単元集合だったので、Unit型の引数にはたかだか1要素しか入りません。なのでUnit×Unitなら、第一成分、第二成分それぞれに「ある」（Unitそのもの）か「ない」（空集合 none）かの2択しかなく、よって r は 4種類。
……と見せかけて、実はAlloyの場合、2種類しかありません。Alloyの直積はstrictな直積（スマッシュ直積とかいいます）になっていて、片方の成分が空集合なら、ただちに全体も空集合になります*2。なので、第一成分、第二成分とも「ある」か、両方ともなかったことになるかの2択なのです。
一方、一般的な集合の直積、集合圏の直積はstrictではなく、なので片方が空集合というだけで全体が空集合と完全にイコールにはなりません（同型にはなるけど）。ということで、ビミョーに違うんですね。
なので roは、本当なら「第一成分と第二成分がともに空でない場合に単元集合を返す、そうでなければ空集合を返す」と書くべきなんでしょうが。現実的には、どっちも空でないかどっちも空か、しか選択肢がないので、片方だけ参照する、という上の定義で成り立ってるわけです。

Alloyプリミティブの直積 -> じゃなくて、新たに一般的な直積を起こせばよかったのかもしれませんが、面倒くさかったのでした。はい。

*1:天下りに同型射を与えればいいんですけどね。

*2:スマッシュ直積云々はこちらでもちらっと書いてますが、って8年半も前の記事だよ。わーお。

Alloyで直和を考える

Alloy

前回の記事に檜山さんが反応してくださいまして。いやレスつけにくい記事ですいません。

せっかくなので、檜山さんの記事をまんまAlloyに翻訳してみよう…と思ったのですが*1、実は大きな問題があって。

Alloyには、直和を直接扱う言語要素がないんですなー。

ということで前振りとして、Alloyで直和を書き下してみて、どうなるかってのを観察してみます。

今回使うAlloyの記述全文はGistに貼ったので、よろしければそちらを参照のこと。

えーまず

いきなりですが、直和をこさえます。どーん。

enum Tag { Fst, Snd }

fun prod1(a, b: univ): Tag -> univ {
  Fst -> a + Snd -> b
}

prod1が、適当な集合a, bを受け取って（univは何でもアリな型です。java.lang.Objectみたいな）、aとbの直和を返す関数。返り値の型 Tag -> univ が直和型です。脳内でそういう風にフィルタかけて読んで下さい。
やってることは見ての通り、１番め・２番め（Fst, Snd）ってタグを付けた上で集合和を取るんですね。
prod って書いてるのは、上記の檜山さんの記事にある「（圏論的）直積＝（圏論的）直和」に倣ってるので、ここでは良いネーミングじゃないかもですが。

試しに

run prod1

とか打ってevaluate ... してみても、ビジュアル的にはあんまり面白くないものが出ます。Evaluatorボタンを押して、prod1に適当な引数渡して評価してみてください。

対角、余対角

さて、任意の要素を直和に持っていく対角Δは次のように書けます。

fun diag (a: univ): Tag -> univ {
  Fst -> a + Snd -> a
}

diagがΔに相当する関数です。Fstタグ、Sndタグに同じ要素を入れた直和を返します。

一方、直和から要素に潰す余対角∇は

fun codiag (a: Tag -> univ): univ {
  { b: univ | b in Fst.a or b in Snd.a }
}

とか書けます。直和のFstタグ側かSndタグ側か、どちらかにある要素の集合、です。
…ですがこれ、もっと簡単にかけて、

fun codiag (a: Tag -> univ): univ {
  Tag.a
}

です。ついてるタグを忘れる操作。


そして、対角と余対角を合成すると、idと同じになります。
これは以下のアサーションで反例が出ないことからわかっていただけるかと。

cmp_id: check {
  all x: univ | x.diag.codiag = x
}

単位元

さてここで、直和操作の単位元について考えてみます。これは、空集合（Alloyでいう none）でございます。檜山さんの記事にあった、零対象がこれに当たります。
noneとの直和取ったものは元の要素と同型です。
これは、noneとの直和取って、タグ忘れたら元に戻る、という意味の以下のアサーションで反例が出ないことから確かめられます。

zero_is_unit1: check {
  all x: univ {
    prod1 [x, none].codiag = x
    prod1 [none, x].codiag = x
  }
}

２項関係に拡張

さてさて、集合（＝単項関係＝アリティ１の関係）について、直和を考えることができました。
次は、２項関係＝アリティ２の関係の直和について。またいちいちこさえます。

fun prod2 (f, g: univ -> univ): Tag -> (univ -> univ) {
  Fst -> f + Snd -> g
}

prod1 とまったく理屈は同じです。

そして２項関係を考えたからには、他のものとの結合を考えたくなりますね。なりませんか？なるでしょ？
ということで。結合も作ります。（言語要素にないってめんどくさいねー）

fun join2 (x: Tag -> univ, r: Tag -> (univ -> univ)): Tag -> univ {
  Fst -> (Fst.x.(Fst.r)) + Snd -> (Snd.x.(Snd.r))
}

わかりますでしょうか。Fstタグ付きはFstタグ付き同士、Sndタグ付きはSndタグ付き同士で結合して、改めてタグを付け直しております。
直感的には x.r って操作をやりたい訳なんですが、直接は上手くいかないので、この関数で結合のドットを代用しようという腹です。

で、こうしてやると、元の檜山さんの記事にあった足し算の定義

Δ;(f×g);∇

ってのが書けるようになります。こんな↓感じ。

fun sum2 (f, g: univ -> univ): univ -> univ {
  { x, y: univ | y in x.diag.join2 [ prod2 [f, g] ].codiag }
}

diagがΔ、prod2[f,g] が f×g、codiagが∇。
適当なxに対して y ∈ x;Δ;(f×g);∇ となるようなyを集めて、ペア (x, y) の集合を作っているわけです。2項関係はペアの集合でできています。よってこれは、間に Δ;(f×g);∇ が成り立つような2項関係を作っているわけです。

これも run sum2 とかやって、Evaluatorで遊んでみてくださいな。


しかし、ですね。
Alloyでは、２項関係同士の足し算は直接書けて

f+g

なんですなー。

ということで、この２種類の足し算が同じもの、っていう、以下の様なアサーションを書いてみます。反例でないはずです。

sum_equiv: check {
  all f, g: univ -> univ | sum2 [f, g] = (f + g)
}

結論

以上、回りくどくなりましたが。
Alloyには表面上プリミティブに存在しない直和ですが、裏側に暗黙的に存在してて、立派に足し算を成立させることができているのです。

ということで、時間があったらこの結果を使って、Alloyで檜山さんの記事を書き直す試みをやってみます。時間があれば。

*1:実は前回も同じようなことを考えて途中でヘタれたのでした。

ドメイン付きクリーネ代数をAlloyで

Alloy 論理 算譜

久々すぎて、はてなの書き方を忘れてしまいました。

さて（脈絡なし）：

上記の記事を今更読んだのですが*1、そういや私め、昔テスト付きクリーネ代数…の拡張のドメイン付きクリーネ代数（Kleene Algebra with Domain, KAD）をAlloyで書いてみたことがありまして。
cf. [cs/0310054] Kleene algebra with domain -- arXiv
GitHubに置いてあるので、とりあえずリンク貼っときます。
このモデルでは、クリーネ代数はシグネチャProp上の2項関係 Prop->Prop で表現していて、ブール値はPropの集合で、乗法はドット結合、論理積は集合積で書いてました。たとえば、

(p∧q)・f = p・(q・f)

は

    (p & q).toKA.f = p.toKA.(q.toKA).f

と書けて（toKAはブールをクリーネ代数に持っていくおまじない）、こんな↓アサーションを書いてやっても反例は出ないようにはなっております。

def_and: check {
  all p, q: set Prop, f: Prop->Prop {
    (p & q).toKA.f = p.toKA.(q.toKA).f
  }
} for 10

以上、ほとんどメモ的な内容で具体的な説明なしで大変不親切なのですが。
最近またKADが自分内でリバイバルし始めてて、本当はがっつり解説書こうかと思ったんですが何かダレた。一部直観的でないところがあったり、今見るとイマイチだなーと思うところもあったりですが、とりあえず。
気分が乗ったら追加でまた書くかも。

*1:ちょうど自分がKATを知った頃に読んだのがこれで、そうかー檜山さん的にはイマイチなのかー、と思った記憶。

シグネチャのフィールドにある関係の多重度 続き

Alloy

昨日の日記 の続き。 id:koji8y さんから、トラックバックで

じゃあ，昨日のスタート Alloy の演習中に僕らが表現したかったこと，

sig A {
	r: B -> C
}

で，各 A の各 r が one to one の関係 (functional かつ injective な関係) となること*1を表現するにはどう記述したらいいでしょうね?
（略）

sig A {
	r: B -> C
}{
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in r and b->c2 in r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in r and b2->c in r) => b1 = b2
	}
}

とすると，表示したインスタンスは求めている形になっていそう．

でももっと簡単に記述できるるのではないかと...

と追加質問いただいたんですが…これって

  sig A {
    r: B lone -> lone C
  }

では？シグネチャファクト中の

  all b: B, c1, c2: C {
    (b->c1 in r and b->c2 in r) => c1 = c2
  }

って制約は

  all b: B {
    lone b.r
  }

と同じ意味に読めます。

実際、下記のように書いたアサーションで反例は（スコープをいくつにしても）出ないです。
（アサーションを記述するため、シグネチャファクトや宣言制約を述語内に書き下しています）

sig A {
	r: B -> C
}
sig B, C {}

pred p1 {
  all a: A {
	// functional (left-unique)
	all b: B, c1, c2: C {
		(b->c1 in a.r and b->c2 in a.r) => c1 = c2
	}
	// injective (right-unique)
	all b1, b2: B, c: C {
		(b1->c in a.r and b2->c in a.r) => b1 = b2
	}
  }
}

pred p2 {
  all a: A | a.r in B lone -> lone C
}

assert equivalence {
  p1 <=> p2
} 

check equivalence for 6

シグネチャのフィールドにある関係の多重度

Alloy

さて、スタートAlloy中、頂いたテクニカルな質問のうち1つに、当日うまく答えられませんでした（すいません… orz）。

ちゃんと考え直したので(^^; ここに書いておきます。（thx to @masahiro_sakaiさん）

質問

以下のようなシグネチャ宣言があったとする。

sig A {
  r: B one -> one C
}

ここで、Bのスコープを1にすると、任意の a: A から得られる a.r が全部同じになってしまう。
たとえば、以下のようなコマンドで反例が出ない。

check {
  all disj a1, a2: A | a1.r = a2.r
} for 3 but 1 B

たとえば a1.r は空で、a2.r は空でないような可能性があるように思うが、なぜないのか？

回答

まず、シグネチャのフィールドにある関係は、次のように解釈されます。（Alloy本 p.261）

…したがって、例えば

sig S {f: e}

という宣言によって導入される制約は、（fを通常の変数とした場合の）fが式eの部分集合であるという制約ではなく、以下のような制約になる。

all this: S | this.f in e

よって、先ほどのシグネチャA内のフィールドrの宣言は、

all a: A | a.r in B one -> one C

という制約だと解釈されます。（thisはaに置き換えました）

更に、関係の中の多重度についてですが、（Alloy本 p. 76）

多重度は単なる省略記法であり、標準的な制約に置き換えることができる。以下の多重度制約は、

r: A m -> n B

以下のように書き換えることができる。

all a: A | n a.r
all b: B | m r.b

とあります。コロンは in と読み替えても意味的には同じです。

ということで、先ほどの制約式を、更に展開すると

all a: A | all b: B | one b.(a.r)
all a: A | all c: C | one (a.r).c

となります。

なので、Bのスコープが1だと、B、C ともに空で a.r が常に空になるか、B、C ともにサイズ1で、aによらず a.r が存在して一意に定まるか、いずれかになります。

追記

続きを書きました → シグネチャのフィールドにある関係の多重度 続き - たけをの日記＠天竺から帰ってきたよ

注：bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。