Arantium Maestum

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

論文メモ：The Next 700 Programming Languages

プログラミング言語 論文メモ

プログラミング言語理論の最初期の金字塔の一つ、The Next 700 Programming Languagesを読み直したので論文メモ。これは過去に何回か読み直している個人的にも非常に思い入れのある論文。論文メモ書きたいなとここ数ヶ月ずっと思っていた。

背景

The Next 700 Programming Languagesは1966年にPeter Landinが発表した論文で、LISPやALGOL（そしてラムダ計算）を下敷きに、ある種理想のプログラミング言語の雛形としてISWIM（If You See What I Meanの略）を提唱している。このISWIMは実用に耐える実装はされなかったものの、後続の関数型言語のほぼすべてに多大な影響を与えた。CやJavaがALGOL系言語なら、Scheme、ML、HaskellはISWIM系言語である。

概要

前述のとおり、論文の主眼はISWIMという高級言語「群」の解説である。

Introductionから引用すると：

Most programming languages are partly a way of expressing things in terms of other things and partly a basic set of given things. The ISWIM (If you See What I Mean) system is a byproduct of an attempt to disentangle these two aspects in some current languages.

ISWIM is an attempt at a general purpose system for describing things in terms of other things, that can be problem-oriented by appropriate choice of "primitives."

とある通り、具体的なプリミティブ（整数やら浮動小数点数やら）については言及せず、何かしらのプリミティブが用意されている前提で、どのように大きなプログラムを組み立てていくか、という部分に集中している。

ちなみに論文のタイトルは

"... today... 1,700 special programming languages used to 'communicate' in over 700 application areas." -- Computer Software Issues, an American Mathematical Association Prospectus, July 1965.

という、論文の冒頭で引用されている文から来ているようだ。つまり1965年にコンピュータが利用されていた700のドメインに対して、各ドメイン固有のプリミティブをISWIMに追加することで700の言語ができるという話らしい。

章立て

論文本体は以下のセクションに分かれている：

  1. Introduction
  2. The where-Notation
  3. Physical ISWIM and Logical ISWIM
  4. Four Levels of Abstraction
  5. Abstract ISWIM
  6. Relationship to LISP
  7. The Characteristic Equivalences of ISWIM
  8. Application and Denotation
  9. Note on Terminology
  10. Eliminating Explicit Sequencing
  11. Conclusion

追加で最後にDiscussionがある。論文自体がCommunications of the ACMに載ったようなので、その一環としてこういう「論文についてのディスカッション」の議事録も載っていたのだろうか。

詳細

各セクションを個別に見ていく。

Introduction

ISWIMとはプリミティブの集合に対しての組み合わせ方を共通要素として持つ言語族で、ドメインから独立したプログラミング言語共通のロジックの部分を摘出した定義を持つ、とLandinは主張する。特に変数や関数の定義・利用については、対象がどんなドメインであってもすべての言語で定義されていることから、共通化できるはずだ、と書いてある。

またIntroductionの最後に

ISWIM is thus part programming language and part program for research. A possible first step in the research program is 1700 doctoral theses called "A Correspondence between x and Church's λ-notation.''

とある。ここの1700の博士論文というのも、前述の"... today... 1,700 special programming languages used to 'communicate' in over 700 application areas."という文から来ている。つまり1965年に存在していたプログラミング言語をラムダ計算に対応させる研究が必要だという一種のジョークである。（ジョークというのは1700言語すべてに対して研究が必要、というポイントに関してで、特定の言語、例えばALGOLなどは実際にLandinやReynoldsによってラムダ計算との対応が研究されている）

The where-Notation

ISWIMの新規性の一つはwhere（と機能的には同一の別構文であるlet）によるローカル変数定義である。今でこそLisp、ML、Haskellなどで普通に見るletやwhere式だが、大元はISWIMである（Lispはこの時点ですでに存在していたがlet式はISWIMからの輸入）。ただしletというキーワードによる変数定義はBASICが最初。あちらは命令型らしくLET文である。

Physical ISWIM and Logical ISWIM

ALGOL60と同じく、ISWIMも本体は文字列に対する依存性のないLogical ISWIMである、が論文などで書き表すために特定の文字列に依存したPhysical ISWIMが（複数）考えられる。この論文で表示されているのはPhysical ISWIMのうちの一つであるReference ISWIMになるらしい。

この「文字列に依存」というのは不思議な気もするが、1966年というとASCIIが初めて制定された1963年から三年後、大幅な改訂を受ける1967年の一年前なので、今想像できるよりも切実なポイントなのかもしれない。

Four Levels of Abstraction

ISWIMは以下の四つの層に概念的に分かれる：

  1. Physical ISWIM
  2. Logical ISWIM
  3. Abstract ISWIM
  4. Applicative Expressions

PhysicalとLogicalの違いは前述のとおり実際に使える文字列が限定されているかどうか。Abstract ISWIMは抽象構文のレベルの概念で、Logical ISWIMのようなカッコやインデントに関するルールは捨て去られている。Applicative ExpressionはAbstract ISWIMをさらに脱糖した「ISWIMのカーネル」となる。

Applicative ExpressionsについてはLandinの1964年の論文The Mechanical Evaluation of Expressionsでより詳しく解説されている。SECD抽象機械で直接実行できるIRだ。

Abstract ISWIM

Abstract ISWIMは前述のとおり抽象構文である。以下の概念が存在する：

amessage

プログラム全体。aexpressionかadefinitionになる。

aexpression

式。変数を含むプリミティブ、関数適用、条件分岐、リスト、let/where式の五種類が定義されている。（let/where式のことをbeetと呼んでいる。"...abbreviates beta-redex"とのこと）

adefinition

定義。変数（あるいは変数のリスト）への代入、関数の定義、継続を利用したジャンプ的なprogram point、再帰的定義、複数定義、where付き定義の六種類。

Program pointが面白く、pp f(x) = x(x+1)のような形で普通の関数のように定義されるが、この関数が呼び出されると、呼び出し元のwhere式の評価がその時点で終わり、式全体の値が関数呼び出しの結果になる。whereがネストした場合どういう挙動になるのか気になるところだが、論文には説明は載っていない。

Relationship to LISP

ISWIMは1960年に出たLISPを強く意識している。LISPの持っていたラムダ計算ベースの関数型言語っぽさをより強力の押し進め汎用化したものだと言える。

Relationship to LISPのセクション冒頭を引用すると：

ISWIM can be looked on as an attempt to deliver Lisp from its eponymous commitment to lists, its reputation for hand-to-mouth storage allocation, the hardware dependent flavor of its pedagogy, its heavy bracketing, and its compromises with tradition.

とある。

  1. LISPはその名のとおりシンボリックなリスト処理が主眼な言語だった（特に1960年代では）のに対して、 ISWIMはドメインを特定しない
  2. LISPは動的なメモリ確保の頻繁さによる効率の悪さが問題視されていたが、ISWIMは（ガベージコレクションは必要とはいえ）where/letを使うことによってメモリのプリアロケーションが可能になる
  3. LISPは（特に命令型な部分について）実行機械に依存している機能が多いがISWIMは抽象機械を使うことでそのような機能を特定のマシンに依存することなく実装できる
  4. 構文がS式じゃない。where/let式の存在、中置演算子、そしてオフサイドルールによるインデントベースの記法を採用している

5番目のLISPの欠点はCompromises with traditionだとあるが、よく読むとこの点については触れられていない。

このセクションの５項目めは逆にISWIMが継承しようとしたLISPの美点である：

The most important contribution of Lisp was not in list-processing or storage allocation or in notation, but in the logical properties lying behind the notation. There ISWIM makes little improvement because, except for a few minor details, Lisp left none to make. There are two equivalent ways of stating these properties.

(a) Lisp simplified the equivalence relations that determine the extent to which pieces of program can be interchanged without affecting the outcome.

(b) Lisp brought the class of entities that are denoted by expressions a programmer can write nearer to those that arise in models of physical systems and in mathematical and logical systems.

プログラムの一部を別のコードに変換しても結果が同一であると保証される厳密な同値関係のルールが、命令の羅列であった過去の言語に比べて非常に明瞭になり、コードに出てくる式が表す対象がより数学的・論理的なモデルに近くなったのがLispの最大の功績だとLandinは考えている。

The Characteristic Equivalences of ISWIM

前述のとおり、ISWIMがLispから継承した「プログラムの部分式に基づいた同値関係が明確」という点をLandinは非常に重要視している。

その最大の理由は：

The practicability of all kinds of program-processing (optimizing, checking satisfaction of given conditions, constructing a program satisfying given conditions) depends on there being elegant equivalence rules.

つまりプログラム自体を処理対象（それが手動であれ自動的であれ）とするため、ということだ。

同値関係のルールには四つのカテゴリがある：

  1. 部分式が同値な場合、式全体に置いてどのような同値関係が成り立つか
  2. 変数・関数に関連した同値関係
  3. 特殊形（条件分岐、リスト、再帰）とそれに関連するビルトインに関する同値関係
  4. ISWIMに追加される特定ドメインのプリミティブに関する同値関係

各グループについて実際にルールを列挙している。特にグループ２に関しては「ISWIMの純粋な部分に限って」ラムダ計算の重要な結果であるChurch-Rosser Theoremが成り立つのがポイント。

Application and Denotation

既存のプログラミング言語に対して数式などがよりシンプルである構造として

  1. 式がネストした部分式の組み合わせでできていること
  2. 一つ一つの部分式が何かを意味していること（数、真偽値、関数など）
  3. ある式の意味（つまり「値」）は、その式を構成する部分式の値によって決定されること。ある部分式の「値」以外の性質には影響されないこと

が挙げられる。特にcが数式のシンプルさに大きく寄与しており、プログラムが関数型であるかについての真のテストはcを満たしているかどうかだとLandinはいう。

前述のISWIMの同値関係は、ISWIMの純粋なサブセットに関してcを満たすことを保証している。

明確な言及はないがこのセクションは表示的意味論の話になっていると思う。表示的意味論の歴史の中でこの論文がどういう位置付けになるのかは今後調べてみたい。

Note on Terminology

プログラミング言語やプログラムについて使われる用語としてprocedural, nonprocedural, algorithmic, heuristic, imperative, declarative, functional, descriptiveなどがあり用語の混乱がみられるがISWIMをベースに考えるといくつかの独立した軸が見られる、という話。ついでにISWIMを最もよく表す言葉として「denotational language」という新しい用語も提唱している。やはりdenotational semanticsとの繋がりを感じる。

Eliminating Explicit Sequencing

既存の命令型言語（ALGOLなど）でGO TOなどを排除するために単一の文や式でより大きな処理を行うようプログラムを書き換える、という「ゲーム」がよく行われていたらしい。この場合「ゲーム」というのがどういう意味を持つのかよくわからないが・・・。とにかく、ALGOLでもそのようなことがある程度は可能だったが、ISWIMはより式ベースな言語であり、かなり機械的に「命令の直線的な羅列」なプログラムを、大きな式に変換することで明示的な実行シーケンスを消すことができる。

Conclusion

ISWIMの目的はプログラミング言語を「特定ドメインでの実用上必要になる機能」から抽象化し、すべてのドメインで必要となる雛形の論理構造を明らかにすることだった。

The question arises, do the idiosyncracies reflect basic logical properties of the situations that are being catered for? Or are they accidents of history and personal background that may be obscuring fruitful developments? This question is clearly important if we are trying to predict or influence language evolution.

「今後のプログラミング言語の進化を予想・影響」というのは普通は「鬼が笑う」レベルの大袈裟な話なのだが、この論文に関しては（少なくともアカデミックなプログラミング言語研究における）現代まで連なる言語の進化の源流となっているのがすごいところだ。

余談

ISWIMは現代の静的型付き関数型言語（HaskellやML）の源流であることは間違いないのだが、それ自体は動的型付き言語である。スッキリした記述と静的型を同居させるには1970年代初頭のLCF MLで型推論が開発されるのが必要だったようだ。

前述のとお李、論文の最後にDiscussionがあるのだが、NaurやFloydが「インデントベースの構文って大変じゃない？」という話をしていて、ここ十数年でよく見たPython構文談義が1960年代にもされてたのが面白い。

またStracheyが

Nearly all the linguistic features, such as where and while and and and recursive, that Peter Landin has been talking about are incorporated as an integral part of a programming language being developed at Cambridge and London called CPL.

と言っていて非常に興味がある。CPLに関して何か文献ないかな・・・

文献で言えばこの論文のReferencesが

1 LANDIN, P. J. The mechanical evaluation of expressions. Comput. J. 6, 4 (Jan. 1964), 308-320.

2 --. A correspondence between ALGOL 60 and Church's Lambda-notation. Comm. ACM 8 (1965), 89-101; 158-165.

3 --. A formal description of ALGOL 60. In Formal Language Description Languages for Computer Programming, T. B. Steel, Jr. (Ed.), North Holland, Amsterdam, 1965.

4 --. An abstract machine for designers of computing languages. (Summary). IFIP65 Proc., Part II.

で自分の論文・記事だけなのが男らしくて笑えた。

Acknowledgementsで

The author is grateful for helpful discussions with W. H. Burge. Wider influences on the investigation of which this paper is one outcome are mentioned in [1]. Of these the main ones are the publications of Curry and of McCarthy.

と書いてあるので、より広範囲は参考文献はThe mechanical evaluation of expressionsを見てくれ、ということなのか。