日本ソフトウェア科学会第 32 回大会 (2015 年度) 講演論文集

Homotopy Type Theory によるパッチ理論の拡張
佐藤善紀

三好博之

本発表では C. Angiuli，E. Morehouse，D. R. Licata，R. Harper によって行われた Homotopy Type Theory(HoTT) による Darcs スタイルのパッチ理論の定式化を複数ファイルからなるリポジトリの場合に拡張する．複数ファイルに拡張する際のポイントとなるのは，単一ファイルの場合と異なりファイル名（識別子）とファイルの内容を明示的に区別する必要があることである．パッチを適用する対象が複雑になっても，identity type があることによりその対象についてのパッチという概念が容易に定義できることを示す．

ができる，すなわち可逆である．パッチを基礎として

1 はじめに考えると，Darcs ではリポジトリをパッチのシーケン

近年ソフトウェアの大規模化に伴い，ソフトウェスの結果と見なすことが出来る．何らかの形式的枠組

ア開発の多くの現場でバージョン管理システムが使みをもちいてリポジトリやパッチを表現し，パッチをわれようになっている．バージョン管理システムは，基礎として構築されたバージョン管理システムの形式ファイルの変更記録を管理するためのシステムであ化はパッチ理論と呼ばれる．

り，ファイルについてどのような変更をしたか，新し

一方で 2006 年前後に，ホモトピー論と Martin-Löfいファイルを作成したか，存在するファイルを削除しtype theory の間に密接な関係があることが発見さたか，などの変更に関するすべての情報をリポジトれ，Homotopy Type Theory (HoTT) と呼ばれる新リと呼ばれるデータベースに保存する．このリポジ

しい分野が生まれた [1]．例えばホモトピー論で扱う，

トリによってバージョン管理システムはファイルを特空間 X ，空間 X の点 a，b，空間 X 内の a から b へ定の過去の状態に戻すことや，ファイルの異なる複数のパス p をそれぞれ type theory の，type X，type Xのバージョンを管理することなど多くの機能を提供の項 a，b，identity type の項 p : a =X b に対応させする．

ることができる．実際，Martin-Löf type theory の

本発表ではバージョン管理システムの一つである

任意の type 上の identity type 全体は ∞-groupoid

Darcs について形式化を考える．Darcs では パッチ構造（weak higher category の特別な場合）を持ちとはリポジトリの内容の変更を意味する．例えばファ[2] [3]，一方で ∞-groupoid 構造はホモトピー論におイルの内容を編集したり，新しいファイルを追加したいて空間を分類する．HoTT はホモトピー論と higher

り削除したらリポジトリの内容は変更されたことにcategory theory を踏まえた上で，このような対応関なる．また Darcs ではパッチの処理は元に戻すこと

係に基づいて，Univalence Axiom (UA) と higher in-An extension of a patch theory in homotopy typetheory.
Yoshinori Sato, 京都産業大学大学院理学研究科, Divisionof Science, Kyoto Sangyo University.
Hiroyuki Miyoshi, 京都産業大学理学部数理科学科, Dept.
of Mathematics, Kyoto Sangyo University.

ductive types (HIT) により Martin-Löf type theoryを拡張したものである．

C. Angiuli，E. Morehouse，D. R. Licata，R.
Harper は，パッチに identity type の項すなわち空間内のパスを対応させることで，リポジトリ内にファイルが単一の場合の Darcs のパッチ理論を HoTT を用

以下，等号の添字は自明な場合には省略する．

いて定式化した [4]．本発表ではこの研究を踏まえて，さらに恒等パス，パスの逆，パスの合成などのパさらに現実的な開発モデルに近付けるためリポジトリスの演算を定義することが出来る．つまり，空間のに複数のファイルが存在する場合の定式化を与える．

各点 a から型 a = a の項を作ることができ，その項を refla で表し恒等パスだと解釈する．同様に任意

2 パッチ理論の点 a から点 b のパス p に対応する項を p : a = b とリポジトリとは，ディレクトリ，ファイル，ファイし，p の逆向きのパスを考えると型 b = a の項を作る

ルの中身が集まったものである．このリポジトリを形ことが出来て，その項を !p と表す．任意の２つの項式的に変更するのをパッチと呼ぶ．各パッチにはパッp : a = b と q : b = c から，型 a = c の項を作ること

チが適用できるリポジトリを表す domain と，パッができ，その項をパス p と q の合成に対応するもの

チを適用した後のリポジトリを表す codomain を持と見なして q ◦ p と表す．これは Martin-löf 型理論でつ．例えばあるファイルを消去するパッチはリポジ推論できる事実と整合性がとれている。

トリにそのファイルが存在しないと適用できないか

そのように考えてホモトピー論のモデルにおいて成ら，domain はそのファイルが存在するリポジトリでり立つ事実を、型理論に取り入れたものが Homotopyある．また codomain はそのファイルが存在するリポType Theory である。具体的には新たに導入されジトリになる．

たのは Univalence Axiom (UA) と higher inductive

リポジトリにパッチを適用してもリポジトリを変化

types (HIT) である。前者は各型階層で、identityさせないパッチを no-op パッチと呼ぶ．これはパッチ操作の単位元である．さらにここで考えるパッチ理論

type と依存型を用いて 2 つの型のホモトピー同値が∼ (A =∼ B)型として定義できることを用いて、(A = B) =ではすべてのパッチは可逆であるという性質を持つとという型として表される公理である（同値関係 ∼=はする．つまりパッチを p とすると undo パッチ!p がそれぞれ適切な型階層に属するとする）。

存在し，パッチ p を適用した後に undo パッチ!p を

後者は空間における点と経路に関する帰納的定義

適用するとリポジトリは元の状態のままである．さらを可能にするために導入された機構である。パッチ理に，一般化して undo パッチ!p を適用した後にパッ論を定式化する際にはこの拡張された部分が主要な

チ p を適用することもできてリポジトリは元のまま点で用いられている。通常の帰納法では，自然数ならであるとする。これによりパッチ全体を groupoid とば二つの generator，zero : Nat と succ : Nat→Nat にみなすことが出来る．

よって帰納的に定義できる．この様に inductive typeは generator によって帰納的に定義される．Higher

3 ホモトピー型理論

Inductive Type は generator として点だけでなく，一Homotopy type theory (HoTT) の基本となる考え

つ次元が上の path も含める事により inductive typeは Martin-löf 型理論をホモトピー論によって解釈すを一般化したものである．

るということである．
型理論の型 A をホモトピーの空間 A，また型 A の項 a を空間 A の点 a だと解釈する．全ての型 A と4 単一のファイル（を持つリポジトリ）に関するパッチ

項 a，b について identity type a=A b が存在する．こC. Anguiuli et al. による 1 つのファイルに行を追の identity type の項 p : a=A b を点 a から b へのパ加したり削除したりする抽象的なパッチの定式化はスだと解釈する．さらに a=A b は型であるから，こ以下の様なものである．まず m 行のファイルから nの型の任意の項 p, q : a=A b についても identity type

行のファイルへの変化を考える．任意のファイルの変p=a=A b q が存在する．この型 p=a=A b q の項がパス p

化は，ファイルの特定の場所に 1 行を追加する操作からパス q へのパス，つまりホモトピーに対応する．

(パッチ)ADD_@_::_と特定の場所の 1 行を削除する操作（パッチ）RM_::_の繰り返しによって実現するこ

rmP :｛n : Nat｝ (l : Fin n+1)とが出来る．よってそのような操作の列（シーケン(h:History 0 n+1) → doc h = doc (RM l::h)ス）をパッチヒストリー Histroy m n と呼ぶ．同じ

ここで doc h はヒストリー h から生成されるファ変化を実現するヒストリーは複数ありうる．よってそイルを表す型である．のような History を同一視することにより抽象的なHistory の定義と同様に，抽象化されたパッチをパッチという概念を定式化することが出来る．これは適用する順番を交換したとき行番号を調整すればパッ

実際には次のように同一視を考慮した HIT (quotientチを同一視出来る，ということを表す高次のパスは以higher inductive type) によって定義できる．

下の様に表現される．

space History : Nat → Nat → Type where

addP-addP-＜ :｛n : Nat｝ (l1 : Fin n+1)[] : History m n(l2 : Fin n+2) (s1 s2 : String)

ADD_@_::_ :{m n : Nat}(s : String)(h : History 0 n) → l1 ＜ l2 →(l : Fin n+1) →PathOver (x.doc h=doc x) ADD-ADD-＜

History m n → History m n+1(addP s1 l2 ◦ addP s1 l1)

RM_::_ : {m n : Nat}(l : Fin n+1) →(addP s1 l1 ◦ addP s2 (l2-1))→ History m n+1 → History m n

addP-addP-≥ :｛n:Nat｝ (l1:Fin n+1)

ADD-ADD-< : {m n : Nat}(l1 : Fin n+1)

(l2 :Fin n+2)(s1 s2 : String)(l2 : Fin n+2)(s1 s2 : String)(h:History n) → l1 ≥ l2 →(h : History m n) → l1<l2 →PathOver (x.doc h=doc x) ADD-ADD-＜

ADD s2 @ l2 :: ADD s1 @ l1 :: h)(addP s1 l2 ◦ addP s1 l1= (ADD s1 @ l1 :: ADD s2 @ (l2-1) :: h)(addP s1 (l1+1) ◦ addP s2 l2

ADD-ADD- ≥ : {n : Nat}(l1 : Fin n+1)
(l2 : Fin n+2)(s1 s2 : String)

addP-rmP，rmP-addP，rmP-rmP についても同様に定義できるので省略している．

(h : History m n) → l1 → l2 →ADD s2 @ l2 :: ADD s1 @ l1 :: h)

5 複数のファイルを持つリポジトリ= (ADD s1 @ l1+1 :: ADD s2 @ l2 :: h)

この節では複数のファイルの集まりすなわちリヒストリーの同値関係を定義するためには 2 つの操

ポジトリに対するパッチを考える．前節と同様に作の組み合わせとして ADD-ADD 以外にも，RM-ADD，History m n を m 行のファイルに適用でき，n 行のADD-RM，RM-RM も定義する必要があるが，同様に定ファイルにするパッチのシーケンスの型とする．パッ

義できるのでここでは省略している．

チシーケンスはパッチがどのように合成されてきた

空ファイルに適用できるヒストリー，つまり型かを辿ることが出来るからパッチヒストリーと呼ぶ．

History 0 n の要素は一意的にファイルを決定する．

History 0 n の項は 0 行のファイルつまり，空ファ

このようなヒストリーは，ファイルの空間のパス，すイルに適用できて n 行のファイルにするパッチヒス

なわち identity type で表現される抽象化されたパットリーである．このパッチヒストリーは一意にファイチの context（その抽象化されたパッチが適用できるルを決定するからパッチヒストリーはファイルだと見ファイルを特定するヒストリー）と考えることが出なせる．ここまでは前節と同様の議論である．

来る．

space R : Type where

ここで，複数のファイルを持つリポジトリにファイルを追加するリポジトリパッチとファイルを削除する

doc :｛n : Nat｝→ History 0 n → Rリポジトリパッチを考える．さらに同一ファイルの内addP :｛n : Nat｝(s : String) (l : Fin n+1)

容を変更するパッチを別に扱うことも考えられるが，(h:History 0 n) → doc h = doc (ADD s@l::h)

ここではそれは一旦ファイルを削除してから新たにファイルを追加すると考えて単純化する．
複数のファイルを持つリポジトリ内のファイルには名前（識別子）が必要である．なぜなら同一内容でrmf : (d : D) → (RD : Rep)
→ doc RD = doc(f-set-minus d RD)
さらに addf-addf，addf-rmf，rmf-addf，rmf-rmf，ファイル名が異なるファイルが存在しうるからであを用いた同値性も，同名のファイルの有無によって場る．ここでは議論を単純にするために名前として自然合分けすることにより，高次のパスを用いることに数を用いると名前付きのファイルの型は依存和を用いよって検証が可能であると思われる．て Σ(n : Nat) R と表せる．簡略化のためにこの型を D と呼ぶことにする．つまり名前が付いたファイ6 結論と展望ルを d とすると d : D である．

本発表では複数のファイルを持つリポジトリに対次に複数のファイルを持つリポジトリの型 Rep をするパッチも単一ファイルと同様に定式化することを定義する．Σ 型の要素はペアなので，リポジトリを示した．今後は単一のファイルの時の実装への翻訳

名前付きファイルのリスト（もしくは有限集合）と考interp や複数のパッチのマージ merge について議論えることにより，名前付きファイルをリポジトリに追し，Agda において検証を行いたい．本稿では UA は加する関数 f-set-plus と，リポジトリから名前付き直接は現れなかったが，interp を議論するときにはファイルを削除する関数 f-set-minus はリスト操作本質的にその解釈が重要になる．と場合分けを用いて容易に定義できる．するとリポジトリの型は以下のように定義できる．

space Rep : Type where[] : Rep

7 謝辞
本研究は JSPS 科研費 23320008 の助成を受けている．

f-set-plus : D → Rep → Rep
f-set-minus : D → Rep → Rep

参 考 文 献以上からリポジトリに対するパッチ理論は以下のよ[1] IAS Project, Homotopy Tyep Theory, 2014.
[2] P. L. Lumsdaine “Weak ω-category from intensional type theory, Typed lambda calculi and applications, 6:1-19,2010.
[3] B. van den Berg and R. Garner, “Types are weak
ω-groupoids, Proc. of the London Mathematical Society, 102(2):370-394, 2011.
[4] C. Anguiuli, E. Morehouse, D. R. Licata and R.
Harper, “Homotopy Patch Theory (Expanded Version)“, Proc. of ICFP2014, 2014.

うに同一視を考慮した HIT を用いることにより ARep
上の identity types をパッチとして定義できる．

space ARep : Type where
doc : Rep → ARepaddf : (d : D) → (RD : Rep)
→ doc RD = doc(f-set-plus d RD)