11/11/13 15:44:37.16
Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね
論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど
再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか
そういうのはよくわからない・・・
せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい
::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども