Coq のファーストクラス モジュールについて詳しく教えてくれる人はいますか? Coq のモジュールがファーストクラスではないことはわかっています。理由を知りたいのですが？将来、Coqのモジュールがファーストクラスになる可能性はありますか?
どうもありがとうございました
1 に答える
2
確かではありませんが、私が理解しているように、それは本質的に2つの点から来ています。
Coqは保守的です。その主なアプリケーションのいくつかは検証にあるため、Coq はほとんどの場合、セマンティクスが十分に理解されている構造に制限されています。
従属型の設定では、ファーストクラスのモジュールはかなりわかりにくく、完全には理解されていません。 特に、定義の計算/リダクションの動作をモジュールの外でどの程度可視化する必要がありますか? 何もない場合、これはレコード タイプとして既に利用可能です。しかし、リダクション動作の一部またはすべてが目に見える場合、その量を正確に定量化することは難しいため、結果として得られるモジュールのセマンティクスを分析することは非常に困難です。
私は関連文献の専門家ではないので、2については間違っているかもしれませんが、これが基本的な状況であるという印象を受けました.
于 2013-05-05T22:46:34.557 に答える