call/ccと古典論理のカリー・ハワード対応 - 再帰の反復blog「直観主義論理のカリー・ハワード対応」の続き。 call/ccと継続 call/ccというのは、gotoを強力にしたものだと思っておけば良い。ただしScheme以外のプログラミング言語では、あまり見かけない機能。 例えばブロック構造から抜け出すための命令がある言語を考える。どのブロックから抜け出すかはラベルで指定する。またラベルはギリシャ文字で表すことにする。とりあえず次のような感じになるだろう。jumpの部分を実行するとブロックから抜け出す。 :α{ ... ... jump α; ... // ここは実行されない }でも、ブロック自体が値を持っている(値を返す)ようにした方が汎用的になる。例えば、次のプログラムはflagが真ならxに1が代入され、偽なら2が代入される。 x = :α{ ... ... if (flag) { jump α 1; } ... 2; }値を返すにしても返さな
