圏論好き集まれ
■ このスレッドは過去ログ倉庫に格納されています
0383132人目の素数さん
2012/01/18(水) 08:46:29.00>ある形式的体系(シンタクス)Aに対する圏論的意味論というか圏論的モデルとは、
>Aのモデルの圏論の言葉による特徴付け(Aのモデルという概念の圏論の言葉による公理化)であって
>Aの具体的なモデルではない。
シンタクスAのモデルってのは、Aそのものを圏と見たときにAからの函手(あるいはその range)なので、
「Aのモデル」という概念を与えることと、「Aを圏としてみる」ことは同じこと、というか一方を決めれば他方は自動的に決まる、ということですね。
>圏論的な領域理論の走りであり典型でもあるのはSmyth & PlotkinのSIAM論文だろうが
>あれは型無しλのモデルである逆極限法によるD_\inftyの構成を圏論の言葉に写したもの。
>ところが、型無しλのモデルとしては全然違ったP_\omegaやT^\omegaといった
>普遍領域による手法もあり、そういう点でSmyth & Plotkinのは型無しλのモデル
>(あるいはその中の外延的モデルに限定したとしても)全般を圏論の言葉で特徴付けたものではない。
シンタクスAに対して、そのモデルは何か、を定義したところで、
そういうモデルが存在するかというのは別問題なんですね。
勿論、AからAへの恒等函手という自明なモデルは存在するのだけれど、
これではモデルとして役に立たない。
ここでモデルとして役に立つ、というのは、例えば以下のような利用法が念頭にある。
シンタクスAに等式理論が入っていたとして二つのラムダ式(あるいは何らかのプログラム)がそのシンタクスで等しくないことを示したいときに、
モデルである函手による値が異なれば、その等式理論ではその二つは等しいことは言えないと証明できる。
恒等函手のような自明なモデルだと、
この函手による値が異なることを示すのは等式理論でその二つが等しくないことを示すことに他ならないので、
モデルとしては何も役に立っていない。
こういう意味で役に立つモデルを具体的に作るのが領域理論の目的で、
「圏論的にされた領域理論」はその具体的な作り方を圏論の言葉で表したもの。
従って「圏論的意味論」と「圏論的にされた領域理論」は、関係はあれどもまるっきり別のもの。
■ このスレッドは過去ログ倉庫に格納されています