Sovmöss i Underlandet

Name: Ikegami Daisuke Blog: イネムリネズミ日記 Twitter ID: @ikegami__

[sovmoess-blog-blog]

Zen のカスタマイズを GitHub に上げた

昨日の続き

Zen theme をフォークして変更を commit した。

Zen theme (forked)

Add a search box

Change width

Enable MathJax

詳細は project Wiki に。

[sovmoess-blog-blog]

Tumblr のテーマ ZENを適用した

ZEN を適用した。ZEN は MIT ライセンスらしい。

とても満足した。さらに、いくつかの機能を付け加えた：

MathJax

Search tag

ポストの横幅の調整

ZEN テーマを適用した後、どのようにカスタムテーマの CSS/HTML を編集したのかを書く。執筆時のもので、将来は何の保証もしない。

MathJax を使う

Getting Started with MathJax : Secure Access to the CDN に従う。

できれば、ZEN が提供しているように

if:Enable MathJax

みたいな選択肢を設定画面に与えたいけど、まだできていない。

Markdown 記法なら、

$$x \oplus y$$

が、MathJax によって数式表示される（注：上記の説明は 4 spaces による <pre> なので、数式表記されない）。

$$x \oplus y$$

Markdown の文頭 > による <blockquote> の中も、MathJax は展開される：

4.4.4 Graded rings and modules

(snip)

We conclude this section with a concrete example. Let $$I = (x_1^2 - x_2 x_3, x_3^2 x_4, x_1 x_2 x_3, x_4^3) \subset S = K[x_1, x_2, x_3, x_4].$$ -- Grobner Bases in Commutative Algebra (Graduate Studies in Mathematics), Viviana Ene and Jürgen Herzong, p.75

Search tag フォームをヘッダに配置する

Tumblr Theme には {SearchQuery} がある。 そこで RSS の表示の右にフォームを置く。

できれば ZEN が提供しているように

if:Enable Show SearchTag

みたいな選択肢を設定画面に与えたいけど、まだできていない。

ポストの横幅を狭める

横組の場合は1行26文字が理想的であることが突き止められている。 26文字を越えたあたりから、最初の文字の記憶が失われ始める。

-- レイアウトデザイン―レイアウト基本マニュアル (常用デザインシリーズ) p.44

モニタ 1280 × 800 での僕のウィンドウで、各行 40 文字程度であってほしい。ZEN の #container の width は 900px だが、700px に上書きした。

まとめ

ZEN に MathJax や Search tag を追加するリクエストはそれぞれ投げてもよいと思う。一方、ポストの幅などは各自が設定すればいいだろう。Tumblr の自由な theme は嬉しい。

[sovmoess-blog-blog]

x,y,zを自然数とする。このとき、x=3ならばy=5になる。あるいは、y=5ならばz=8になる。

表題にある問題は @noricoco さまが提出したもの。Togetter にまとめがある。

正しいのになぜかみんなが「変だ！」という問題：　x,y,zを自然数とする。このとき、x=3ならばy=5になる。あるいは、y=5ならばz=8になる。

— norico (@noricoco) May 29, 2012

いつものように Agda で解いたんだけど、思いのほか時間がかかりました。被害者を増やさないために記録を残します。結論：Coq はいいものだ。

まず最初に Agda のインストール。慣れてるはずなのに、ここでつまずいた。のたうちまわったあげくインストールできたのだが、そんな苦労は見たくないだろうから説明は後に回す。

gist にあげた最終的に得られた証明譜をあえてペーストする：

module Noricoco where open import Data.Empty using (⊥-elim) open import Data.Nat using (_≟_; ℕ) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Relation.Binary.PropositionalEquality using (_≡_) open import Relation.Nullary using (yes; no) triv : (x y z : ℕ) → (x ≡ 3 → y ≡ 5) ⊎ (y ≡ 5 → z ≡ 8) triv x y z with y ≟ 5 ... | yes p = inj₁ (λ _ → p) ... | no ¬p = inj₂ (λ q → ⊥-elim (¬p q))

さらさらと書けました、かっこいい！？残念ながら Agda の場合そういうふうにはいかない。対話的に証明を完成させるシステムなので、計算機とユーザがお互いに殴り合うことになる。ちなみに計算機のほうが強い（なにかがおかしいが、「対話的」定理証明系ではそれが日常である）。

最初に考えるのは、日本語で書かれた問題をどうやって Agda 語にするかである。自然数と「または」と等号が特別に必要なので、Agda 標準ライブラリからそれぞれ Data.Nat Data.Sum Relation.Binary.PropositionalEquality を open import する必要がでてくる。こういうことが初心者にはわからない。サジェストしてくれるシステムにならないと、誰も使わないよ？

一方、Agda では「すべての」や「ならば」は特にモジュールを必要としない。肝心の問題を triv と名づけた。最近の Agda は 3 とか書くと Data.Nat に定義してある suc を使って内部で suc (suc (suc zero)) に変換してくれる。

-- 最初に書いた証明譜 module Noricoco where open import Data.Nat open import Data.Sum open import Relation.Binary.PropositionalEquality triv : (x y z : ℕ) → (x ≡ 3 → y ≡ 5) ⊎ (y ≡ 5 → z ≡ 8) triv = ?

ここからネタバレになってしまうので、証明を自分で考えたい人は読むのをやめてほしい。

キモは y = 5 にある。この = は等号であって代入ではない。Agda と Agda 標準ライブラリでは = の代わりに ≡ を使う決まりになっている。

最初に考えつくのは次の証明譜である：

triv : (x y z : ℕ) → (x ≡ 3 → y ≡ 5) ⊎ (y ≡ 5 → z ≡ 8) triv x 5 z = ? triv x y z = ?

一つ目の ? は簡単に解決できるのだが、二つ目の ? は簡単ではない（と思う）。Agda のパターンマッチは強力だが、「 y が 5 ではないこと」を陽に証明に使うのは困難である。だれか挑戦してください、難しいよね？

Data.Nat における ≡ が決定可能であることに気がつくと、証明譜を改良することができる（そのためにも Data/Nat.agda をあらかじめ読んで理解する必要がある）：

triv : (x y z : ℕ) → (x ≡ 3 → y ≡ 5) ⊎ (y ≡ 5 → z ≡ 8) triv x y z with y ≟ 5 ... | foo = ?

ここで Agda の対話的操作がかっこよく決まる。ゴール ? のなかで C-c C-c foo (文字シンボル foo について make a case する)と、書きかけのコードが自動的に変換される:

triv : (x y z : ℕ) → (x ≡ 3 → y ≡ 5) ⊎ (y ≡ 5 → z ≡ 8) triv x y z with y ≟ 5 ... | yes p = ? ... | no ¬p = ?

やったー。これで y = 5 であるかないかの証拠をはっきりともらう。最初の ? が「x = 3 ならば y = 5」に対応することに気がつきさえすれば、ゴールを解決するのは難しくない。より難しいのは最後の ? で、Agda で矛盾を証明するテクニックが必要になる。どうやればいいのか困ったのだが、ウェブで検索したら私の文章がでてきた。そろそろ記憶力の低下を補わねばならない。

こういうのは Coq で書けばよいのであって、最初に挙げた togetter のログを見てほしい。先人たちが Coq で証明を書いています。現行安定版の Agda のどこが Coq と違っていいの？と聞かれたら、ちょっと長くなるが我慢して聞いてほしい。「タクティクスはないです。Coq のゴールで、どのようなタクティクを使えば、よりゴールが証明完了に近づくのだろう？という悩みが Agda にはありません。理詰めで型を合わせることが証明になっており、人間が賢ければ、ストレスなく証明が終わる」「その代わり Agda では Agda 標準ライブラリという先人の智慧を使わないと、証明譜がやたら長くなる傾向があります。Agda のパターンマッチの強力さと非力さに悲しい思いをします。証明が完了するまで Agda は人間の入力を拒み続けるので、辛抱が大事です。折れず負けず不屈の魂で、証明完了の喜びをわかちあいましょう、うわあこれは宗…（おわり）」

残りは苦労話。今日 Agda のレポジトリの head を取ってきて build したら、syb を陰に使っていて失敗した。高速化のために syb から geniplate に移行する作業を進めているらしいが、一方で syb をやっぱり使いたいというダメなソースコードになっており、コミッタの人は早く判断していただきたい。つぎの AIM まで待たなければならないのか？しかたないので、安定版を導入すべく cabal update; cabal install Agda-executable して設定をすます(簡単に言うが時間のかかる操作である)。Agda 標準ライブラリを darcs pull したら failed してむぎぎーとなる。darcs repair でも失敗する。darcs get にも失敗する。darcs のバージョンの問題を疑い、cabal install darcs したらできなかった。Agda の依存性解決に失敗する恐れがあるから、と Cabal に言われた。これだから Haskell は…いや Haskell は悪くない、悪いのは Cabal である。

Snow Leopard にしてから、configure に Aqua を使うように設定した Emacs の configure --with-ns がコケる。Emacs 23 も 24 もだめ。Leopard ではうまくいってたのに。Terminal.app は Unicode の数学記号を上手に表示できないので論外。iTerm だと Emacs のミニバッファが文字化けする。X11 な Emacs のビルドにもこけるありさまで xterm は Happy Hacking Keyboard の入力に対応するのが面倒だ。

しょうがないので Aquamacs を使うことにする。Aquamacs はデフォルトのフォントサイズが小さすぎるし、ぼくの .emacs を拒む。そういう意味で使いたくないエディタだが Agda のためだと思えばしかたがない。

Gentoo Prefix の app-editors/emacs-23.4-r2 のビルド失敗のログを残しておく。ぐぐるといろいろでてくるんですけどね…

(snip) checking AppKit/AppKit.h usability... no checking AppKit/AppKit.h presence... yes configure: WARNING: AppKit/AppKit.h: present but cannot be compiled configure: WARNING: AppKit/AppKit.h: check for missing prerequisite headers? configure: WARNING: AppKit/AppKit.h: see the Autoconf documentation configure: WARNING: AppKit/AppKit.h: section "Present But Cannot Be Compiled" configure: WARNING: AppKit/AppKit.h: proceeding with the compiler's result checking for AppKit/AppKit.h... no configure: error: `--with-ns' was specified, but the include files are missing or cannot be compiled.

直すためには configure.ac をいじらないとダメっぽい。CFLAGS をごにょごにょするだけでいいよってどこかに書いてあったけどそれだけではダメでしたよ？

僕が遭遇した問題の解決策を求めてこの記事を訪れた人は残念でした。どこか別を当たってください。

[sovmoess-blog-blog]

If you'd be interested in a 2nd edition of Real World Haskell, please RT and think about filling out this quick survey: http://bit.ly/ooydix Bryan O'Sullivan(@bos31337)

@donsbot の最近の RT より。なんで 1 年前のツイートを RT してるのか理解に苦しむ（後記：reddit Haskell でキャンペーンやってたのでそれだ）のだけど、Real World Haskell 第二版を求めるひとは、上記のアンケートに答えるといいと思う。

[sovmoess-blog-blog]

「第一回関数型言語勉強会 大阪」に参加しました

2012-05-19 に行われた第1回 関数型言語勉強会 大阪の参加記録です。この記事を tweet するときは、#fpstudy のハッシュタグをつけていただくと参照しやすいです、よろしくお願いします。目次：

あえて自己紹介的な何か

改善された発表スライドと発表の補足

他の発表者の皆様の発表まとめと感想など

懇親会での「公開しても構わない」ネタ

今後の課題、参考資料

あえて自己紹介的な何か（発表スライドには書かなかったので）

私の発表は LT でしたので余計なスライドは入れない方針をとりました。自己紹介しなかったのでこの場でします。いままでどんなプログラミング言語を触ってきたかについてだらだらと。

プログラミングを初めて知ったのはファミリーベーシック V1.0 でした。自分ではプログラムを書きませんでした。ただ、今は亡きベーマガの投稿プログラムを写経した記憶があります。ファミリーベーシックは言語仕様は面白くて、特にゲームを作るための独自命令がいくつもあったのを覚えています。省メモリプログラミングが必要で PEEK と POKE が飛び交うプログラムが至上とされ、良いゲームほどひどい（褒め言葉）プログラムでした。

次に触ったプログラミング言語は LOGO です。新宿 NS ビルでソニー様が主催した、親子で体験するプログラミング講座みたいなのがあったのです。非常に教育的な内容でした。しかし自宅には LOGO の環境がなく（今思えばファミリーベーシックで LOGO インタプリタ作ればよかったのかな…）それっきりで終わってしまいました。

高校に入学したときお祝いと称して PC-9801 DA (3.5 インチフロッピーモデル) を買ってもらいました。秋葉原の店員さんがとても教育的な人で、QuickBASIC と Quick C の両方を推薦してもらいました。QuickBASIC は非常に洗練されており、初めてまともに動くプログラムを自力で何か作った覚えがあります。一方、Quick C というか C は #include <stdio.h> の意味がわからないレベル（当時）だったのでまるで活用できませんでした。しかし、当時の MS-DOS 3.3C のメモリモデルとかアーキテクチャについてはぼんやりと把握した記憶があります。C でプログラムを書くようになったのは大学に入学してからです。友人は Nifty Serve に入っており様々な情報を入手してましたが、僕は入っておらず C プログラミングについてまったく無知だった。

大学に入ると NeXTSTEP が待ってました。NeXTSTEP に付随する Objective-C 1.0 開発環境はとても優れていて、いままでのプログラミングとは何だったのか…と思い知りました。在学中の 4 + 2 = 6 年間ずっと Objective-C でいろいろなものを作りました。特に LifeGame の実装が単位取得の条件になったので、GUI 含めてかなりキアイの入ったものを作りました。『ライフゲイムの宇宙』がすばらしい参考文献です。グライダー銃で仮想計算するとかやりましたね。#include <stdio.h> が何かがようやくわかった。それから Tcl/Tk の講習を受けて何か書きました。

NeXTSTEP は Unix がベースでしたがどちらかというとマイナーな部類でしたので fj.sources や anonymous FTP で提供されていたツールのビルドに失敗することが当たり前でした。そこで、ソースだけでなく configure や Makefile を自分で作りなおすという経験をしました。いま Gentoo がお気に入りなのはその影響もあります。

大学にはいって関数型言語にも触れました。Mathematica と Emacs Lisp です。プログラミング言語の視点から見ると当時の Mathematica はいろいろな不満点がありました。効率のよい計算をするためには関数プログラミングが不可欠でした。特に書換え系(term rewriting)の知識を持っていると計算が早く終わります。Mathematica でプログラム書くより Objective-C 使いたくなったので、Objective-C の C ブリッジで Mathematica の C API (MathLink) を叩くライブラリを書きました。イリノイ大学の人々がそういうことを独立にやっていたので、email で連絡を取り合いオープンソースをいじるという体験を初めてしました。API の重要性に気がついたのはこのときが最初で、いまでも設計の優れた API を見るたびに感心しています。当時の Emacs Lisp も別の意味でいろいろな不満点がありました。DRY 原則を保つために関数プログラミングが必要でした。YaTeX をいろいろカスタマイズしました。

博士後期課程の 3 年間では趣味で ruby 研究で C を使っていました。Objective-C が恋しかったので、つてを得て NeXT Station を一台手元に置いていました。ruby の C 拡張使ってライブラリを書いたら高林さんに使ってもらえたりしました。研究がスランプに陥っていたので、その代償としてプログラムばかり書いていました、この頃の話は前にも書いたけど。関数型言語も相変わらず Mathematica や Emacs を使っていたので何かをちまちまと書いてました。ruby の C 拡張で Mathematica の C API を叩くということもしました。述べたように Objective-C で書いた経験があったので難しいことは何一つないです。あと Mew を使い始めたので自分のためのカスタマイズを書いていました。Mew はすばらしかった。

関数プログラミングが業務になったのが就職後の一年目で、このとき初めて関数プログラミングが学問でもあるということを知り驚きました。fj.comp.lang.* は見てましたがプログラミングが研究として成り立つってのは頭に入ってなかった。そういえば、師匠は関数型言語のコンパイラを書いてそれで職を得ていたわけで、もっと早くからわかっているはずのことを、なにもわかっていなかった。2004 年に業務命令で Haskell を速習し ghc 6.4 を使って Haskell でプロダクツをいくつか書いて現在に至ります。卒業して 9 年目にしてようやく師匠の仕事ぶりを理解できる立場になりました。昔話を聞いてみたいものです。

まとめると、プログラミング言語遍歴は BASIC → LOGO → C / Objective-C / Mathematica / Emacs Lisp → Ruby → Haskell です。関数型言語の背後にある関数プログラミングの概念を学術的に学びはじめました。教科書だけでなく論文も読むようになりました。現在に至ります。今回の勉強会に参加するにあたって、「言語を問わず」って主催者の人に言われたので、わたしの身の回りにある関数型言語の処理系をいくつか触りました。いいきっかけになりました、ありがとうございます。

改善した発表スライドと発表の補足

今回補欠枠にもかかわらず発表の機会を下さった勉強会幹事の皆様に感謝いたします。

ところで勉強会のプログラムはだいたいが曖昧で、実際聞いてみると Haskell 固有の話題が特に注意なく散見されたので、発表寸前にスライドを増やしました。

まずは、入門編ということで、「関数型言語の基礎」について、勉強しませんか？

今回の勉強会は「関数型言語とはなんぞや」という考え方に重きをおこうと思いますので、特定言語にこだわるつもりはありません。

参加対象者：関数型言語に興味がある人。初学者〜中級レベル

ATND の勉強会のページより抜粋

次回は皆さんの発表がつながるように事前に打ち合わせしたほうがいいと思います。簡単なことではないということを理解していますがそのうえでよろしくお願いします。また、発表に対する質問時間をもっと用意してください。今回は質疑応答が足りませんでした（セッション枠で 30 分目一杯使った人が多かったこともある）にもかかわらず、最終的に時間は 20 分ほど余りました。懇親会に参加して質問しまくった方はそれが正解です。

第1回関数型言語勉強会 大阪 LT 資料

View more presentations from ikegami__

わたしのスライドです。今では手に入りにくくなってしまった「関数プログラミング」の良書を集めてそれを紹介するというのが目的でした。ついでに今手に入る本も紹介しました。関数型言語全般の背景知識として持っておいて損はない情報です。べつにこれらのことを知らなくても関数型言語を使う業務に就けましたが（わたしのことです）事前に知っておいたほうが経験的によい事柄です。対象はオブジェクト指向はわかっているんだけど、関数型はよくわからないという人です。@tanakh さんのツイートと、@nushio さんの白眉の自己紹介文を断ることなく引用しました。お二人にはとても感謝しております。@nushio さんの表明「抽象化が実行速度を向上」は、誤解を生まないように気をつけて紹介しました。

ひとつ反省すべき点があって、OOP で抽象化・構造化するとき「クラス」を使うんだよって説明したんですが、プロトタイプベースな OOP の存在を忘れていました。だれか突っ込んでくださいよ。プロトタイプベースなら記述の自由度がそもそも高いので、抽象化構造化はプログラマのセンス次第でどうとでもなるでしょう。おわり。他にも反省すべきところがあるかもしれないので速やかに指摘してください。

@yoshihiro503 さんから「Real World Haskell は Haskell を学ぶうえで良い本ですか？」という質問をもらったと思うのですが、「現在ではよくないので次の版を待ちましょう」と答えました。Real World Haskell の初版は 2007-2008 年に書かれていて、ghc 6.8.2 のコードで溢れているので、現状の ghc 7 系列と互換性がなくなる具体例があり初心者がはまってしまうのでお勧めできなくなりました。写経ができないので非常に残念です。たとえば、19 章の divby5.hs は ghc 7 では違う書き方をします。ghc 7.4.1 で試してみるとこうなる：

-- file: ch19/divby5.hs divBy :: Integral a => a -> [a] -> Maybe [a] divBy = divByGeneric divByGeneric :: (Monad m, Integral a) => a -> [a] -> m [a] divByGeneric _ [] = return [] divByGeneric _ (0:_) = fail "division by zero in divByGeneric" divByGeneric numerator (denom:xs) = do next <- divByGeneric numerator xs return ((numerator `div` denom) : next)

% ghci -ignore-dot-ghci (snip) ghci> :l "ch19/divby5.hs" (snip) ghci> :m + Control.Monad.Error ghci> (divByGeneric 50 [1,2,0,8,10])::(Integral a => Either String [a]) *** Exception: division by zero in divByGeneric （Real World Haskell Web 版 19 章では、 ここで Left "division by zero in divByGeneric が出てくることを期待している）

これをどのように直したら ghc 7.4.1 に対応するかは、次回以降のエントリをお待ちください…（きっと他の誰かがやる）初心者が写経すると混乱しますよね…あとは Control.OldException の話題とかですね… OldException は後方互換性のために残されてますが、この文章を書いているいまではその代わりに Control.Exception を使うことになってる。このような、ghc の歴史をちょろっと知ってる人がすぐ指摘できる程度の問題を解決できないのが Real World Haskell 初版の残念な点。

Real World Haskell（原著のほう）の次の版が出るらしいという噂は聞いていますがあくまで噂のレベルです（freenode #haskell で見た記憶が）。ghc は過去のバージョンのコードが動かなくなるような変更を平気でやるので（その代わりに新しく良い機能が次々と導入される）、Haskell のプロダクトを業務で使うにはいろいろ苦労することがあります。処理系のバージョンを気にしなければいけない点は Haskell に限らずどのプログラミング言語でも言えることですが。

「関数型言語は他のパラダイムの言語と比べて何が良いのか、勉強する前に教えてほしい」と質問されても答えに窮します。強いて言えば「読みやすく書きやすく短くなる」ことですが、これは関数型言語を理解していないと読めないし書けないし短くできないので、「いいから勉強してください」としか答えられません。わたしの能力不足です。「数学/英語/美術/etc.を勉強して何が良いのか、勉強する前に教えてほしい」という質問に似ています。豊かになるんですよ。

最近のプログラミング言語は関数型言語の良い部分を取り入れているので、関数型言語じゃなくてもいいという正論もあります。正直、現代の事情を鑑みると、関数型言語を自称する言語を勉強するメリットは昔に比べて減っています。関数型言語は簡単には習得できないし、何らかの理由で勉強したい or 上司に言われたので勉強せざるを得ないと思った人（わたしのような）が勉強すればいいでしょう。

何から勉強したらいいかわからない、その疑問はもっともで、誰か身近な guru に聞いてください。わたしもメールをもらったらお返事を書く程度には余裕があります。Twitter は今は止めています。

他の発表者の皆様の発表まとめと感想など

プログラム順ではなく、実際の発表順に感想を書きます。タイトルも ATND の仮ページにあるものではなく、できるだけ実際のスライドにあったものにします。講評できるほど偉くはないです。

たのしい関数型 by @s_kozake さん

たのしい関数型

View more presentations from 信一 小酒

スライドのほぼいたるところに突っ込まれるスキがあると思います。もし事前にスライドを公開していたら、もしかすると、皆さんの力を借りて直せたかもしれません。

@s_kozake さんとは懇親会でお話できました。とても感じの良い方です。お知り合いになれて良かった。願わくば今回のご発表を通じて間違えて理解しておられることを正していただきたいです…

今日からはじめる Clojure by @kuchitama さん

今日から始めるClojure

View more presentations from Kiyotaka Kunihira

Clojure の丁寧な説明でした。インストールの方法から、leiningen の使い方、Clojure の導入まで。Kyoto.clj というミーティングの紹介。行ってみたいですが、次回の Kyoto.clj っていつどこでやるんでしょうね？

関数型って？ by @kitora_naoki さん

第一回関数型言語勉強会 大阪

View more presentations from Naoki Kitora

この発表にも突っ込まれるスキがたくさんあります。Haskell を始めとする純粋な関数型言語の特徴を関数型言語の特徴と言うのは語弊があります。

記憶が確かなら、今回の勉強会の司会をつとめてくださった方です。ありがとうございました。

C#er が F# ちょろっと這い寄られた感想とか by @Posaune さん

C#erがF#に這い寄ってみた

View more presentations from Hiroshi Maekawa

F# の導入と IDE の紹介でした。IDE がある関数型言語 F# はすばらしいですね。あと、おまけスライドで紹介されていた、学習記録を GitHub で管理するテクニックはなるほどなと思いました。

ここで最初の休憩がありました。発表の突っ込みをしたかったけれど、その元気は自分の発表のために温存しなければならなかった。

プログラムを計算する話 by @uskz さん

わたしが関数型言語勉強会 大阪に参加したかった理由その 1. でした。その 2. は @syamino さんの話でそちらはあとで書きます。

@uskz さんらしい発表だったので皆さんにとってもよい休憩時間だったと思われます。わからない発表を聞くときは休憩すればいいんですよ？

数式は手書きでスキャンするのがいいですね。わたしもスキャナが欲しいです。発表の内容は Richard Bird & Oege de Moor の "Algebra of Programming" にある具体例の紹介でした。が、前口上として、なんで Algebra of Programming なのか？の部分が面白かったです。非常に怪しい前口上でした（褒め言葉）。非常によい本ですが古書なので高いです。

Algebra of Programming の内容（の第一章）は Haskell に限らず modern functional programming language における高等テクニックです。つまり簡約戦略が strict でも non-strict でも成り立つ話です。今回の集まりでは「関数型言語ならなんでも通用する話をせよ」という要求が主催者サイドからありました、という意味で適切な内容でした。@uskz さんが発表してなかったら、ぼくが代わりに同じ内容を発表していたかもしれません。

Algebra of Programming の最終章は貪欲法と運算を示します。@uskz さんはサービス良くこの最終章の具体例まで持ち込んだので、さすがに 30 分間で全部言うのはエクストリームスポーツだと思いました。次回に分ければもっとよかったのに。全部聞けたわたしにとってはありがたい話でしたが。

@uskz さんの話を日本語で知りたい人は「運算 プログラミング」というキーワードで検索しましょう。演算ではなく運算です。Google が勝手に「もしかして 演算」とお節介を焼きますが、運算で検索しましょう。運算は calculational program transformation の訳語です。『関数プログラミングの楽しみ』Jeremy Gibbons and Oege de Moor 著の 5 章 86 ページ目から読みはじめるのが簡単かもしれません。この本の運算の説明では圏論が陽に出てこないので（とはいえ 10 章の Arrow by Ross Peterson で圏論が出てくるのですが…)。

@uskz さんの発表の途中で出てきた Fokkinga の再帰定理 (Fokkinga's mutual recursion theorem) は、@uskz さんの計算につかうものなのですけど、説明できるほど深くわかってないのでググってください。

途中まで補足を書いていたのですが、Web で可換図を書くことが非常に面倒なので、いつかやることにします。その代わりに、"Algebra of Programming" の第一章の最初の具体例を Haskell に書き直したものをお見せします。

-- よくある自然数 Nat の定義 data Nat = Zero | Succ Nat deriving Show -- 足し算 plus m Zero = m plus m (Succ n) = Succ (plus m n) -- かけ算 mult m Zero = Zero mult m (Succ n) = plus m (mult m n) -- 足し算とかけ算って、似てるよね？（えっどこがですか…よく目を凝らしてください） foldn :: a -> (a -> a) -> Nat -> a foldn c _ Zero = c foldn c h (Succ n) = h (foldn c h n) -- foldn を用いて plus, mult を書き直すと… plus' m = foldn m Succ mult' m = foldn Zero (plus' m)

@uskz さんは計算効率の面から fold を紹介していましたが、効率関係なくても説明できる概念です。plus' がよりよく見えてきて、愛情がわいてきます。この例はあまりにも単純すぎますが、現実に使うコードでも同様のテクニックを用いてコードの改善（または改悪）ができます。プログラムの変換は重要な考え方で、その方法のひとつとして Algebra of Programming があります。foldn は天下りにやってきたものではなく、計算による理由付けから自然に導出されるものです。@uskz さんの手書きのスライドはそういう計算をやっています。まだいろいろ言いたいですが、紙面の都合上というか、この文章全体が書き終わらなくなってしまうので中途半端に終えます。

関数型脳になろう! by @its_out_of_tune さん

Material

View more presentations from _TUNE_

スライドをみてください、Java です。Java で何か見せればすごいと思いますが、なにもすごいところはスライドにはなかった…この次は型とワイルドカードでなにかやってくださいよ（わがまま）。

@its_out_of_tune さんとは懇親会で楽しくお喋りしました。東京からわざわざ来られていて体力と行動力に驚きました。@melponn さんの体力と行動力はふだんから見聞きしているのであまり驚かない。

わたしの発表がここでありました（前に述べたので省略）

Inverse FizzBuzz のはなし by @quassia88 さん

20120519 inverse fizzbuzz を解いてみよう

View more presentations from HiroSuga

Inverse FizzBuzz の話でした。@quassia88 さんの GitHub リポジトリにマテリアルがあります。

Inverse FizzBuzz は問題を読んでから Haskell ならリスト内包表記とガードで瞬殺じゃないかなと考えました。実際 @notogawa さんのやりすぎでない方のコードと似たコードを考えていました。いま読むと、このコードにも、わたしが書いた（非公開）コードもバグがあるような気がするけど、わたしが疲れているだけだろうか？まあともかく宣言的に書けるのは間違いない。

スライド 26 ページにあるコーナーケースを突くテスト項目に感心しました。関数プログラミングでもテストは大事。

多相Variantの紹介 by @kyon_mm さん

OCamlの多相Variant紹介 #fpstudy

View more presentations from Kyon Mm

@irof さんをいじるネタがまったく理解できませんでした。スライドの説明はわかりました。OCaml はすごい。

わたしが知る限り、Haskell に多相 Variant はまだなくて (ghc 7.4.1)、しかし似たことは 型クラスの変態拡張 すればいいという話があります。いつかさらなる変態拡張で入るかもしれないな、使い道がどこにあるかわからんけど。@keigoi さんのモジュールの集約に多相バリアントを使ってみたをあとで読む。香川先生の Polymorphic Variant in Haskell はその後どうなったんですかね？例によってOleg Already Did Itだったらしいが？

ラムダ計算で代数的データ型を表現する方法 by @syamino さん

代数的データ型をラムダ計算の中で表現する方法

View more presentations from syamino

@syamino さんはブログで説明しなおしています。発表スライドだけでなく記事も読みましょう。

λ計算の教養を積みましょうという話です。関数プログラミングだけをしていると、こういうことに気がつかないので、結果的に知識の浅いプログラマになってしまいます。それはよくない。

この発表を聞いた後は Mogensen-Scott encoding について調べればいいと思います。自明でない encoding があってそれのおかげでいろいろなことがつながります。

こういう話を聞くには質疑応答の時間が必要で、それが用意されていなかったのは残念でした。

スタート SML# by @keita44_f4 さん

スタート SML# の Ustream をすでに見ていたわたしにスキはなかった。何度でも同じことをいろいろな場所で紹介することはとても重要です。SML# のためのパーサライブラリとか作ったら喜ばれるのかしら。もうすでにあるのかな。

Haskell 入門 by @irof さん

スライドはこちら。

Haskell 入門というより、HSpec 入門でした。HSpec は大変よいものです。

関数型言語でプログラム書くときでもテストは重要です。テストのための標準言語はなんですか？といわれれば、それが xSpec (x にはいろいろなプログラミング言語の名前が入る）。xSpec には作法があって文法があって関数があって標準出力フォーマットがある。これらは、テストの標準言語として進化し改善されているので、オレオレテストフレームワークを使うくらいなら、xSpec を試したほうがよい。実装とテストはコードを分けるべきで、そういう意味で Python の doctest より xSpec のほうがよい。

懇親会での「公開しても構わない」ネタ

懇親会で一番重要なことは「席取り」です。つまんない人のそばに座ってしまうと、ひたすら食べて飲むだけの時間になってしまい非常に残念なことになる。次に重要なのは、あらかじめ話しておきたい事情を事前にまとめておくことである。

勉強会に行くたびに後悔しているのでそろそろ書いておかないといけない気がするので書きますが，個人的な意見として，勉強会に行くときの準備で一番重要なのは「この勉強会・懇親会には○○さんと××さんが来るから，○○さんと××さんに問い詰めたいことリストを整理してまとめておこう」かと．

— 鉱物君さん (@Cryolite) 5月 19, 2012

さすが Cr(ry) センセイやで。まあそれはともかく、わたしは @syamino さんの隣で @quassia88 さんの向いで大変よい席を取りました。背もたれがあるなしも見過ごしがちなポイントです。席取りがゲームの勝敗をにぎるカタンというゲームを毎日やるといいです。@melponn さんと @fadis_ さんがものすごい大声で話しまくっておられたので「ちょっとやめないか？」と言いたかったのを自省しつつ、お二人の仲の良さをうらやましく思いつつ、テーブルに話題を振る係をした。そういうことが好きなので。

まあだいたい聞きたいと思ったことは聞けた。なんかここで書きたいなと思ったことがあったんだけど、忘れてしまったぞ。「@syamino さん、そのまま君の道をつっぱしれ」と陰ながら思ったことだけは書いておく。@quassia88 さんとはいい酒を飲んだ（ぼくはウーロン茶でしたが）。終盤に各テーブルへ移動し一人残らず全員と挨拶しておしまい。

今後の課題、参考資料

「関数型言語の話題を初心者向けに話す」を字面通りに受け取って貴重な休日に話を聞きにきたひとたちには本当に申し訳ないことだと思う。まあだいたい勉強会はいろんな人がしゃべるので話題が散逸するのはしかたのないことだけれど。戦犯探しをしてもしょうがないので（ぼくが戦犯かもしれんし）、次回以降に改善してほしい。関西人ならツッコむところはツッコむべきやろ、そこ。

これからの方向性は３種類にわかれると思うので書いてみる。わたしが思いついてない他の選択肢は当然いろいろあると思います。

初心者〜中級レベル re-visited

Getting started

Killer applications

一つ目は単純に第一回の反省を活かして、初心者のひとの意見をもっと大事にする会にすること。あるいは二つ目は各関数型言語のインストールから Hello, world までの手順を紹介すること。これはスライドでなくても構わなくて、ただ URL を示せばいい。最後は関数型言語を使いたくなるようなスゴイ成果物を皆に見せること。ご検討ください。

（おまけ）実はお昼に焼肉の会があったのですが、それが楽しかったです。特に名古屋の皆さんとお会いできたのは幸いでした。企画してくださった @uskz さんに感謝です。なんばまで頑張って行きましたよ…

観測範囲内の参加記録一覧でおしまいにします、抜けてるのがまだあるかもしれない（Twitter の #fpstudy で検索）：

@bleis さんの参加記録

@emaxser さんの参加記録

@irof さんの参加記録

@its_out_of_tune さんの参加記録

@krrrr38 さんの参加記録

@moririring さんの参加記録

@ore_public さんの参加記録

@Posaune さんの参加記録

@s_kozake さんの参加記録

誰か？の参加記録

誰か？の参加記録

[sovmoess-blog-blog]

「第一回関数型言語勉強会 大阪」に参加しなかった人へ

この記事は tumblr. の予約投稿システムにより 2012-05-18 に自動的に公開されます。

Medical disclaimer : この記事は情報科学の専門家が書いたものではありません。読者の皆様、知りたいことは専門家に聞きましょう。

目次：

はじめに

「関数型言語」とはなにか

関西という土壌と純粋関数型言語 Haskell （昔話）

まとめ

はじめに

第一回関数型言語 大阪 というイベントが 2012-05-19 に行われます。記事を執筆している時点で、45 人が参加、33 人が補欠という人気ぶりです。僕は参加者サイドなのですが、参加しない about 33 人にも楽しい何かを伝えたいと思い、こうして筆を取っています。

なにか meeting を始めるためには前準備が必要です。The Internet を会場に求めるとオカネが発生するわけですが、関西に安い場所は存在しない（ようだ？）。部屋の capacity のことも考えなくてはならない。公民館は安価に確保できるひとつの候補ですが about 50 あたりが閾値になります。また、50 人の参加者全員が laptop 使うと公民館のブレーカが落ちます。笑えない話です。できるだけ多くの皆さんが快適な環境（すなわち、Wi-Fi インタネッツのことだ！）で meeting をしたいわけです、が、それは簡単ではない。今回のイベントに参加できなかったおおぜいの人がいるのはしかたがない。

次の節では、「関数型言語」とはなにかを僕なりに述べます。そして、関西という土壌と純粋関数型言語 Haskell の昔話をして、最後にまとめを書きます。

「関数型言語」とはなにか

「関数型言語（Functional Programming Language）」と自称するプログラミング言語はたくさんあります。したがって、「関数型言語」とはなにか？という質問の答は「くどくどくど…」です。

この答は読者を失望させること間違いなしです。しかし、冷静になっていただきたいのですが、「命令型言語（Imperative Programming Language）」とはなにか？あるいは、「手続き型言語（Procedural Programming Language）」とはなにか？という質問ならばどうでしょうか。やはり、「くどくどくど…」という答しかないように思われます。

つまり、表題の「関数型言語」とはなにか、という問いはそもそも答がありません、と思います。

その代わりにパラダイムを考えることにしましょう。読者にとって一番身近なパラダイムは、おそらく「オブジェクト指向（Object-oriented Paradigm）」でしょう。オブジェクト指向言語はオブジェクト指向を背景に持つプログラミング言語です。同様に、関数型言語は「関数プログラミング（Functional Paradigm）」を背景に持つ言語だと定義します。

ここで余談。関数プログラミングの代わりに「関数型プログラミング」と言う場合もあります。困ったことに、「型」には少なくとも二種類の意味があるので初心者にとって混乱の原因となっています。一つは「関数型」の型ですね、これは自然に使われます、たとえば「手続き型」の型のように。もう一つは、プログラミング言語における「型（type）」です。「静的型付き（statically typed）」や「動的型付き（dynamically typed）」の型のことです。

さて、関数プログラミングとは何か？という質問に集中しましょう。関数プログラミングはパラダイムであり、以下の項目からなります：（恣意的に選びました）

関数とはなにか？（特に、再帰的定義）

データとはなにか？（特に、帰納的定義）

簡約

高階関数

型

この５つの項目が関数プログラミングというパラダイムか？という問いかけは正当です。言い足りないこともありますし、不適切なこともあるでしょう。お許しください。読者の皆様からのリアクションを待ちます。

関数を再帰的に定義すること、および、データを帰納的に定義することにより、プログラムの意味がより明確になります。何と比べているかというと、そうでない定義と比べています。

簡約 (reduction) という言葉は聞き慣れない言葉かもしれません。「わたしたちの書いたプログラムの意味はなにか一通りに定まるのか？」という問いかけに対して、簡約の概念があるので、「はい」と言えます。計算とは簡約です。

高階関数によりプログラムの抽象化が可能になり結果として簡潔なプログラムができあがります。何と比べているかというと、高階関数を用いていない場合と比べています。高階関数の概念を最初に導入したのは Backus 先生の FP だそうです（Meijer 先生から聞いた）が、高階関数による抽象化抜きに関数プログラミングを楽しむことは難しいでしょう。

型は最後の武器です。動的でも静的でもどちらでも pros/cons がありますね。型に関する沢山のことを話したいのですが、ここでは筆を置きます。

以上 5 つをもって関数プログラミングと定義しました。プログラミング言語 C でオブジェクト指向のようなプログラムを書くことは可能です。同様に（！？）、プログラミング言語 C で関数プログラミングのようなプログラムを書くことも可能です。それがよいことかどうかとは別です。関数プログラミングはパラダイムであり、たとえば実行速度とは関係ありません。

関数プログラミングに含めなかった概念を並べます：

状態

単一代入

簡約戦略

etc.

関数プログラミングをたったの 5 つの項目で定義したのですから，関数プログラミングに含まれない概念は沢山あります。

いくつかの関数型言語はデフォルトで状態が不変にするように設計されています。しかし、現実的な要求から可変な状態をつくることも可能です。同じことが単一代入についても言えます。破壊的変更可能な変数はあります。言語のデザインです。単一代入を強制すること、すなわち純粋（pure）な関数型言語は一派にすぎません。ISWIM が最初の pure functional programming language であると Meijer 先生から聞きました。簡約戦略について strict か non-strict かどうかも言語のデザインです。これらは、関数型言語の背景にある関数プログラミングというパラダイムには含まれません。

言語に固有な概念とそうでないものを分けることで、関数型言語をその視点からとらえることができます。皆様も一度考えてみてはいかがでしょうか。

関西という土壌と純粋関数型言語 Haskell （昔話）

話題を変えます。関西にかつて存在した Haskell 同好会とわたしの歴史を紹介します。年表です：

2002-02 : QuickML 0.1 公開

2003-02 : haskell-jp ML 再オープン on QuickML

2004-04 : 某 Haskell プロジェクトにいけがみが参加

2005-06 : いけがみが haskell-jp ML に参加

2005-09 : 吉田さんのメールで Haskell 同好会が立ち上がる

このたび、Haskell同好会を立ち上げました。 この同好会では普段集まる機会の少ないHaskellerと、 関西を中心に交流を深めることを目的としています。 と言ってもHaskellに精通していないと参加できないというわけではなく、 Haskellにちょっとでも興味がある方なら誰でもwelcomeです。 もちろん関西以外の方でも構いません。

2005-09 関西オープンソース 2005 に参加（吉田さんが交渉してくださる）& 第一回 Haskell 同好会

具体的な中身についてなのですが、基本的なコンセプトは 「Haskellという言語は他の言語と何が違うか」を説明するということで良いでしょうか。 おそらくHaskellについて語るときに一番最初に語りたくなるのは遅延評価だとかモナドだとかいったものでしょうし、こういった言語的な特徴から眺めてみるのが一番やりやすいのではないかと思います。

2005-11 第二回 Haskell 同好会（吉田さんによる提案）関西オープンフォーラム

まずお題を決めるのが先決です。僕（注：吉田さん）が考えたのは次の二つです * 勉強会 言語上の特徴やテクニックなどについて学ぶ つぶしが効かないので、個々のソフトの使いかた（作り方ならOK？）を学ぶというのはあまりしたくないです * 討論会 現状のHaskellの問題点や普及させるには何が必要かについてみんなで意見を出し合う

Haskellの現状の問題点を洗い出して、それを改善するには具体的にどういうことをすれば良いかというのを探るためのものです。折角多様なメンバが集まっているので日本発でHaskellに貢献できたらなぁと思っています。

2006-01 第三回 Haskell 同好会記録消失

2006-02 Haskell 合宿が提案されるも参加者が集まらず流れる…

2006-11 関西オープンフォーラム Haskell 同好会（庶務：いけがみ）

2007-06 オープンソースカンファレンス北海道 2007 に出張（担当：いけがみ）

2009-12 GHC 6.12.1 がリリース。System.IO が UTF-8 をサポートする（ターニングポイント）

2011-02 haskell-jp メーリングリストが QuickML から Google グループに移行

こうして歴史を振り返ると、Haskell 同好会にとって関西オープンフォーラムとオープンソースカンファレンスが重要な役割を果たしたことがわかります。関係者各位に感謝いたします。

歴史を掘り起こすにあたって以下のサイトにお世話になりました。ありがとうございます。

HaskellJP wiki

HaskellJP wiki ミラー

blade.nagaokaut.ac.jp haskell-jp メーリングリストアーカイブ

sampou.org haskell-jp メーリングリストアーカイブ

まとめ

『今回の勉強会は「関数型言語とはなんぞや」という考え方に重きをおこうと思いますので』という前置きに答えるべく関数型言語のわたしなりの定義を挙げました。この定義が普遍的であると考えないでください。つぎに、関西に存在した Haskell コミュニティの紹介をしました。願わくば皆様とわたしの手で復活させたいと思います。

参考にしたオンラインの資料です：

"関数プログラミングのエッセンスと考え方", 小笠原 啓, IT Planning Inc. 2012-03-05, SEA Forum in March 2012, [PDF]

"C9 Lectures: Dr. Erik Meijer -- Functional Programming Fundamentals", Chap. 1 of 13.

en.Wikipedia のいろいろは参考になったりならなかったり

この記事を書くにあたって参考にした文献をアフィリエイトします。お手元に置きたくなった人は以下のリンクを経由してください。わたしにささやかな報酬がもたらされます。ただし、これらは古書です。

[sovmoess-blog-blog]

独りカタン（対CPU）でランク一位を達成したので記録。262戦91勝というのはまだ縮む余地があって単純にやりなおせば良いのだろうけど、最終面をクリアするのに2時間くらいかかるので面倒…CPU相手に初期マップだとほとんどわたしが勝つのでつまらなくなり、騎士と古城拡張を何度もだらだらクリアしていたらいつの間にかランク一位になっていたという。騎士と古城拡張はオリジナルよりも考えることが多いし狭いマップで13点を誰が最初に取るかドキドキする展開になる。10点を取ってから13点に増やすのが簡単ではない模様。右も左もわからなかった頃はランク七位あたりをうろうろしており、一位なんてとてもとてもと思っていたのだがどうしたことか。ランク二位のHildegard女史（画像左下に映っている）は憎たらしいキャラクターで実際強い印象があるのでついに凌駕したということで感慨深いです。

[sovmoess-blog-blog]

執筆中

なにか書きます。とりあえずパーマリンクを作成する。ダッシュボードに変なものが現れますがすみません。

[sovmoess-blog-blog]

Leopard から Snow Leopard にアップデートした記録

5 月の連休のプロジェクトとして手元の MacBook Pro を Leopard から Snow Leopard にアップデートする作業を完了した。Snow Leopard が世に出たのは 2009 年 8 月末である。なぜいままで放置していたかというとバックアップを取らねばならぬと考えていたからである。バックアップを取るのはめんどくさい。しかしそれは杞憂であった。

Snow Leopard は梅田ヨドバシでは売っていなかった。曰く、 Lion が出たので Snow Leopard は売らないことにしたらしい。しかし Lion は AppStore でないと手に入れることができず、そのためには Snow Leopard が必要である。どうしろというのか。幸運なことに（今できるかどうかは知らないが）Apple Store で Snow Leopard が入手できた。このリンクがいつまでも有効であることを願うばかりである。実家の MacBook も Leopard なのだ。

当初の計画では Snow Leopard にアップデートしたあと続けざまに Lion にアップデートするはずであった。しかし「Lion の TimeMachine は AFP(Apple Filing Protocol) 3.3 を要求する」ために断念した。わたしの持っている NAS は対応していないし、NAS の netatalk のバージョンを上げる方法も面倒である（後述）。こういうとき、安物の NAS を買ってしまったことを後悔する。まだ 1TB も空いているのに下手を打てばゴミになるのだ。どうしてくれようか。

ホームディレクトリのスナップショットを取り、 /Applications/ を復元できるようにメモを取り、/Library/Fonts に溜め込んだフォント 1370 書体の出所はどこかと探しまわり、Books.app や Papers.app に登録したありとあらゆる文献リストをつくり、~/.ssh/ が確実に保存されたかびくびくし、 Web サービスのアカウント情報をかきあつめて、他にもいろいろとしたのだが、とにかく机の上は書き散らした紙でいっぱいになった。すべては無駄な行為であった。

「ふつうにインストールしたらふつうになにもかもが残った」のである（これは私の経験であり皆さんがどうなるかは知りませんよ？）。

今後 Lion にせざるをえない状況に陥ったとき NAS のファームアップデートを騙して telnet を開けて、 AFP 3.3 をサポートする netatalk を危険を覚悟でインストールするという作業時間をなんとかひねり出す必要がある。失敗する可能性を考えると面倒なことだ…

[sovmoess-blog-blog]

2012-05-04 (Fri) のことである。約束ができないとはいえ参加の意図を告げぬまま集合場所に待機するという大変失礼なことをした。やってはならぬことである。今回は特別だ。

正規の参加者が揃ってしまうと当然そのまま店に移動するので、そのようなことにならぬように待ち伏せた。さりとてこちらにも辛抱できる範疇があり 30 分前でちょうどよかろうと予測したのだが正解であった。ほとんどの参加者は集合時間よりも前に来られた、感心なことである。全員が揃ったところでぴたりと来られた主催者の末永さんにも感謝である。私は皆様に参加を許されたらしい。

3 次会までおつきあいした。楽しかった。

連休たてつづけに NPCA の活動をみたり三条大橋に突如現れるなどしたりして無理がたたり翌日はほぼ寝たきりになった。いまは回復したからいいものの危ない橋を渡るのはいけません。

[sovmoess-blog-blog]

2012年の文化祭行きました、昨日と今日の二日間。楽しかったです。ウェブに情報をあげてはいけない、というルールがあるようなので（？）直接的な表現は避けます。展示デモ・部誌・いにしえのパーツ達・ステージ発表、どれもさすがでしたすごい。来年も行きたくなります。

ぼくは萩谷昌己著『関数プログラミング』日本評論社を一日一冊住吉に運び渡しました。片方は部長に、もう片方はとある OB にあげます。この行為にはなにもヒモづけられていないので余計な心配は無用です。ただ 50 数名の NPCA 部員にさしあげられないのは残念でした。読みたい部員は部長にたかるといいよ。

部長に一冊あげたときはぼくの心持ちも軽く荷物も軽くなりよかった。逆に二冊目をとある OB にあげたときは辛い気持ちがあり渡すのに時間をかけてしまいました。「本当にいらんのか？」という問いに「いらない」と答えるのは難しい。実際、二日目は住吉に行く前に全 228 ページ丸暗記すべく朝から昼まで読んでいたくらいです。人間の未練とは。

あげました。

ぼくが読み終えた本の需要はいろいろあるようで、これで計 4 名の皆様方に「欲しいよ」という本をあげることができました。あと「欲しいよ」とは言ってないひとに圏論の本を一冊おしつけたこともあった。すまぬすまぬ。

縁とは不思議なもので友人から本をもらいうける行為は灘高 OB にして同期の M 氏が最初でした。彼は僕に木下是雄著『理科系の作文技術』中公新書をくれた。「申し訳ないよ」「読み終えたあと返してくれていいから」というやりとりをしたのを覚えています、14 年前のことです。まだ返してないし彼も返してほしいとは思っていないだろう。

院試に合格したあと勉強会で読んだ数学の演習書を後輩に全部おしつけたこともあった、これは黒歴史なので封印しています。

本の貸し借りと、さしあげてひきとる行為はだいぶ違います。未練がある本は暗記するまで読んでさしあげるということを学習しました。今後も読み終えた本を誰かにあげる行為続けようと思いますので「欲しいよ」というリクエストをください、お待ちしております。とはいえ全てのリクエストにお応えすることは無理です。このたび手をあげるのが遅かった finalfusion さん、なにかを期待している t_teruya さんは次の機会を狙ってください。

[sovmoess-blog-blog]

Element of Programming/プログラミング原論読書会参加記録

前の記事にも書いた Element of Programming/プログラミング原論読書会に参加しました。参加者のみなさんは本をひたすら読み、わからないことを誰かに質問するという形式。僕は Chap. 1 を時間内に読み通すことができたので満足です。

読書会を始めるにあたって Alex のスライドにある「剰余を求めるプログラム」の紹介をしました。スライドの 11 page です。

T remainder(T a, T b) { // Precondition: a ≧ b > 0 if (a - b >= b) { a = remainder(a, b + b); if (a < b) return a; } return a - b; } // First appears in Rhind Papyrus

ー Stanford EE Computer Systems Colloquium (2010-11-03) [PDF]

これは剰余を計算するプログラムであって剰余の定義とは異なります。つっこみどころがたくさんあるコードで、このプログラムが剰余を返すことの説明に Alex 自身も時間を割いている。僕が気になるのは以下：

このプログラムは剰余の定義に沿う計算をしているのか

再帰が止まるのは何故か

以上のことがわからないので Elements of Programming を読んでいます。ユークリッド整域の定義と、自然数における剰余の一意性の証明を忘れていたのでやり直しました。

-- mod :: Integral a => a -> a -> a が Prelude に存在することはいまは忘れる remainder m n | m < n = m | m == n = 0 | otherwise = remainder (m - n) n

この Haskell プログラムの再帰が止まりますよ、ただし \(n > 0\) にかぎる、というのはわかります。型エラーにならないので \(n \leq 0\) のときは error にしたほうがいいかな。剰余の定義に沿う計算をしているかどうかは自明ではない…

なお上記の remainder の型は決まります：

-- 再掲 remainder :: (Ord a, Num a) => a -> a -> a remainder m n | m < n = m | m == n = 0 | otherwise = remainder (m - n) n

(<) を使うので Ord a である必要があり、(-) を使うので Num a である必要があり、(==) を使うためには Eq a である必要がありますが Ord a ないし Num a から Eq a が従う ので大丈夫。

横道終わり。remainder ごとき本気で証明やりたかったら Coq でやればいいですが、プログラミング言語でカジュアルにやりたい、特に C++ でやれるならそれでいいじゃないですかと思っています。これは誰かがすでに通った道なのだろうか？Elements of Programming は答えてくれるのでしょうか（つづく）

[sovmoess-blog-blog]

Elements of Programming 予習記録

この記事は tumblr. の予約投稿システムにより 2012-04-27 (Fri) に自動的に公開されます。

Elements of Programming/プログラミング原論読書会というイベントが 2012-04-28 (Sat) に行われます。ここに予習の記録を残します。関係ないことも交じる。

経緯

@uskz ぼくも Elements of Programming 持っていて、持っているだけなので勉強会の需要はあります

— Ikegami Daisukeさん (@ikegami__) 3月 24, 2012

2012-04-22(Sun)

重い腰を上げて目次に目を通し前書きを読む。Chap. 1 が大事らしい（そりゃそうだ）。Chap. 2 -- 5 がひとまとまり、Chap. 6 -- 11 がひとまとまり、Chap. 12 でなにかがあり、あとがきがある。あやうく読み飛ばすところであったが、本書で用いる数学記号が App. A に、プログラミング言語（C++ の subset）が App. B にあるらしい。

手元に届いたときは Chap.1 で挫折した（早い）ので、その反省を活かすべく、次の順番で読むことにする：

目次

前書き

App. A

App. B

あとがき

Chap. 1

Chap. 2 -- 5 または Chap. 6 -- 11

Chap. 12

App. A の中に見慣れない数学記号 \(⟦ i, n ⦆\) を見つける。なんだこれは。意味が書いてあるけどわからない、ついでに MathJax ではサポートしていない記号だよ（2011 年時点）といわれてがっくりくる。LaTeX コンパニオンを舐めるように読んだのに。Unicode の数学記号にはありました。

Catamorphism や bananas and lenses の記号ではない、はずだー。

App. B は必要になったら読むことにするという気持ちで素通り。僕は C++ わかってない。

著者の意図に反して、あとがきから読む。これは正解だったと思う、論文の読み方と同じだ。

ここで時間切れ、1 時間の読書でした。MathJax と格闘していた時間のほうが長い。次の日に続く。

2012-04-23(Mon)

Elements of Programming 公式サイトに参考資料のスライド[PDF]と YouTube の講演ビデオへの参照があることに気がつく。約 1 時間半のビデオだ、ぼけーっと聞くのを 3 周すればいいだろうと踏む。今日は一周目。ビデオ 43:50 のあたりで Plan of the Book が紹介されることに気がつく。「Chap. 1 は飛ばしてもよい、また戻ってくればよいのだから」とか聞こえるぞ…次の日に続く。

2012-04-24(Tue)

Nothing.

2012-04-25(Wed)

Chap 2. を先に読もうとするが、Chap. 1 に現れる定義を理解せずに読み進めるのは無理であった。そこで、しかたなく Chap. 1 を読みはじめ、1.2 節まで読了。表と数式と証明のスケッチができあがる。定義には必ず具体例が伴うべきですよ？約 2 時間かけてもたかだか 3 ページしか進まない。知らない英単語が次々と現れる。幸い図書館には『大きな活字の新コンサイス英和辞典』があるから翻訳に要する時間は短くて済む、大きな活字はよい。

ついでに。図書館で飯高茂センセイの『いいたかないけど数学者なのだ』を見つけて読む。新谷卓郎センセイの読書ノートが主たる内容だった。満足。読み終えたので私の amazon wish-list からそれを削除した。鷹羽狩行様の俳句の本に目を通す。100 万ドル欲しいので『数学七つの未解決問題 -- あなたも 100 万ドルにチャレンジしよう!』を読む。これらの本はさらさら読めるのにどうして？という気持ちで一杯だ。竹内外史センセイのコラム中にでてきた Razborov and Rudich の natural proof を知る。100 万ドルの懸賞がかかっている七つの問題について著者らによる解決（？）への取り組みが書かれており良い。特に「ポアンカレ予想（予想ではなくペレルマンにより 2003 年に証明済み、100 万ドルは辞退）」をとりあげているのが興味深い。無念であり満足であろうナムサン。本書にペレルマンの証明はみあたらない。

進展。悲しい思いを抱きつつ夕飯を食べながら Alex さんの講演（前述 2012-04-23）を聞く、これで 2 周目。「この本は難しい！簡単ではない。プログラミングはワンダフルだ。Formal method は数学とプログラミングの間にある良いものだ、が、本書で取り扱うのは異なる数学である。本書は圏論を必要としない…」など、拝聴する。次の日に続く。

2012-04-26(Thu)

Nothing.

2012-04-27(Fri)

このペースでは Chap. 1 の予習を最後までやり通すことができない。締切駆動による学習が始まる。一方で、明日の集合場所に慣れていないので行動に余裕が必要である。結果として Chap.1 を終えることがなくてもいいかという気分になった。ただただ読んで考えて書くプロセス。夕食時に Alex の動画 3 周目を見る。見終えた。その後も続けて 1.3 節まで読了、見開き 1 ページを片付ける。残り 1.4 -- 1.7 節を飛ばして、1.8 節 Conclusion を読む。もう知らない、明日でかける間になんとかすればいいでしょ。

予習の記録をここに終える。なお、僕が必要としているのは手続き型プログラミングについて共通認識を持てるか否か（共通の認識とはつまり言葉として）である。たとえば GoF が必要であり必要でないということと同じであるが読者諸賢には伝わらない奇妙な日本語かもしれない、ご容赦。

[sovmoess-blog-blog]

標準純音聴力検査記録

Medical disclaimer : この文書は医学の専門家が書いたものではありません。読者の皆様、知りたいことは医者に聞きましょう。

先日、耳鼻咽喉科で「標準純音聴力検査」をうけました。結果をいただいたのでプロットします（iWork '09 の Numbers.app を使いました。横軸は対数、縦軸は dB です、注意）：

私の耳は右と左で違いがあることがわかります。25 dB が閾値であるとコメントを頂きました（このコメントの是非は責任を持てません：ja.Wikipedia の「聴力レベル」を読むと、やはり 25 dB 以下が「0-障害なし：ささやき声が聞こえる」に相当するそうです。それを決めたのは WHO の聴覚障害等級）。グラフの読み方についてですが、Y 軸（聴力レベル : dB）が小さければ小さいほど、良い結果だそうです。つまり右耳と左耳では、右耳は良く、左耳は悪いことがわかります。左耳がどれくらい悪いかというと、前述の WHO 聴覚障害等級によれば「1-軽度難聴」に相当します。「1 mの距離での普通の声で単語の聞き取り/繰り返しができる」とあります。平均聴力レベルは聴覚障害の dB 区分でいうと右耳が聴者で左耳が軽度軟聴でした。ただし、1kHz--2kHz 周波数帯は左耳も閾値を示しており、日常の生活に困ることはありません。

もし私がオーディオマニアだったら、特に低音がモノラルになるので残念だと思うのでしょう（が、実際のところ、わたしは生活音が好きですし、音楽を聴くことはまれです）。

骨導のマスキングレベルは左右ともに閾値で、安心しました。いつ悪くなるかわからんけどね…

Blindness cuts us off from things, but deafness cuts us off from people. -- Helen Keller

en.Wikiquote.org より

まとめ：

右と左の違いが現れることは、視力だけでなく聴力においても言えます

検査によって自らを知ることができます

医者に行きましょう、早期発見が大切です

[sovmoess-blog-blog]

Reading maketh a full man; conference a ready man; and writing an exact man. -- Francis Bacon

Francis Bacon Quotes by Brainy Quote.

[sovmoess-blog-blog]

HTML5 と tumblr. テーマと僕

HTML5 working draft 2012-03-29 を読んで、特に DOCTYPE 宣言について学びました。というご報告です。より詳しく情報を追いたい方は、HTML5 working draft 最新号 をチェックしてください。

きっかけ： tumblr. のこのページ（まさにあなたが見ているこのページ）のソースの一行目を見ました。

<!DOCTYPE html>

あれ？ DTD についてなにも書いていないのですがどういうことなの…

ちょっと待った、僕の知識は HTML5 より古いので、つまり、僕の疑問は僕に原因があるので、落ち着こう。はい。

invalid ではなく、valid です。DTD はすでに過去のものでした（ざわ…ざわ…）。 「Netscape で center タグ面白い」とかいう僕の頭ですので、HTML5 の規格くらいは「必要に迫られたら」読みましょう。

tumblr のテーマは、いろいろありますが、僕が選んだそれは DTD 指定する DOCTYPE 宣言が入っており、つまり DOCTYPE 宣言が二つもあるよという状況になっていますので、近日中に改めたいです（各ブラウザのためには、DOCTYPE 宣言二つあったほうがいいのかもしれませんけどね…）。

とりあえずの目標は、このサイト全体をまるっと HTML5 working draft に合致させることなのですが、そんなことする暇があれば、内容をまし（どのように？）にすべきであります。

[sovmoess-blog-blog]

数学セミナー 2012 年 5 月号にある竹内郁雄センセイのコラムがすごい件

みなさま、ぼくは今日も花見をしました。

2012-04-12 発売の『数学セミナー 2012-05』日本評論社、もう読まれましたね？ソフトウエアを書くひとは、「コンピュータは数学の応援を求む…竹内郁雄」に、一度目を通しましょう。約束だよ？

2012-04-12 発売の『数学セミナー 2012-05』日本評論社のことです。

この tumblr 文章をお読みの皆様にあてはまるタイプ：「数学は苦手」：同意します。僕も数学は苦手です。『数学セミナー』は、題の「数学」に関係する（しないこともあるけど）雑誌です。どちらかと言えば苦手な読み物でしょう？

そこで、お節介をやきます。

最初のステップとして、広告をフムフムしつつ、数学セミナーの目次を見つけてください。つぎに、竹内先生のコラムのページをお開きください。ここまでは、よろしいですね？

竹内先生のコラムは、おもしろい引用句から始まります。そして、つらつらつらと文章が進みます。次が重要です！竹内先生のコラムを最初から読まない（エッ！？）で、特に最初の見開きの 2 ページは読まない。竹内先生の高度な釣りであるところの引用句から読み始めない。

そして、

記述の科学としての数学

と副題のついたコラムから読み始めましょう。ソフトウエアを書く人へのアドバイスは以上です。Let's try.

このアドバイスに従って読み終えた方は、つぎに、残りのページをお好きなようにお読みになってください。竹内先生、こんな読み方をしてもいいですよね？竹内先生ならびに日本評論社の皆様、そして読者各位、お叱りの言葉をお待ちしております。ホントだよ。

数学徒諸君：

今月と来月の数学セミナー「圏論の歩き方」，丸山さん（オックスフォード大学計算機科学科博士課程）の渾身の双対性記事です．記事を読んで，数年間いろいろ論文やら本やらを読んで，その後もどって丸山さんの記事を読んで，それでもおもしろいであろうという戦慄の記事なのだ．

— Ichiro Hasuo (@IchiroHasuo) April 15, 2012

アヒャ！今月号だけでなく、来月号も面白いそうです。

日本評論社のリンクポリシーのために、適切な引用を tumblr できないのが残念でなりません。したがって、アマゾンアフィリエイトします。それでは、過ぎゆく春を惜しみつつ。