この質問とこのAgda バグ レポート/機能リクエストで説明されているものと非常によく似た、終了チェックに問題があります。

unionWith問題は、以下が終了することをコンパイラーに納得させることです。重複キーの結合関数を使用して、unionWithキーでソートされた (キー、値) ペアのリストとして表される 2 つのマップをマージします。有限マップの Key パラメーターは、マップに含まれるキーの (厳密ではない) 下限です。(このデータ型を定義する理由の 1 つは、AVL ツリーに関するさまざまなプロパティを証明するために AVL ツリーを解釈できるセマンティック ドメインを提供することです。)

参照された質問で説明されている解決策を私の設定に一般化することができませんでした。たとえばunionWith'、 と相互に再帰的に定義された補助関数 を導入すると、次の場合unionWithに後者から呼び出されます。k' < k

unionWith'次に、最初に欠落しているケースを の必要な呼び出しに置き換えて再帰的な結び目を結ぶとすぐに、unionWith終了チェックに失敗します。

追加のパターンも導入しようとしましたが、再帰呼び出しでwithの結果を使用する必要があるため複雑です。（終了チェッカーに役立たないように見えるcompareネストされた句を使用する場合。）with

withこのコンパイルを取得するためにパターンまたは補助関数を使用する方法はありますか? それは簡単な状況のように思えるので、正しいトリックを知っているだけのケースであることを願っています.

(Agda 開発ブランチの新しい終了チェッカーで対処できるかもしれませんが、必要がない限り、開発バージョンのインストールは避けたいと思います。)

Coqを使用して認定プログラムを設計することについて話しているいくつかの異なる研究グループと、少なくとも1冊の本を見ています。認定プログラムの定義についてコンセンサスはありますか? 私が言えることは、それが本当に意味することは、プログラムが完全で型が正しいことが証明されたということだけです。現在、プログラムの型は、空でないこと、ソートされていること、すべての要素が 5 以上であることを証明するリストなど、非常にエキゾチックなものである可能性があります。ただし、最終的には、認定されたプログラムは、Coq が完全で型安全であることを示すものにすぎません。 、すべての興味深い質問は、最終的なタイプに何が含まれていたかに要約されますか?

編集 1

wjedynakの回答に基づいて、以下の回答にリンクされているXavier Leroyの論文「現実的なコンパイラの正式な検証」を見ました。これにはいくつかの良い情報が含まれていると思いますが、この一連の研究のより有益な情報は、Sandrine Blazy と Xavier Leroy によるC 言語の Clight サブセットのための機械化されたセマンティクスの論文で見つけることができると思います。これは、「Formal Verification」ペーパーが最適化を追加する言語です。その中で、Blazy と Leroy は Clight 言語の構文とセマンティクスを提示し、セクション 5 でこれらのセマンティクスの検証について説明します。セクション 5 には、コンパイラーの検証に使用されるさまざまな戦略のリストがあります。. これらは：

1. マニュアルレビュー
2. セマンティクスのプロパティの証明
3. 検証済みの翻訳
4. 実行可能なセマンティクスのテスト
5. 代替セマンティクスとの同等性

いずれにせよ、おそらく追加できるポイントがあり、もっと詳しく聞きたいと思っています.

認定プログラムの定義は何かという最初の質問に戻りますが、それはまだ少し不明確です。Wjedynak は一種の答えを提供しますが、実際には Leroy の作業には、Coq でコンパイラを作成し、ある意味でそれを認定することが含まれていました。理論的には、C->Coq->証明に進むことができるようになったため、C プログラムに関することを証明できるようになりました。そういう意味では、こういうワークフローもありそうですね。

1. X言語でプログラムを書く
2. Coqまたはその他の証明補助ツールでのステップ1のプログラムのモデルの形式。これには、Coq でプログラミング言語のモデルを作成することが含まれる場合もあれば、プログラムのモデルを直接作成すること (つまり、Coq でプログラム自体を書き直すこと) が含まれる場合もあります。
3. モデルに関するいくつかのプロパティを証明します。多分それは価値についての証明です。たぶん、それはステートメントの等価性の証明です（3 = 1 + 2またはf（x、y）= f（y、x）など）。
4. 次に、これらの証明に基づいて、元のプログラムを認定済みと呼びます。

あるいは、プルーフ アシスタント ツールでプログラムの仕様を作成し、仕様に関するプロパティを証明できますが、プログラム自体は証明できません。

いずれにせよ、誰かが定義を持っているなら、私はまだ別の定義を聞くことに興味があります.

値がx : Aあり、 のみを含むセットを定義したいとしますx。

これは私が試したものです：

それを行うより良い方法はありますか？

これが必要な理由の例: ある集合 A にモノイドがある場合、A を唯一のオブジェクトとする圏を形成できます。Agda でそれを表現するには、「A だけを含む集合」と書く方法が必要です。

いくつかの入力:

この関数は、型のベクトルと結果の型から関数型を構築します。

これは、Arity-Generic Datatype-Generic Programming ペーパーの 2 つのコンビネータです。

いくつかの有効な定義:

さらには:

しかし、これは型チェックしません:

エラー：

どうしたの？