問題タブ [agda]

ソートされたリストのデータ型があり、証明に関係のないソートの目撃者があるとします。Agda の実験的なサイズの型機能を使用して、Agda の終了チェッカーを通過するデータ型の再帰関数を取得できるようにします。

さて、そのようなデータ構造に対して定義したい古典的な関数は ですmerge。これは 2 つのソートされたリストを取り、入力リストの要素を正確に含むソートされたリストを出力します。

この関数は無害に思えますが、Agda にそれが合計であることを納得させるのは難しい場合があります。実際、明示的なサイズ インデックスがないと、関数は終了チェックに失敗します。1 つのオプションは、関数を 2 つの相互に再帰的な定義に分割することです。これは機能しますが、定義と関連する証明の両方にある程度の冗長性が追加されます。

mergeしかし同様に、サイズ インデックスを明示的に指定して、Agda が受け入れる署名を持つことができるかどうかもわかりません。これらのスライドmergesortでは、明確に議論しています。そこに与えられた署名は、以下が機能することを示唆しています:

ここで行っているのは、入力が任意の (そして異なる) サイズを持つことを許可し、出力のサイズが ∞ であることを指定することです。

残念ながら、この署名では、Agdaは、定義の最初の節の.ι != ∞ of type Size本文を確認すると、 と不満を漏らしています。xsサイズの型をよく理解しているとは言えませんが、どのサイズの ι も ∞ に統一されるという印象を受けました。おそらく、これらのスライドが作成されてから、サイズ指定された型のセマンティクスが変更されたのでしょう。

では、私のシナリオは、意図されたサイズの型のユースケースですか? もしそうなら、どのように使用すればよいですか？ここでサイズ化された型が適切でない場合、以下が行うmergeことを考えると、上記の最初のバージョンが終了チェックを行わないのはなぜですか:

私は次のことを証明しようとしています：

私は Adga を初めて使用し、どこから始めればよいかさえわかりません。提案やガイダンスはありますか？明らかに、紙の上で証明するのは非常に簡単ですが、Agda に何を伝えればよいかわかりません。

pow 関数を次のように定義しました。

Mac に agda をインストールできません。私はここから指示を受けています：

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.MacOSX

Haskell プラットフォームをインストールすることができ、cabal update を実行すると動作します。私が実行すると：

最初にインストールされ、現在は再インストールのオプションが提供されているので、それは正しいと思います。最後のコマンドを実行すると問題が発生します。

出力します

Windows のインストールの方がはるかに簡単に思えるため、仮想ボックスへのインストールも試みましたが、.msi ファイルを実行しようとすると、「このファイルはお使いのプロセッサと互換性がありません」というエラーが表示されます。仮想ウィンドウが最大 8 つのプロセッサ (最大) を使用できるようにしたので、それがオプションになるとは思えません。どんな助けでも大歓迎です。

私はこのレマを証明しようとしています

しかし、別の関数である reverse-helper が目標に到達し続けており、それを取り除く方法がわかりません。ガイダンスや提案はありますか？