2009-07-15 [長年日記]
λ. “Observational equality, now!” by Thorsten Altenkirch, Conor Mcbride, Wouter Swierstra
Thorsten Altenkirch らの Observational equality シリーズ最新作、といっても2007年のだけど。
通常の内包的型理論で何かやろうとすると、propositional equality が関数の外延性 (∀x. f x = g x) ⇒ f = g を満たさないために、いろいろ面倒なことになる。一方で、外延性を単純に公理として追加すると、canonical form に簡約出来ない閉項が出てきてしまう。 また、propositional equality から definitional equality を導くことを許す外延的型理論では、関数の外延性は成り立つが、definitional equality の判定が決定不能になるので、型検査が決定不能になってしまう。 まとめると、以下の三つの性質を同時に満たす型理論はこれまでなかった。
- propositional equality が関数の外延性 (∀x. f x = g x) ⇒ f = g を満たす
- 閉項はその型の canonical form に簡約出来る (canonicity)
- definitional equality (≡) と型検査が決定可能
この問題を解決しようとする著者らのアプローチが observational equality を用いる observational type theory (OTT)。基本的には等号をすべての型に対して一様に定義するのではなく、値の振る舞いに着目した等号を型の構造に応じて定義していく。 例えば、関数型A→Bだったらすべての引数に対する値が等しいことによって定義するとか。
ただ、それだけではうまくいかなくて…… (省略)
著者らの前の論文 Towards Observational Equality からの大きな変化としては以下の二つ。
- 通常の型の世界(set)と命題の世界(prop)の明確な分離
- Type-directed quotation による definitional equality の拡張
通常の型の世界(set)と命題の世界(prop)を明確に分離し、setでの計算にpropから影響を与えられるのは矛盾を導けたときだけであることを示している。それによって、矛盾しない限りpropには幾らでも規則を追加出来るようになる。それによって、これまでのややこしかった構成が非常に簡単になっているように思える。
また、型主導で canonical form (やボックス)への置き換えを行う Type-directed quotation を用いて definitional equality を拡張し、命題を proof irrelevant にしている。 これにより、S≡T implies (s[Q:S=T〉 : T) ≡ (s : T) が成り立つようになり、definitional equality が成り立つ型の間での型変換が無視できるようになる。 それによって、これまで懸念だった、帰納的データ型をW-Typesにエンコードする場合の問題が解決する。
Agda2上への実装が示されていて、分かりやすかった。
