論文メモ：Programming Language Semantics - It's Easy as 1,2,3
Graham HuttonのHaskellを使ったプログラミング言語意味論のチュートリアル論文Programming Language Semantics - It's Easy as 1,2,3を読んだのでメモ。
HuttonはOCamlでMonadic Parserを作ってみる（前編） - Arantium Maestumの元ネタである「Programming in Haskell」という本の著者でもある。
概要
プログラミング言語の意味論は複雑な印象がある。そもそもプログラムの意味を厳密・数学的に定義するというのが難しそう（というか何をしているのか想像がしにくい）上に、操作的意味論やら表示的意味論やらいろいろな流派があって混乱しやすい。
この論文では非常に簡単な非チューリング完全な言語を使ってそれら意味論について解説した上で、その簡単な言語がどのようにプログラミング言語研究に有用になり得るかを「この言語のための抽象機械を導出する」「この言語に例外処理を追加して、その言語のコンパイラの正しさを証明する」という事例を通して紹介している。
簡単な言語
プログラミング言語意味論だとWinskelのFormal Semantics of Programming Languagesなどが有名で、この本だとIMPという単純化された命令型言語を使って各概念を解説している。IMPは関数などもあるチューリング完全な言語で、実用的な言語に比べると簡単であることは間違いないのだが、やはりそれなりの複雑さを持つ。
それに対してHuttonの提唱する言語はBNFだと
E ::= Z | E+E
Haskellだと
data Expr = Val Integer | Add Expr Expr
つまり構成要素が整数と和だけ。
Huttonによればこれが意味論を掘り下げるのにちょうどいい簡単さだという。
重要なポイントとしては構成要素が非常に少ないのにネストでツリー構造になり得るところらしく、これが例えばE ::= Zero | Succ Eのようなペアノ数だけの言語などだと直線的な構造にしかならないという点が微妙とのこと。
逆にラムダ計算などで導入される変数・関数などは大事な概念なのだが、これらを省略した簡単な言語でも十分研究するに足る、ということがこの論文の主張したいことの一つである。
章立て
セクション章立ては以下のとおり：
- Introduction
- Arithmetic Expressions
- Denotational Semantics
- Operational Semantics
- Contextual Semantics
- Big-step Semantics
- Rule Induction
- Abstract Machines
- Adding Exceptions
- Summary and Conclusion
２〜７は様々な意味論をこの簡単な言語を通して紹介するセクション。８と９は発展的な内容で、著者がこの簡単な言語を実際の（様々な論文として過去に発表した）研究にどう使ったかを説明している。
面白かったポイント
この論文は勉強になった＆こういう「できるだけ簡略化しまくってそこから考え始める」というアプローチは個人的にすごく好みなので読んでいて楽しかった。
- セクション3と4でDenotational SemanticsがFoldに、Operational SemanticsがUnfoldにそれぞれ対応している、という話
- セクション8の言語の定義から式変換で正当性を証明しながら抽象機械を導出する流れ
- セクション9のコンパイラの正しさの証明手法
あたりが特に面白かった。また、各セクションでHutton自身が発表したこの簡単な言語を使った関連研究が参考文献として挙げられており、それらを追っていくのも楽しそうである。読んでみて面白かったらまた紹介したい。
