Coqスレat TECHCoqスレ - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト119:デフォルトの名無しさん 11/11/13 15:44:37.16 Coq'Artの14章あたりにもある程度載ってるんだけども形式的な説明というわけでは無いね 論理や集合論の命題と型付きラムダ計算の式が1対1対応するっていう性質を使ってるってことは聞くけど 再帰型の定義が計算体系に及ぼす影響が対応する論理体系にどういう影響与えるかとか そういうのはよくわからない・・・ せいぜい構築子の無い型の値を仮定するのとFalseぶち込むのが対応してどちらも滅茶苦茶になるとか、そういうのぐらい ::=はiffに対応するとか|は排他論理和に対応するんだなぁというのは経験則でみえてくるけども 120:デフォルトの名無しさん 11/11/13 19:01:45.89 ×型付きﾗﾑﾀﾞ計算の式 ○型付きﾗﾑﾀﾞ計算の型 121:デフォルトの名無しさん 11/11/19 09:32:29.84 >>118 構造的帰納法に関しては俺はTAPLで勉強したな。あの本は丁寧で わかりやすい。 122:112 11/11/21 12:32:03.21 >>119-121 いろいろと情報提供ありがとうございます。いまはCoq'Artの14章で奮闘中です。もともと英語が苦手 なのですが、贅沢は言ってられません。TAPLって、Benjamin C. Pierceの「Types and Programming Languages」のことですよね。あたってみます。（砕けたりして。トホホ） 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch