- 「Turing-completeでなければ安全だ」という類いの議論は数学的な意味からずれており、非チューリング完全性は停止性・決定性・サンドボックス化のような実用的性質とは大半が別物である
- 実行時間が入力に対する 原始再帰関数 で制限される Turing Machine の計算は、原始再帰関数としても書き直せる
- 原始再帰関数は常に停止するが、
2^(2^N) のように急速に増大する関数も作れるため、停止保証 がそのまま実用的な実行時間を意味するわけではない
- 実務では、停止しないプログラムと何十億年後に終わるプログラムは似た問題を生み、Turing-complete な言語でも ステップカウンタ によって強制停止させられる
- 設定言語の品質は Turing-complete かどうかよりも、決定性、明確な意味論、純粋性、セキュリティ・サンドボックス化、実行時間制御、単純性により大きく左右される
Turing-completeness 議論の中核的な誤解
- インターネット上のプログラマは、特定ドメインで「Turing-complete ではない」ことを利点や要件のように語ることが多い
- しかし Turing completeness は数学に由来する具体的な用語であり、実務者が求めるさまざまな性質の代名詞として使うと意味がぼやける
- 実際に必要なのは、停止保証、高速実行、決定的動作、サンドボックス化、単純な設定言語といった性質であり、これらは Turing completeness とは大半が直交している
- この違いを理解するには、原始再帰関数（Primitive Recursive Functions, PRF） に関する簡単な理論結果が必要になる
十分に高速な Turing Machine は PRF に変換できる
- Turing-complete な言語で書かれたプログラムでも、実行時間が
O(2^(2^N)) より速いと分かっていれば、同じアルゴリズムを 非チューリング完全言語 でも実装できる
- ほとんどの実用的問題は
2^(2^N) より速く終わる領域に入る
- したがって非チューリング完全言語は、実務上の計算能力を有意に制限するわけではなく、計算を統制する特別な能力を自動的に与えるわけでもない
- 実務の観点では次の二つのプログラムは事実上同じ問題を生む
- 停止しないプログラム
- 10億の10億倍のようなステップ数の後にしか停止しないプログラム
- Turing-complete な言語でも実装段階で ステップ数を数え、一定上限の後にエラーで停止させれば、非停止問題そのものは単純に防げる
FSM: 常に停止するが表現力は制限される
- Finite State Machine(FSM) は文字列を入力として受け取り、「yes」または「no」を返す認識器である
- FSM は有限個の状態集合、開始状態、yes 状態集合、遷移関数から構成される
- 入力の各シンボルに対して遷移関数を繰り返し適用した後、最終状態が yes 状態かどうかで結果が決まる
- FSM の表現力は 正規表現（regular expression） と等価である
- FSM は入力長に線形で動作し常に停止するが、あらゆる文字列集合を認識できるわけではない
- たとえば
1、010、00100、0001000 のように、1 の両側に同じ数の 0 がある文字列集合は FSM では認識できない
- 十分に長い入力では状態が繰り返されてサイクルが生じ、そのサイクル区間を複製しても FSM は依然として yes 状態に到達するが、文字列条件は壊れてしまう
Turing Machine: FSM に可変テープを加えたモデル
- Turing Machine(TM) は FSM のように状態と遷移関数を持つが、不変の入力ではなく可変テープ上で動作する
- 各ステップで TM は現在のテープシンボルを読み、次の操作を行う
- 現在のシンボルを新しいシンボルで置き換える
- 内部状態を変える
- ヘッドを左または右に 1 マス移動する
- TM が halt 状態に到達すると停止し、その時点のテープ内容が結果になる
- FSM が二値認識器であるのに対し、TM は関数を計算する装置である
- TM は必ず停止するとは限らず、テープを行き来し状態を変え続けても最終状態に到達しないことがある
Universal Turing Machine と計算能力
- TM のプログラムはユーザー入力として与えられるコードではなく、遷移関数そのもの にハードコードされている
- しかし任意の TM と入力をテキストファイルとしてエンコードし、それを解釈する「インタプリタ」TM を作ることはできる
- このような TM が Universal Turing Machine であり、入力として与えられた別の TM をシミュレートする
- Python で TM インタプリタを作れ、逆に Python インタプリタも TM で実装できるので、両者は計算能力の面で等価と見なせる
- FSM は TM より弱い
- TM は FSM をシミュレートできる
- TM は、両側に同じ数の
0 があり中央に 1 がある文字列をテープ操作で判定できる
- FSM は同じ問題を解けない
テープは二つのスタックとして見なせる
- TM のテープは、一般的なプログラミング言語で直接実装するには扱いにくい抽象化である
- テープとヘッド位置は 二つのスタック として表現できる
- ヘッドの左側の内容は左スタック
- ヘッドの右側の内容は順序を逆にした右スタック
- ヘッドを左または右に動かす操作は、一方のスタックから pop し、もう一方に push する操作に置き換えられる
- したがって TM は「二つのスタックを持つ FSM」と等価な計算能力を持つ
- スタックのシンボルが
0 と 1 だけなら、スタック自体を一つの自然数としても表現できる
- top の確認:
stack % 2
- pop:
stack / 2
- push
x: stack * 2 + x
Turing Machine の限界: Halting Problem と Rice 型の結果
- すべての TM はテキストとしてエンコードできるため、可能な TM を無限リストとして並べられる
- 対角線論法を使うと、TM で計算できない関数が存在することを示せる
- より具体的な例が Halting Problem である
- TM のソースコードと入力が与えられたとき、その TM がいつか停止するかを判定する問題である
halts(program, input) が常に正しく停止すると仮定すると、自分自身のソースコードを入力として受け取る weird プログラムで矛盾が生じる
- 停止すると判定すれば無限ループに入り停止しない
- 停止しないと判定すれば即座に終了する
- したがって
halts は、ある場合には誤るか、ある場合には停止しないはずである
- より一般には、任意の TM について、動作を保存する非自明な性質をアルゴリズムで判定することはできない
- 構文的性質は確認できるが、リファクタリング後も保たれるような動作特性は一般には判定できない
原始再帰関数: 常に停止する計算装置
- 原始再帰関数(PRF) は自然数のタプルを受け取り、自然数を一つ返す関数として定義される
- 基本関数は
zero と succ である
- 関数合成により定数を作れる
succ(zero) = 1succ(succ(zero)) = 2
- 一般再帰は許されないが、反復回数があらかじめ固定された制限付きループ
LOOP(init, f, n) は許される
LOOP(init, f, 0) = initLOOP(init, f, 1) = f(init)LOOP(init, f, 2) = f(f(init))
- 核心となる制約は、反復回数
n がループ開始前に固定され、ループ本体でループカウンタを変更できない点である
PRF で基本的なプログラミング構成を作る
- 加算は
add(x, y) = LOOP(x, succ, y) として定義できる
- 乗算は
mul(x, y) = LOOP(0, add x, y) として定義できる
- べき乗は
pow(x, y) = LOOP(1, mul x, y) として定義できる
- これにより急速に増大する関数も作れる
pow_2(n) = pow(2, n)pow_2_2(n) = pow_2(pow_2(n))
pred を基本関数に追加すれば、飽和減算とブール演算を作れる
sub(x, y) = LOOP(x, pred, y)and(x, y) = mul(x, y)not(x) = sub(1, x)if(cond, a, b) も算術式で表現できる
- 比較演算、剰余、除算も、上限付き反復と条件式を使って実装できる
PRF のデータ構造と TM シミュレーション
- PRF は複数引数を受け取れるが、結果は自然数一つなので、データ構造を自然数にエンコードする必要がある
- 対
(a, b) は 2^a * 3^b で表現できる
- 構成要素を取り出すには、特定の素数の最大指数を求めればよい
fst(p) は p を割り切る 2 の最大冪指数であるsnd(p) は p を割り切る 3 の最大冪指数である
- 同様の方法で三つの値
(S, stack1, stack2) も一つの自然数にまとめられる
- TM の設定は次の三要素で表現できる
- 現在の状態
S
- テープ左側のスタック
- テープ右側のスタック
- スタック操作は剰余、乗算、除算で実装できるため、TM の 単一ステップ を PRF でエンコードできる
LOOP(initial_config, single_step, n) を使えば、TM を正確に n ステップだけシミュレートできる- 問題は十分な
n が分からないことだが、実行時間が何らかの PRF で制限されるなら、その回数だけ反復するように作れる
- 結局、実行時間が原始再帰関数で制限された TM の計算は PRF で置き換えられる
PRF の限界: 常に停止しても TM ほど強くはない
- PRF は常に停止するが、停止するすべての関数を表現できるわけではない
- TM で計算できるが PRF では計算できない関数が存在する
- それを示すために、PRF 構文木の 深さ を基準に成長率の上限を置く
- 深さ
d 以下の PRF は、ある単項関数 A_d より速く増大できないよう上限を設定できる
A(d, x) は次のように定義される
A(1, x) = x + 1A(d + 1, 0) = A(d, A(d, 0))A(d + 1, x) = A(d, A(d + 1, x - 1))
- この定義では、再帰呼び出しごとに
(d, x) が辞書式順序で小さくなるため、TM で計算すれば停止する
a(x) = A(x, x) はどの PRF よりも速く増大し、TM では計算できるが PRF では計算できない
実務に戻ると: 非チューリング完全性だけでは不十分
- Turing Machine は停止しないことがある
- FSM や PRF のように常に停止する装置でも、速く終わる保証はない
- PRF は
2^(2^N) のような大きな関数を計算できるため、停止保証だけでは実用的な実行時間は保証されない
- 現実の多くのアルゴリズムは実行時間が PRF で制限されるため、非チューリング完全な装置でも表現可能である
- Turing-complete な計算を PRF 的にする一般的方法は、反復カウンタを追加し、カウンタが大きくなりすぎたら強制停止することだ
設定言語に本当に必要な性質
- 設定言語が「非 Turing-complete」を設計目標として掲げることは多いが、実際に必要なのはより強い複数の性質である
-
決定性
- 設定言語は 決定的 でなければならない
- Python の
id([]) のように実行ごとに異なる値が出る動作は、一般プログラミングでは許容されても設定には不向きである
- 設定はインクリメンタルビルドやキャッシュシステムのキーとして使われることが多く、非決定性が入るとキャッシュ動作が不安定になる
-
明確な意味論
- 言語の動作は、参照可能な基準として明確に固定されていなければならない
- ASLR を無効にし特定の allocator を使って Python の
id([]) を決定的にすることはできても、その結果が予測可能であるとか、実装間で同一であるとは保証されない
- 別実装や Python のバージョン変更でも同じ動作を保証するには、意味論が明確である必要がある
-
純粋性
- 設定が環境変数やディスクファイルを読めると、設定の意味が評価環境に依存する
- キャッシュを正しく機能させるには、設定言語は 純粋性 を持つべきである
-
セキュリティとサンドボックス化
- 純粋性とセキュリティは、どちらも一般 IO を公開しないことで達成できる
- ただし両者の目的は異なる
- 純粋性は結果が非決定的になるのを防ぐためのものだ
- セキュリティは、攻撃者にアクセストークンのような資源を露出させないためのものだ
-
実行時間制御
- IO を制御しても、悪意ある設定が CPU を焼く サービス拒否 攻撃は可能である
- 実行時間保証のためには二つのアプローチがある
- 処理を入力サイズに直接比例する明白な線形構造に制限する
- 各原子的ステップごとにカウンタを減らし、カウンタが 0 になったら停止する metered execution を使う
-
単純性
- 設定言語は、ユーザーが単純なプログラムを書くよう誘導すべきである
- 再帰や無限ループを禁止することは、単純性を促すためのスピードバンプになりうる
- ただし PRF の例が示すように、そのような禁止は任意の再帰的プログラム記述を完全には防げず、ただ回りくどいコードが必要になるだけである
- 関連例として some roundabout code を参照できる
最終整理
- 入力に対する実行時間が何らかの原始再帰関数で制限される Turing Machine アルゴリズムは、原始再帰関数としても実装できる
- 非チューリング完全性は停止保証という一つの性質を与えうるが、実務で必要な実行時間上限や設定言語の品質を自動的に保証するものではない
- 設定言語設計で重要なのは Turing completeness そのものより、決定性、明確な意味論、純粋性、サンドボックス化、実行時間の計量、単純性である
1件のコメント
Hacker Newsのコメント
自己宣伝: https://www.nayuki.io/page/primitive-recursive-functions
記事の結論部に設定言語に関するかなり良い基準があるが、現在の言語の中でその全部、または大半を満たすものがあるのか気になる
Dhallは意図的に全域関数型言語なので「チューリング完全でない」方向に進んでおり、Cueには関数がないので再帰するものもない
RCL [3] は基準を満たしていると思う。決定的で純粋であり、計量された実行を提供し、ファイルシステムアクセスをサンドボックス化している。サンドボックスポリシーが許可すればファイルを読めるが、そのようなファイルはソースコードの一部と見なされ、importと同じように動作する
RCLでは、著者が述べた理由から「チューリング完全でない」方向には進みたくなかった。プログラムが最終的に終了するという事実は実務ではあまり有用な性質ではなく、逆にAgdaのような全域関数型言語でも非常に複雑なプログラムを書けるため、非チューリング完全性が単純なプログラムや設定を保証するわけではない
RCLのすべてのループには境界があるが、関数があるので再帰も可能だ。末尾呼び出しはないため、当初はネイティブスタックのオーバーフローを防ぐために再帰深度制限を入れていたが、ファザーが定数スタック空間で実行されながら停止する関数を見つけ出し、今も完全には理解できていない:
let f = g => g(g(h => k => g(g(h)))); f(f)結局、このような病的な関数を表現できることは実務上の問題にはならない。実行ステップ数の制限、つまり「ガス制限」や著者の言う「計量された実行」を設ければよい。コードを単純に保つうえでは、組み込みの反復構造に境界があり、再帰が不便であることが良い誘導装置になるが、結局もっとも価値ある道具はコードレビューと良い判断だ
[1]: https://dhall-lang.org/
[2]: https://cuelang.org/
[3]: https://rcl-lang.org/
Dennis RitchieのMITでの研究は、彼がループプログラミングと呼んだテーマに焦点を当てていた
The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
ほぼすべての現代のプログラマーが基本的に従っている構造化プログラミングは、実質的に原始再帰関数の方向へ押し進めるパラダイムだ。構造化プログラミングがpopや関数型のような他の2類型に比べてほぼ普遍的に受け入れられたため、Dijkstraの「goto文は有害」論文を混同しているように思える
原始再帰関数は計算可能関数全体を含むわけではないが、終了が保証される直感的な関数はほぼすべて含む。もちろん、ループに入る時点で反復回数が分からないループが実際に必要な場合もあるが、本当に必要なときだけ使えば避けられる足撃ちだ
COBOLでさえ、無制限のgotoをALTER命令へ移す形で近代化された。現代的で有用な言語の中で、PR関数を許さない言語は思い浮かばない
Cでも
whileを避け、fall throughを明示的に避けるように書けば、ほぼ常に必ず終了する全域関数のコードを作れるMLの型推論のような病的なケースもある。複雑度クラスに比べて実際のコストははるかに安いので、全域関数ではなく、言語がこのような使用を制限しにくいとしても受け入れる価値がある
実用的に見れば、どの言語もおおむねこうした基準の大半を支えるデフォルトを提供しているが、それを強制する制約は言語の有用性を深刻に制限するだろう。評判の悪いSOLIDやCleanフレームワークでさえ、このモデルの方向へ押し進めていると思う
構造化プログラミングがあまりに普及したため、この点を忘れやすく、場合によっては教えられなくさえなっている。年寄りのひげ面の立場からすると、
WHILEなどの危険性を学んだ記憶があるO(2^(2^N))より速く動くという言い方は、おそらく単純化しようとした表現だろうが、「非常に大きな数」という部分は信頼を少し損ねる正確には「非常に速く増加する関数」と言うべきだと思う。あるいは、プログラムが
O(2^(2^N))ステップ未満で終了するという意味に見える制限された言語のほうが一部の用途に向いている、という最初の部分だけを見ると、利点は必要なステップ数の上限を静的に計算できることなのではないかと思う。
そうすれば、どんな入力に対しても制限に違反する計算は拒否し、意味のあるエラーを返せる。
一方、チューリング完全な言語にランタイム制限をかける方式では、関心のある一部の入力に対して制限を低く設定しすぎることがある。実行して制限に引っかかるまでは分からない。C++のテンプレート再帰でこういうのをたまに見る。
自分が完全に混乱しているだけかもしれないので、もっと詳しい人が説明してくれるとうれしい。
悪いワークフローが失敗するまでに数倍余計にかかっても、それでもミリ秒単位なので大きな被害はないと思う。
たいていこの問題は、誰かが問題領域を有向非巡回グラフとして扱ったものの、「非巡回」を強制できないときに出くわす。問題を有向非巡回グラフとしてモデル化するのは、フロドから指輪を受け取るか悩むダーク・ガラドリエルのようなものだ。「皆が私を愛し、絶望するだろう」。こういうものを作る人たちは、いつも自分たちが誇るに値する以上にはるかに誇らしげでいる。
結局、高価で複雑な解決策に引き込まれた顧客は資金が尽き、自分たちの問題もずっと小さく見え始める。すると文字どおり、作業あたりのコストを十分に下げて顧客の事業を維持できないアプリだけが残る。
私はそれよりも、静的型検査、nullなし、変更なしといった先行するハンマーをすり抜けたバグを捕まえるための、道具箱のもう一つのハンマーとして使うほうに興味がある。
有限時間内に終了するという事実は整合性を証明してくれるわけではないが、私がコードは有限時間内に終了すると宣言したのにコンパイラが同意しないなら、そのコードは間違っていると信じる。
早期終了が実行時間に影響するには遅延評価や短絡条件文を仮定する必要があるが、実用言語なら普通はそうしたものを備えることになる。
n log nだが、入力サイズに対して二次の上限を持つ。それならクイックソートの計算を拒否するのか。さらに極端な例として、Hindley–Milnerアルゴリズムは指数時間の上限を持つが、実際には線形時間で動くことが多い。
ただし、それが本当に強い要件になる状況は一つも思い浮かばない。「クエリの実行に時間がかかりすぎました」というエラーを出せないシステムがどれほどあるだろうか。
終了しない／境界があるという原則に基づくバックエンドWebプログラミング言語を使ってみたいと思っていた。
すべての関数について、与えられた状態と引数に対して実行が境界内に収まることをコンパイラに証明し、Xが下限でYが上限であることを示せる、という構想だ。この情報はエントリポイントまで伝播する。
より強い意味論が必要だという著者の意見に同意しており、それでこの言語を考えた。プログラムの実行時間について保証が欲しいことは多い。
中核は原始再帰関数ベースになるだろうが、実際にはチューリング完全にもなり得る。Rustが不正なborrowは拒否しつつ、生ポインタ用に
unsafeを提供するように、この言語も単純な反復のプリミティブを基に上限を計算するか、unsafe演算子を使って境界に関する代替の式を提供させることになるだろう。記事の短い不満／動機の部分がよく理解できない。
「通常、特定の領域ではチューリング完全ではないことが利点、あるいは要件として称賛される。私はそうした議論の大半が誤解していると思う――チューリング完全ではないという言葉は、人々が期待する意味ではない」という部分だ。
なぜそうした議論が間違っているのか。ほとんどの形式解析ツール、たとえば Coq、Isabelle、Agda は通常、関数が終了することの証明を要求する。これはその関数が全域関数であることを証明するのと同じで、したがって原始再帰的であることを意味するのではないのか。
最近のCEL関連の議論でも出ていた。
https://news.ycombinator.com/item?id=40954652
記憶が正しければ、これはco-NPオラクルを持つNP、または多項式階層の第2レベルと同値だ。小さな問題でも可能ではあるが高価だ。
こうしたツールは、プログラムを全域関数になるように構造化するときに最もよく機能する。その中で、構造化プログラミングにおいて
FORだけを使う、または反復回数が制限されたWHILE／再帰だけを使う方法が最も一般的だ。SATとだけ関係はあるが、Schaeferの二分法定理で扱われる扱いやすい形が、私が思いつく中で最も近づきやすい見方だ。
Agda、そしておそらく他のツールも、終了する非原始再帰関数の一部について終了性を証明できる。もちろん全部は不可能だ。
記事が不満を述べている誤解は、おおよそこういうものに見える。「チューリング完全性は計算ができるという意味で、非チューリング完全性は計算ができず、良い設定言語の性質を持つという意味だ」。
記事の要点は、非チューリング完全でも計算コストが大きかったり厄介だったりすることは多くでき、設定言語なら単に非チューリング完全であることよりも、はるかに厳しい制限が必要だということだ。
私は CUE の開発者です。CUE は原始再帰的であり、「良い」設定言語に望まれる基準も満たしています
[0] https://en.wikipedia.org/wiki/Rule_110