はじめてのCubical

HoTT

Thierry Coquandたちが、univalenceと両立する、dependent type theoryの新しいcomputationalなmodelを作ったと言っている
A model of type theory in cubical sets
http://www.cse.chalmers.se/~coquand/mod1.pdf

これを実装した処理系は
Implementation of Univalence in Cubical Sets
https://github.com/simhu/cubical
に置いてある。適当にcabal installとかすればインストールできる


#新しい処理系なので、若干の仕様変更により、ここに書いたコードは、そのままでは動かなくなっているっぽい。面倒なので修正はしない


細かいことはわたしもよく分かってないけど、今までHoTT(homotopy type theory)というのは、机上の空論だったわけだけど、(Coquandたちが間違ってなければ)これは人類史上初のHoTTの処理系ということになる(このようなモデルは他にもあることは否定されてないので、また挙動の違う別のHoTT処理系が存在しうるかもしれないが)。

#univalenceが成立するということは、functional extensionalityが成立するということで、今まで、そういうtype theoryを作るというのは、色んな人が苦心してきた問題であるので、大きな前進と言える

#quotient typeも作れる

#HoTTから現れたもう一つの新しい概念であるhigher inductive typeについては、現時点では実装されてない


ホモトピー論では、simplicial setというものがよく使われるけど、cubical setというのもあるらしく(今回初めて聞いた)、多分それと関係するのだけど、cubical setの定義は、上の論文にホモトピー論と無関係に与えられている。まぁ、今のところ、これで何でうまくいくのか、理論的なdetailは理解できてない


使用しているtype theoryは
A simple type-theoretic language: Mini-TT
http://www.cse.chalmers.se/~bengt/papers/GKminiTT.pdf
というのを、ほぼそのまま使っているっぽい。これもよく分からないけど、"Mini-TT is a step towards a simple and definitive core language for the proof-assistant Agda based on versions of Martin-Lof Type Theory"とか書いてあるので、何かそういうもんらしい


上のHoTT処理系(便宜的にcubicalと呼んでおく。普通にcabalでinstallすると、cubicalという実行ファイルが得られるので)は実用に使うようなものではなく、あくまで論文の参照実装という位置づけだと思うので、使いやすくはない(CoqやAgdaを実用で使ってるぜって人がいたら、おもちゃみたいなもんだと思う)。マニュアルとかもないけど、syntaxは若干Agdaっぽい(というか、Haskellっぽいと言うべきか)


まず初歩的な例として、こういうの↓を書いて、test.cubとして保存して、cubical test.cubとか打って、File loaded.とか言われれば成功

module test where

-- identity function
id : (A:U) ->A ->A
-- id A x = x
id = \A x -> x

-- S combinator
S : (A B :U) -> A  -> (A->B) -> B
S A B a f = f a

Nat : U
data Nat = zero | succ (n:Nat)

add : Nat -> Nat -> Nat
add = split
  zero -> \y -> y
  succ n -> \y -> succ (add n y)

List : (A:U) -> U
data List A = nil | cons (a:A) (b:List A)

foldr : (A:U) -> (B:U) -> (A -> B -> B) -> B -> List A -> B
foldr A B k z = split
  nil -> z
  cons y ys -> k y (foldr A B k z ys)

このコードにはcubical特有のことは何もないので、何をやってるかは、CoqやAgdaを使ったことあれば分かるはず。Uは多分UniverseのUで、CoqのTypeみたいなもんと思う(SetとかPropはない)。cubicalでファイルを読み込むと、プロンプトが出るので、add zero zeroとかすれば、zeroと評価される



cubicalらしいこととして、
Observational Equality, Now!
http://www.cs.nott.ac.uk/~txa/publ/obseqnow.pdf
の1.1にextensionality lawを手で入れると、canonicityが壊れるよ！という例が書いてあるので、これをやってみる

module ott where

Id   : (A : U) (a b : A) -> U
Id = PN

refl : (A : U) (a : A) -> Id A a a
refl = PN

funExt : (A : U) (B : (a : A) -> U) (f g : (a : A) -> B a)
         (p : ((x : A) -> (Id (B x) (f x) (g x)))) -> Id ((y : A) -> B y) f g
funExt = PN

J : (A : U) (a : A) -> (C : (x : A) -> Id A a x -> U) -> C a (refl A a) ->
      (x : A) -> (p : Id A a x) -> C x p
J = PN


ext : (A B:U) (f g:A->B) (p : (x:A) -> Id B (f x) (g x)) -> Id (A->B) f g
ext A B = funExt A (\_ -> B)

subst : (A : U) (a b : A) (p : Id A a b) (T:A->U) -> T a -> T b
subst A a b p T d = J A a (\ x q -> T x) d b p

Nat : U
data Nat = zero | succ (n:Nat)

add : Nat -> Nat -> Nat
add = split
  zero -> \y -> y
  succ n -> \y -> succ (add n y)

id : (A:U) ->A ->A
id A x = x


add0 : Nat -> Nat
add0 n = add zero n

add0_eq_id : Id (Nat->Nat) add0 (id Nat)
add0_eq_id = ext Nat Nat add0 (id Nat) p
   where
      p : (n:Nat) -> (Id Nat (add0 n) (id Nat n))
      p n = refl Nat n

-- compare with "subst (Nat->Nat) add0 add0 (refl (Nat->Nat) add0) (\_ -> Nat) zero"
test : Nat
test = subst (Nat->Nat) add0 (id Nat) add0_eq_id (\_ -> Nat) zero

PNというのは、処理系に組み込まれてるってことだと思う(多分)。ott.cubを読み込んで、testをevalすると、これはzeroであることが分かる


だから何やねんという感じではあるけど、例えばCoqで同等のコードを

Definition idfun (A:Type) := (fun (x:A)=>x).
Definition add0 := plus 0.
Axiom ext :forall (A B:Type)  (f g:A->B) (p : forall(x:A),f x=g x) , f = g.
Theorem add0_eq_id : add0 = (idfun nat).
Proof.
   apply ext.
   auto.
Defined.

Definition subst (A:Type) (a b:A) (p:a=b) (T:A->Type) : T a -> T b.
   induction p.
   auto.
Defined.

とか定義して、

Eval compute in (subst (nat->nat) add0 (idfun nat) add0_eq_id (fun _=>nat) 0).

を見ても、0にはならない。一方、

Eval compute in (subst (nat->nat) add0 add0 (eq_refl _) (fun _=>nat) 0).

と対比すると、こっちは0になる。直感的には、この2つの式が等しくてもよさそうなものだけど、多分、Coqでは、(subst (nat->nat) add0 (idfun nat) add0_eq_id (fun _=>nat) 0)が0になることは証明できない(当然、0以外の値になることも証明できない)。Coqでも、univalence axiomを手で入れてやって、頑張って証明を書くと、これが0になることが証明できるのだと思う(書けた人は、教えてください)。冒頭で書いた別のモデルがありうるというのは、univalence axiomを仮定しても、こういうclosed termの値が全部決まるかどうか保証はない(Voevodskyは一意に決まると予想している)ということだと思う


あと、quotient typeが作れるってのは実用的に重要かもしれない。今までは、こういうのをSetoidとかで凌いでたんだと思うけど。quotient typeの例は、examples/quotient.cubに、Z/2Zの例が載っている。詳細は見てない