おがさわらなるひこのオープンソースとかプログラミングとか印刷技術とか

おがさわらなるひこ @naru0ga が技術系で興味を持ったりなんだりしたことをたまーに書くブログです。最近はてなダイアリー放置しすぎて記事書くたびにはてな記法忘れるのではてなブログに移行しました。

クリエイティブ・コモンズ・ライセンス
特に断りがない場合は、本ブログの筆者によるコンテンツは クリエイティブ・コモンズ 表示 - 継承 4.0 国際 ライセンスの下に提供されています。

プログラミング言語意味論読書会 第1回 実施編

前回のエントリ d:id:naruoga:20090429:1241023562 で書いたことの続き。

まあそんなわけではじめることにしたんですが、まずは雑駁な感想から。

  • よかったこと
    • むちゃくちゃ面白かった。この面白さについては後ほど。
    • なんとなく今後の方向性が見えてきた気がする。
    • 次回開催時に、どんな内容をやるか、って話がある程度できそうな気がするので、メンバーが増やせるかもしれない
  • 反省点
    • いくら「ぐちゃぐちゃいわずにまずやってみる」が目標だったとはいえ、開口一番「さて、今日はどう進めましょうか?」はないだろ>オレ
    • 電源と可能ならば無線LANはやっぱり欲しかったなぁ。
    • 学習辞典じゃなくてまともな辞書が欲しい。英和と英英両方あった方がいいかも。
    • 今回は二人だからなんとかなったけど、情報を共有できる手段が欲しい。仮訳を置いたりとかね。はてなグループかなんかでやればいいのかし?
    • 手書きしたい。百均でホワイトボード買って持っていけばよかった。

できたこと

まあ2時間半ほど額を付き合わせて、こんな感じで進めていきました。

  • Preface をざっと見て(訳さない)この本の目的を探る
  • 目次を大雑把に舐めて、議論がどんな風に進むのかをおさえる
    • 全部は訳してないけど、最初にまずばーんと前提を定義して、後半は具体的になっていくからちょっと簡単になるかなーなんて想像しました。Part だけ一覧で書くとこんな感じ。

I Judgements and Rules (判断?と規則)
II Basic Semantics (基本的意味論)
III Static and Dynamic Semantics
IV Function Types
V Finite Data Types
VII Dynamic Types
VIII Variable Types
IX Control Flow
X Types and Propositions
XI Subtyping (派生型のこと?)
XII State
XIII Modalities
XIV Laziness
XV Parallelism (これは APL 的な平行性?)
XVI Concurrency (こっちは並列ですよね)
XVIII Equivalence (同値性)

  • で、眺めていくと Part I "Judgements and Rules" がどうも肝っぽい (Part II 以降は抽象度が下がってわかりやすくなるっぽい) ので、逐語訳になることを恐れずに見ていこうじゃないかと。
    • んで 1. Inductive Definitions (帰納的定義、でいいのかな) の 1.1 Objects and Judgements を見て絶句。ちょっと引用すると、
n nat       n is a natural number (n は自然数)
n = n1 + n2 n is the sum of n1 and n2 (n は n1 と n2 の和)
a ast       a is an abstract syntax tree (a は抽象構文木)
τ type      τ is a type (τ は型である)
e:τ         expression e has type τ (式 e の型は τ である)
e⇓v         expression e has value v (式 e の値は v である)

これが全部 Judgement だっていうんだから目が点。少なくとも「判断」とかそういうものじゃないだろうと。

    • そこで頭を付き合わせて悩む悩む。味噌はたぶん「意志」なんじゃないのか。つまり「オレはここでは n は自然数だとするよ」みたいな。プログラミングの世界だから、自然とそうあるってのはなくて、全部プログラマがなにか意図して記述するじゃない?
    • ということで出てきた訳語が「表明」。もしかしたら数学の分野だと定訳あるのかもしれないけど、ひとまずこれでいこう。
      • ということで現時点では Judgement(表明) というのは「オブジェクト*1の属性またはオブジェクト間の関連の宣言」であろうと理解。
      • もひとつ Judgement Form(表明形式) って概念があって、これは Judgement で表明されている属性または関連そのもののことを指す、と。
    • 次の一文がまた意味がとりにくかったけどたぶんこんな感じ。

ある Judgement Form に対しての Judgement を instance
この Judgement Form を predicate
これらで言及されるオブジェクトを subject と呼ぶ

    • その後「この章は入り口だから簡易記法を採用するけど、より詳細な記述は後で出てくるからね」とかいう投げやりな記述があって 1.1 節おしまい。

結局この日はここまででタイムアップ。ページにして1ページと1/4ぐらい。このペースでやってると500回必要なのか? と思うけど、語彙が増えてくるからそんなことはないでしょう。多分。だといいな。

何が面白いの?

非常に口では説明しにくいのですが(いや指で説明してるわけですが)、上の Judgement のところの読み解きとかはすごいエキサイティングだったわけですよ。

パートナーの tsuyoshikawa さんは多分英語そのものはオイラより達者です。彼は勉強の筋がよくて、語源主義なんですよね。たとえば Judgement って言葉を単純に辞書引いて納得するんじゃなくて、語源から突き詰めてくタイプ。彼のそういうところは武器になりました。

一方オイラは如何に語威力がないところで英文を読むかってタイプなので、自己弁護だけどいいバランスだっかと思います。

でもぶっちゃけTOEIC900点とか英語一読してすらすら意味がとれるタイプじゃないし、数学的素養はふたりともそれほどない。いわば切れ味が微妙なナタを腰にぶらさげて二人きりで地図も持たずにジャングルに入っていくようなもんです。

その状況下で Judgement って言葉でこの著者が何を言おうとしているのか、instance とか predicate とか subject とか何をいってるのか、そういうのが分かってきて、ああ、この本は今後こういう風な論理展開をしようとしてるんだ、ってのが見えてきたときは、目の前の蔦を必死にナタで払っていたらぱっと高台に出て先の展望が少し見えたような感じがしました。すごい快感だった。すごい頭使ったから知恵熱出そうだったけどそれでも快感だった。


こんな言葉でオイラの感じた快感が伝わるかどうか分からないんだけど、教官してくれる人がいたら次回イベントに参加してくれるとうれしかったりします。
あー、今から楽しみ♪

*1:無論オブジェクト指向でいうオブジェクトとは異なります。