眠気と戦う日々

眠気と戦いながらいろいろと書くブログ

TAPL読書会@名古屋# 1に参加しました

ちょっとした前置き

TaPL? TAPL? どっちなんでしょう。 ということで8月2日に開催されたTAPL読書会@名古屋#1に参加しました。 短歌会館というところの和室を借りて行いました。非常に雰囲気の良い所でしたので、お勧めです。 ただし無線LANとかはないので注意しましょう。

当日のメモ

3章. 型なし算術式

プログラミング言語を定義するための定義とかが書かれている章。

3-2

プログラミング言語の経験からニュアンスでBNFモドキを理解してきたが、これを数学的に見ていく。
succ trueとかの怪しげなものを定義可能。これについては後で言及がある。
ここで重要なのは「{true, false, 0} ∈ T」での「T」は「構文的に有効な項をすべて含む集合」。
「明らか」という単語は使ってはいけない。

3-4

プログラムを「どう評価するか」 -> 意味論

  • 操作的意味論(TaPLではこれ)
  • 表示的意味論
  • 公理的意味論

「どちらかというと意味論ではなく意味定義だよね」

3-5

まずは真偽値だけで考える。 -> 図3-1参照
vは評価の最終結果となり得るtの部分集合。
27ページで示されていることについて、導出は1パターンしか存在しないことが証明できる。
正規形: これ以上評価できない項。値。
多ステップ評価: t -> t'を何回も繰り返すのをt -> *t'

個人的感想

多少駆け足気味でしたが、mzpさんを始めとする講師役の方々の説明が非常にわかりやすかったため、なんとかついていくことが出来ました。
プログラムの評価とか、数学的に見た時の考え方とかその辺をやったのが初めての経験で、非常に面白かったですね。
4章をちらっと見た感じだと、次からはプログラミング言語を見ていくようなので、そちらも楽しみです。

謝辞

企画、及び進行をしてくださったmzpさん、ありがとうございました!
隣でわからないことについて逐一教えてくださったよんたさん、ありがとうございました!

各種リンク

TAPL読書会@名古屋 #1 - TAPL読書会@名古屋 | Doorkeeper

mzpさんの真偽値のみの言語における決定性の証明コード(Coq)