Arantium Maestum

プログラミング、囲碁、読書の話題

論文メモ：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のようなペアノ数だけの言語などだと直線的な構造にしかならないという点が微妙とのこと。

逆にラムダ計算などで導入される変数・関数などは大事な概念なのだが、これらを省略した簡単な言語でも十分研究するに足る、ということがこの論文の主張したいことの一つである。

章立て

セクション章立ては以下のとおり：

  1. Introduction
  2. Arithmetic Expressions
  3. Denotational Semantics
  4. Operational Semantics
  5. Contextual Semantics
  6. Big-step Semantics
  7. Rule Induction
  8. Abstract Machines
  9. Adding Exceptions
  10. Summary and Conclusion

２〜７は様々な意味論をこの簡単な言語を通して紹介するセクション。８と９は発展的な内容で、著者がこの簡単な言語を実際の（様々な論文として過去に発表した）研究にどう使ったかを説明している。

面白かったポイント

この論文は勉強になった＆こういう「できるだけ簡略化しまくってそこから考え始める」というアプローチは個人的にすごく好みなので読んでいて楽しかった。

  • セクション3と4でDenotational SemanticsがFoldに、Operational SemanticsがUnfoldにそれぞれ対応している、という話
  • セクション8の言語の定義から式変換で正当性を証明しながら抽象機械を導出する流れ
  • セクション9のコンパイラの正しさの証明手法

あたりが特に面白かった。また、各セクションでHutton自身が発表したこの簡単な言語を使った関連研究が参考文献として挙げられており、それらを追っていくのも楽しそうである。読んでみて面白かったらまた紹介したい。

プログラミング言語における再帰の初出はLISPではなかった

Lisp

ポール・グレハムの記事の一つにWhat Makes Lisp Different?というものがある：

www.paulgraham.com

ポール・グレハムらしくよく書かれていて、C言語などと比較した場合のLispの特徴をうまく捉えているように思う。

その中の一つが

  1. Recursion. Recursion existed as a mathematical concept before Lisp of course, but Lisp was the first programming language to support it. (It's arguably implicit in making functions first class objects.)

こうある通り、私も今まで深く考えたこともなく「プログラミングにおける再帰はLispが由来」と考えていたのだが、前回の記事を書くときに「そういえば再帰って本当にLispが初出？」と疑問に思ったので調べてみた。

結論から言うと違った。関数（というかコンピュータ上のサブルーチン）の再帰的定義とそれを可能とする関数スタックを持つ言語はLISPの先にあり、そしてMcCarthyはLISPを作るにあたってその言語に明確に影響を受けている。

その言語はIPL（Information Processing Language）である。

IPL

1950年代のAI研究の一環として、RAND CorpでLogic Theory Machineという定理証明系が実験的に開発されていた。そのLogic Theory Machineを実装するための言語として作られたIPLは、扱うデータ構造として数値ではなくシンボルと任意のネストが可能なリスト構造を持っていた。そして数学的な定理を形式仕様として記述できるようにするため、再帰的な定義ができるということが非常に重視されていたようだ。Programming the logic theory machineという論文で解説されている。（Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part Iの５つしかない参考文献の１つ）。

McCarthyのHistory of LISPも話はIPLから始まる。

My desire for an algebraic list processing language for artificial intelligence work on the IBM 704 computer arose in the summer of 1956 during the Dartmouth Summer Research Project on Artificial Intelligence which was the first organized study of AI. During this meeting, Newell, Shaw and Simon described IPL 2, a list processing language for Rand Corporation’s JOHNNIAC computer in which they implemented their Logic Theorist program.

ただしこのMcCarthyの論文ではIPLの機能についてはあまり触れられておらず、上記の文の続きは：

There was little temptation to copy IPL, because its form was based on a JOHNNIAC loader that happened to be available to them, and because the FORTRAN idea of writing programs algebraically was attractive.

となっている。

実際IPLのWikipediaページでも

IPL is an assembly language for manipulating lists

と書かれており、コードサンプルをみるかぎりその通りだと思う。

しかし、それにしても「リスト処理」だけではなく「再帰」「スタック」の概念がIPLからきているというのはかなり重要なポイントだと思われる。

Brief History of the Stackという論文からの孫引きになってしまうが、KnuthのThe Art of Computer Programmingに：

The programming of stacks in linked form appeared first in IPL, as stated above; the name ”stack” stems from IPL terminology (although ”pushdown list” was the more official IPL wording) and it was also independently introduced in Europe by E.W. Dijkstra.

と書いてあるとのこと。ただしサブルーチンの戻り先をスタックとして保持するというアイデアはA.M. Turingのグループが1947年に発表していたらしい。

余談だが数あるLISP関連の名著のうちの一つParadigms of Artificial Intelligence Programmingで紹介されているGeneral Problem Solverは元々IPL開発者たちによってIPLで書かれたAIプログラムである。

さてIPLはシンボリックなリスト処理に特化していて再帰や関数スタックを備えていた言語ではあったのだが、特定マシンのアセンブリに近い構文、ガベージコレクションの欠如、そして実験的実装ということでのプログラム実行効率の悪さなどの問題も多かった。

特定処理以外では「FORTRANの方が高級言語」というレベルだったようだ。McCarthyはIBM社へのコンサルタント業の一環として、FORTRANにリスト処理機能を追加した言語の実装を提言する。

FLPL

その結果IBM社内で実装されたのがFORTRAN-Compiled List Processing Language(FLPL)である。1960年に（McCarthyのLISP論文が出たのと同年）IBMからスバリそのものな論文A Fortran-Compiled List-Processing Language が出ている。

Faced with this program, Newell, Shaw, and Simon, in programming a heuristic theorem-proving system for the propositional calculus, simulated (by programming) a kind of associative memory (henceforth referred to as an NSS memory) in which lists of arbitrary length and organization could be generated by annexing registers from a common store [5].

（Newell, Shaw, SimonというのはIPLの開発者たちである）

When the present authors embarked upon their effort to simulate a geometry theorem-proving machine, it was early decided that an NSS organization of memory would best serve their purpose, and consideration was given to the translation of a Johnniac IPL for use with the IBM 704 computer. However, J. McCarthy, who was then consulting for the project, sugested that FORTRAN could be adapted to serve the same purpose. He pointed out that the nesting of functions that is allowed within the FORTRAN format makes possible the construction of elaborate information-processing subroutines with a single statement.

リスト処理機能が使えるアセンブリ言語であるIPLよりも、ネストした関数などをサポートする高級言語であるFORTRANにリスト処理を追加したほうが便利だ、とMcCarthyが提言したとある。

FLPLで個人的に特に面白かったのはこの箇所：

The following are examples of this class : XCDRF(J), XCARF(J), XCPRF(J), XCSPF(J), XCTRF(J)

Extract contents of the (decrement, address, prefix, signed prefix, tag) register of the word stored in location J.

よく見ると、最初の二つはCDRとCARだ。ちなみにCONSはそのままでは存在せず、XDWORDFとXLWORDFという関数を組み合わせて新しいCONSセルをリストの先頭に追加するようになっていたようだ。

LISPの語源がLISt Processingの略であることは有名な話だが、LISPが作られる直前に、LISP開発者のMcCarthyの提言でIBMが「List Processing」を名前に含み、CARとCDRを持つFORTRAN拡張を作っていた、というのは面白い。

ではなぜMcCarthyはFLPLを使わずLISPを作ったのか？

History of LISPによると

While expressions could be handled easily in FLPL, and it was used successfully for the Geometry program, it had neither conditional expressions nor recursion, and erasing list structure was handled explicitly by the program.

そして

At this point a new language was necessary, since it was very difficult both technically and politically to tinker with Fortran, and neither conditional expressions nor recursion could be implemented with machine language Fortran functions - not even with “functions” that modify the code that calls them. Moreover, the IBM group seemed satisfied with FLPL as it was and did not want to make the vaguely stated but obviously drastic changes required to allow conditional expressions and recursive definition. As I recall, they argued that these were unnecessary.

とある。（Conditional expressionはMcCarthyはFORTRANで関数として実装したことはあったらしいが、引数が関数に渡される前に評価されてしまうので嬉しくなかったらしい）

そういうわけで1958年にMcCarthyはMITでAI研究を始めるにあたって、それに最適な再帰や条件分岐式を持ち、リスト処理に長けた高級言語を開発する。FORTRANに似せた構文であるM式で記述された、S式で表されるシンボルとデータを扱うためのLISt Processing言語LISPである。その後M式は打ち捨てられ、S式でコードもデータも統一的に記述する形に洗練されたのはよく知られているとおり。

メインストリームへの影響

C言語などのメインストリームな言語で再帰や三項演算子があるのはALGOLで採用されたからだと思うが、ALGOLに両者を加えるべきだと最初にいったのはMcCarthyのようだ（再帰が最終的にALGOLに加えられたのはDijkstra、Wijngaarden、Naurが最後の最後にAmsterdam Plotで他の委員会メンバーに気付かれずにLanguage Reportに入れたからだが）

なのでIPL -> FLPL -> LISP -> ALGOL -> ... -> Cという流れで再帰と条件分岐式がメインストリーム言語につながっていったわけだ。

数学における再帰的定義の歴史

余談ではあるがRobert SoareのComputability and Recursionによると数学的帰納法を利用した再帰的な定義は19世紀以前から使われており、それが厳密な定義であると証明したのはデデキント（1888年）、そしてその上でペアノがペアノ数に関する定義を1889~1891の間に書き上げた、とのこと。

1930年代にゲーデル、チャーチ、クリーネ、チューリングらがPrimitive RecursiveやGeneral Recursiveといった関数の集まりと計算可能性の関連を研究していき、その結果RecursionとComputabilityが数学的論理学の用語として混同（というと強すぎるかもしれないが）され出した、という経緯があるらしい。

論文メモ：Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I

論文メモ Lisp

John McCarthyの1960年に発表された論文Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part Iのメモ。

背景

「Artificial Intelligence」という用語の名付け親であるMcCarthyが、自身が助手らと作ったLISP言語を世に出した論文である。ちなみにPart IIは存在しない。

1960年ということはFORTRANやALGOL58はすでに出ているが、CやPASCALの登場の10年以上前（Cは1972、PASCALは1970）。COBOLの言語仕様が決定されたのも1960年だ。

LISPは開発が始まったのは1958年でギリギリCOBOLより先に実装されているので、FORTRANに次いで二番目に古い現存のプログラミング言語だと呼ばれている。FORTRAN、LISP、COBOLすべて時代とともにかなり変わってきているので、正直「今でも使われている」と言っていいのか微妙な気もするが・・・

概要

一言で言うならば、数値（のみ）ではなくシンボル（およびシンボルを組み合わせたデータ構造）を数学的な再帰関数を表す式で操作する、というプログラミングの方法を提唱した画期的な論文である。

COND式と再帰によるチューリング完全な計算、λ記法による無名関数式、言語の関数が関数の操作対象であるS式で表現できると言う自己言及性、LISP自身で書かれたLISPのmetacircular evaluator、高階関数、ガベージコレクションなど後のLISP方言や関数型プログラミング言語の重要な概念が詰まっている。

またLISPの特徴であるS式はもちろん登場するのだが、プログラミング記述言語としては（実際にはすぐに消えた）M式という記法が使われている。

各セクションの見出しは以下のとおり：

  1. Introduction
  2. Functions and Function Definitions
  3. Recursive Functions of Symbolic Expressions
  4. The LISP Programming System
  5. Another Formalism for Functions of Symbolic Expressions
  6. Flowcharts and Recursion
  7. Acknowledgments

このうち３、４、５が論文の根本部分。

詳細

各セクションを個別に見ていく。（ただしIntroductionとAcknowledgementsは割愛）

2. Functions and Function Definitions

そもそもどのような関数を実行できるシステム・言語を作りたいのか？という話がされている。

サブセクションは：

  1. Partial Functions
  2. Propositional Expressions and Predicates
  3. Conditional Expressions
  4. Recursive Function Definitions
  5. Functions and Forms
  6. Expressions for Recursive Functions

aとbは比較的簡単なことしか書いていないので省略。

cのConditional ExpressionsはLISPの新規性とのこと。（ちなみにセクション２はLISP言語そのものの定義ではなく、LISPで表現したい数学的な関数の定義である）

(p1 →e1,···,pn →en)のような形の式で、→の左側pnが条件式、その条件式が評価されて真なら→の右側enが評価されて式全体の結果となる。条件式が偽なら次の条件・結果ペアに移る。結果が真な条件式がない場合は式の結果が未定義。

今なら関数型言語で完全にお馴染みだが、この時点では新しかったらしい。その頃のFORTRANを見てみると、条件式の結果によって制御が特定のラベルの飛ぶGOTO的なIF文であって、評価されて全体として結果を返すIF式ではなかったようだ。

dのRecursive Function Definitionsでは、そのIF式（というかその拡張であるCOND式）を使うと再帰的な関数定義というのが一つの式で書ける、という話。

eのFunctions and Formsで任意の数式を「引数を適用できる関数」に変換するための記法としてChurchのλ記法が導入される。

最後にfで「λ記法だと再帰的な関数が表現できない」という話が出てくる。そのため、label(a, E )という記法で「Eという式全体をaという名前に束縛、ただしEの中でaという名前が出てくる場合は再帰」という式を表すようにしてある。Yコンビネータの話はまったく出てこないのが（現代からすると）意外。

ちなみにMcCarthyの書いたHistory of Lispでは後ほどDavid ParkがYコンビネータ的な理屈でlabelはいらないという指摘をしたらしい：

D.M.R. Park pointed out that LABEL was logically unnecessary since the result could be achieved using only LAMBDA - by a construction analogous to Church’s Y-operator, albeit in a more complicated way.

3. Recursive Functions of Symbolic Expressions

このセクションで前述の数学的な関数を表現するための言語を定義していく。この論文の心臓部分。

サブセクションは以下のとおり：

  1. A Class of Symbolic Expressions
  2. Functions of S-expressions and the Expressions That Represent Them
  3. The Elementary S-functions and Predicates
  4. Recursive S-functions
  5. Representation of S-Functions by S-Expressions
  6. The Universal S-Function apply
  7. Functions with Functions as Arguments

aのA Class of Symbolic ExpressionsでS式を定義。CONSセルのネストによってリストを表現する、などのLISPERや関数型言語界隈ではお馴染みの話。

bのFunctions of S-expressions and the Expressions That Represent ThemでS式からS式への関数について解説し、それらを表現するためのメタ表現であるM式を定義。M式はcar[cons[(A · B); x]]のように表記される。

cのThe Elementary S-functions and PredicatesではS式に対する原始的な関数５つ、atom、eq、car、cdr、consを定義している。Elementaryというのはこの場合「Atomic」と同義だと思うが、すでにatomという単語を「S式の最小要素」を指すのに使っているので別の単語を使っているのだろうか。

dのRecursive S-functionsでは上記の５関数を条件分岐と再帰とで組み合わせることで定義できる関数の例を見ていく。理論的にはこれでチューリング完全になって計算可能なすべての関数が表現できる。

eのRepresentation of S-Functions by S-Expressionsでは、M式で表現されていた「S式からS式への関数」がS式で表現できる、ということを見ていく。

fのThe Universal S-Function applyでは「S式で表現された関数と引数となるS式を評価する関数」であるapplyとeval、そしてそのヘルパ関数がM式で定義されている。ここがこの論文の最も有名な箇所だろう。16ページの後半から17ページの終わりにかけてLISPのmetacircular evaluator（つまりその言語自身で書かれたインタプリタ）が定義されている。

最後のgのFunctions with Functions as Argumentsではいわゆる高階関数の話がされている。maplistやsearchなど「関数を引数にとる関数」の話だ。ちなみにTurnerのSome History of Functional Programming Languagesでは

The M-language of McCarthy (1960) is first order, as there is no provision to pass a function as argument or return a function as result.

There has been much confusion about this because McCarthy (1960) uses λ- abstraction — but in a completely different context from (Church 1941).

と書いてあるが、この「g. Functions with Functions as Arguments」の部分で：

One such function is maplist[x;f] with an S- expression argument x and an argument f that is a function from S-expressions to S-expressions. We define

maplist[x; f] = [null[x] → NIL; T → cons[f[x]; maplist[cdr[x]; f]]]

と書いてあるのでTurnerの誤解ではないだろうか？元々はM式で定義されるのはS式からS式への関数だとあるので、引数にM式の関数が取れるというのは唐突な話ではあるし、、M式自体は言語として実装されることもなくinformalな記法として使われるに留まったようなので、well-definedではないと言えばそのとおりだとは思うが・・・

4. The LISP Programming System

LISPをどうやってコンピュータ（IBM704）で実装するか。

サブセクションは：

  1. Representation of S-Expressions by List Structure.
  2. Association Lists
  3. Free-Storage List
  4. Elementary S-Functions in the Computer
  5. Representation of S-Functions by Programs
  6. Status of the LISP Programming System (February 1960)

S式は連結リストで表現できるよ、ついでにLISPでは連想リストでシンボルと他の何かを対応させるのを多用するよ、とまあ自明な話をした上で、cのFree-Storage Listではメモリのアロケーションとガベージコレクション（マーク＆スイープ）について解説している。

dのElementary S-Functions in the Computerはatom、eq、car、cdr、consの実装面ではあらかた自明だと思われるが、

“car” is a mnemonic for “contents of the address part of register.” “cdr” stands for “contents of the decrement part of register.”

というのが（LISPERの間では常識だと思うが）面白ポイント。

eのRepresentation of S-Functions by Programsについては、上記５つを組み合わせた関数の実装について。基本的に難しいのは再帰関数の部分で、これまではあまり一般的ではなかったPush-down List（Stackのこと）を使うことで「関数を表現するサブルーチンが使うレジスタの内容を安全に退避させる」という機能を実現している。

fのStatus of the LISP Programming System (February 1960)によると、論文がでた1960年の時点ですでにAPPLYはIBM 704上で実装されており、S式の評価、特定のS式で定義された関数の機械語へのコンパイル（60倍ほどの計算速度向上が見られたとのこと）、遅いながらも浮動小数点数の演算などが可能となっていたらしい。

（ちなみにIBM704はSystem 360以前なので1 byte = 6 bit、1 word = 36 bitなマシン）

5. Another Formalism for Functions of Symbolic Expressions

S式に似たL式という表現を紹介している。S式のようなネストしたリストではなく、ATOMが１文字な直線的な表現（なのでLinear Expressionの略でL式）。

S式におけるATOM、EQ、CAR、CDR、CONSなどに対応する形の関数が文字・文字列を対象として定義でき、そしてS式のそれらがL式の言語で実装できるのでS式言語はL式言語に含まれる、という主張らしい。詳しい解説がないのでちゃんと理解できているかは怪しいが、つまりL式言語の入力として「S式の文字列表現」は受け入れられるし、その上でS式言語のインタプリタをL式言語で実装できる、という話だと個人的には認識している。

この話は何が嬉しいのかはわからない・・・。

6. Flowcharts and Recursion

これまでは条件分岐や再帰を含んだ数学的な関数をどうやってコンピュータプログラムとして実行するかという話だったが、このセクションでは（非常に簡単に）任意のコンピュータプログラムをこのような数学的関数で表現できるのかという問題を見ていく。

理論的には全部チューリング完全なのだから対応しているはずだが、実際にはどう対応させるのか？というのがポイント。

コンピュータプログラムをフローチャートとして表現して、そのフローチャートが再帰関数の集まりで表現できるということを確認していく。

余談

論文の本文ではほぼ言及がないが、LISPはIPLという先行言語に影響を受けており、参考文献に「A. NEWELL AND J. C. SHAW, Programming the logic theory machine」という論文が載っているがこれがIPL言語の解説である。このIPLとFLPLというLISP前夜ともいうべき二つの言語については別途記事を書きたい。

Compiling with ContinuationsとORBITの関係

言語処理系 論文メモ

前回の記事でも紹介したOlin ShiversのT Programming Languageに関する回顧録で

It had a big influence on Andrew Appel, at Princeton, who subsequently adopted a lot of the ideas in it when he and Dave MacQueen's group at Bell Labs built the SML/NJ compiler for SML; Andrew described this in the book he subsequently wrote on that compiler, Compiling With Continuations. ... So the lineage of the CPS-as-compiler-IR thesis goes from Steele's Rabbit compiler through T's Orbit to SML/NJ.

という文章があった。

確かに時系列的にもORBITがSML/NJに影響を与えているのは想像に難くないなとは思うのだが、どれだけはっきりと影響を受けているのかが気になった。

Compiling with ContinuationではReferencesにORBITの論文が含まれてはいるものの、本文中での言及は一回のみ。例えばIntroductionなどでは一度もORBITの名前は出てこないので、CPS変換の手法の多くがORBITから来ている、というような印象は受けない。

実際のところどうなのかなーと不思議に思っていたのだが、少し探してみるとAppel & Jim名義のContinuation-Passing, Closure-Passing Styleという論文が1988年に出ていた（POPL1989に出したとは書いてあるが、採択されたのかどうか？）。

この論文には随所にORBITの名前が出てきていて、かなり影響を受けているのがわかる。

なにせOverviewの第一段落に：

Rather than hack a register allocator into the abstract stack machine, we decided to try a continuation-passing style (CPS) code generator. Kranz’s ORBIT compiler shows how CPS provides a natural context for register allocation and representation decisions.

と書いてあるくらいで：

The ORBIT compiler translates CPS into efficient machine code, making representation decisions for each function and each variable. ORBIT does an impressive set of analyses in its back end, but they’re all tangled together into a single phase. We have a series of phases, each of which re-writes and simplifies the representation of the program, culminating in a final instruction emission phase that’s never presented with complications.

とORBITを下敷きに、より綺麗なアーキテクチャにしてあることが窺える。

他にもRABBITやCAMへの言及もあり、いくつかの先行研究に影響を受けていることがわかるのだが、Overviewやベンチマークの対象などで最も頻出しているのがORBITだ。さらに謝辞にORBIT作者のDavid Kranzへの言及がある：

David Kranz made many useful suggestions about benchmarks.

というわけでSML/NJがCPS形式をIRにした上で最適化しているのがORBITの強い影響を受けてのことだというのは確かのようだ。Compiling with Continuationsではまあ先行研究への言及よりも手法の解説を優先した、ということだろう。

またこのContinuation-Passing, Closure-Passing Styleという論文はCompiling with Continuationsのさわりだけ把握したい、という場合は便利ではないだろうか。

ちなみにAppelの有名なSSA is functional programmingもORBITコンパイラの作者の一人であるKelseyのA correspondence between continuation passing style and static single assignment formを下敷きにしている。

論文メモ：ORBIT: An Optimizing Compiler for Scheme

言語処理系 論文メモ

CPS形式のコンパイラIRについて調べていてORBITというコンパイラについての話が出てきたので、1986年に出た論文ORBIT: An Optimizing Compiler for Schemeを読んでみた。

ORBITはGuy SteeleのRABBITというScheme Compilerから「CPS形式をIRとして使う」というアイデアを受け継ぎ、さらにそのIRに対して最適化を行うことでより実用的なコンパイラを目指したもの。Yale大学で研究が行われていたらしいLisp方言T Programming Languageのコンパイラとして実装された。T Programming Languageに関しては、なぜかPaul GrahamのウェブサイトにOlin Shiversの回顧録が載っている。

新規性

T言語はアカデミックなリサーチ言語に留まらず、実際にユーザのいる実用的なScheme実装だったらしい（ただしこの段階ではまだSchemeもスタンダードされていないので、「Steele & SussmanのLambda Papersに影響されたLexical ScopeなLisp」くらいの意味だが）。RABBITは完全にアカデミックな成果物（Steeleの修士研究）なので、ORBITはCPS IRを採用した初の実用的コンパイラだと言える。

ORBITコンパイラ中身の新規性としては

The new ideas in Orbit include:

  1. An extension to CPS conversion called assignment conversion that facilitates treatment of assigned variables. (See section 3.)

  2. Compact and efficient runtime data representations, the most important being those for lexical closures, which are represented in different ways depending on information gleaned from a static analysis of their use. (See sections 4 and 5.)

  3. A register allocation strategy based on trace scheduling that optimizes register usage across forks and joins (and which, because of CPS conversion, includes procedure calls). (See section 6.)

  4. An integral table-driven assembler that uses hints from the code generator to order blocks so as to min- imize the number and size of jumps. (See section 7.)

  5. A technique for defining the behavior of primitive operations in Scheme source modules rather than in the internal logic of the compiler. (See section 9.1.)

  6. Flexibility in configuring the runtime support system for user programs. (See section 9.2.)

とのこと。特に１と２は自作言語を作る上でも参考になりそう（３以降は少しマニアックというかプロダクト感が強い印象）

コンパイラのフェーズ

ORBITによるコンパイルは９つのフェーズを通る：

  1. α変換
  2. CPS変換
  3. 代入変換
  4. 最適化
  5. 関数宣言の追加
  6. クロージャのアロケーション戦略決定
  7. クロージャのデータ表現決定
  8. コード作成
  9. アセンブル

１、２は最近ブログでも書いたので割愛。

３の代入変換（Assignment Conversion）というのはSchemeの変数がset!で破壊的代入可能なのだが、その対象となる変数に関しては値をMLでいうところのrefつまり明示的にミュータブルなcellに変換してしまう、というコンパイラ・パス。Schemeが裏でMLみたいになっている、というのはなかなか面白い。

5、８、９は面白いことが書いてあるのだが割愛。最適化とクロージャに関する決定について見ていく。

最適化

フェーズ４の最適化に関しては以下の８つが行われている：

1 ((lambda () body)) => body

無名な０引数関数を定義し、即呼び出している場合はクロージャを作成せずに関数本体の式をそのまま評価するような形にする。

2 ((lambda (x) (. . . x . . . ) y) => (. . . y . . . ) if x is referenced only once or if it appears that the reduced cost of accessing y offsets the increase in code size that results from duplicating Y.

いわゆるβ簡約。

3 Constant folding of primitive operations, including conditionals.

定数畳み込み。

4 Substituting values that are defined in this module or in another module whose declaration file (see section 3.6) is being used in the compilation

これは定数畳み込みに近いものだろうか？

5 Removing unused arguments to procedures.

CPS変換をしているので関数の引数は副作用がないことが保証されている。なので使われない仮引数は消されても大丈夫（実引数の評価時に副作用がある場合、CPS変換で引数じゃなくても副作用が起こるように変換されている）

6 Removing side-effect free calls whose results are not used.

これはまあ当然。こんなコードが本当にコンパイラに渡されるのだろうか？CPS変換などの経緯でそういう無駄なコードが作成されるのだろうか。

7 Various optimizations specific to primitive operations, involving multiple value returns, mutually recursive definitions, etc.

多値の扱いなど、このブログ記事では詳細には立ち入らないが論文に書いてある詳細（3.5 Other Transformationsの部分）がなかなか面白い。CPS変換していることで、関数のリターンは別の関数（継続）の末尾呼び出しになるわけで、タプルなどのデータ構造を使わず直接「二つ以上の値を関数から返す」ということが表現できるようになる。

8 Transformations of conditional expressions to effect “boolean short-circuiting;”

ネストしたif式はいろいろと変換が可能らしい。

The organization and simplicity that CPS and assignment conversion bring to the intermediate code allows a few fairly simple transformations such as these to produce highly optimized code.

というわけでCPS形式は最適化しやすい、とのこと。コードのプリミティブの少なさと、複雑な式が現われる箇所に対する厳しい制約のおかげで、少数かつ簡単な最適化が効きやすい、というのがメリットのようだ。

Closure Strategy/Representation Analysis

クロージャ（主に関数内の自由変数によって捕捉される「環境」）をヒープ・スタック・レジスタのどこで表現するかはコンパイラが決定する。関数がどこで使用されるか（あるいはどこで使われるかがある程度予測可能かどうか）が静的に解析され、それを元にレジスタに置けるか、それがダメならスタック、それがダメならヒープ、とクロージャの置かれる領域が決定される。

またRepresentation Analysisとしては、同じ（あるいは重なり合っている）環境を共有する関数らをクロージャ化する場合には同一のストラクチャにまとめてしまうことで環境部分の重複を避ける、Closure Hoistingという手法が使われる。

それ以外

レジスタの割り当てやコード作成、アセンブルなどに関してもいろいろ工夫があるようで論文では結構詳しく書かれている。ここでは割愛。

その後

主著者のDavid Kranzはこの研究をそのまま書き上げて博士論文にしたらしい。同じ題名「ORBIT: An Optimizing Compiler for Scheme」をつけたようだ。残念ながらこちらは軽く検索した範囲ではネット上に見つからなかった。

CPSをIRとして使ったコンパイル手法はORBIT/T Programming Languageの後、Appel他のSML of New Jerseyにも使われており、Appelはその経験をベースにCompiling with Continuationsという本を書いている。そこからANFが出てきて云々、という話は以前ブログに書いた通り。

そろそろCompiling with Continuationsを実装しながら読むべきかもしれない。

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む（後編）

型理論 論文メモ

前回はSubstitution関連で少し寄り道したが、今回こそはPrincipal Type Schemes for Functional Programsの中核である

  • type inference
  • Robinson's unification algorithm
  • algorithm W

の話。

type inference

For assumptions A, expressions e and type-scheme σ we write

A ⊢ e:σ

if this instance may be derived from ... inference rules

以前でたAssertionにおけるA |= e:σと、今回の型推論のA ⊢ e:σの違いについては、前者が「式を評価した結果（つまり値）の型についての主張」なのに対して、後者は「式から静的に（実行することなく）導き出される型についての主張」なのがポイント。

しかし

Proposition1 (Soundness of inference). If A ⊢ e:σ then A |= e:σ.

とあり、型推論の結果は、プログラムの実行・評価の結果と一致することが証明できる。

型推論の規則は６つ：

  • TAUT （式変数の型）
  • INST （全称量化のインスタンス化）
  • GEN （自由型変数の全称量化）
  • COMB （関数適用）
  • ABS （関数）
  • LET （LET）

個人的に重要だと思えるポイントは二点。

まず、この型推論の規則はアルゴリズムではない、という点。型推論を自動的にしようと思ったら、現在の式を推論規則の下部にマッチさせて、規則の上部の式を推論していく、という流れになる。しかしINSTとABS規則に関しては一意に上部の式が決まらない。INSTに関しては「型のどの部分を全称量化のインスタンスとみなすか」ということがわからないし、ABSに関しては引数の型がわからない。型推論を自動で行うアルゴリズムには、ここら辺をうまく埋めるような追加の処理が必要になる。

もう一つのポイントはHindley Milner型推論の最大の特長であるLetによるポリモーフィズムの導入。ABSとLET規則の対比に注目するとわかりやすい：

ABSの規則：

A_x ∪ {x:τ′} ⊢ e:τ
------------------
A ⊢ (λx.e):τ′ →τ

LETの規則：

A ⊢ e:σ        A_x ∪ {x:σ} ⊢ e′:τ
---------------------------------
A ⊢ (let x = e in e′):τ

まずABSのA_x ∪ {x:τ′}とLETのA_x ∪ {x:σ}の違いが重要で、ABSは引数部分がtype、LETは変数がtype schemeとして型付けされている。typeとtype schemeの違いは全称量化子が出てこれるかどうかなので、LETの場合のみ導入される変数が多相な型として推論され得ることがわかる。

そしてなぜLETではそのような推論が可能でABSでは無理か、というとLETの場合は上部に追加でA ⊢ e:σがあり、変数のtype schemeはそこから来ている、ということがポイントになっている。ABSの場合は引数の型はどうにかして関数のボディの方から推論しなくてはいけないのに対して、LETではlet x = e in e'のeの式に対して型推論して、そのtype schemeを使えばいい。

Robinson's Unification

次に必要になるのは、型変数を含むかもしれない二つの型がunifyできるか（型変数への任意の代入で同一の型にできるか）を調べ、unifyできるとしたらその型変数の変換を表すSubstitutionを返すUnificationアルゴリズム：

... we require the unification algorithm of Robinson [6].

Proposition 3 (Robinson). There is an algorithm U which, given a pair of types, either returns a substitution V or fails; further

(i) If U(τ,τ′) returns V , then V unifies τ and τ′, i.e. V τ = τ′.

(ii) If S unifies τ and τ′ then U(τ, τ′) returns some V and there is another substitution R such that S = R V.

Moreover, V involves only variables in τ and τ′.

Unificationの対象になるのはtype schemeではなくtypeであることに注意。

実はPrincipal Type Schemes for Functional Programsではアルゴリズムの詳細が出てこない・・・　Robinsonの元の論文は1965年のA Machine-Oriented Logic Based on the Resolution Principleのようで、効率が非常に悪いのでその後の研究で出たMartelliとMontanariのAn Efficient Unification Algorithmなどで代用されるのが普通のようだ。

型推論を実装したい場合、Unification部分はこの論文以外から持ってくる（あるいは自前で実装する）必要がある。

Unificationの条件で気になるのはこの部分：

(i) If U(τ,τ′) returns V , then V unifies τ and τ′, i.e. V τ = τ′.

これだと(α_1 -> int)と(int -> α_2)がunifyできないように見える。というのはSubstitutionは必ず型変数から型への変換なので、V τ = τ′のような片方のみへの適用だと片方の型変数はintにできるが、もう片方の型変数は残ったまま、かつintを型変数に変換することはできない、というわけでunificationが失敗してしまう。正しくはV τ = V τ′ではないか？

ちなみに前回悩んでいたSubstitutionにSubstitutionを適用する話だが、Unificationの条件２を見ると：

(ii) If S unifies τ and τ′ then U(τ, τ′) returns some V and there is another substitution R such that S = R V.

となっていて、例えばVが[int/α_1]でSが[int/α_1, int/α_2]だった場合[int/α_1, int/α_2] = [R int/α_1]というのは如何なるRでも成り立たない。なのでSubstitutionにSubstitutionを適用するのはS = R ++ [R τ_i/α_i]が正しいはず。

Algorithm W

ついにアルゴリズムWについて。

まず、何をするアルゴリズムかというと：

Given A and e, if W succeeds it finds a substitution S and a type τ, which are most general in a sense to be made precise below, such that S A ⊢ e:τ.

アルゴリズムの内容は、式の形に対するパターンマッチだ。この記事ではパターンマッチの項目ごとにOCamlの擬似コードを書いていく。

ちなみに：

There are obvious typographic errors in parts (ii) and (iv) which are in the original publication. I have left the correction of these as an easy exercise for the reader.

とのことなので、擬似コードの方は（多分正しく？）修正してある。

まずは冒頭：

W (A,e) = (S,τ) where

let rec w assumptions expr = match expr with

式が変数の場合：

(i) If e is x and there is an assumption x:∀α1,...,αnτ′ in A then S = Id and τ=[βi/αi]τ′ where the βis are new.

| Var x -> (match find x assumptions with
  | Some (generic_vars, ty) ->
    let new_vars = make_new_vars (List.length generic_vars) in
    let ty = substitute_type (List.combine generic_vars new_vars) ty in
    ([], ty)
  | None -> failwith "Variable not found in assumptions")

式が関数適用の場合：

(ii) If e is e1 e2 then let W(A,e2)=(S1,τ2) and W(S1 A, e2)=(S2,τ2) and U(S2 τ1, τ2→ β)=V where β is new; then S=V S2 S1 and τ=Vβ.

| Call(e1, e2) ->
  (let s1, ty1 = w assumptions e1 in
   let s2, ty2 = w (substitute_assumptions s1 assumptions) e2 in
   let beta = make_new_var () in
   let v = unify (substitute_type s2 ty1) (TyAbs(ty2, beta)) in
   ((merge_substitution v (merge_substitution s2 s1)), (substitute_type v beta)))

式が関数の場合：

(iii) If e is λx.e1 then let β be a new type variable and W(Ax∪{x:β},e1)=(S1,τ1); then S=S1 and τ=S1β→τ1.

| Lambda(var1, e1) ->
  let beta = make_new_var () in
  let s1, ty1 = w ((var1, beta) :: (remove var1 assumptions)) e1 in
  (s1, TyAbs(substitute_type s1 beta, ty1))

let式の場合：

(iv) If e is let x = e1 in e2 then let W(A,e1)=(S1,τ2) and W(S1Ax∪{x:S1A(τ1)},e2)= (S2,τ2); then S = S2 S1 and τ = τ2.

（注：{x:S1A(τ1)}は正しく表示されないが、論文の中ではS1Aの上に横線があり、closure of τ1 in S1 Aである）

| Let(var1, e1, e2) ->
  let s1, ty1 = w assumptions e1 in
  let s2, ty2 = w ((var1, (closure (substitute_assumptions s1 assumptions) ty1)) :: (substitute_assumptions s1 (remove var1 assumptions))) e2 in
  (merge_substitution s2 s1, ty2)

パターンマッチに合致しないケース：

NOTE: When any of the conditions above is not met W fails.

| _ -> failwith "Failed to match patterns for algorithm W"

Unificationの内容はまだはっきりしないが、それ以外の部分は論文に従うだけで比較的簡単に実装できそう。（まだsubtitute_Xやclosureなどのヘルパ関数は実装できていないが、これらはそう難しくないはず）

Principal type scheme

ちなみにタイトルにもある通り、この論文の主眼は「プログラムのprincipal type schemeを推論したい」というもの。

そもそもprincipal type schemeとは何か？

Given A and e, we will call σp a principal type-scheme of e under assumptions A iff

(i) A ⊢ e:σp

(ii) Any other σ for which A ⊢ e:σ is a generic instance of σp.

要約するとA ⊢ e:σpを満たすもっともジェネリックなtype scheme、ということになる。

アルゴリズムWはprincipal type schemeを推論する、というのが重要な結果：

Our main result, restricted to the simple case where A contains no free type variables, may be stated as follows:

If A ⊢ e :σ for some σ, then W computes a principal type scheme for e under A.

ちなみに証明はこの論文には載っておらず、

The detailed proofs of results in this paper, and related results, will appear in the first author’s forthcoming Ph.D. Thesis.

とのこと。まあ実装する分にはそこまで重要ではないとも言える。

まとめ

というわけで主要な概念とアルゴリズムWの実装の大筋がわかった。Unificationについては別の記事で実装も含めて見ていきたいと考えているが、それ以外では自作言語に型推論をつけるための最低限の道具立ては整ったはずなので楽しみ。

Algorithm W実装のためにPrincipal Type Schemes for Functional Programsを読む（中編）

型理論 論文メモ

前回「type inference、Robinson's unification, algorithm Wを見ていく」と書いたが、その前にsubstitutionについてつらつらと考えてみたい。

S is a substitution of types for type variables, often written [τ_1/α_1,...,τ_n/α_n] or [τ_i/α_i]

とある通り、substitutionは型変数から型へのマッピングだ。typeはτ ::= α | ι | τ → τなので、自由な型変数が出てくることも可能。極論すれば[α_1/α_1]のようなsubstitutionも定義上は可能だし、[α_1/α_2, α_2/α_1]のようなsubstitutionもあり得る。

後者のようなsubstitutionだと、適用する順序が結果を変える可能性があるか？とも思ったのだが

If S is a substitution of types for type variables ..., and σ is a type-scheme, then Sσ is the type-scheme obtained by replacing each free occurrence of α_i in σ by τ_i

とある。字義通りに読むならeach free occurrence of α_i in [τ_1/α_1,...,τ_(i-1)/α_(i-1)]σではないので、順番は関係なさそう。

つまり[α_1/α_2, α_2/α_1](α_1 -> α_2)は(α_2 -> α_1)になるはず。

次に

S = RV

の解釈について考えたい。（S, R, Vはすべてsubstitution）

substitutionなので最終的にはtype schemeに適用するわけだ。つまりRVσのような形になる。

ここで「まずσ'=Vσと適用して、Rσ'を返す」という処理はあり得るだろうか？

S = RVと論文に出てくるので、RVは一つのsubstitutionとして表せるはず。

一番簡単な表し方は単に二つのsubstitutionをappendすることだが、そうするともしVの型の中にRでsubstituteされる型変数が含まれている場合、「まずσ'=Vσと適用して、Rσ'を返す」という結果にはならない。

なのでV=[τ_i/α_i]とすればV'=[R τ_i/α_i]とVの型にRを適用した新しいsubstitution V'を用意した上で、SはRとV'のconcatenationという形になるはず。

もう一つの解釈としてはS=V'そのまま。Substitutionとしてはむしろこれが素直な解釈か？ただし、Rの型変数がその後適用されるσに出てきてもsubstituteされないということになるが・・・

まとめると

V = [τ_i/α_i]

だとして

S = RV

の解釈としては

S = R ++ V
S = [R τ_i/α_i]
S = R ++ [R τ_i/α_i]

の三通りが考えられ、後者二つが最もあり得そう。素直なのは二番目、一番汎用性がありそうなのは三番目。Principal Type Schemes for Functional Programsでどちらが使われる想定なのかはAlgorithm Wの詳細を見ていけばわかるはず（そうだといいなぁ）。

というわけで次こそはtype inference、Robinson's unification、そしてalgorithm Wの詳細の話。