TAPL 読書会 第 5 回

今日は TAPL 読書会の第 5 回でした. 型の話をひたすらしてきました.

PARTAKE http://partake.in/events/9e460004-25c1-4c0b-b6a9-a2aa0443ab23

今日は余裕が無く会場に向かう電車の中でのみ予習した, という酷い状態で参加してきました. 9 章が型付き lambda 計算の話で, 今までの章の内容の組み合わせのような章だったのでなんとかその場で読めました. いつも 1 章分終わるかどうか, というペースなのですが, 今回は延長して終わらせました.

以下は kencoba さんのメモです. 話しいてる内容をその場でメモっていただいているので, 細かいとこまでメモしてあって助かります.

http://d.hatena.ne.jp/kencoba/20110409/1302330632

最後の Curry-Howard のあたりで話題に出した住井さんの記事というのは以下の IT Pro の記事です. なんと「型から実装が決まる」というめちゃくちゃ面白い話です.

http://itpro.nikkeibp.co.jp/article/COLUMN/20071005/283903/?ST=develop

言語処理系にはすごく強い興味があるのもあって読書会はすごく面白いのですが, それよりなにより型に引き寄せられる人に面白い (というかマニアックな) 人が多く, 濃いメンツが集まっていて楽しいです. 懇親会も行きたかったのですが事情により不参加. こっちの事情の方が大事ですし.

また来月にあるので, ゴールデンウィークもあることだし今度は予習をしていこうかと思います. 発表形式の方がスムーズなのは確かなんですよね. 他にも色々忙しいですが, そんなこと言わずに発表準備をしようと思います.

ライツアウトを代数的に見る (1)

みなさん, ライツアウトというゲームは知ってますか? 少し前に流行ったので知ってる人も多いでしょう. 4×4のマス目にボタンが配置されていて, ゲームの初期状態ではいくつかは光っています.

光ってるボタン:

光っていないボタン:

初期状態:

■ □ □ ■
■ ■ □ □
□ ■ ■ ■
□ □ □ □

ここで真ん中のボタンを1つ押すと次のように光り方が変化します.

□ □ □
□ □ □
□ □ □
↓
□ ■ □
■ ■ ■
□ ■ □

■ ■ □
■ ■ □
□ □ □
↓
■ □ □
□ □ ■
□ ■ □

このゲームのゴールは全てのボタンを光らせることです. (全てのボタンの光を消す, というのも考えられますが, 問題としては同じなので光る方を選びました.)

問題になるのは,

  • 初期状態だけを見てこのゲームはクリアできるのか?
  • 任意の初期状態に対してクリアする方法があるのか?

といったところです. これを数学的に扱っていきます.

線型代数の応用としてのフーリエ解析

Twitter で @siritori さんにフーリエ解析のことを語っていたら, それなりな長さになってました. ブログ1本分くらいあるんじゃないかと. ブログ記事の代わりにリンクを載せておきます.

http://togetter.com/li/109574

けっこう読んでもらっているようですね. 自分は何かを噛み砕いて人に説明するのが好きなようです. また機会があったら, こんな数学教室を開きたいと思います.

それでは.

Licenses