19/03/31 08:06:09.95 pd4YzCEG.net
>>38
つづき
どれも sheaf を使っているのだけど，なんで sheaf でないといけないかというとたぶん，ある世界 w に個体 a があったとして，世界 v が w から到達可能なとき v において a に対応する個体 b が一意に定まってほしい，ということなのだと思う。それがうまく定まるということが locally isomorphic という条件で表されているように見える。
こういう意味論だと，世界が変わったときに存在していたものが存在しなくなったり二つに分裂したりすることはない(NSS では「近傍を適切に選べば」という前提付きになる，のかな)。
昔そういうことの起きる意味論である counterpart semantics を少し触ったことがあるのだけど，あれは理論的に扱いづらい印象があった。とにかく話がきれいにならない。sheaf であればそれよりは大人しいので扱いやすくて公理化もできるのだろう。
URLﾘﾝｸ(profile.hatena.ne.jp)
kozimaさんのプロフィール Hatena 最終更新日: 2019/02/14
(抜粋)
一行紹介
数学とか論理とか競技プログラミングとか
プログラミングも好きといえば好きですが、実用的な何かを作ったことはあまりないような気がします。特にメタプログラミングと型理論に興味があります。普段よく使う言語は Common Lisp と OCaml です。
全体的に見て、物事を抽象化し、それを何らかの言語で記述することに興味があるような気がします。最近は，人間の知的活動の背景にある構造全般に興味があるのかなー，と思い始めました。
学校
Kyoto University
(引用終り)
以上