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」のことですよね。あたってみます。（砕けたりして。トホホ）
123:デフォルトの名無しさん
12/02/10 07:07:56.25
URLﾘﾝｸ(proofcafe.org) に日本語訳を上げて下さっている方の書き込みがあったので、ここに書いておきます。
一部訳に打ち間違いがあります。どこに言ったら良いのかわからないので、ここに書いておきます。
URLﾘﾝｸ(proofcafe.org)
の[マップ（Map）関数]のちょっと上に「理宇土」とあります多分「リスト」の誤変換だと思います。
この訳のお陰で大変楽して勉強できてます。ありがとうございます。
124:デフォルトの名無しさん
12/02/10 09:10:05.55
URLﾘﾝｸ(proofcafe.org)
の
rememberタクティック
のちょっと前に「なるべくintrosを使うタイミングを送らせ」の「送らせ」は「遅らせ」だと思います。
よろしくお願い致します。
訳ありがとうございます。
125:デフォルトの名無しさん
12/02/10 09:35:05.24
報告するならgithubのissue tracker
URLﾘﾝｸ(github.com)
か
wikiの専用ページ
URLﾘﾝｸ(www16.atwiki.jp)
でやるほうがいいと思うよ
126:デフォルトの名無しさん
12/02/10 17:57:06.05
>125
ありがとうございます。そっちに書いときます。
127:デフォルトの名無しさん
12/02/11 16:49:49.67
うわーはずかしいtypo。直しておきます。レポート感謝。
128:デフォルトの名無しさん
12/02/16 10:19:23.91
0 と 1 だけのタイプを作りたいと思い
Inductive my : Type := O : my .
my is defined
my_rect is defined
my_ind is defined
my_rec is defined
は上手く動作するのですが
Coq < Reset my.
Coq < Inductive my : Type := O : my | 1 : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | 1 : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
Coq < Inductive my : Type := O : my | (S O) : my .
Toplevel input, characters 32-33:
> Inductive my : Type := O : my | (S O) : my .
> ^
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
となって上手く定義できません。どうやれば 0 と 1 だけのタイプを定義できるんでしょうか。
129:デフォルトの名無しさん
12/02/16 13:24:10.57
Inductiveで列挙するのはコンストラクタの名前とその型。
値を並べられるわけではない。
130:デフォルトの名無しさん
12/02/16 22:24:41.28
1を名前に使えない
Inductive my : Type := O : my | one : my .
ならいい
131:デフォルトの名無しさん
12/02/18 11:13:09.87
O(:nat)もコンストラクターなんじゃない？
132:デフォルトの名無しさん
12/02/26 23:56:37.37
なんか >>60 が変な扉を開いてしまったかもしれない。
「関数型ガール」
URLﾘﾝｸ(www16.atwiki.jp)
133:デフォルトの名無しさん
12/03/09 10:10:41.05
>129
>130
>131
>132
回答ありがとうございます。
134:デフォルトの名無しさん
12/03/09 10:17:33.18
O を起点として
O と (S O) だけの Typeとか
O と (S O) と (S (S O)) だけの Type とか
O と (S O) と (S (S O)) と (S (S (S O))) だけのTypeとか
...
を作りたかったのですが、そうするにはどういうコマンド入れたら良いのでしょうか>
レベル低い質問ですみません。
Inductive my : Type := O : my | S : my -> my.
こうしちゃうと O と (S O)だけじゃなく (S (S O))も myタイプになってしまうのでどうしたらよいのかわかりません。
135:デフォルトの名無しさん
12/03/09 10:57:54.37
>>134
証明を引数として取るコンストラクタを使うとか
Require Import Arith.
Inductive my (n:nat) : Set :=
| myO : my n
| myS a : a <= n -> my n.
Section my1.
Let my1 := my 1.
Definition my1_0 : my1 := myO 1.
Program Definition my1_1 : my1 := myS _ 1 _.
End my1.
136:デフォルトの名無しさん
12/03/09 23:40:56.06
Inductive Fin : nat -> Type :=
| FinO n : Fin (S n)
| FinS n : Fin n -> Fin (S n).
というのをcoq-clubで見た。
137:名無しさん
12/03/15 01:21:22.24
ネット務
138:デフォルトの名無しさん
12/03/20 10:49:54.36
>>135
>>136
ありがとうございました。
またやってみます。
139:デフォルトの名無しさん
12/04/19 09:20:01.83
Software Foumdationsの翻訳がとりあえず最後まで終わりました！
というわけでお願いなのですが、読んでください。
で、誤字脱字誤訳など指摘頂けると助かります。