論理式と方向

いつもの Agda の話題ですが、論理式には方向がない 例えば、

　a = b

と書いてあっても、a が出力とか b が入力とかない。一方で、関数(λ式)には方向がある

λ x → y

では x が入力で、y が出力になります。

Agda だと、数学的構造は record や data で書きます。record は積で and でつながったもの、data は排他的論理和で case 文の集合みたいな感じ。

で、Agda の library とかを見ると、record Hoge と record IsHoge とかが組で出てる。良くわからなかったんだけど、どうも、

record Hoge ( input : InputType ) where
field
output : OutputType
isHoge : IsHoge input output

record IsHoge ( input : InputType ) (output : OutpoutType ) where
field
property : ppro inupt output

みたいに使うらしい。filed は名前と型、つまり、名前の付いた変数とか論理式が来るわけですが、record の引数は入力、field には出力、つまり、その数学的構造で存在が主張されるものを列挙します。例えば、有界な実数の集合には最大値にになる極限が存在して上界というとか、そんなの。

その入力と出力は数学的構造の性質(公理)が要求されるわけですが、それらは論理式なので方向性はない。それを IsHoge にわけて書くという方式らしい。

こうすると、

lemma1 : (input : InputType) → Hoge input → ...
lemma1 input hoge = ...

とすると、Hoge i での IsHoge の性質が使えるようになる。つまり、

∀ input → ∃ output such that IsHoge input output

というわけ。Hoge の存在を示す時には、

lemma2 : (input : InputType ) → Hoge input
lemma2 input = record { output = ... ; isHoge = record { property = ... } }

という風にするらしい。なるほど。

で、今までにやった圏論(クライスリ圏とかLimitとか)を、これにそって書き直したんですが...

　　仮定が余計とか、仮定が足りないとか

が若干でて、少しはまりました。一通り書き直して、だいぶ、見通しが良くなったみたい。普遍問題では入力は圏A,Bと関手Uで、それがUに対するLimitの存在につながるとか、ちょっとあやふやだったところが理解できたみたい。形式大事だな。

IsHoge のみで書くことも可能で、初期の頃のはそういう風に書いていて、必要なものは module input に書くとかしてたみたい。楽なんだけど、

Hoge → Fuga

みたいにならないで、

(x y z : ...) IsHoge x y z ... → IsFuga x w q

とかで、 x y z とかの仮定にいろいろ余計なものが入ったり、うっかり書きそびれたりしていたようです。

Programming 的には Hoge が interface で、IsHoge が実装だと言えないこともないかな。