末尾再帰最適化で遊ばれよう

正直、ここ(via ここ)で語られてるような高度な話は理解できない(いつわかるようになるのか？！)ので封置。個人的には、末尾再帰最適化判定問題は、言語仕様よりも下のレイヤに位置するオプチマイザの特性の話として、その範疇でまとめていいんじゃないかと思う。

さて、そもそものきっかけの問い「処理系が末尾再帰最適化をしているかを、処理系で動くコードから判定できるか」を定式化すると、

• ソースコードXを翻訳系Tでコンパイルして実行形式aを得る。aを実行して、Tが末尾再帰最適化能力を持つか否か判定したい。そうなるようなXを求めよ

ってあたりか。

しかし、何人かが実験して示してるように、人の目で見て末尾再帰最適化してくれそうでも、Tが末尾再帰最適化をしてくれるか否かはかなり気まぐれ…いや、より科学的な言い方をすると、末尾再帰最適化するか否か、Tの中の人しか知りようがない基準で決定されるっぽい。このような状況では、Xが末尾再帰最適化されないからといって、Tに末尾再帰最適化能力がないとは断言できない。(対して、Xが末尾再帰最適化されたなら、Tが末尾再帰最適化能力を持つことが立証されるのだが…)
つまり、Tが末尾再帰最適化能力を持たないことを証明するXは存在しないのであって、上の定式化はill-defined。修正が要る。

普通に考えて、有力な案は次の形か。

• ソースコードXを翻訳系Tでコンパイルして実行形式aを得る。Xが末尾再帰最適化されたかどうか判定せよ(手段は問わない)

こう修正すると、ill-definedさはなくなる。どんなソースコードXとどんな翻訳系Tをもってきたって、最悪でも翻訳結果aの逆アセンブルリストを読めばyes/noで結果が出て、それが問題の答えである。

しかし、翻訳結果a自体に判定させたいという最初の目的がどっかに逝ってしまった…

これを解消するには、XをTに与えるかわりに、Xに判定ロジックを仕込んだX'をTに与えねばならない。はい、もうおわかりだと思いますが、その際「X×Tの末尾再帰最適化有無」＝「X'×Tの末尾再帰最適化有無」が保障されないとダメ。そもそものきっかけの問いは、この配慮なしには問いとしてすら成立しない。

という観点で、id:yaneuraoさんのところにコメント(「逃避王女」名義)を書かしていただいたのデス。