Just $ A sandbox

プログラミングと計算機科学とかわいさ

Theorem Prover Leanの紹介

Agda Isabelle 定理証明

Microsoftが開発したTheorem Prover Leanを紹介します.

特徴

他の言語と軽く比較する.
あくまで個人的な感想です.

Lean Coq*1 Agda Isabelle
証明の書き方 structured proof, tactic, 函数定義 tactic 函数定義 structured proof, tactic
開発環境 emacs emacs, CoqIDE emacs jEdit
ドキュメント × ◎ ○ △
implicit parameter ○ ○ △ (型を使わないので不要)
Equational Reasoning ○(builtinなものはOK. 独自演算子は条件付き) ？(知らない) ◎ ○(基本的にbuiltinなもののみサポート)
自動証明 ×(なし？) ○(auto, omegaなど) △(emacsのautoコマンド) ◎(auto, force, sledgehammerなど)
ライブラリ ◎ ○？ △ ○
パフォーマンス ○？ ？(知らない) × ○

証明の書き方

なんとstructured proof(上から下向きに書ける), tactic, 函数定義の全ての書き方をサポートしている.
他の言語から入ってきた人にも優しい仕様.

開発環境

インストールはバイナリがあるのでそれを入れるだけ.
インストールするとleanemacsというアプリケーションが使えるようになる.
leanemacsではリアルタイムチェッカーが走るし, エラーメッセージも見やすいので(emacsが嫌いじゃなければ)そんなに悪くないと思う.

ドキュメント

公式サイトにTutorialとかがある.
HTML版はブラウザ上でLeanを動かすこともできてすごい.

しかしドキュメントらしきものはこのtutorial.pdfくらいしかなく, より詳細な情報でまとまった文章はおそらく存在しない.
Leanを本格的に使うならここが一番問題.

implicit parameter

カリーハワード対応を使って証明を書くような言語では, implicit parameterが使えるのは結構重要.
Coqは割と優秀と聞く一方で, Agdaは少し省略するとしょっちゅう警告ばかり出す.

ここに関してはLeanもそれなりに優秀で, たくさん省略してもエラーになったり警告が出たりはしない.

Equational Reasoning

独自演算子に対してのReasoningは, それがグローバルに定義された演算子なら, refl attributeなどを対応する命題に付与することで使えるようになる.
ただしstructure(データ型を定義するときに使う)内の演算子に対しては使えないなどの制約があるらしい.
同値関係を含む構造を定義して, それに対するreasoningを書くことが出来ないので微妙に不便.

ちなみに, reasoningはsubst(a == b & ==> P a == P bなど)を自動でやってくれるようで, 実はこれのおかげでLeanでreasoningをすると非常に証明が楽になる.
a == bを指定すると, aの部分を現在のGoalの左辺から探して代入する操作をやってくれるのでこちらでsubstを指定する必要がない.
Leanの目玉機能の一つ.

自動証明

ドキュメントにも書いてないから多分ないです.

追記:
どうもblastがそれに当たるらしい.
blast派生のコマンドがいくつかあって, 代表的なものとしてsimp(simp attributeがついた定理を適用する), rec_simp(帰納法が使える？)などがある.

ライブラリ

(駆け出しの言語にしては)標準で結構色々なものが揃っている.
HoTTライブラリが用意されているあたりもポイント.
拡張子 .hleanがそれ.

ところで, 現在LeanファイルをHTMLやpdfファイルに変換するツールなどはない.
ので.leanファイルを直接見る以外に証明を読む方法がないので(ファイルの依存関係がややこしい場合は特に)結構不便.

パフォーマンス

ちょっと書いた限り重くなったりする気配はあんまりない.
リアルタイムチェッカーが走っている割には軽くて快適. (ここでAgdaの方をチラ見する)

所感

色んな書き方ができるのは, 参入コストが下がると考えれば悪いことではないと思う.
Equational Reasoningでsubstを指定しなくていいのは予想以上に楽だったので, 普段苦労している人はこれだけでも触ってみる価値はあるかもしれない.
あとはリファレンスさえしっかり作ってくれれば2016年以降流行る可能性があるかもしれない.
むしろ流行ってくれ.

証明の例

参照

*1:Coq使ってないので適当言ってるかも.

オートマトンで遊ぶやつを作った

Haskell

この記事はHaskell Advent Calendar 2015 18日目の記事です.

Automatoy(オートマトン)で遊ぶやつを作ったので紹介します.

github.com

ブラウザで遊べる.
以下それっぽい解説.

Automatoyについて

http://myuon.github.io/automatoy/

"Def"タブでオートマトンを定義.
"Check"タブで与えられた文字列のacceptance checkができる.
"Conversion"タブでいくつかのサンプルオートマトンを読み込んだり, NFAをDFAに変換(いわゆるpowerset construction)できる.

また, 右上のImport/Exportでjsonに変換したり, jsonを読み込んだりできる.

もう少し扱えるオートマトンのバリエーションを増やしたり, acceptance checkにアニメーションを取り入れたり, アルゴリズムを増やしたり(complementとかそういうやつ)したら面白そう.
ものすごく気が向いたら頑張って開発する. (たぶんしない)

オートマトンの絵を書くのには, Cytoscapeを使った.
Haskellでコードを書いて, HasteでJavascriptにコンパイルしている.

HasteとTemplateHaskell(以下TH)

Hasteでは現在THがサポートされていないのでlensを含む, THが使われているライブラリをインストールして使うことができない.
lensの場合は, THを含まないより簡単なパッケージとしてlens-familyがあるのでこれを使った.

さて, lensには便利なmakeLensesという機能(TH)があるのでこれを使いたいのだが, lens-familyでこれをやるためには以下のコードを書く必要がある.

data Hoge = Hoge { _f1 :: k1, _f2 :: k2, .. , _fn :: kn }

f1 :: Lens' Hoge k1; f1 = lens _f1 (\p x -> p { _f1 = x })
.. -- フィールドの個数だけ繰り返す
fn :: Lens' Hoge kn; fn = lens _fn (\p x -> p { _fn = x })

これが最高に面倒くさい(特に, 各fiの型をそれぞれ宣言しなければならないことと, _fiとfiのいずれもexportしないといけないところ)のでどうにかしたかった.

これを解決する1つの方法として, Extensible Recordsを提供するextensibleというパッケージを使うというのがある.

extensibleはTHを使っているのでこれをそのままHaste環境にインストールはできないけれど, 少しアイデアを借りてそれらしいもの(もっと簡単なやつでよい)を実装することにした*1.

Union Type

結局以下のようなことができれば良い:

  • k1 .. kn型をまとめて管理するコンテナ(リストのようなもの)を用意する
  • コンテナへのアクセサとしてlensを提供する. getter "fi"のようにして値にアクセスできるようにする
  • アクセサはコンパイル時にvalidかどうかをチェックする. 存在しない名前などはコンパイルエラーにする. (コンパイル時にやる必要があるかどうかは趣味の問題だけれど, タイプミスなどはコンパイルエラーにしてくれた方が明らかに便利なので今回はコンパイル時にやる)

1番目はヘテロリスト(1-kind list)でよい.
2番目は型クラスを使って上手くやろう.
3番目は文字列の代わりにSymbolを使えば良い.

実装

data HList (xs :: [*]) where
  HNil :: HList '[]
  HCons :: x -> HList xs -> HList (x ': xs)

data Union (xs :: [*]) = Union (HList xs)

data (:<) (s :: Symbol) a = Tag a
data Name (s :: Symbol) = Name

実際にUnionを使うときは, Union <("intValue", 20), ("charValue", 'a')> のように, Symbolと値をペアにして使う.
これを(s :: Symbol) :< (a :: *)でペアを表すことにしている.
Nameは単にSymbolのみを型としてつかえるようにするもの.

class MakeLense (xs :: [*]) (s :: Symbol) out | xs s -> out where
  getter' :: Name (s :: Symbol) -> HList xs -> out
  setter' :: Name (s :: Symbol) -> (out -> out) -> HList xs -> HList xs

instance MakeLense ((k :< v) ': xs) k v where
  getter' _ (HCons (Tag v) _) = v
  setter' _ f (HCons (Tag v) xs) = HCons (Tag $ f v) xs

instance {-# OVERLAPPABLE #-} MakeLense xs syb out => MakeLense ((k :< v) ': xs) syb out where
  getter' k (HCons _ xs) = getter' k xs
  setter' k f (HCons x xs) = HCons x $ setter' k f xs

getter :: (MakeLense xs s out) => Name (s :: Symbol) -> Getter' (Union xs) out
getter syb = to $ \(Union hl) -> getter' syb hl

setter :: (MakeLense xs s out) => Name (s :: Symbol) -> Setter' (Union xs) out
setter syb = setting $ \f (Union hl) -> Union $ setter' syb f hl

lenses :: (MakeLense xs s out) => Name (s :: Symbol) -> Lens' (Union xs) out
lenses syb = lens (^. getter syb) (\u x -> set (setter syb) x u)

以下のような感じで使う.

data Flag = A | B | C deriving (Show)
data Gender = F | M deriving (Show)
type Ext = Union ["flag" :< Flag, "money" :< Int, "gender" :< Gender]

runExt :: StateT Ext IO ()
runExt = do
  lenses (Name :: Name "flag") .= B
  lenses (Name :: Name "money") += 30
  g <- use (getter (Name :: Name "gender"))
  case g of
    F -> lenses (Name :: Name "gender") .= M
    M -> lenses (Name :: Name "gender") .= F

main = do
  print "hoge"

  let iniExt = Union $ HCons (Tag A) (HCons (Tag 0) (HCons (Tag F) HNil)) :: Ext
  print $ iniExt ^. getter (Name :: Name "flag")
  print $ iniExt ^. getter (Name :: Name "money")

  ext' <- execStateT runExt iniExt
  print $ ext' ^. getter (Name :: Name "flag")
  print $ ext' ^. getter (Name :: Name "money")

Name :: Name "hoge"などと書かなければいけないのは面倒だけれど, 最初に書いたような面倒は多少軽減されたはず.

課題とか

このままだとUnion型の値を定義するのが面倒とか, 存在しないキーがあるときのエラーメッセージがあまりユーザーフレンドリーでないなどの問題がある.
ので, そのへんはextensibleの中では結構上手く解決されているので興味がある人はData.Extensible.Fieldなどを読むとよいでしょう.
自分は下のコードで大体満足しているけれど.

全体

MakeLense.hs(ちょっとだけ改良版)のコードは以下.

MakeLense.hs · GitHub

*1:正確に言えばここからアイデアを借りたわけではなくて, 以下のような実装を考えていたら「これは全く同じことがすでにextensibleで実装されているな」と気がついたわけです. 余談.

『ふたりのハードプロブレム』 感想

感想

ncode.syosetu.com

以下, ネタバレ注意.

ジャンルとしてはSFでしょうが, 話自体は人間ドラマに重きが置かれているという印象でした.
登場人物がみんな感情豊かで人間臭いのがまた良いところ.
あまりあらすじ等を確認していなかったので, 前情報なしだといい意味で期待を裏切られて, 読んでいて楽しかったです.

例えば希海は自堕落でコミュニケーション能力が低くて, さらに自己評価も低いという負の側面が強い人間ですが, ルーミングの時はちゃんと相手に向き合って能力を発揮したり, リコには気を遣ってあげたりという優しい一面も見えます.
正負の側面がキチンと見えるので, 登場人物がちゃんと活きていて, 感情移入しやすいのはそれだけで良いところでしょう.
登場人物達は物語が進むと, ちゃんといいところだけでなく悪いところも(希海の場合は逆ですが)見えるので, みんなが人間臭く感じられるのが良いです.
個人的には, それまで掴みどころがなかった東さんの, ラスト間際で希海との会話の中で発している『私の若い頃』という言葉の重みがすごく好きです.
ここの会話は東さんが暗い過去を背負っていることがしっかり反映されているセリフで, さり気ないしあからさまではないのにその重みが感じられるところが好きです.

前半ではリコの性格が希海とは対照的に, 特に記憶がないだけ純粋で無邪気な世間知らずのアンドロイドといった印象な分, 後半の記憶を取り戻してからの希海への物言いと閉律症になってからの性格の変化には驚かされます.
リコには終始アンドロイドという記号が与えられ作中でもそれに振り回されるという雰囲気こそありますが, 後半のリコの変化には確かに人間臭さがあり, 確かにリコも人間として描かれているのだと思えます.
そのためにリコの心についての悩みは余計ややこしいし本人もすごく悩んでいるようですが, リコの描かれ方を見ているとその答えはもう出ているのではないかとも思います.

少し話は変わりますが, 希海はずっと『機械になりたい』と繰り返していて, 本人の目の前でなんてことを, と読者としては思います.
ここでの機械というのが何を指しているのかは少し曖昧で, 希海の言い方的には何か産業ロボットに対応するものを指しているのかなとも思いますが作中に出てくる機械はアンドロイドくらいで, しかもリコも自分のことをはっきりと機械と言います.
機械のリコがこんなに悩み苦しんでいるのに機械になれば救われると考えているのはなぜだろう？という疑問が残りました.
でも逆に希海にそういう思いがあるからこそ, リコが自分は機械だから苦しくないはずみたいな(正確なセリフを忘れたので曖昧)強がりを言うシーンでは切なさを感じてしまうのかもしれません.

アンドロイドだけかと思ったら精神世界のアクロバティックバトルが描かれたり, キャラクターの印象がガラリと変わって裏の面が見えたり, そういう意味で期待を裏切られたので読んでてとても楽しかったです.
どこかから借りてきたような不思議語彙の数々も相まって硬派なSFの印象ですが, 希海とリコが成長し, 二人で助けあって苦難を乗り越えるドラマはとても純粋で心を動かされました.
続編が出ればまた読みたいです.