第2回プログラム等価性クイズ:回答編

問題編:http://d.hatena.ne.jp/sumii/20090716/p1

ということで、回答はMLばかりでしたが(&出題もMLにすべきでしたが)、最後まで無理をしてJavascriptに書くと、

var global;
function g(local) {
  global = local;
}
f(g);
global();

のような文脈C[f]を考えれば、C[f5]は(全体の実行が)停止しないのにC[f6]は停止するので、f5とf6は文脈等価になりません。

追記:「f5やf6が終了した後に無限ループしても良かったの?」とか「グローバル変数なんてずるい!」とか思った人は、

function call_f(g) {
  f(g);
}
function g(local) {
  function g2(local2) {
    local = local2;
  }
  call_f(g2);
  local();
}
call_f(g);

なる文脈C[f]も同様に(文脈等価性の)反例となります。(追記終わり)

さて、このように実際に反例があって文脈等価にならない例はまだ良いのですが、本当の問題は文脈等価になる場合(の証明)です。例えばf6を少し変えて、

function f7(g) {
  var x = 0, y = 0;
  function d() { d(); }
  function h() { if (x == 0) { y = 1; } else { d(); } }
  g(h);
  if (y == 0) { x = 1; } else { d(); }
}

という関数f7は(例えばreferenceを入れたλ計算において)f5と文脈等価でしょうか?*1 等価な場合は(数理論理学的に)証明してください。…などと言い出すと、いきなり研究レベルの問題になります。答えの例は私の最近の論文をご覧ください、と最後に宣伝。

*1:ロンドン大学クイーン・メアリー校のヤン講師による例だそうです。