variable-free type theoryの圏論的な解釈について
の続き. いくつか疑問が解消されたのでそれについて.
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を持つ) - subst
id
は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もしたい.
参考文献
- https://ncatlab.org/nlab/files/CurienGarnerHofmann.pdf variable-free syntaxの出処
- http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.4410 category with attributesによる解釈
- http://iso.mor.phis.me/archives/2011-2012/stage-2012-goteburg/report.pdf extension, shiftの記法や圏論での解釈のアイデアは主にここから