名残

プレゼント・デイ　プレゼント・タイム

言語処理系周りの用語とコンパイラの構造

言語処理系

これからは、自分が興味を持った技術とか理論に関して書き散らしていくつもり。
おそらく当面は ↓ の本を読んだ感想とか言語処理系の開発進捗について載せていく

今日は「コンパイラの構成と最適化」を読み進めたので、その要約を書く

１章「はじめに」

言語処理系周辺の用語の定義

1. コンパイラ

高級言語で書かれたプログラムを、機械向き言語 (計算機での実行に適した言語) のプログラムに翻訳するためのプログラム

2. 変換系

ある言語 (原始言語) で書かれた (原始) プログラムを他の言語 (目的言語) の (目的) プログラムに変換するためのプログラム

3. インタプリタ (翻訳系)

高級言語に都合よく設計された VM の言語 (中間言語) に変換して、それを解釈実行するプログラム

計算機が特定のプログラム言語に対して設計されているわけではなく、高級言語で書かれたプログラムを機械語のプログラムに直接変換するのは難しいことが多いため、よく用いられる

利点：コンパイラ / インタプリタの開発が比較的容易

欠点：目的プログラムの実行速度が遅い

4. 前処理系

原始プログラムのレベルで前処理的な変換を行う変換系

5. (言語)処理系

原始プログラムのコンパイルから実行までに必要なすべてのシステムを合わせたもの

関係性の図式化

↓ こんな感じ

２章「コンパイラの簡単な例」

コンパイラの論理的構造/物理的構造について説明されていた。
式の構文解析を理解するための準備としてスタックの原理と後置記法、操車場アルゴリズムが解説されていたがググればすぐわかるので言及しない。

コンパイラの論理的構造

1. 字句解析

(入力: 原始プログラムの文字列, 出力: 解析結果を表すトークン列)

原始プログラムのソースコードを先頭から１字１字調べながら、プログラムの基本要素であるトークンを切り出していく

2. 構文解析

(入力: トークン列, 出力: AST (抽象構文木))

プログラムのどの部分がどの文法規則に対応するかを解析し、文法的に正しければその構造を反映した木構造データである AST を出力する

3. 中間語生成

(入力: AST, 出力: 中間語)

AST をそのまま中間語とすることもあるが、より目的コードに近い形として AST の構成要素を実行順に整列したものを中間語とすることもある。複数の中間語を用いるコンパイラもある

中間語の例：RTL (Register Transfer Language)
レジスタとのデータのやり取りを手続き的に記述する中間表現 (intermediate representation) で、GCC でも実際に使われているらしい。すごい

※ これを構文解析と同時に行うコンパイラも存在している

4. 最適化

(入出力: 中間語)

目的プログラムを、実行効率のよいものにする

中間語の列の中で無駄なものを省いたり、順序を入れ替えたりして、より効率のいい目的プログラムを吐き出せるようにする

最適化のタイミングは様々：

  • 構文解析の直後
  • 中間語の生成直後
  • 目的コードへの変換直後

5. コード生成

(入力: 中間語, 出力: 目的プログラム)

機械語の目的プログラムを生成し、ファイルに出力する

主ルーチンからサブルーチンまで、そのプログラムの実行に必要なプログラムをまとめて一度にコンパイルする場合は、コード生成完了後にすぐ実行することができる

C や Fortran などのように、主ルーチンやサブルーチンを別々にコンパイルする場合は、目的プログラムは別々のファイルに出力される。それらを結合して実行可能ファイルを出力するには、リンカやリンケージエディタが必要になる

コンパイラの物理的構造

相 (Phase)

コンパイラの論理的構造の各段階を指す

パス (Pass)

言語処理系のなかで、１つの言語の変換を担当するルーチン群

例えば字句解析と構文解析が異なるルーチンに分離され、ソース全体をトークン列に変換したものを字句解析ルーチンから構文解析ルーチンに渡す構成の場合、ここには２つのパスが存在していることになる

構文解析ルーチンが先行して呼び出され、サブルーチンとして適宜字句解析ルーチンが呼び出される構成の場合、１つのパスにまとまっていることになる

１パスコンパイラ

論理的構造のすべてを１パスにまとめてしまう実装

中心的役割を担うのは構文解析ルーチンで、通常は最適化の相がない

コンパイル時間が短いのでデバッグ時には都合がいい

マルチパスコンパイラ

複数のパスに分かれた実装

複数の原始言語に対応するには「字句解析」〜「中間語生成」のパス (フロントエンド) を原始言語ごとに開発して、以降のパス (バックエンド) は共通化すればいい

さらに複数の目的言語に対応するには「コード生成」のパスだけを目的言語ごとに開発すればいい (この場合「コード生成」のみがバックエンドに属する)

特に最適化のためのパスを持ったものを「最適化コンパイラ」と呼ぶ

最適化の効果を高めるためには各種の解析が必要になるので、そのためにパスをさらに複数に分割することも多い

なお中間言語を実際のマシンに依存しない形にすれば、その最適化のパスは共通化できる

複数のパスに分ける他の理由

  • メモリの節約 (昔のコンパイラはメモリ不足になるのを防ぐためにパスを分けてたらしい)
  • 言語仕様 (例えば飛越し命令を含む目的プログラムを吐き出すのが厄介だったりするらしい)

雑なまとめ

今回はまぁ言語処理系・コンパイラに関しての基本的な概念を整理する感じだったので「それはそう、大事」って感想しかない

これからは具体的な字句解析・構文解析の理論や実装に触れていく予定

あと今まさに開発している、自作言語「Psyche (プシュケ)」を wasm に変換するコンパイラについての話も絡めながら進めて行けたらいいなぁ、なんて考えている

おしまい

操作的意味論とか数理論理学とか Coq とか

TL;DR

  • いろんな本を使って操作的意味論と数理論理学を学び始めた
  • MBP にインスコした CoqIde で Coq を書き始めた
  • #100DaysOfCS を始めた

はじめに

先日、大学の図書館でいろいろと本を借りてきました。

操作的意味論や数理論理学を学んで、プログラミング言語についての理解を深めることが目的です。
今回は上で太文字にしてある２冊を扱いますが、他の本についても、また別の記事で言及したいと思います。

操作的意味論について

CoPL を使って学んでいます。操作的意味論は、プログラムをどのように操作・計算して実行結果を得るか、という視点からの「意味の与え方の体系」です。プログラムの意味論はこれを含めて３種類あり、あとの２つは「公理的意味論」と「表示的意味論」です。「プログラム意味論」という本で詳しく解説されているらしいので、後々学んでいきたいと思います。

CoPL には優れた「演習システム」があり、Webサイト上で演習問題を解いて、自動採点機能を利用することができます。今は算術式の評価・簡約に関する演習問題を解き進めています。今後メタ定理の証明を行うので、後述する Coq で記述してみようかなぁと思ってます。

数理論理学について

「情報科学における論理」という本を使っています。
今は第１章「命題論理」で充足可能性について学んでいます。

CoPL で今後学ぶ「推論」などの分野で、この数理論理学で学んだことが役に立つらしいです。

Coq に入門した

ここまで紹介してきた２冊には、証明問題がいくつも掲載されています。
もちろん僕も手を動かしてそれを解いてますが、PC上で専用の言語を使って半ば機械的に証明をしたり、証明の過程をテキストに起こして GitHub 等で管理したいという思いがありました。

このような理由から、前々から気になっていた Coq に触れてみることにしました。
Coq はプログラムの仕様を検証するためによく用いられる証明支援システムです。
今の僕にはよく分かりませんが、高階述語論理というものを採用しているため、検証器としての表現力はかなり高いらしいです。

環境構築

MacBook Pro (2017) に導入することを想定しています。
まず、GitHub リポジトリの Releases ページから dmg ファイルを落とします。
今回は Pre-release ではなく Latest release の 8.8.2 をダウンロードしました。
マウントすると .app ファイルが入っているので、Applications フォルダに移動して起動します。

さっそく定理証明してみる

手始めに、f(x) = x + 100, g(x) = x - 100 を定義して、定理 g(f(x)) = x が成り立つことを証明します。 エンジニアHubというサイトのこの記事を参考にしました。見よう見まねで証明を記述してみます。

帰納法を使って証明してみる

こんな風に、induction タクティクスで帰納法を使うことができます。
フォロワーさん曰く、fix タクティクスや inversion タクティクスを用いることも出来るらしいです。

※ タクティクス：Coq の証明開発モードで用いる道具

まとめ・目標

初のブログ記事ですが、いかかでしたか？

実は昨日から、100DaysOfCS (CS=Computer Science) ということで、100日間CS関連の理論を学んで、毎日進捗を報告し続けるチャレンジを始めています。

ある程度進捗が出たら、まとめてこのようなブログ記事にして公開するので、これからもよろしくお願いします！