眠気と戦う日々

眠気と戦いながらいろいろと書くブログ

コンピュテーション式の変形後を覗き見る #FsAdvent

はじめに

この記事はF# Advent Calendar 2014の10日目の記事です。
前日はbleisさんの「クラスのコンストラクタ呼び出し時にプロパティも同時に初期化する」でした。

本日はTipsからちょっと外れてネタをご紹介します。
タイトルにもある通り、コンピュテーション式のお話です。

コンピュテーション式とは何ぞや

式変形により、言語の提供する構文の意味を変更することのできる強力な機能です。
その辺りの細かいことなどを知りたい場合は言語仕様を読みましょう。
さて、今回はその「式変形」に着目してみました。

本題

式変形という素敵ワードを聞き、そこで湧き上がる疑問があります。
すなわち「式変形するって言うけど、それって本当に言語仕様通りなの? 同じように動作するだけで、実は違ったりしない?
当然、気になりますよね? 気にならないわけないですよね?
気にならない人も気になってきたかと思います。
はい。
てことで、コンピュテーション式の式変形を追いかけて行きましょう。
具体的には手を動かして変換した結果と、コンピュテーション式を変換したあとの式木を表示する感じです。

題材

とは言ったものの、複雑なコンピュテーション式を手で変換するのは骨が折れます。
なので今回は極端に単純な例でいきます。
具体的には以下の様な感じで。

type SimpleBuilder () =
  member this.Return(x) = x
  member this.ReturnFrom(x) = x
  member this.Bind(x, f) = f x

let simple = SimpleBuilder ()

とりあえずこれだけあれば、以下の様なコンピュテーション式を書くことができます。

let ret = simple {
  let x = 10
  return x
}

今回はこれを考えていきましょう。

手動での変形

それでは早速行きましょう。
まずもっとも「外側」の部分の規則は以下です。

builder-expr { cexpr }

これが以下のようになります。

let b = builder-expr in {| cexpr |}

そして、変換規則はbleisさんの過去記事「詳説コンピュテーション式」にある以下の規則を用います。
今回はカスタムオペレータについては考慮しませんし、題材となるコンピュテーション式ではとりあえずこれで十分だからです。

{| cexpr |}T (cexpr, fun v -> v)

これで前準備は十分ですね。それでは本格的に変換していきます。

letを変換する

はい、それではまずは一番最初に出てくるlet x = 10の変換から行きましょう。
letの変換規則は以下のようになっています。

T(let p = e in ce, C) = T(ce, fun v -> C(let p = e in v))

これに従って変換します。

(* 元の形 *)
let ret = simple {
  let x = 10
  return x
}

(* 全体の変形 *)
let ret =
  let b = simple
  {| let x = 10 in return x |}

(* {| cexpr |} 形式を T(e, C) の形に変換 *)
let ret =
  let b = simple
  T(let x = 10 in return x, fun v -> v)

(* letの変換規則に従って変換 *)
let ret =
  let b = simple
  T(return x, fun v -> (let x = 10 in v))

はい、letの変換はここまでです。
それでは次はreturnの変換です。

returnを変換する

returnの変換規則は以下のようになっています。

T(return e, C) = C(b.Return(e))

これに従って、letを変換した結果をさらに変換してみましょう。

(* letの変換規則に従った変換結果 *)
let ret =
  let b = simple
  T(return x, fun v -> (let x = 10 in v))

(* returnの変換規則に従って変換 *)
let ret =
  let b = simple
  (fun v -> (let x = 10 in v)) (b.Return(x))

(* 簡約 *)
let ret =
  let b = simple
  let x = 10 in (b.Return(x))

はい、これにて手動変換終了です。

自動変形を覗き見る

それでは次に自動の方を見て行きましょう。
自動での変換結果を覗き見るために必要なのはRunとQuoteです。
Quoteがあると、Runの引数として式木が与えられます
これを覗き見るため、とりあえず以下のように書き換えます。

type SimpleBuilder () =
  member this.Return(x) = x
  member this.ReturnFrom(x) = x
  member this.Bind(x, f) = f x

  member this.Quote(x) = x
  member this.Run(expr) =
    Console.WriteLine(expr.ToString())

はい、とりあえずまずは式木をそのまま表示する感じですね。
これを実行すると、以下の様な結果が得られます。

Let (x, Value (10), Call (Some (Value (Program+SimpleBuilder)), Return, [x]))

これをこちらの資料に従って、読みやすいように変えてみましょう。

Letの読み替え

まず最初に登場するのはLetです。
Letはlet式のことですね。
この資料に従って、以下のようにします。

Let (var, expr1, expr2) = let var = expr1 in expr2

これを行う関数を定義します。
とりあえず今回は表示が目的ですし、式木を受け取って文字列を返却する感じでいいでしょう。
てことでこんな感じです。

let rec evaluate = function
  | Let (var, expr1, expr2) ->
    sprintf "let %s = (%s) in (%s)" (var.ToString()) (evaluate expr1) (evaluate expr2)

それでは次、expr1に当たる箇所で出てくるValueの読み替えを実装していきます。

Valueの読み替え

Valueは定数値を表しています。 こちらの資料に従って以下のようにしましょう。

Value (obj * Type) = obj

objはその定数値、Typeはその型を表していますので、今回はobjのみを文字列に変換してみましょう。

let rec evaluate = function
  | Let (var, expr1, expr2) ->
    sprintf "let %s = (%s) in (%s)" (var.ToString()) (evaluate expr1) (evaluate expr2)
  | Value (obj, _) ->
      obj.ToString()

まだまだ行きます。 次はCallです。

Callの読み替え

Callは関数呼び出しのことです。 こちらの資料に従って以下のような感じにします。

Call (Some instance, methodInfo, arguments) = instance.methodInfo(arguments)

Some instanceはインスタンスメソッドの呼び出しの場合にのみ入るインスタンスの式木です。 methodInfoはそのままですね。呼び出す対象となるメソッドです。 argumentsはその引数です。 これらを踏まえ、以下のように実装します。

let rec evaluate = function
  | Let (var, expr1, expr2) ->
    sprintf "let %s = (%s) in (%s)" (var.ToString()) (evaluate expr1) (evaluate expr2)
  | Value (obj, _) ->
      obj.ToString()
  | Call (Some instanceExpr, methodInfo, arguments) ->
    let args = List.map evaluate arguments
    sprintf "(%s).%s(%s)" (evaluate instanceExpr) (methodInfo.Name) (List.reduce (sprintf "%s, %s") args)

そろそろ終わりが見えてきました。

その他の解釈

さて、それでは残りです。
残りは単純に引数の値を文字列化しちゃいましょう。
ということで、evaluate関数の最終形はこちらです。

let rec evaluate expr =
  match expr with
  | Let (var, expr1, expr2) ->
    sprintf "let %s = (%s) in (%s)" (var.ToString()) (evaluate expr1) (evaluate expr2)
  | Value (obj, _) ->
      obj.ToString()
  | Call (Some instanceExpr, methodInfo, arguments) ->
    let args = List.map evaluate arguments
    sprintf "(%s).%s(%s)" (evaluate instanceExpr) (methodInfo.Name) (List.reduce (sprintf "%s, %s") args)
  | _ ->
    expr.ToString()

それではこれを使い、コンピュテーション式の変形後を覗きこんでみましょう。

自動変形の結果

以前定義していたSimpleBuilderは以下の様な感じでした。

type SimpleBuilder () =
  member this.Return(x) = x
  member this.ReturnFrom(x) = x
  member this.Bind(x, f) = f x

  member this.Quote(x) = x
  member this.Run(expr) =
    Console.WriteLine(expr.ToString())

これのRunでevaluate関数を実行し、中身を表示します。

type SimpleBuilder () =
  member this.Return(x) = x
  member this.ReturnFrom(x) = x
  member this.Bind(x, f) = f x

  member this.Quote(x) = x
  member this.Run(expr) =
    Console.WriteLine(evaluate expr)

そして実行します。 結果は下のような感じです。

let x = (10) in ((Program+SimpleBuilder).Return(x))

Program+SimpleBuilderの部分はインスタンスを表しているので、これを以下のように読み替えてしまいましょう。

let b = simple
let x = (10) in (b.Return(x))

そして、Runの結果がコンピュテーション式の結果となるので、以下のようにします。

let ret =
  let b = simple
  let x = (10) in (b.Return(x))

はい、これにて完了です。

結果比較

それでは2つの結果が出揃いましたので、比較してみましょう。
まず手動です。

let ret =
  let b = simple
  let x = 10 in (b.Return(x))

次に自動です。

let ret =
  let b = simple
  let x = (10) in (b.Return(x))

()は単なる表示用なので無視すると完全に一致しますね。

まとめ

このレベルのシンプルなコンピュテーション式であれば仕様通りということがわかりました。
ところでこの記事、一番の収穫はQuoteを定義するとRunで式木が得られるというTipsだと思うんですが、どうでしょう。
次点で資料リンク。

ということで本日は以上です。
明日はgab_kmさんです。楽しみですね!

追記・あわせて読みたい

本エントリに対するツッコミをbleisさん、pocketberserkerさんが書いてくださいました。
既存のコンピュテーションビルダーに対してRun/Quoteを追加するより良い方法など、素晴らしいTipsを紹介してくださっています。
エントリはこちらです。

ありがとうございました!

リスト反転関数が単射であることを証明する

久々の記事もまたCoqでソフトウェアの基礎ネタです。 今回はList_Jにおける練習問題「rev_injective」について。

問題のTheorem

Theorem rev_injective: forall l1 l2: natlist,
  rev l1 = rev l2 -> l1 = l2.

ソフトウェアの基礎ではCoqコードではありませんが、型Xの部分をnatとしてCoqコードにするとこんな感じになります。 これについて証明していきましょう。

定理の意味を確認

まずはとにかく定理を見てみましょう。

Theorem rev_injective: forall l1 l2: natlist,
  rev l1 = rev l2 -> l1 = l2.

revはリストを反転させる関数です。 つまりこの定理は、

rev関数の結果が一致するならば、引数のリストは一致する

ということになります。

証明開始

まずはとにかくintrosしてみましょう。

l1: natlist
l2: natlist
H: rev l1 = rev l2
===========================
l1 = l2

定理の中にあった仮定の「反転したリスト同士が一致した時」が前提として用意出来ました。 今回の証明ではこれを使います。

前提を見てみる

それでは重要な前提を確認。

H: rev l1 = rev l2

反転したリストは一致する

です。 ということは、どうやらsubgoalのl1 = l2をどうにかして反転したリストの形式に変更すれば証明できそうです。 どうすればいいでしょうか。

リストの性質

そこで、リストの性質を見なおしてみましょう。 リストは偶数回反転させることで、元のリストと等しくなるという定理がありました。 つまり、

l1 = rev (rev l1)
l1 = rev (rev (rev (rev l1)))
l1 = rev (rev (rev (rev (rev (rev ...

rev l1という形を見つけられました。 これを証明することで利用することが可能になります。 この補題rev_involutiveとして、利用しましょう。 「ソフトウェアの基礎」を最初から順にやっていると、きっとすでに定義されているかと思います。

反転した反転リスト

それではrev_involutiveを使ってみます。 先ほどintrosしたばかりの定理に対して、rewriteしてみましょう。

Proof.
  intros.
  rewrite <- rev_involutive.
l1: natlist
l2: natlist
H: rev l1 = rev l2
===========================
l1 = rev (rev l2)

求めていたものが手に入りました。 あとは作業です。

Proof.
  intros.
  rewrite <- rev_involutive.
  rewrite <- H.
l1: natlist
l2: natlist
H: rev l1 = rev l2
===========================
l1 = rev (rev l1)

Hによって書き換えると、今度は先程も見た形です。 今度はrev_involutiveを逆向きに適用しましょう。

Proof.
  intros.
  rewrite <- rev_involutive,
  rewrite <- H.
  rewrite -> rev_involtive
l1: natlist
l2: natlist
H: rev l1 = rev l2
===========================
l1 = l1

はい、あとはいつもの様にして終わりです。 最終的にはこんな感じ。

Proof.
  intros.
  rewrite <- rev_involutive,
  rewrite <- H.
  rewrite -> rev_involtive
  reflexivity.
Qed.

以上です。

内部でFixpointの関数を呼ぶ関数を定義した時にsimplだと証明できない

はい、表題のとおりです。
Coqを勉強していたらよくわからない挙動にぶつかったのでメモ。

問題のコード

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Definition oddb (n:nat) : bool := negb (evenb n).

そこまで難しいもんじゃないです。 要するに偶数判定関数をFixpointの再帰関数として定義し、それを内部で呼ぶ奇数判定関数をDefinitionで定義しています。 これだけ見ると何の問題もないのですが……。

simplで証明できない

Example test_oddb1 : (oddb (S O)) = true.
Proof. simple.

とまあこんな感じで証明を行おうとすると、

oddb 1 = true

のまま動かない。 一旦動かすようにしてみます。

幾つかパターンが有ります。

oddbをFixpointで定義する

先ほどのDefinitionで定義していたoddbをFixpointで定義することでsimplが使えるようになります。

Fixpoint oddb (n: nat) : bool := negb (evenb n).

Example test_oddb1 : (oddb (S O)) = true.
Proof. simpl. reflexivity. Qed.

unfold oddbをsimplの前に実行する

関数名を定義に置き換えるunfoldを使うことで、simplが使えるようになります。

Proof. unfold oddb. simpl. reflexivity. Qed.

computeをsimplの代わりに使う

Proof. compute. reflexivity. Qed.

終わりに

computeが何やっているのか全然わからず。

Twitterで教えて頂いた感じだと複数のtacticを組み合わせたもののようです。

各種リンク

ソフトウェアの基礎

TAPL読書会@名古屋# 1に参加しました

ちょっとした前置き

TaPL? TAPL? どっちなんでしょう。 ということで8月2日に開催されたTAPL読書会@名古屋#1に参加しました。 短歌会館というところの和室を借りて行いました。非常に雰囲気の良い所でしたので、お勧めです。 ただし無線LANとかはないので注意しましょう。

当日のメモ

3章. 型なし算術式

プログラミング言語を定義するための定義とかが書かれている章。

3-2

プログラミング言語の経験からニュアンスでBNFモドキを理解してきたが、これを数学的に見ていく。
succ trueとかの怪しげなものを定義可能。これについては後で言及がある。
ここで重要なのは「{true, false, 0} ∈ T」での「T」は「構文的に有効な項をすべて含む集合」。
「明らか」という単語は使ってはいけない。

3-4

プログラムを「どう評価するか」 -> 意味論

  • 操作的意味論(TaPLではこれ)
  • 表示的意味論
  • 公理的意味論

「どちらかというと意味論ではなく意味定義だよね」

3-5

まずは真偽値だけで考える。 -> 図3-1参照
vは評価の最終結果となり得るtの部分集合。
27ページで示されていることについて、導出は1パターンしか存在しないことが証明できる。
正規形: これ以上評価できない項。値。
多ステップ評価: t -> t'を何回も繰り返すのをt -> *t'

個人的感想

多少駆け足気味でしたが、mzpさんを始めとする講師役の方々の説明が非常にわかりやすかったため、なんとかついていくことが出来ました。
プログラムの評価とか、数学的に見た時の考え方とかその辺をやったのが初めての経験で、非常に面白かったですね。
4章をちらっと見た感じだと、次からはプログラミング言語を見ていくようなので、そちらも楽しみです。

謝辞

企画、及び進行をしてくださったmzpさん、ありがとうございました!
隣でわからないことについて逐一教えてくださったよんたさん、ありがとうございました!

各種リンク

TAPL読書会@名古屋 #1 - TAPL読書会@名古屋 | Doorkeeper

mzpさんの真偽値のみの言語における決定性の証明コード(Coq)

24時間耐久ハッカソンを企画/主催しました

人生初のハッカソン企画/主催してしまいました。
細かい流れなどはpocketberserkerさんのtogetterがあるので、そちらを御覧ください。
http://togetter.com/li/567360

#24hack is 何

24時間ぶっ通しでハッカソンやりましょう! という企画です。
難しいことありません。

  • 24時間ぶっ通しでハック
  • 特定の何かをやるのではなく個人がやりたいことをやる

これだけ守れば自由な感じです。
公開直後に「あたまおかしい」というツイートが24時間以内に5回ほど流れたので、きっとこわい系ではなくあたまおかしい系イベントでしょう。
別名デスマーチハッカソン、もしくはデスマソン。

「何でこんなの思いついたんですか!」

始まりから終わりまで全て仕事が悪い。
ピー時まで労働しているとか寝ることしかできないじゃないですか。
帰ってからハックとかやってる暇もなく寝るしかないじゃないですか。
フラストレーションたまるじゃないですか。
そうなると、たまには脳みそ溶かすようなハッカソンやりたいじゃないですか。
じゃあ24時間でやりましょう!
何もおかしなことないです。
はい。

感染する「あたまおかしい」

まあそんな事情もありまして、connpassにて公開しました。

http://connpass.com/event/3144/  

公開してから「あたまおかしい」のツイートが大量に。
そしてなごやの方々が悪乗り開始
24時間以内に「名古屋会場」「大阪会場」の開催が決定しました。
そしてしばらくして……

http://llhitori.doorkeeper.jp/events/5322  

何故か海を超えた24hack。
実にあたまおかしい感じです。
そして、

https://twitter.com/mrgchr/status/381545912343883776  

なんとサンディエゴでも開催決定。
ここまで来ると「あたまおかしい」は感染性の何かなのでしょう、きっと。
しかもTwitterとかで感染するたちの悪さも兼ね揃えているようです。
これを見ているあなたもきっと……
かゆい
うま

当日のハイライト in 東京会場

  • まずは昼飯ということで開始予定時刻から1時間は遅れてスタート
  • ハングアウトでの接続にiPhone使うも爆熱+プチプチ切れるので諦める
  • どうにかなって接続してさあハック開始
  • したのは一人
  • 突然脱ぎ始める主催者
  • ねこはるさん襲来
  • あくらる提督が着任しました
  • 前半戦終了時点でハックしているの二人
  • 某氏は発言の責任とって爆発すべし
  • 倒れゆく参加者たち
  • あくらるさん寝ながら暴れる
  • 主催者戦死
  • 【悲報】ねこはるさん、壊れる
    • クッキーをひたすら数える
    • クッキー消滅を嘆く
    • 「クッキーゲームでこんなにエキサイトするとは思いませんでした」
  • サンディエゴでの開催が決定
  • 主催者土下座謝罪
    • 私「この度はこのようにあたまおかしいイベントを企画してしまい申し訳ございませんでした」
    • mzpさん「次はいつやりますか?」
    • 私「あ、いつやりましょうね?」
    • mzpさん「12月で」
    • 私「じゃあそれで!」
  • 進捗どうですか?
    • D言語いろいろとやりました
    • Haskellで音出しました
    • 艦これアカウント作って第三艦隊まで開放しました
    • 3734.6cps
  • 次は健康的に12 * 2の24hack_2dayでどうでしょう

やったこと

  • D言語復習のTodoアプリ(永続化なし)
  • D言語のxUnit framework徐々に形になってきてる感じ
  • XMonadを布教された

中でもXMonadが素晴らしいです。
一部まだ出来てない箇所があるので、その辺をどうにかすれば愛用できそうな感じです。

総括

なんだこのあたまおかしいイベントは(驚愕)。
深夜の悪乗りって怖いですね。皆様もお気をつけ下さい。

それはそうと、実際に主催した感想としては非情に申し訳ない感じです。
Webカメラの準備は勿論、主催者が寝るとかないですよね。
ただとても楽しかったので、今後もこういったイベントは積極的にやっていきたい感じです。
24時間耐久含めて。