眠気と戦う日々

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

#今日の30分 ルール

そもそもコレは何?

自分が4月1日から始めた学習活動です。 一ヶ月ほど継続できたので、忘れないように基本ルールと、自分の現在のルールを残しておきます。

基本ルール

「#今日の30分」を始めるにあたり、基本ルールとして下記3つを定めました。

  • 短くてもいいので、毎日必ず一定時間勉強する
  • 勉強した成果、感想などを必ずSNSなど*1に書く
  • 1週間に1回、必ずその週の振り返りをする

自分の場合、これに従って「1日30分前後勉強する」、「毎日の成果はTwitterに書く」、「振り返りはKPTを使う」としました。

自分の現在のルール

上記の基本ルールのほかに、毎週の振り返りなど*2でルールを追加しています。 基本的には思いついたら順次試しており*3基本ルール以外は削除してもいいものとしています。

現在の自分のルールは、下記の通りです。

  • 毎日必ず30分前後勉強する
  • 本を読むとき、自分の言葉で言い換えてメモする
  • 本を読むとき、別の本に繋がりそうな箇所をメモする
  • 勉強した成果、感想などを必ずTwitterに書く
  • 本を呼んでいる最中に書いたメモはTwitterに公開する
  • 1週間に1回、必ずその週の振り返りをする
  • 1週間に1回、その週のまとめをブログに書く
  • 振り返りの内容をブログに書く

他の人がやる場合

需要あるか知りませんけど、もしも他の人がコレをやる場合、必ず基本ルールのみの状態から始めたほうがいいんじゃないでしょうか。 どのような学習方法がやりやすいのかは、人によって違うと思うので。

*1:自分以外に公開されていればどこでもいいです

*2:突発的に追加することもあります

*3:効果測定していないことが現在の問題です

#今日の30分 ログ

ツイート

オマケ

f:id:zakky_dev:20180429221857j:plain

#今日の30分 ログ

ツイート

オマケ

f:id:zakky_dev:20180422233629j:plain

#今日の30分 ログ

ツイート

オマケ

f:id:zakky_dev:20180415234400j:plain

#今日の30分 ログ

ツイート

オマケ

f:id:zakky_dev:20180409003954j:plain

コンピュテーション式の変形後を覗き見る #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.

以上です。