この記事の精神に基づいて、依存型のラムダ計算を実装しました。公理。ただし、より複雑なことを行うために誘導型を追加したいと考えています。
その方法は2つ考えています
私はどちらの方法も好きではありません。最初のものはレベルが低すぎて、高級言語からコア言語に変換するのにかなりの労力が必要です。2 番目の方法は、複雑な帰納型の再帰原理の生成には多くのコーナー ケース (正/負の発生) があるため、非常に手間がかかり、エラーが発生しやすくなります。
これはどのように行うことができますか？タイプは、Coq、Agda、Idris などの既存のシステムでどのように実装されていますか?
申し訳ありませんが、イドリスについては知りません。
Agda については、Ulf Norell Phd Thesisを出発点としてお勧めしますが、システムはその後進化しました。
Coq はリストに 3 番目の箇条書きを導入します: 自動生成された述語です。your_type_rect各帰納型には、ユーザーに対して自動的に定義され、your_type_recとyour_type_ind(特別な場合は後者のみ)という名前の 3 つの (特殊な場合には 1 つ) の帰納スキームが付属しています。これらは言語の実際の用語であり、ユーザーのために自動的に生成され、induction戦術によって使用されます (最後の用語については 100% 確信が持てません)。公理ではありません。
実際、この自動生成をシャットダウンして、誘導スキームを自分で書くことができます。
に関するいくつかのドキュメントは、こちらinductionにあります。Coqメーリングリストで質問することをお勧めします.Coqメーリングリストでは、開発者がCoqの内部についてより多くの洞察を得ることができます.
ベスト、V.