第２回プログラム等価性クイズ

たまには自分の研究に関係がある（かつ専門家以外にもわかる）話題ということで、プログラム等価性(program equivalence)に関して書いてみます。プログラム等価性というのは「二つ（ないし二つ以上）のプログラムが等価」という性質のことで（そのまんまやんけ！）、「等価」の粒度によって様々な「プログラム等価性」があります。その中でも

任意の文脈（プログラムの「使い方」や「呼び出し方」のようなもの）Cにおいて、C[P]（文脈CにおいてプログラムPを実行する計算）が停止するならば、C[Q]も停止するし、逆も成り立つ

というプログラム等価性を文脈等価性(contextual equivalence)と呼ぶことがあります。

例えばJavascript風*1の命令型言語で、

function f1(g) {
  var x = 1;
  g();
  return x+1;
}

という関数f1と、

function f2(g) {
  var x = 2;
  g();
  return x;
}

という関数f2は、（reflectionっぽい機能とかを無視すれば）文脈等価になります。どんな呼び出し方をしても、f1とf2は両方とも停止する（あるいは両方とも停止しない）と考えられるからです。停止する・しないという定義なので、実行速度などは無視します。また、関数呼び出しのためのスタックを含め、メモリは無限にあると仮定します。

一方、例えば

function f3(g) {
  var x = 1;
  g(x);
  return x+1;
}

という関数f3と、

function f4(g) {
  var x = 2;
  g(x);
  return x;
}

という関数f4は文脈等価になりません。文脈C[f]として

function d() { d(); } /* 停止しない関数 */
function g(x) {
  if (x > 1) { d(); }
}
f(g);

みたいな使い方を考えると、C[f3]は停止するのにC[f4]は停止しないからです。

…などというつまらない能書きはこれぐらいにして、さて、

function f5(g) {
  function d() { d(); } /* ←追記３の理由で追加・修正 */
  g(d);
}

なる関数f5と、

function f6(g) {
  var y = 0;
  function h() { y = 1; }
  g(h);
  function d() { d(); } /* ←追記３の理由で追加・修正 */
  if (y == 1) { d(); }
}

なる関数f6は文脈等価でしょうか？（dは上と同様、呼び出されると停止しない関数とします。）　つまり、C[f5]は停止するけれどもC[f6]は停止しない（ないしその逆）、という文脈Cは存在するでしょうか？　繰り返しになりますが、ここでは停止性だけを考えているので、コンソールやネットワークへの入出力とか、実行効率とかは「等価」の定義に含まれていません。（なお、上のf5, f6は私が考えたわけではなく、昔からよく知られている例です。念のため。）

答えはCMの後で。

ヒント(?): 前回（３年以上前！）のクイズ

shiroさんからツッコミが入ったので追記：exceptionとか（C言語でいう）exitとか、setjmp/longjmpとかcall/ccとかも無しでお願いします（あると簡単すぎるので）。我田引水すると、こういう「アレは無し」「コレも無し」という追記を何度もしないためには、計算モデルの数学的定義が必要になります。:-) 知っている方のために、ここでは参照(reference)入りの型無しλ計算あたりを考えています。

追記２：関数を==で比較するのも（簡単すぎるので）禁止。やはり言語を定義せずに出題するのは無理があったでしょうかorz。非形式的には、ネスト可能な第一級関数と静的スコープの変数と破壊的代入と整数演算からなる言語、ということで…

追記３：dを上書きするのもやめてください。;_; 問題を修正しました。最初からML（ただし例外は無し）で書けばいいのに無理してJavascriptなんか使うから…＞自分

*1:本当のJavascriptは自信がないので…