読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

variable-free type theoryの圏論的な解釈について

myuon-myon.hatenablog.com

の続き. いくつか疑問が解消されたのでそれについて.

var-free type theoryについて

  • syntaxはcontext, type, term, substからなる.
  • contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtypeだけの列になる).
  • typeはground typeと関数型A → Bとsubstが代入された型(σ[s]の形をしているもの)のいずれか.
  • termは1と代入された項M[s]のいずれか.
  • substはidと合成f . gとshiftとextension<f:subst, M:term>のいずれか.

termは型付けをde Bruijn indexで考える.
term1はcontextの直近のtypeに対応する項とみなす. 例えば, Γ,σ ⊢ 1:σなどである.

substはcontextの間の変換とみなす.
例えばΓ ⊢ id:Γid(Γ)=Γを表す. また, 合成は通常と逆向きに書くらしい(多分見やすさの都合).
shiftはindexをすべて1つ加算するような変換とみなす. 例えばΓ,σ ⊢ ↑:Γはindexが上に1つずれるので一番新しいtypeσを忘れるものとみなす.

extensionのtyping ruleは次のようなものである:
Γ ⊢ f:Γ', Γ' ⊢ σ, Γ ⊢ M:σ[f] ⇒ Γ ⊢ <f,M>:Γ',σ

これは, Mによってcontextに新しいtypeを付け加える操作と考えることができる.
あるいは, 変換fをMによって拡張したものとみなしてもよい.

locally cartesian closed categoryでの解釈

ML theoryはLCCCとイイカンジに対応する.
ここではcategory with attributesを使った解釈を使うことにする.

すると上で導入したsyntaxはLCCC(cwa)でいい感じに解釈できる.

  • contextはobject, contextΓのtypeはΓ-cod morphismとみなす.
  • type Aをもつtermは, Aに対応するmorphism(shift)のsection.
  • substはmorphismとみなす.

以上の対応で, 上のsyntaxはcwaの構造で超いい感じになる.

  • function typeはPi-typeを使って定義するので一旦忘れる. (論文にあるようなcwaを構成するとdependent product/sum, extensional identity typeを持つ)
  • substidはidentity, 合成はcompositionになる.
  • shiftはcwaのcanonical projection operatorになる.
  • 代入された項M[s](M:Γ → Γ,A, s:Γ'→Γ)はpullbackΓ'×Γ,A[s]overΓのUMPから誘導されるmorphism
  • extension<f,M>はpullbackの対角線にあたるmorphism(Mとfのliftを合成する).
  • 1=<id,id>はpullbackのUMPからつくる.

Set model

上のだけだとよく分からないのでSetで解釈する.

  • shiftはshift写像<gi,a:A> ~> <gi>
  • termはこのsectionなので, A型の値の追加, <gi> ~> <gi,a:A>になる. これはa:Aと同一視できる.
  • 代入項に登場するpullbackはΓ'×Γ,A[s] = {(gi', gi, a) | s(gi')=gi, a=M} = {(gi',M)}と同一視できる.
  • よってM[s]<gi'> ~> (<gi'>,M)とみなせる.
  • extensionは<f,t:A> = ↑*f . t ; <gi'> ~> <gi',t> ~> <f(gi'),t>になる.

特に特徴的なのはextensionの拡張で, fによる変換をtで拡張したもの, i.e. fの変換に加えてtの値を写像に追加するものと考えることができる.
extensionっぽさがあってとてもよい.

余談

もともとML type theoryのcwaでの解釈の話を調べていてvar-free syntaxが出てきたので何かしら関係はあるのだろうと思っていたけど, ちゃんと直感的にいい感じに対応していて超すっきりした.

ついでに, 普通のλ計算とvar-freeなλ計算の変換を具体的に構成したい.
さらに気が向いたらproof formalizationもしたい.

参考文献