リリカル合宿

3/5〜6 に、リリカル合宿に参加してきました!

7時に電車乗って、開場よりちょっと前に到着。喫茶店でティラミス食べた。

    • F#について (bleis)
      • → コンピューテーション式 (bleis → mzp)
      • モナドについて (mzp)
      • → Coq について + option がモナドであることの証明 (mzp)
        • 証明の似た所は、Ltac でまとめるといい
        • Proof with auto で始めると、〜... で、〜の後に auto で証明終了できる場合に証明完了
        • あひさめ君が Coq を始めるようです
    • F# で LRU キャッシュ
      • bleis とペアプロ
      • VS の構成
        • ソリューション
          • プロダクトプロジェクト
          • テストプロジェクト
            • FsUnit のソース (本当は lib 以下に dll で置く)
          • lib
      • テストコード
        • FsUnit と NUnit.Framework とプロダクトモジュールを open
        • actual |> should equal excepted とか書ける
          • option のときは、actual |> should equal <| Some 〜 とか書く
      • VsVim
        • 挿入モードでの Ctrl + p 使えない (印刷になる)
          • Ctrl + n も駄目 (新規作成になる)
          • (´・ω・`)
  • 昼飯

ラーメン食った。

  • 昼から
    • bleis の git 講座
      • reset 派と checkout 派があるらしい
        • bleis は rebase 派。rebase-tift。
      • Mercurial は git と比べてソースコードが綺麗」
      • git now と git vim 便利そう
    • LRU キャッシュ続き
      • get で 要素と更新されたキャッシュを返さないと・・・
        • インタフェース変わる・・・
        • 問題変更 LRUキャッシュ → ディクショナリ
    • コードレビュー
      • as パターンマッチ
        • × let hoge ({ value = v } as lru) = ...
        • ○ let hoge ({ value = v } as nyan) = let lru = nyan ...
        • あずにゃんぺろぺろ
  • 懇親会

bleis は辛いの苦手。
再帰作る為に y コンビネータ作ってるのに、作るときに再帰使っちゃあれか。楽だからよく使うけど。

    • Expression Problem
      • オブジェクト指向 : 型の追加楽、操作の追加辛い
      • Visitor パターン (オブジェクト指向) : 操作の追加楽、型の追加辛い
      • 関数型 : 操作の追加楽、型の追加辛い
      • OCaml の多相ヴァリアント使うと、両方いい感じに出来る
        • 再帰する代わりに関数を受け取る
    • リリカル上映会
      • 新しい人が来るたびに巻き戻しでたり
      • 2週目(オーディオコメンタリー)の途中で終わった
        • 3時前くらいまで
    • 数名がこっちの部屋で寝ることになった
      • あひさめ君のいびきはなんとかしないとな・・・ (もうすぐ同居人)
  • 2日目
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 も駄目だった
      • 発表は間に合わなかった・・・
  • 帰り

終わってからどえりゃあ行く組に混ざって昼飯食べたけど、結局途中で帰ることにした。(あひさめ君も一緒に)
あひさめ君は豊橋に帰っていったらしい。
自分は実家へ。

3月

もう3月か・・・
ここんとこ研究ばっかであまり書けなかったな・・・

というか、12月末に研究テーマ決まる(しかも変わった)とかあり得ないだろjk・・・
まぁ何とかなったけど。
論文も提出できたし、結果待ちだが多分大丈夫。


もうすぐ東京住まいか。新生活に夢広がりんぐ。
ただ、新居初期費用半端ないっす・・・


そして来月から働くらしい。
働く・・・ん・・だよね・・・、うん。

第14回名古屋Scala

1/21 に、第14回名古屋Scala勉強会に参加してきました。

今回はコメントがなかったので、本の中身を追っていく感じに。

  • 29章 ScalaJava の結合
    • akka
      • Scala からも Java からも使える、Scala のアクタを書き換えた的なやつ
    • アノテーション
    • 存在型
      • 言語でフルサポートされている - 素晴らしい
      • 存在型はとてもよく使われるらしい
        • Java から使うときだけじゃないよ!
      • 型パラメータの _ (Java の ?) は、存在型を使ってこんな風になってるよ!って話
        • 別に _ の為だけに存在型があるんじゃなくて、存在型はもっと一般的なものだよ!
  • 30章 アクターと並行プログラミング
    • アクタは、リアクティブプログラミングに繋がるらしい
    • receive
      • 待って、来たら進む (ブロックする)
    • react
      • 終わったら終わり (先へ進まない)
    • case object
      • OCaml でいうところの、of のないヴァリアントの時は、case class じゃなくて case object 使う
        • case class は of ありのヴァリアント
    • ivar とか mvar とか
    • アクタがモナドになるとかならないとか
      • bind : receive, return : ...
    • receive の中で receive するのは(・A・)イクナイ!!
      • ヘルパアクタ使う
    • 30.6は次回へ
    • 教養としての Scala
    • 30章と31章はいよいよ大詰めな感じ
      • 時間もいっぱい取ろう
    • 32章と33章は結構どうでもいい
    • 「ここ分からない!」ってところコメントしよう!
      • 大体、「こんなネタがあるよ!」になっている
        • それはそれで面白いけど
    • 日帰りだったので、懇親会から少し早く帰った

NGK忘年会2010

12/ 4 に、NGK忘年会2010 に参加してきました。


ラーメン食ったり、Mac見てたりして少し遅れた・・・
メモ取れたところから。

  • イベント・コミュニティの話
    • 勉強したいことがあったら勉強会をひらいてみる
      • 続けるのはたいへん
    • Git と GitHub を体験しながら身につける勉強会
      • bleis さんありがとう
        • テライケメン
    • RedBull ウォッカ
  • わらび餅
    • わらび餅を作ってきたので休み時間に食べてください
    • 忠告くれた人にわらび餅ひとパックプレゼント
      • 場数踏んでください
        • 場数は踏んでます
      • なんでスカートはいてるんですか
        • 難しい質問なんで懇親会で
  • グダ生な日々
    • gotomeeting 素敵
  • CSNagoya
    • 実体は誰も把握してないとか
    • dominion525と付き合ってる日々
    • claなんとかさん双子説
    • dominion525の友達の友達の友達が彼女になった → 結婚
    • 勉強会を立ち上げると結婚できる!
  • Coq から Ruby へ
    • 隣でお見合いやってる中で Coq やったり
    • Coq
      • 最近アツい!
        • SkillMaps で2位
    • 自動生成されたコード
      • lambda とか禍々しい感じ
    • 年越しで証明しよう
    • ・・・という話を Ruby会議でします
  • EPUB + iPad 紙の本から自由になりたい
    • ちゃんとした話だと謝る流れ
    • デスクをすっきりさせよう
  • セミナールーム
    • ニューキャストさん
    • 千種駅すぐ
    • 料金
      • ムリョ
    • 本にしたい!っていうのも是非
      • これは ムリョ じゃない
  • concrete5 Japan 名古屋ユーザーグループ
    • カレー部は週に1回カレーを食べないといけない
      • 幽霊部員が多いとか
  • 懐古厨 傾向と対策
    • 懐古厨:俺むかしそれ10年前にそれ使ってたわー
    • 86年代はゆとり乙らしい
    • おっさんホイホイとか
  • 名古屋でもPrelにからめて集まってみなイカ
    • イカ帽子
    • どえりゃあ で
    • 第6回 12/25
      • クリスマス関係ない人もそうでない人も是非
    • 勉強会主催してるけど結婚できた例しがない・・・
  • Git と Hudson の連携について
    • イカ帽子
      • 侵略されたw
    • 「俺のLT発表資料がこんなに短いわけがない」
      • 資料間に合わなかった
    • 会社での作業
    • みんなも mzp さんのフックスクリプトのページ、ブックマークするといいよ!
    • 「あ、消しちゃったw」
  • ConvivialNetの近況報告
    • やっぱり侵略されたw
    • なんとか大学の誰得FWつかえねぇ → 自分達で作ればいいじゃない
    • 最新鋭の設備
      • 最新鋭の若者
      • あとは、まぁ。
  • OSS 奨励賞の貰い方
    • 川崎市民なのに名古屋に毎回出てました
    • 強力なOSSプロダクトを作る/翻訳する
  • OpenStreetMap 小ネタ集
    • OpenStreetMap
      • 自由な地図情報データ作成を目的
    • iPhone4 の GPS 精度がとても高い
    • 「こうして、MS は神になりました」
  • とあるアプリのつくる部 - アンドロイダー
    • また侵略されたw
    • 下は 1,2歳のAndroidユーザーから、上は大人の世界まで
    • みんなのラーメンタイマー
      • つ部の人たちが熱い議論をしているとか
      • 技術の無駄遣い
    • 流しそうめん
      • ペットボトルをホッチキスで繋げて・・・
        • 「そうめんつゆを忘れた...だと...?」
        • 「名古屋の人は素材の味が好きなんだ!」
  • Boost.勉強会 名古屋(仮) の開催予定について
    • 仕事は、「日本の平和を守るお仕事」
    • bleisさん主催で Boost.勉強会 名古屋 やるよ!
      • bleis「GitGit!SQLかわいいよSQL!」
        • Boost名古屋・・・
    • 10万3千個のクラスライブラリ とかはありません
    • C++っていうと闇の軍団が怖い」
    • 情報は Boostjp にて
    • 「テライケメン!」
  • UML と Cloud のススメ
    • UML : うしのモヤモヤしたラク書き
    • 「うしが喋ります」
    • シーケンス図のお話
      • わからいんで、Cloud
        • ref #1 芸能界の闇
    • モデリングといえば、ETロボ婚
  • 懇親会
    • 今日だけ肉解禁でもいいよね! (医者から控えるように言われてたり・・・)
    • ひたすらオレンジジュース飲んでました (アルコールは薬の都合で飲めなかった・・・)
    • コンストラクタで例外投げるくらいなら、Option 返す creation method 作ればいいじゃない とか

Coq Party

11/27 に、Coq Partyに参加してきました。

資料などはこちら

  • エンジニア・ミーツ・Coq
    • すぐ分かる形式手法
      • 形式手法とは?
        • 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法
          • 仕様化の正しさは終盤のシステムテストまで分からない
            • 結合テストでバグが「こんにちは!」
              • 手戻りコストがとても大きい
          • V字モデルは横軸工程、縦軸は「開発の詳細さのレベル」
      • ソフトウェア開発の不具合の半数は上流工程
        • その半分は下流工程まで見つからない
        • 上流時点で「厳密で、間違い、漏れ、抜け、矛盾の無い仕様」が必要
          • 仕様は自然言語で書かれているため、あいまい
            • or/xor 問題や、if/iff 問題 など
            • 自然言語ではなく、形式的な仕様記述が必要
      • 形式手法
        • 「形式仕様記述言語」によって仕様(形式仕様)を記述し、設計や検証を行う
          • 数学ベースの厳密な定義
          • 形式仕様は仕様の記述の形式化
            • プログラムではない (≒実行できない)
        • 仕様のシミュレーションやコード生成などが出来るツールがある
          • Coqもその中の一つ (定理証明支援)
      • メリット
        • 自然言語より厳密
        • 上流工程で仕様に対する検証が可能
        • 仕様不具合の早期発見
        • 「証明」などの、高い検証能力
      • デメリット
        • 学習コスト
        • 不具合が完全になくなるわけではない
      • 自然言語とプログラムの中間
      • 各工程で仕様等の検証が可能
      • 形式仕様について完全な検証を行いたい場合、証明を行うことができる
        • テストするだけでは、テストケースから外れたものについては検証しきれない
        • 記述した形式仕様に証明を与えることが出来れば、その仕様は「数学的に正しい」ことが保証される
        • 証明された使用から自動生成されたプログラムは、仕様通りの動作をすることが「証明されて」いる
        • 一般に証明はテストに比べ難しいので、コスト高になるといわれている
        • Coq では、「仕様記述」「定理や補題の付与」「証明」「コード生成」
      • まとめ
        • 仕様をどう記述するかはとても大事
        • 形式手法なら厳密に矛盾なく仕様が記述できる
        • 形式仕様を証明すると、テストよりもスゴイ検証になる
    • エンジニア・ミーツ・Coq
      • ProofCafe
        • 名古屋市内のカフェ「どえりゃあ」
          • お見合い席の隣で Coq やったり
          • おしゃれな食事の隣で Coq やったり
      • 定理証明って面白い!
        • パズルゲームみたい!
      • 普通のプログラムでも証明使えそうじゃね?
        • 普段の業務におけるプログラミングでも、証明が役立ちそうな場合は多い
      • 「ProofCafe で Coq を知ったので、会社で普及させようとしてみた」
        • 流石に職場ですぐに使うのは難しい
        • 「なにで出せますか?」「OCaml です」「OCaml 難しいです><」
      • 職場で Coq を普及させるときの難しさ
        • 「1. OCaml ライクな構文」
        • 「2. 証明とプログラミングのギャップ」
        • 「3. 命題を考えるのが大変」
        • 「4. 数学の知識がたりない」
    • 最後に
      • これから形式手法や定理証明などの力が必要になってきそうな予感
      • 新しい技術を積極的に試すのは大事
      • 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
  • Haskell の Data.Map のバグを見たら Coq を 12,000 行書いてしまった話
    • 「形式化おたくになろう!」
    • バランス木が崩れちゃったバグ
      • パラメータの組み合わせが違うと、バランスが崩れる
    • パラメータを 5 -> 4 にしてなおったよってチケットが閉じられた
      • ほんとに大丈夫?
    • アルゴリズムのバグ
      • バランスの定義して、改善したアルゴリズムがバランスすることを証明
        • 中にいれば大丈夫 + 外だと崩れる
          • 外は、崩れる木が存在することを示す (手でいいや)
          • 中は、大変なので Coq で証明
      • Word を使うと 12900 行でもスライド1枚で収まる
    • psatz 便利
      • A <= B を A <= C と C <= B にするのを自動で
    • 証明にインデントを付けるのは大事
      • 場合分けとか
    • Coq これやっとくといいかも
      • Coq のドキュメントが手元にあるといい
      • Coq が自動で作った名前は使わない方がいい
        • バージョン上がると名前変わったり・・・
          • バージョン明記して諦めるという手が・・・
            • 古いバージョンも持っておけと・・・
              • 業務だと開発環境をとっておくことも多い
      • nsatz 便利
      • Ltac 書けるようになった方がいいんじゃないか
    • プログラムに対して 100倍くらい証明にかかる
      • プログラム側 120行に対し、証明12000行とか
    • intuition 便利
  • 定理証明器 Coq と証明付き DSL (FM勉強会の話と Coq を DSL に使う話)
    • Coq を学ぶべき理由
      • テストで発見できるのは間違いだけ
        • 正しいことは保証できない
      • 網羅性のあるテスト書くの大変
      • オレオレ言語に信頼性はあるのか
    • Formal Methods Forum
      • Google グループ
      • もとは Scala-be の Step by Step Scala勉強会
      • 無料の形式手法講習会がなかった
        • やりたいね
      • 個人的には定理証明系の勉強会がしたかった
        • あんまり上流工程に興味ないし・・・
      • Alloy と Coq が中心
      • 関連勉強会
        • TAPL, Stebe Awodey 読書会
    • DSL
      • 特定分野のタスクのために作られた言語
      • 自然言語より簡潔かつ厳密に記述可能
      • 正しさをどう担保するか
        • DSL で書かれたものの正しさ、DSL 自体の正しさ
      • Ott 証明木を書くと、Coq と LaTeX と Isabell に変換してくれる
      • 金融商品 DSL
      • 認可・監査論理
      • Coq で証明されたC言語コンパイラ
        • 生成されたコードは元のCコードと等価であることを証明
      • 外部 DSL と内部 DSL
        • 外部 DSL
          • どうせなら Coq とかを使って言語の正しさを証明したい 
        • 内部 DSL
          • Coq は実は DSL 向いているのでは
      • DSL Host Language としての Coq
        • ユーザ定義の記述を定義できる
          • Notation
            • 定義と一緒に where で記法を定義できる
            • Haskell の do 記法も書ける
            • .. で繰り返しのあるパターンを書ける
            • 予約後の上書きに注意
          • LTac
            • 外部呼び出しもできる (external ...)
              • 脆弱性注意
            • 気をつけないと矛盾を持ち込んで Falso みたいになるかも
  • Coq extraction機構の概要
    • Extraction
      • Coqからプログラミング言語への自動変換
      • 検証対象が直接実行形式になる
      • 対象言語の中で局所的に Coq を利用できる
        • 段階的に利用できる
      • 全部を Coq でやるのは非現実的だけど、対象言語と組み合わせるととても良い
      • 他の検証機のプログラム生成
      • Coq -> X言語を増やしたい
      • Extraction の実装を Coq で書いて Extract とか
      • Extraction 周りは夢がひろがりんぐ
      • 「Coq は使いこなせるけど OCaml はちょっと,という皆さんが Extraction を書けて便利だと思います」
  • From Coq to Ruby Coq から Ruby へ
    • Extraction のうれしさ
      • Coq が使える ← うれしい
      • どの言語の勉強会でも Coq の話が出来る
      • 証明したコードが他の言語から使える
    • 証明駆動には、Extraction が不可欠
    • Ruby の特徴
      • 型がない
        • Extraction 先としては、型がない方が楽
      • ラムダ式がある
      • 関数と変数で名前空間が分かれている
      • パターンマッチがない
    • Ruby に Extraction
      • 「ハッピーですね」「ハッピーかなぁ・・・」「ハッピーですよ」
      • lambda がいっぱい!
      • 美しいコードを出力しようと思わなければ、結構簡単にできる
    • 抽出対象として適している言語
      • 型がない・動的型付け
      • GCがある
      • ラムダ式
        • なくてもオブジェクトでなんとか
      • パターンマッチ・バリアントがある
      • 関数と変数で名前空間が分かれていない
  • 家に帰ったらExtraction to x を書いてみよう (Coq2Clojure)
    • Coq (Gallina) の特徴
    • Scheme
      • 代数的データ型はない
      • 関数はカリー化されない
      • Lisp-1
      • 安心の末尾再帰呼び出し最適化
      • GCあるよ
        • もはや当たり前になってメリットに挙げるのを忘れられやすいGC
          • でもなかったらとても大変
      • Extractionで幾つかのマクロを作る
    • ClojureへのExtraction
    • Ruby
      • カリー化なし
        • 関数はラムダ式の入れ子で
      • メソッドと変数の名前空間が別 (Lisp-2)
      • 代数的データ型は配列で表現
      • 再起用にYコンビネータを自作
    • 型のある言語
    • 依存型のない言語にCoqのやり方を理解させるのは難しいらしい
      • OCamlだと Obj.magic, HaskellだとunsafeCoerce してる
    • 対象にしやすそうな言語
      • JavaScript
        • Lisp-1
        • カリー化、遅延評価、代数的データ型まわりは自分で
        • 関数型な人はreturnではまるかも
      • Python
        • Lisp-1
        • インデントを上手く付けるのが面倒かも
        • returnあった気がする
      • Common Lisp
        • Lisp-2
        • 基本的にはマクロで乗り切れるはず
    • 動的型付け言語こそ証明を!
  • 懇親会
    • あなぷる課金できるようにしようとか
      • あなぷろになろう!
    • Coq はチューリング完全にはならない
      • 停止しない関数書けないし
      • semi-recursion?
  • 帰り
    • 大学が最寄りの駅から徒歩60分って、ぇ・・・

けんろん!〜休日カフェタイム〜 第2話演習!

11/21 に、けんろん!〜休日カフェタイム〜 第2話演習! に参加してきました。

Basic Category Theory for Computer Scientists (Foundations of Computing)

Basic Category Theory for Computer Scientists (Foundations of Computing)


Google Books で見れる


自分は今回(第2話)からの参加。
圏論はちょっと触ってたり、前日に第1話を ust で追っかけたりしたので、演習からだったけど楽しめた。


関数合成のまるが見つからなかったので . で。半群の演算を . から * に。

  • 1.1.8 Example
    • 0 圏
      • 対象、射のない圏
      • object
        • なし
      • arrow
        • なし
      • dom, cod
        • 射がないので問題ない
      • composition
        • 射がないので問題ない
      • id
        • 対象がないので問題ない
  • 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
    • 最小の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
  • 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
  • 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
    • 最小の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
  • モノイド・群
    • モノイド (Monoid : 半群) (M, *) (または (M, *, e))
      • exists e (単位元) in M, forall x in M, e * x = x, x * e = x
      • forall a, b, c in M, (a * b) * b = a * (b * c)
    • 群 (Group)
      • 半群の条件に加え、forall x in M, exists x' in M, x * x' = e, x' * x = e
  • ホモの定義
    • f:M->M' がモノイド (M, *, e) と (M', *', e') の間の準同形写像 (monoid homomorphism) であるとは
      • f(e) = e'
      • forall x, y in M, f(x * y) = f(x) *' f(y)
  • 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)
    • 半群群・環・体・可換や圏など、数字の世界を抽象化して、規則を満たせばどんなものでも便利なテクニックが使えるようにする
    • 大きすぎる自由は不自由
    • 次回は 1.1.7 Ω-Algebra から