[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 49 (1002ﾚｽ)
上下前次1-新
抽出解除 必死ﾁｪｯｶｰ(本家) (べ) 自ID ﾚｽ栞 あぼーん
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
984(2): 2020/04/15(水)13:06 ID:/g+JzMtk(1/9) AAS
>>983
＞証明支援言語Coqが正しいことを、だれがどうやって保証しているのか？
Coqの正当性をCoqで検証すればいいんじゃね？
985(1): 2020/04/15(水)13:10 ID:/g+JzMtk(2/9) AAS
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org
987(1): 2020/04/15(水)13:13 ID:/g+JzMtk(3/9) AAS
>>984
具体的に説明するか
Coq証明系の存在証明をCoqで書いて
プログラムとして抽出すればいいってこと
カリー＝ハワード同型対応
外部ﾘﾝｸ:ja.wikipedia.org
988(1): 2020/04/15(水)13:15 ID:/g+JzMtk(4/9) AAS
>>986
抽出されたプログラムにもう一度証明を食わせて
同じプログラムが抽出されればOK
992(1): 2020/04/15(水)13:25 ID:/g+JzMtk(5/9) AAS
>>989
漫然とインプットデータといわれても困る
公理や定理の式が正しいとして、証明が間違っていたら？ということはない
公理や定理の式が間違っていたら？ それは検証系で検査できることではない
プログラム検証のV&Vで、
後のV(verification 検証)は機械的にできるが
前のV(varidation 妥当性確認）は機械で実施するものではない
省1
994(1): 2020/04/15(水)13:27 ID:/g+JzMtk(6/9) AAS
>>992
誤 varidation
正 validation
996: 2020/04/15(水)13:30 ID:/g+JzMtk(7/9) AAS
>>993
そもそも、理論として出来上がっているかどうかが疑問視されているなら
Coqへの実装は無意味ではないだろう
997: 2020/04/15(水)13:31 ID:/g+JzMtk(8/9) AAS
>>995
もちろん、すぐにはできないが、やらない言い訳はないな
998(1): 2020/04/15(水)13:39 ID:/g+JzMtk(9/9) AAS
>>990
Coqによる検証でも、人間によるテストを全部無くすことはできないが
「人間の証明を、人が再チェックして、確認する」
とかいう機械排除の口実は全く存在しない
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.032s