11/11/11 16:16:46.14
Inductiveな型TからT_rectが生成される原理がどうしてもわからないなあ。
誰か教えてちょーだいな。
113:デフォルトの名無しさん
11/11/12 05:51:58.15
#coq #inductive
>>112 例えば nat_rectならFixpointでも定義できるよ。
Variable P : nat -> Type.
Axiom fO : P O.
Axiom fS : forall n, P n -> P (S n).
Fixpoint nat_rect' n : P n :=
match n with
| O => fO
| S m => fS m (nat_rect' m)
end.
114:112
11/11/12 12:04:00.72
nat_rectぐらいなら、数学的帰納法なんてなじみがあるからなんとなくわかるけど、
例えば
Inductive sand (A B : Set) : Set :=
sconj : A -> B -> sand A B.
から作られるsand_rectなんかは、
sand_rect =
fun (A B : Set) (P : sand A B -> Type)
(f : forall (a : A) (b : B), P (sconj A B a b)) (s : sand A B) =>
match s as s0 return (P s0) with
| sconj x x0 => f x x0
end
: forall (A B : Set) (P : sand A B -> Type),
(forall (a : A) (b : B), P (sconj A B a b)) ->
forall s : sand A B, P s
となって、わかりそうなわからなそうな。上記のSetをPropにかえるともうお手上げ。
いったい何を理解すればいいのやら。どうか神様教えて。
115:デフォルトの名無しさん
11/11/12 12:39:28.72
>>114 nat以外のものも構造的帰納法を表しているだけ。
X_rectのたぐいは自作する必要はないから、関数定義は理解できなくても
型だけわかれば、使えるからそれで いいと思う。
このX_rectがどのように自動生成されるか、Coqの内部のアルゴリズムが
知りたいならば少し勉強が必要かもしれないけれど、普通に使う分にはいらないでしょ。
116:112
11/11/12 16:10:50.99
>>115
ということは、構造的帰納法について、私が理解している以上に何か深いこと、
あるいは、もっと詳しいことがあるということでしょうか。論理式の定義に従って
帰納的に何かを証明するとか、そんなことは何の苦もなく理解してきましたけど、
上記>>114のsand_rectなんぞは、なぜそうなるのかいまひとつわからないのです。
また、sandの定義中のSetをPropにかえたものをpandとすると、pand_rectは
sand_rectのSetをPropにかえただけのものとは異なります。ますますわかりません。
もし構造的帰納法について詳しく書かれた文献等あったらご紹介いただけないで
しょうか。
117:112
11/11/12 20:54:41.74
少しだけわかってきました。sand_rectの型の部分がそうなりそうな気もしてきました。
すると、本体（t:Tにおけるtのこと）がなぜそのように構成されるのか、という疑問に
なりますが、それは半分は発見的経験的に考えないといけないのでしょうか。
また、pand_rectに関しては、sand_rectの(P : sand A B -> Type)の部分が
なぜか(P : Type)になっている。つまりsand_rectにあるPはsand A Bを引数にとってたのに、
pand_rectにあるPはpand A Bを引数にとらなくなっている。
これさえ認めればsand_rectとpand_rectの違いは説明できます。これはなぜなんでしょう？
118:112
11/11/13 09:55:45.41
少しずつわかってくるにつれて、Coqとは直接関係ない気もしてきたのですが、
どなたか教えてくださるか、もしくは良い文献の紹介等していただけないで
しょうか。
自然数の定義を例に話します。
（１）Oを自然数とする。
（２）nを自然数とするとき、S nも自然数とする。
（３）上記（１）（２）によって定められるもののみを自然数とする。
といった具合に自然数を定義することができますが、この（３）をどのように
形式的に表すかをもっと詳しく理解すれば、私の疑問が解けるような気がしてき
ました。
どうか偉い方々、よろしくお願いいたします。
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」のことですよね。あたってみます。（砕けたりして。トホホ）
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の翻訳がとりあえず最後まで終わりました！
というわけでお願いなのですが、読んでください。
で、誤字脱字誤訳など指摘頂けると助かります。