問題タブ [agda]

Agda のドキュメントには、Data.AVLモジュールの使用方法の例がいくつか示されています。

http://darcsden.com/abel/AgdaPrelude/browse/README/AVL.agda

例では、モジュールは、ツリーに格納されている値のタイプとキー タイプの順序を指定する引数を使用して、インポート時に 1 回インスタンス化されます。

同じクライアント モジュールで異なる値の型 (文字列のツリーと数値のツリーの両方) で AVL ツリーを使用するにはどうすればよいですか?

可換モノイド (A, +, イプシロン) を指定して、要素型 A の AVL ツリーの可換モノイドを導出しようとしています。ここで、導出された演算はunionWith +です。AVL ツリーの等価性の概念は、2 つのツリーが同じtoListイメージを持っている場合に等しいというものです。

私はそれunionWith +が連想的であることを証明しようとして立ち往生しています（同等の概念まで）。結合性の証明に使用したいので、交換性と +-cong を公準として持っていますが、まだ証明していません。

bibble問題を次のコードの用語に切り分けました。

ではbibble、z ≈ z(つまりrefl) の証明と(可換性による) の証明があり、これを使用して ≈ 引数の結合も ≈ であるという証明を導き出すx ∪ tree (Indexed.leaf l<u) ≈ (tree (Indexed.leaf l<u)) ∪ xことができると思います。∙-cong

ただし、コンパイラには未解決のメタ変数がいくつか残っているようで、残念ながらメッセージの読み方がよくわかりません。私は何か間違ったことをしているだけですか(証明に関して)、それともいくつかの引数を明示的にする必要があるだけですか?

私は運動しています。これは簡単なことのようです（問題が明らかにリスト分割にあることを示すために単純化されています）：

要するに、2 つのリストの順列を定義できることを宣言します。それらがとによって決定されるとのPermutation等しい要素のペアを持つ小さなリストの を提供できる場合です。xyyzsys

次にlemma-ripTop(まったく別のことをするつもりだったが、ここでは にあるだけidである)リスト ( ) に対してPermutation与えられた何かを証明する必要がある。Permutationy :: ys

1. なぜAgdaが見る必要がzs ++ (y1 :: ys1) == y :: ysあるのか​​ 理解できません（それは私が得るエラーです）-これは型宣言とコンストラクタから明らかであるべきだと思いましたか？つまり、 が入力で与えられたのでPermutation xs (y :: ys)、コンストラクターで証人として提供された分割p::は合計で になるはずy :: ysです。

2. このリストの分割が有効であることを Agda に納得させるにはどうすればよいでしょうか?

エラーメッセージ：

私は Agda プロジェクトに数週間取り組んできましたが、レベルのポリモーフィズムを可能な限り無視しています。残念なことに (またはおそらく幸いなことに)、私はそれを理解し始める必要があるところまで来ているようです。

これまで、レベル変数は、 の 2 番目の引数Rel(または の 3 番目の引数REL) として必要な場合にのみ使用してきました。Setそれ以外の場合は、直接使用するだけで省略しました。現在、レベルを明示的に数量化し、いくつかのタイプのフォームを既存のコードにa渡そうとするクライアント コードがいくつかあります。Set a以下の例でquibbleは、 はクライアント コードを表し、_[_]×[_]_と≈-Listは、 を使用するだけの既存のコードの典型ですSet。

≈-Listここで、追加の level パラメータを使用しての帰納的定義を拡張してa、 type の型引数を取ることができますSet aが、入力と出力の関係のユニバースがどのように変化するかについては不明です。そして、問題はより複雑な定義にまで波及します。たとえば、_[_]×[_]_どのように進めたらよいかわからない場合などです。

与えられた例の署名を一般化してquibbleコンパイルするにはどうすればよいですか? 私が従うことができる一般的なルールはありますか? 私はこれを読みました。

Agda で代数構造の新しいレコード型を宣言する 2 つのスタイルを比較したいと思います。

標準の Agda パッケージで使用されているスタイルに従って、次のようにAlgebra定義できます。BoundedJoinSemilattice

このアプローチでは、 のフィールドは(名前の変更まで) 、、、およびなどの他のより抽象的な構造のフィールドBoundedJoinSemiLatticeと重複します。a をその「スーパータイプ」の 1 つとして表示するには、そのフィールドをスーパータイプのフィールドにマッピングする射影関数 (上記の関数など) を呼び出す必要があります。SetoidSemigroupMonoidCommutativeMonoidBoundedJoinSemiLatticeBoundedJoinSemiLatticecommutativeMonoid

ただし、このフィールドの重複は、あまり具体的でない代数構造からより具体的な代数構造を構築するコードの重要なボイラープレートにつながる可能性があります。より自然な定義は次のようになります (名前CommutativeMonoidを に変更CM):

ここでの考え方は、CommutativeMonoidintoのフィールドを複製するのBoundedJoinSemilatticeではなく、後者が type の単一のフィールドを宣言することCommutativeMonoidです。次に、 を使用して、open...publicそのサブフィールドを含むレコードに「継承」します。実際、これは の標準ライブラリの他の場所で使用されているイディオムとまったく同じですが、Algebra.Structuresここでは継承されたフィールドの名前も変更して、継承コンテキストで適切に名前が付けられるようにしています。

この 2 番目の方法は冗長性が低いだけでなく、 aBoundedJoinSemilatticeから aを作成したいクライアント コードは、作成CommutativeMonoid中のレコードに単純にそれを引数として渡すことができます。一方、BoundedJoinSemilatticeゼロから を構築したいクライアント コードは、中間の を構築する必要がありますCommutativeMonoid。

Algebraモジュールがこの継承スタイルを使用しない 理由はありAlgebra.Structuresますか? たぶん、私が見つけていない 2 番目のアプローチに問題があるか、またはおそらく大きな違いはないでしょうBoundedJoinSemiLattice。CommutativeMonoid、2番目のアプローチの利便性の多くを回復します。

引数の型がインデックスの値に依存し、インデックスが明示的に渡される二項演算子のファミリ (たとえば、セットによってインデックス付けされる) を定義するとします。さらに、ファミリーのメンバーを中置記法で使用できるようにしたいとします。

ここにインデックスがあります。角かっこ [-] は、A を下付き文字として読み取る必要があることを示すと想定されています。x の型は値A に依存し、の定義でA : Setの左側に出現する必要があるため、このような演算にこの構文と互換性のある型シグネチャを与えることは困難です。x : A_<[_]_

syntax宣言に基づいて、次のトリック (ハック?) を試しました。

バイナリ操作で暗黙的なインスタンスを使用しない限り、これはうまくいくようです。フォームの引数を宣言に追加しようとすると{{x}}、syntaxAgda が文句を言います。(不合理ではないかもしれません。)

cmp暗黙のインスタンスを明示的に受け取るバージョンを導入することでイディオムを適応させ、そのバージョンを呼び出す構文のバリアントを定義できるようです。

(引数syntaxをサポートしていないように見えるため、アンビエント B を完全に取得する機能をあきらめずに、 に{{x}}インラインcmp化することはできません。)cmp-explicit

これはハックですか？y の型が x の値に依存し、x が明示的に渡される場合、引数 x と y を反転する別の方法はありますか?

当然、定義する

タイプチェック時にAgdaに文句を言わせxます。

Setoid関数が 2 つの sを要求する方法はありますか?最初のSetoid同等性が後者の同等性を意味しますか? もちろん、これには両方Setoidの がそれらを共有する必要があり、 CarrierandCarrierはパラメーターではなく、代わりにレコード フィールドです。単純に等価性を要求しようとするとCarrier、型チェッカーによって拒否されます。

等式証明でパターン マッチを行わないため、これは機能しません。そのため、さまざまなCarrier型が統一されません。を使用してこれを表現する方法が見つかりませんでしたsubst。

次のコードを検討してください。

Agda (バージョン 2.3.2.2) をロードすると、Agda は最後から 2 番目の行に関連するエラー「次の場所にある未解決のメタ」を出力します。

特にassoc +を指しています。

この警告なしでコンパイルされるように、ヒントを提供するか、コードを変更するにはどうすればよいですか?

もちろん、引数を非表示にすることでそれを取り除くことができますが、それは、必要のない場所であっても、どこでも明示的な引数を指定する必要があることを意味します...