わんくま東京勉強会 #59
5/28 に、わんくま東京勉強会 #59に参加してきました。
中身はもうちょっとしたらきっと書きます。(`・ω・´)
リリカル合宿
3/5〜6 に、リリカル合宿に参加してきました!
- 朝
7時に電車乗って、開場よりちょっと前に到着。喫茶店でティラミス食べた。
-
- F# で LRU キャッシュ
- bleis とペアプロ
- VS の構成
- ソリューション
- プロダクトプロジェクト
- テストプロジェクト
- FsUnit のソース (本当は lib 以下に dll で置く)
- lib
- NUnit の dll
- ソリューション
- テストコード
- FsUnit と NUnit.Framework とプロダクトモジュールを open
- actual |> should equal excepted とか書ける
- option のときは、actual |> should equal <| Some 〜 とか書く
- VsVim
- 挿入モードでの Ctrl + p 使えない (印刷になる)
- Ctrl + n も駄目 (新規作成になる)
- (´・ω・`)
- 挿入モードでの Ctrl + p 使えない (印刷になる)
- F# で LRU キャッシュ
- 昼飯
ラーメン食った。
- 昼から
-
- LRU キャッシュ続き
- get で 要素と更新されたキャッシュを返さないと・・・
- インタフェース変わる・・・
- 問題変更 LRUキャッシュ → ディクショナリ
- get で 要素と更新されたキャッシュを返さないと・・・
- LRU キャッシュ続き
-
- コードレビュー
- as パターンマッチ
- × let hoge ({ value = v } as lru) = ...
- ○ let hoge ({ value = v } as nyan) = let lru = nyan ...
- あずにゃんぺろぺろ
- as パターンマッチ
- コードレビュー
- 懇親会
bleis は辛いの苦手。
再帰作る為に y コンビネータ作ってるのに、作るときに再帰使っちゃあれか。楽だからよく使うけど。
- 夜
- 2日目
-
- F# で Functional Reactive な GUI やってみた
- 関数型言語はGUIが苦手? - まぁ、そんなもんでしょう。 みたいなことが、F#標準で出来るみたいなので、やってみた
- F# で Functional Reactive な GUI やってみた
open System open System.Windows.Forms let main _ = let form = new Form begin Width = 200, Height = 80, Text = "Button" end let button = new Button begin Left = 40, Top = 10, Width = 100, Text = "push" end do button.MouseClick |> Observable.scan (fun n _ -> n + 1) 0 |> Observable.map string |> Observable.add (fun str -> button.Text <- str) do form.Controls.Add button Application.Run form [<STAThread>] do main ()
-
-
- VsVim
- Ctrl + d と Ctrl + u も駄目だった
- 発表は間に合わなかった・・・
- VsVim
-
- 帰り
終わってからどえりゃあ行く組に混ざって昼飯食べたけど、結局途中で帰ることにした。(あひさめ君も一緒に)
あひさめ君は豊橋に帰っていったらしい。
自分は実家へ。
第14回名古屋Scala
1/21 に、第14回名古屋Scala勉強会に参加してきました。
今回はコメントがなかったので、本の中身を追っていく感じに。
- 30章 アクターと並行プログラミング
- アクタは、リアクティブプログラミングに繋がるらしい
- receive
- 待って、来たら進む (ブロックする)
- react
- 終わったら終わり (先へ進まない)
- case object
- OCaml でいうところの、of のないヴァリアントの時は、case class じゃなくて case object 使う
- case class は of ありのヴァリアント
- OCaml でいうところの、of のないヴァリアントの時は、case class じゃなくて case object 使う
- ivar とか mvar とか
- 30.5.4 のコードとか、ivar 使うといいらしい
- ivarについては、このへんとか
- futureパターンやるときに出てきたりするらしい
- アクタがモナドになるとかならないとか
- bind : receive, return : ...
- receive の中で receive するのは(・A・)イクナイ!!
- ヘルパアクタ使う
- 30.6は次回へ
- 他
- 教養としての Scala
- 30章と31章はいよいよ大詰めな感じ
- 時間もいっぱい取ろう
- 32章と33章は結構どうでもいい
- 「ここ分からない!」ってところコメントしよう!
- 大体、「こんなネタがあるよ!」になっている
- それはそれで面白いけど
- 大体、「こんなネタがあるよ!」になっている
- 日帰りだったので、懇親会から少し早く帰った
NGK忘年会2010
12/ 4 に、NGK忘年会2010 に参加してきました。
ラーメン食ったり、Mac見てたりして少し遅れた・・・
メモ取れたところから。
- イベント・コミュニティの話
- 勉強したいことがあったら勉強会をひらいてみる
- 続けるのはたいへん
- Git と GitHub を体験しながら身につける勉強会
- bleis さんありがとう
- テライケメン
- bleis さんありがとう
- RedBull ウォッカ
- 勉強したいことがあったら勉強会をひらいてみる
- わらび餅
- わらび餅を作ってきたので休み時間に食べてください
- 忠告くれた人にわらび餅ひとパックプレゼント
- 場数踏んでください
- 場数は踏んでます
- なんでスカートはいてるんですか
- 難しい質問なんで懇親会で
- 場数踏んでください
- グダ生な日々
- gotomeeting 素敵
- CSNagoya
- 実体は誰も把握してないとか
- dominion525と付き合ってる日々
- claなんとかさん双子説
- dominion525の友達の友達の友達が彼女になった → 結婚
- 勉強会を立ち上げると結婚できる!
- Coq から Ruby へ
- 隣でお見合いやってる中で Coq やったり
- Coq
- 最近アツい!
- SkillMaps で2位
- 最近アツい!
- 自動生成されたコード
- lambda とか禍々しい感じ
- 年越しで証明しよう
- ・・・という話を Ruby会議でします
- EPUB + iPad 紙の本から自由になりたい
- ちゃんとした話だと謝る流れ
- デスクをすっきりさせよう
- セミナールーム
- ニューキャストさん
- 千種駅すぐ
- 料金
- ムリョ
- 本にしたい!っていうのも是非
- これは ムリョ じゃない
- concrete5 Japan 名古屋ユーザーグループ
- カレー部は週に1回カレーを食べないといけない
- 幽霊部員が多いとか
- カレー部は週に1回カレーを食べないといけない
- 懐古厨 傾向と対策
- 懐古厨:俺むかしそれ10年前にそれ使ってたわー
- 86年代はゆとり乙らしい
- おっさんホイホイとか
- 名古屋でもPrelにからめて集まってみなイカ
- イカ帽子
- どえりゃあ で
- 第6回 12/25
- クリスマス関係ない人もそうでない人も是非
- 勉強会主催してるけど結婚できた例しがない・・・
- Git と Hudson の連携について
- イカ帽子
- 侵略されたw
- 「俺のLT発表資料がこんなに短いわけがない」
- 資料間に合わなかった
- 会社での作業
- Redmine + Hudson + Git
- みんなも mzp さんのフックスクリプトのページ、ブックマークするといいよ!
- 「あ、消しちゃったw」
- イカ帽子
- ConvivialNetの近況報告
- やっぱり侵略されたw
- なんとか大学の誰得FWつかえねぇ → 自分達で作ればいいじゃない
- 最新鋭の設備
- 最新鋭の若者
- あとは、まぁ。
- OSS 奨励賞の貰い方
- 川崎市民なのに名古屋に毎回出てました
- 強力なOSSプロダクトを作る/翻訳する
- 狙いは Delphi
- OpenStreetMap 小ネタ集
- OpenStreetMap
- 自由な地図情報データ作成を目的
- iPhone4 の GPS 精度がとても高い
- 「こうして、MS は神になりました」
- OpenStreetMap
- とあるアプリのつくる部 - アンドロイダー
- また侵略されたw
- 下は 1,2歳のAndroidユーザーから、上は大人の世界まで
- みんなのラーメンタイマー
- つ部の人たちが熱い議論をしているとか
- 技術の無駄遣い
- 流しそうめん
- ペットボトルをホッチキスで繋げて・・・
- 「そうめんつゆを忘れた...だと...?」
- 「名古屋の人は素材の味が好きなんだ!」
- ペットボトルをホッチキスで繋げて・・・
- Boost.勉強会 名古屋(仮) の開催予定について
- UML と Cloud のススメ
- UML : うしのモヤモヤしたラク書き
- 「うしが喋ります」
- シーケンス図のお話
- わからいんで、Cloud
- ref #1 芸能界の闇
- わからいんで、Cloud
- モデリングといえば、ETロボ婚
- 懇親会
- 今日だけ肉解禁でもいいよね! (医者から控えるように言われてたり・・・)
- ひたすらオレンジジュース飲んでました (アルコールは薬の都合で飲めなかった・・・)
- コンストラクタで例外投げるくらいなら、Option 返す creation method 作ればいいじゃない とか
Coq Party
11/27 に、Coq Partyに参加してきました。
資料などはこちら。
- エンジニア・ミーツ・Coq
- すぐ分かる形式手法
- 形式手法とは?
- 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法
- 仕様化の正しさは終盤のシステムテストまで分からない
- 結合テストでバグが「こんにちは!」
- 手戻りコストがとても大きい
- 結合テストでバグが「こんにちは!」
- V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」
- 仕様化の正しさは終盤のシステムテストまで分からない
- 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法
- ソフトウェア開発の不具合の半数は上流工程
- 形式手法
- 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う
- 数学ベースの厳密な定義
- 形式仕様は仕様の記述の形式化
- プログラムではない (≒実行できない)
- 仕様のシミュレーションやコード生成などが出来るツールがある
- Coqもその中の一つ (定理証明支援)
- 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う
- メリット
- 自然言語より厳密
- 上流工程で仕様に対する検証が可能
- 仕様不具合の早期発見
- 「証明」などの、高い検証能力
- デメリット
- 学習コスト
- 不具合が完全になくなるわけではない
- 自然言語とプログラムの中間
- 各工程で仕様等の検証が可能
- 形式仕様について完全な検証を行いたい場合、証明を行うことができる
- テストするだけでは、テストケースから外れたものについては検証しきれない
- 記述した形式仕様に証明を与えることが出来れば、その仕様は「数学的に正しい」ことが保証される
- 証明された使用から自動生成されたプログラムは、仕様通りの動作をすることが「証明されて」いる
- 一般に証明はテストに比べ難しいので、コスト高になるといわれている
- Coq では、「仕様記述」「定理や補題の付与」「証明」「コード生成」
- まとめ
- 仕様をどう記述するかはとても大事
- 形式手法なら厳密に矛盾なく仕様が記述できる
- 形式仕様を証明すると、テストよりもスゴイ検証になる
- 形式手法とは?
- エンジニア・ミーツ・Coq
- ProofCafe
- 名古屋市内のカフェ「どえりゃあ」
- お見合い席の隣で Coq やったり
- おしゃれな食事の隣で Coq やったり
- 名古屋市内のカフェ「どえりゃあ」
- 定理証明って面白い!
- パズルゲームみたい!
- 普通のプログラムでも証明使えそうじゃね?
- 普段の業務におけるプログラミングでも、証明が役立ちそうな場合は多い
- 「ProofCafe で Coq を知ったので、会社で普及させようとしてみた」
- 職場で Coq を普及させるときの難しさ
- 「1. OCaml ライクな構文」
- 「2. 証明とプログラミングのギャップ」
- 「3. 命題を考えるのが大変」
- 「4. 数学の知識がたりない」
- ProofCafe
- 最後に
- これから形式手法や定理証明などの力が必要になってきそうな予感
- 新しい技術を積極的に試すのは大事
- Coq は触れてて楽しいし、証明できると嬉しい
- 没ネタ
- 「坊や一緒に定理証明をしようよ!」「おとーーさん!おとーさん!魔王が Coq を進めてくるよ!」
- すぐ分かる形式手法
- ProofCafe で学んだこと
- なぜ Coq を勉強しているのか
- 今井さんと出会ったから
- 「λ!λ!λ!」
- 今井さんと出会ったから
- Scala
- 緩い感じの関数型言語
- 「λ^3」(λキューブ)
- 証明が出来るよ!(Coq)
- ProofCafe 1回
- リストの操作とか、その性質の証明とか
- 「Coq 楽しい」
- ProofCafe 2回 CPDT 2章
- 難しいが、全体を俯瞰しているだけなので、わかんなくてもいいよ
- 3章から頑張ろう
- CPDT翻訳
- ProofCafe 3回 CPDT 3章
- CPDTに「みなさんお気付きのとおりこれはラムダ計算の構文です。HOASです。さあこれをCoqでも使いましょう」と書いてあって、前提知識が足りないことに気づく
- 難しい・・・
- ProofCafe 4回 ハンズオン
- 再度Listを定義して、関数書いて好きな定理を証明しよう
- ペアプル!
- ProofCafe 5,6回 CPDT 4章
- tactic
- change tactic 便利っぽい
- 「transitivity が好き」
- 「injection より inversionのほうがいい」
- 「今人気の tactic 出そう」
- 「info auto で auto でやった tactic を出せる」
- 「俺のスキなタクティクス elim,ring,omega,inversion,transivity,assert」
- あなぷるからひろってきたタクティクスの使用数ランキング
- プログラマのためのCoq - zyxwvの日記
- 証明の過程が知りたい
- バージョン管理しながらやるといい感じ
- 初めての Coq
- なぜ Coq を勉強しているのか
- Haskell の Data.Map のバグを見たら Coq を 12,000 行書いてしまった話
- 「形式化おたくになろう!」
- バランス木が崩れちゃったバグ
- パラメータの組み合わせが違うと、バランスが崩れる
- パラメータを 5 -> 4 にしてなおったよってチケットが閉じられた
- ほんとに大丈夫?
- アルゴリズムのバグ
- バランスの定義して、改善したアルゴリズムがバランスすることを証明
- 中にいれば大丈夫 + 外だと崩れる
- 外は、崩れる木が存在することを示す (手でいいや)
- 中は、大変なので Coq で証明
- 中にいれば大丈夫 + 外だと崩れる
- Word を使うと 12900 行でもスライド1枚で収まる
- バランスの定義して、改善したアルゴリズムがバランスすることを証明
- psatz 便利
- A <= B を A <= C と C <= B にするのを自動で
- 証明にインデントを付けるのは大事
- 場合分けとか
- Coq これやっとくといいかも
- Coq のドキュメントが手元にあるといい
- inria よく落ちる
- mzp さんがミラーサイトを作っている
- Coq が自動で作った名前は使わない方がいい
- バージョン上がると名前変わったり・・・
- バージョン明記して諦めるという手が・・・
- 古いバージョンも持っておけと・・・
- 業務だと開発環境をとっておくことも多い
- 古いバージョンも持っておけと・・・
- バージョン明記して諦めるという手が・・・
- バージョン上がると名前変わったり・・・
- nsatz 便利
- Ltac 書けるようになった方がいいんじゃないか
- Coq のドキュメントが手元にあるといい
- プログラムに対して 100倍くらい証明にかかる
- プログラム側 120行に対し、証明12000行とか
- intuition 便利
- 定理証明器 Coq と証明付き DSL (FM勉強会の話と Coq を DSL に使う話)
- Coq を学ぶべき理由
- テストで発見できるのは間違いだけ
- 正しいことは保証できない
- 網羅性のあるテスト書くの大変
- オレオレ言語に信頼性はあるのか
- テストで発見できるのは間違いだけ
- Formal Methods Forum
- DSL
- 特定分野のタスクのために作られた言語
- 自然言語より簡潔かつ厳密に記述可能
- 正しさをどう担保するか
- DSL で書かれたものの正しさ、DSL 自体の正しさ
- Ott 証明木を書くと、Coq と LaTeX と Isabell に変換してくれる
- 金融商品 DSL
- 認可・監査論理
- Coq で証明されたC言語コンパイラ
- 生成されたコードは元のCコードと等価であることを証明
- 外部 DSL と内部 DSL
- 外部 DSL
- どうせなら Coq とかを使って言語の正しさを証明したい
- 内部 DSL
- Coq は実は DSL 向いているのでは
- 外部 DSL
- DSL Host Language としての Coq
- ユーザ定義の記述を定義できる
- Notation
- 定義と一緒に where で記法を定義できる
- Haskell の do 記法も書ける
- .. で繰り返しのあるパターンを書ける
- 予約後の上書きに注意
- LTac
- 外部呼び出しもできる (external ...)
- 脆弱性注意
- 気をつけないと矛盾を持ち込んで Falso みたいになるかも
- 外部呼び出しもできる (external ...)
- Notation
- ユーザ定義の記述を定義できる
- Coq を学ぶべき理由
- Coq extraction機構の概要
- Extraction
- Coqからプログラミング言語への自動変換
- 検証対象が直接実行形式になる
- 対象言語の中で局所的に Coq を利用できる
- 段階的に利用できる
- 全部を Coq でやるのは非現実的だけど、対象言語と組み合わせるととても良い
- 他の検証機のプログラム生成
- Coq -> X言語を増やしたい
- Coq ソースコード内 plugins/extraction (8.3) (8.2だと contrib/extract)
- Extraction の実装を Coq で書いて Extract とか
- Extraction 周りは夢がひろがりんぐ
- 「Coq は使いこなせるけど OCaml はちょっと,という皆さんが Extraction を書けて便利だと思います」
- Extraction
- From Coq to Ruby Coq から Ruby へ
- Extraction のうれしさ
- Coq が使える ← うれしい
- どの言語の勉強会でも Coq の話が出来る
- 証明したコードが他の言語から使える
- 証明駆動には、Extraction が不可欠
- Ruby の特徴
- 型がない
- Extraction 先としては、型がない方が楽
- ラムダ式がある
- 関数と変数で名前空間が分かれている
- パターンマッチがない
- 型がない
- Ruby に Extraction
- 「ハッピーですね」「ハッピーかなぁ・・・」「ハッピーですよ」
- lambda がいっぱい!
- 美しいコードを出力しようと思わなければ、結構簡単にできる
- 抽出対象として適している言語
- 型がない・動的型付け
- GCがある
- ラムダ式
- なくてもオブジェクトでなんとか
- パターンマッチ・バリアントがある
- 関数と変数で名前空間が分かれていない
- Extraction のうれしさ
- 家に帰ったらExtraction to x を書いてみよう (Coq2Clojure)
- Coq (Gallina) の特徴
- Scheme
- ClojureへのExtraction
- Scheme ベース
- Ruby
- 型のある言語
- 依存型のない言語にCoqのやり方を理解させるのは難しいらしい
- 対象にしやすそうな言語
- JavaScript
- Lisp-1
- カリー化、遅延評価、代数的データ型まわりは自分で
- 関数型な人はreturnではまるかも
- Python
- Lisp-1
- インデントを上手く付けるのが面倒かも
- returnあった気がする
- Common Lisp
- Lisp-2
- 基本的にはマクロで乗り切れるはず
- JavaScript
- 動的型付け言語こそ証明を!
- 懇親会
- あなぷる課金できるようにしようとか
- あなぷろになろう!
- Coq はチューリング完全にはならない
- 停止しない関数書けないし
- semi-recursion?
- あなぷる課金できるようにしようとか
- 帰り
- 大学が最寄りの駅から徒歩60分って、ぇ・・・
けんろん!〜休日カフェタイム〜 第2話演習!
11/21 に、けんろん!〜休日カフェタイム〜 第2話演習! に参加してきました。
- USTREAM
- 本
Basic Category Theory for Computer Scientists (Foundations of Computing)
- 作者: Benjamin C. Pierce
- 出版社/メーカー: The MIT Press
- 発売日: 1991/08/07
- メディア: ペーパーバック
- 購入: 3人 クリック: 57回
- この商品を含むブログ (15件) を見る
Google Books で見れる
自分は今回(第2話)からの参加。
圏論はちょっと触ってたり、前日に第1話を ust で追っかけたりしたので、演習からだったけど楽しめた。
関数合成のまるが見つからなかったので . で。半群の演算を . から * に。
- 1.1.8 Example
- 0 圏
- 対象、射のない圏
- object
- なし
- arrow
- なし
- dom, cod
- 射がないので問題ない
- composition
- 射がないので問題ない
- id
- 対象がないので問題ない
- 0 圏
- 1.1.11 Example
- 3 圏
- object
- A, B, C
- arrow:dom->cod
- f:A->B, g:B->C, h:A->C, idA:A->A, idB:B->B, idC: C->C
- composition (.)
- g . f = h, f . idA = f, idB . f, g . idB = g, idC . g = g, h . idA = h, idC . h = h, idA . idA = idA, idB . idB = idB, idC . idC = idC
- composition associativity ( (a . b) . c = a . (b . c) )
- 定義できる全てのパターンで場合分け or
- a, b, c のどれかは id なので、3パターンで場合分け
- id
- A:idA, B:idB, C:idC
- object
- 最小の3圏
- object
- A, B, C
- arrow:dom->cod
- idA:A->A, idB:B->B, idC: C->C
- composition
- forall f in arrow, f . f = f
- composition associativity
- (f . f) . f = f . f = f
- f . (f . f) = f . f = f
- id
- A:idA, B:idB, C:idC
- object
- 3 圏
- 1.1.9 Example
- 1 圏 (最小)
- object
- A
- arrow:dom->cod
- idA:A->A
- composition
- idA . idA = idA
- composition associativity
- (idA . idA) . idA = idA . idA = idA
- idA . (idA . idA) = idA . idA = idA
- id
- A:idA
- object
- 1 圏 (最小)
- 1.1.10 Example
- 2 圏
- object
- A, B
- arrow:dom->cod
- f:A->B, idA:A->A, idB:B->B
- composition
- f . idA = f, idB . f = f, idA . idA = idA, idB . idB = idB
- composition associativity
- 定義できる全てのパターンで場合分け or
- 全て id が、どれか1つが f の、4パターンで場合分け
- id
- A:idA, B:idB
- object
- 最小の2圏
- object
- A, B
- arrow:dom->cod
- idA:A->A, idB:B->B
- composition
- forall f in arrow, f . f = f
- composition associativity
- (f . f) . f = f . f = f
- f . (f . f) = f . f = f
- id
- A:idA, B:idB
- object
- 2 圏
- モノイド・群
- ホモの定義
- f:M->M' がモノイド (M, *, e) と (M', *', e') の間の準同形写像 (monoid homomorphism) であるとは
- f(e) = e'
- forall x, y in M, f(x * y) = f(x) *' f(y)
- f:M->M' がモノイド (M, *, e) と (M', *', e') の間の準同形写像 (monoid homomorphism) であるとは
- 1.1.6 Example
- モノイド (Monoid : 半群) の圏 Mon
- もん圏
- object
- モノイド
- arrow:dom->cod
- モノイド間の準同形写像 f:M->M'
- composition
- (g . f)(x) = g(f(x)) (x in dom(f))
- (g . f) は monoid homomorphism
- (M, *, e) -f-> (M', *', e') -g-> (M'', *'', e'') として、
- (g . f)(e) = g(f(e)) = g(e') = e''
- (g . f)(x * y) = g(f(x * y)) = g(f(x) *' f(y)) = g(f(x)) *'' g(f(y)) = (g . f)(x) *'' (g . f)(y)
- composition associativity
- (h . (g . f))(x) = h( (g . f)(x) ) = h(g(f(x)))
- ( (h . g) . f )(x) = (h . g)(f(x)) = h(g(f(x)))
- id
- forall o in object, exists id in arrow, forall x in Mo, id(x) = x
- id(e) = e, id(x * y) = x * y
- (id . f)(x) = id(f(x)) = f(x), (f . id)(x) = f(id(x)) = f(x)
- forall o in object, exists id in arrow, forall x in Mo, id(x) = x
- モノイド (Monoid : 半群) の圏 Mon