並列論理和の続き - sumiiのブログ

http://d.hatena.ne.jp/sumii/20070511/p6

の続き。質問の仕方からわかったかもしれませんが、教科書的解答は「（逐次言語では）実装できない」です。たとえば、名前呼び(call-by-name)や値呼び(call-by-value)のλ計算（要するに逐次関数型言語）では、簡約規則についてよく考察すれば、porは定義できないことが証明できてしまいます。

ところが、（たとえば領域理論などの）表示的意味論では、porも「計算可能」な連続関数になります。ということは、たとえば「関数fを受け取って、fがporを実装していればtrueを返す」という関数is_porと、「fを受け取り、falseを返す」という関数は、操作的意味論では等価なのに表示的意味論では等価でなくなってしまいます。

ということで、

（普通の）λ計算はあくまで逐次言語に過ぎず、（porのような意味での）並列計算は表せない
領域理論などの表示的意味論は、逐次言語ではなく「並列言語」のモデル

ということになります。

ところで、「λ計算はTuring機械と計算能力が同等」「Turing機械は逐次でも並列でも計算能力が同等」のはずです。これは上述の考察と矛盾しません。「計算能力が同等」というときに、特定の型（たとえば自然数から自然数へ）の関数しか考えていないからです。そこを曖昧に理解していると混乱します（というか、私は学生のときに混乱しました）。

P.S. 実は私が本当に答えを知りたい質問：

上の答えはあくまで「教科書的解答」なのですが、ひょっとしてC言語あたりならば、何か酷い方法:-)でporマクロを定義できたりしないのでしょうか？　もちろん、関数の中身を読んで、マシン語レベルで並列CPUをエミュレートすれば可能なはずですが、そうではなく標準的というか移植性のある（ANSI/ISO規格でwell-definedな）方法で…
実はλ計算にもとづく逐次関数型言語(PCF)にプリミティブとしてporだけ追加すれば、操作的意味論での等価性（文脈等価）と表示的意味論での等価性は一致する(!)ことが知られています。では、porを追加しなくても等価性が操作的意味論と一致するような表示的意味論は存在しないのでしょうか？（項モデルなど自明な場合は別として、ゲーム意味論等？）　そういう意味論が存在したとして、is_porと恒偽関数の等価性はどのように証明されるのでしょうか。

追記：この分野の世界的専門家である某先生から~~ツッコミ~~情報提供が。提供された情報の内容については（自分が）勉強しているところなので、しばらくご容赦を…＞皆様

追記２：

http://www.math.sansu.org/u/diary/?date=20070514#p02

コメントを投稿させていただいたのですが、どうも表示されないので一応。（moderatedなだけかもしれませんが、他所のtDiaryで、unmoderatedなのに表示されなかった経験もあるので…）

問題設定としては、

(A) （無限ループ以外の）副作用が発生する場合は「未定義動作」（どうなっても良い）あるいは「処理系依存」として気にしない。

(B) 「一方がtrueになるならば、もう一方の副作用は実行されない」ことを要求する。

のどちらでもOKです。後者は前者以上に実装困難ですが。