日々の流転

λ. predicativeな型理論であるということ

Agdaで(2階ラムダ計算の)パラメトリシティに関する命題を証明してみようと思い、以下のようなコードを書き始めたのだが、Forallのところで「Sort comparison failed」と怒られてしまった。

Rel (X,Y::Set) :: Type
  = X->Y->Set
 
FunRel (|A,B,C,D::Set) (R::Rel A B) (S::Rel C D) :: Rel (A->C) (B->D)
  = \(f::A->C)-> 
     \(g::B->D)-> 
       ((a::A) |-> (b::B) |-> R a b -> S (f a) (g b))
 
Forall (F::Set->Set) :: Set
  = (X::Set) -> F X
 
ForallRel (|F,G::Set->Set) (R::(A,B::Set)|->Rel A B->Rel (F A) (G B))
  :: Rel (Forall F) (Forall G)
  = \(f::Forall F)-> 
     \(g::Forall G)-> 
      ((A,B::Set) |-> (S::Rel A B) -> R S (f A) (g B))

しばらく悩んで、ようやくAgdaがMartin-Löf流のpredicativeな型システムであることを思い出した。FやCCのようなimpredicativeな型システムと違って、こういう定義は出来ないのだった。関数の型のソートに関する規則を、Adga の Structured Type Theory と、λ-cubeのスタイルで形式化したCC とで比べてみると良くわかる。λ-cubeでは返り値の型のソートが関数の型のソートになる。一方、Structured Type Theory では直観的には引数の型のソートと返り値の型のソートの最小上界が関数の型のソートになる。

アホだなオレ。しかし、impredicativeな型システムに慣れてる人が使うと絶対ハマると思うよ、これ。

それで思ったが、そうなるとGHCのCore言語をAgdaのコードに変換してゴニョゴニョってのは問題が起こりそうな気がするな。GHCのCore言語は一応Fω風のimpredicativeな型システムだったと思うので。

λ. Describing and Reasoning on Web Services using Process Algebra. Gwen Salaün, Lucas Bordeaux, Marco Schaerf

を読んだ。

ITシステムでbisimulationの説明をしていたときに、bisimulationの意味がわからないが使ってみた というのを誰かが見つけてきて面白かった。

bisimulationの(余代数的/圏論的な)定義は知っているけど、weak bisimulation と strong bisimulation については知らない。調べなくては。weak bisimulation は behavioral equivalence とは違うよね?

(2005-09-16 追記) strong bisimulation が普通のbisimulation。τアクションによる違いを無視するのが weak bisimulation 。http://www.lix.polytechnique.fr/~catuscia/teaching/DEA/General/Exercises_James/exercises.pdf の「4 Definition: CCS operational equivalences」が分かりやすかった。