プログラミングシステム (A25)

※この記事は「記事25」

実用的な(意味のある)演繹システムは、その一部としてプログラミングシステムを含んでいます。プログラミングシステムはプログラミング言語を持ちます。プログラミング言語には、完全に抽象的・概念的な数学的形式言語(例:ラムダ計算の言語)から、現実に使われている実在プログラミング言語、その中間にある疑似プログラミング言語など様々です。

内容:

データ領域とプログラム

プログラミング言語で扱うすべてのデータの集合をデータ領域〈data domain〉といいます。データ領域は、単なる集合ではなく、色々な条件を満たす必要がありますが、とりあえずは集合としましょう。データ領域の簡単な、そして理論的な話で一番よく使われる例は N = {0, 1, 2, ...} です。一般的な話では、D と表すことにします。

「プログラム」という言葉も解釈が多様で、多義語・曖昧語ですが、ここでは: プログラム〈program〉とは、特定のプログラミング言語〈programming language〉で書かれたテキスト(よく「コード」という)で、数学的な関数を表現するものだとします。(通常の曖昧な用法に比べて、「プログラム」をとても限定的に定義しているので注意。)

プログラムで表現される関数は、次の形をしています。

  • f:X1×...×Xn⊇→Y
  • X1, ..., Xn, Y ⊆ D

ここで、'⊇→' は、関数が部分関数〈partial function〉であることを示します。部分関数は、関数値が未定義であることを許す関数です。計算科学で「関数」と言ったら(デフォルトで)部分関数のことだと思ってください。通常の数学的な関数を意味したいときは、全域関数〈total function〉と呼びます。

プログラムがエラー・例外・無限走行などで値を出さない〈結果を返さない/戻さない〉とき、値は⊥〈ボトム〉だとみなすと、部分関数を排除できます。⊥を使えば、プログラムで表現される関数は、次の形をしています。

  • f:X1×...×Xn→Y∪{⊥} (全域関数)
  • X1, ..., Xn, Y ⊆ D

次の2つのやり方は一長一短があり、選択は趣味的です。檜山は両方使います。

  1. 部分関数を使う。
  2. 異常値を表す⊥〈ボトム〉を使う。

Pがプログラム(プログラミング言語で書かれたテキスト〈コード〉)だとすれば、それは関数(部分関数、同じことだが値に⊥を許す関数)を表すので、その関数を 〚P〛 と書きます。プログラムPと関数〚P〛を区別しましょう。絶対に区別しましょう。何があっても区別しましょう。

〚P〛:X1×...×Xn→Y∪{⊥} のとき、X1をPの第1引数領域〈first argument domain〉、…、XnをPの第n引数領域〈n-th arugument domain〉、Yを戻り値領域〈rturn-value domain〉と呼びます。「引数」「戻り値」はプログラマ達の方言〈ジャーゴン〉です。

任意の関数 f:X1×...×Xn→Y∪{⊥} が、対応するプログラムを持つわけではありません。むしろ、ほとんどの関数はプログラムを持ちません。そのことは、集合の基数に関する議論から分かります。Dが可算無限なら、D→D の関数の全体は非可算無限になります。プログラム(コード)は可算無限個しかないので、すべての関数を表現するのは無理です。

P \mapsto 〚P〛 は一意対応ですが、関数fに対して、それを表すプログラム(があるとして、それ)はたくさんあります。次の状況を考えれば明らかでしょう。

  • 優秀な(正しいプログラムを書く)10人のプログラマが、正確な仕様を与えられてプログラムを書きました。それらを、P1, P2, ..., P10 とします。これらのプログラムは(字面として)同じでしょうか?

「プログラム(のコード) → 関数」という対応も関数〈写像〉ですが:

  1. 全射ではない。プログラムで表現できない関数がある。めちゃくちゃイッパイある。
  2. 単射ではない。関数を表現するプログラムはひとつとは限らない。

別な言い方をすると:

  1. どんな関数でもプログラムで表現できると思うな!
  2. 関数を表現するプログラムがひとつだと思うな!

実行環境と走行

プログラム(のコード)に名前を付けたものを、ここでは手続き〈procedure〉と呼びます。普通は、これも「関数」と呼びますが、数学的な関数と区別するため「手続き」にします。

手続きの集合(有限集合)をライブラリ〈library〉と呼びます。ただし、同じ名前が2個以上現れてはいけません。メカニズムをプログラマの言葉で言えば、手続き名をキーにしてプログラムを引ける辞書〈ディクショナリ | ハッシュマップ〉がライブラリです。

プログラミング言語はライブラリにより機能拡張できます。組み込み手続き以外に、ライブラリで定義された手続きを使ったプログラミングができます。プログラムPがライブラリLを前提に書かれているとき、PはL上のプログラム〈program over L〉といいます。モジュール、パッケージなどは、ライブラリを組織化するときの単位を意味します(今は組織化は不要)。

書かれたプログラム〈テキスト | コード〉は、そのままでは単なる文書(特殊な言葉で書かれた読み物)に過ぎません。プログラムを実行する装置を、ランタイムシステム〈runtime system〉、エグゼキュータ〈executor〉、マシン〈machine〉、エンジン〈engine〉などと呼びます。ここでは、実行機械と呼びます。プログラムの実行〈execution〉は、走行〈run〉とも呼ばれます。

実行機械と走行の数学的な定式化(数学的なモデル)は:

  • E:ProgPL×D*→D∪{⊥} という写像〈関数〉
  • ProgPL は、プログラミング言語PLで書かれたプログラムの集合
  • D* = D0 + D1 + D2 + D3 + ...

D*とは、データのタプルの集合です。

  • D0は、何でもいいから単一要素の集合。単一要素に長さ0のタプル () をとることが多い。
  • D1は、長さ1のタプル (x) の集合。だが、D1はDと同一視して、D0 = D とする。
  • D2は、長さ2のタプル、つまりペア (x1, x2) の集合。
  • D3は、長さ3のタプル、つまりトリプル (x1, x2, x3) の集合。
  • 以下同様。
  • 足し算記号'+'は集合の直和を表す。とりあえずは、'∪'と同じだと思ってよい。

注意:DとD1を区別しないのは、通常のタプルに対する通常の数学の態度です。区別してもかまいません。また、後で出る(予定の)計算的タプリングでは、D1に相当する集合(D1そのものではないので、D<1>と書く)はまったく異なることになります。

n引数〈n-argument〉のプログラムPが関数fを表現していることは:

  • (∀)(x1, ..., xn)∈Dn.( E(P, (x1, ..., xn)) = f(x1, ..., xn) )

プログラムに対するスコットブラケットを使えば:

  • (∀)(x1, ..., xn)∈Dn.( E(P, (x1, ..., xn)) = 〚P〛(x1, ..., xn) )

プログラムおよび関数に対する引数型・戻り値型の指定である X1×...×Xn→Y をプロファイル〈profile〉と呼びます。実在のプログラミング言語の多くは、プログラム/手続きにプロファイルを指定できます。タチの良いプログラミング言語では、実行の前に、プロファイル違反(引数型違反、戻り値型違反)を構文的に判断できます。

実行前に引数プロファイル違反を検出できない場合も想定して、次を仮定します。

  • (¬)( (x1, ..., xn)∈X1×...×Xn ) (⇒) 〚P〛(x1, ..., xn) = ⊥

つまり、実行時・引数型検査が働きます。また、実行後の戻り値型検査を実行することにより、次も保証できます。

  • (x1, ..., xn)∈X1×...×Xn (⇒) (〚P〛(x1, ..., xn) ∈ Y) (∨) (〚P〛(x1, ..., xn) = ⊥)

プログラミング言語と実行機械は、ライブラリにより拡張できます。PがライブラリL上のプログラムのとき、裸の実行機械EにライブラリLをロード〈load〉した状態の実行機械を E(+L) とします。「ロード」はプログラマ方言です。プログラムP内でライブラリLに入っている手続きを呼び出し〈call〉たとき、呼び出された手続きも問題なく実行可能だというだけです。「呼び出し」もプログラマ方言で、手続きを実行することを擬人化した表現です。

裸の実行機械に、次の機能を加えた(抽象的な)装置を、プログラムの実行環境〈runtime environment〉と呼びます。

  1. 構文的または実行時の引数型検査
  2. 構文的または実行時の戻り値型検査
  3. ライブラリによる拡張(ライブラリを階層化して、いくらでも拡張できる)

これらの機能が内部的にどうやって実現されているかは、まったくのブラックボックスでかまいません。プログラマは実行環境の内部メカニズムを知る必要はありません。重要なのは、次の事実です。PはライブラリL上のプログラムで、プロファイルは X1×...×Xn→Y だとして:

  1. E(+L)(P, (x1, ..., xn)) = 〚P〛(x1, ..., xn) ←これ、超重要
  2. (x1, ..., xn) ∈ X1×...×Xn ではないときは、どうせ正常終了しないので、考える必要はない。
  3. 正常終了して、E(+L)(P, (x1, ..., xn)) ∈ Y ではないことは起こらないので、考える必要はない。

プログラミング言語、データ領域、実行環境の全体をプログラミングシステム〈programming system〉と呼びます。歴史的経緯から、演繹システムの一部になっているプログラミングシステムを算術システム〈arithmetic system〉、または単に算術〈arithmetic〉と呼びます。ゲーデルをはじめ多くの人が使ったプログラミングシステムがホントの「算術」だったからです。

  • データ領域は、N = {0, 1, 2, ...}
  • プログラミング言語は、自然数論(≒算数)を形式化した形式言語〈人工言語〉
  • 実行環境は、自然数の計算が出来る抽象機械(概念的電卓)

本来の算術プログラミングシステムは低機能なので、プログラミングの難易度は高く、大規模なプログラムを書くのは大変です。実際に具体的に書き下す代わりに、理論的な結果(存在定理)を適宜使っても、それでも大変です。現存するプログラミング言語のような“高級言語”を使えば、ゲーデルが実装した算術ソフトウェアをもっと楽に実装できます。

プログラムと計算可能関数

プログラムPがライブラリL上で定義されていれば、ライブラリをロードした(ライブラリで拡張した)実行機械 E(+L) で実行できます。E(+L) をひとつの実行機械と考えて、E' = E(+L) と置けば、プログラムPは新しい実行機械E'で実行できる、と言えます。このため、ライブラリによる拡張にはイチイチ言及しないことにします。必要があれば、ライブラリを追加して実行環境をリッチにする、と考えます。現実のプログラミングシステムもそうなっています。プログラマは日常的に、自分のプログラミングシステムをライブラリ(モジュール、パッケージ)で拡張しています。

fをプログラムにより定義されている関数とします。つまり、

  • プロファイルが X1×...×Xn→Y であるプログラムPがある。(Pがひとつだけではないが、どれか選ぶ。)
  • (x1, ..., xn)∈Dn に対して、(x1, ..., xn)∈X1×...×Xn ならば、f(x1, ..., xn) = E(P, (x1, ..., xn))

このような関数を(当該のプログラミングシステムにおける)計算可能関数〈computable function〉と呼びます。

  1. fは、X1×...×Xnの外では定義されてない。X1×...×Xnに入らないデータを考える必要はない。
  2. (x1, ..., xn)∈X1×...×Xn であっても、f(x1, ..., xn) が未定義(値が⊥)なことはある。
  3. f(x1, ..., xn) ≠ ⊥ ならば、f(x1, ..., xn)∈Y は保証される。
  4. 数学の普通の関数との大きな違いは、引数領域に入っている「正しいデータ」を入力しても、正常な出力が得られない(エラー・例外、無限走行する)ことがあること。
  5. 計算可能関数 f(x1, ..., xXn) が値を持つ (⇔) プログラムPが、引数 (x1, ..., xXn) に対して停止〈正常終了 | terminate〉する。
  6. 計算可能関数 f(x1, ..., xXn) が値を持たない (⇔) プログラムPが、引数 (x1, ..., xXn) に対して停止しない

ここで、「停止しない」は停止=正常終了の否定を意味するテクニカルタームなので、国語辞書的に停止するプログラムが「停止しない」ことはあります。エラーで停止、例外で停止などの場合です*1

計算可能関数の概念は、選んだプログラミングシステム(プログラミング言語/データ領域と実行環境)に依存します。が、経験上、ある程度の機能性を持つプログラミングシステムならば、計算可能関数のクラスは一致してしまうことが知られています。この事実を、(メタに)証明可能な命題として定式化することは出来てないので、現状では経験則です(予想でさえない)。(チャーチ/チューリングの提唱として3月に話した。)

余談: 計算可能関数の概念は、プログラミングシステムがなければ定義できません。しかし、定義のために選んだプログラミングシステムに依らないのです。計算可能関数は(プログラミングシステムに対して)相対的な概念ではなくて、絶対的・普遍的な概念なのです。これは、(檜山には)非常に不思議な現象で、「なんでそうなのか?」知りたいのですが、よく分かりません。漠然と、計算可能な関数を射とする圏(チューリング圏と呼んでいる人がいる)を公理化して、「すべてのチューリング圏は圏同値である」という命題を証明すればいいのかな、と思ってます。興味があれば、http://m-hiyama.hatenablog.com/entry/20181004/1538625265 も参照。

fが計算可能関数のとき:

  1. fが (x1, ..., xn) で、⊥でない値yを持つことを f(x1, ..., xn)↓= y と書く。
  2. fが (x1, ..., xn) で、⊥でない何らかの値を持つことを f(x1, ..., xn)↓ と書く。
  3. fが (x1, ..., xn) で、値が⊥であることを f(x1, ..., xn)↑ と書く。

記号「↓」は、「地に足が着いている」という意味(コジツケ)だそうです。「↑」は値が空に向かって飛んじゃうので発散=停止しない、と。

fを表現するプログラムPを使って書けば:

  1. f(x1, ..., xn)↓= y (⇔) E(P, (x1, ..., xn)) = y かつ y ≠ ⊥
  2. f(x1, ..., xn)↓ (⇔) E(P, (x1, ..., xn)) ≠ ⊥
  3. f(x1, ..., xn)↑ (⇔) E(P, (x1, ..., xn)) = ⊥

あるいは:

  1. f(x1, ..., xn)↓= y (⇔) Pは (x1, ..., xn) に対して停止して、正常値yを返す。
  2. f(x1, ..., xn)↓ (⇔) Pは (x1, ..., xn) に対して停止する。
  3. f(x1, ..., xn)↑ (⇔) Pは (x1, ..., xn) に対して停止しない。

プログラムに関する形容詞「停止する/しない」を、対応する計算可能関数にも使って、次のようにも言います。

  1. f(x1, ..., xn)↓= y (⇔) fは (x1, ..., xn) に対して停止して、正常値yを返す。
  2. f(x1, ..., xn)↓ (⇔) fは (x1, ..., xn) に対して停止する。
  3. f(x1, ..., xn)↑ (⇔) fは (x1, ..., xn) に対して停止しない。

プログラムとそれが定義する関数を区別せよ!というモットーからすると好ましくない言葉使いですが、よく使われます。関数そのものではなく、関数の背後のプログラム実行に言及していることをお忘れなく! テクニカルタームの解釈は、国語辞書的にボンヤリ・ナントナク考えるのではなく、定義に基づき解釈することが大事です。

*1:停止する「停止しないプログラム」という分かりにくい表現を避けるため、エラーや例外が発生したらすぐに無限ループに入る、と約束することができます。これなら、異常事態発生はすべて無限走行になります。