問題タブ [agda]

帰納的データ型とパターンマッチングの状態に関するAgdaマニュアル：

正規化を確実にするために、帰納的発生は厳密に正の位置に現れる必要があります。たとえば、次のデータ型は許可されていません。

コンストラクターへの引数にBadの負のオカレンスがあるためです。

誘導データ型にこの要件が必要なのはなぜですか？

_+_-Operation forは通常、Nat最初の引数で再帰的に定義されるため、型チェッカーがそれを知ることは明らかに自明ではありませんi + 0 == i。ただし、固定サイズのベクトルに関数を記述すると、この問題に頻繁に遭遇します。

一例: アグダ関数を定義するにはどうすればよいですか

nベクトルの最後に最初の値を置くのはどれですか?

Haskellでの簡単な解決策は

私は次のようにAgdaで同様に試しました：

ただし、タイプ チェッカーは次のメッセージで失敗します (これ{zero}は、上記のswap-Definition のケースに関連しています)。

それで、私の質問: アグダにどのように教えm == m + zeroますか? swapそして、そのような関数をAgdaでどのように書くのですか?

prefixAppベクトル関数をベクトルのプレフィックスに適用する Agda関数を作成しました。

prefixApp長さの引数を明示的に指定せずに使用できるという事実が気に入っています。

( xorV : Vec Bool 2 -> Vec Bool 1Vector-Xor-Function はどこにありますか)

postfixApp残念ながら、長さの引数を明示的に指定せずに使用できる -functionの書き方がわかりません。これまでの私の関数定義は次のようになります。

ただし、postfixApp常に長さの引数が必要なようです。例えば

postfixAppこの非対称性を解消する方法、つまり、明示的な長さ引数なしで機能する関数を作成する方法を知っている人はいますか? 私は別の機能が必要だと思いsplitますか？

私は次の定義を持っています：

次の補題を証明するのは簡単です。

しかし、次の補題を証明する方法が見つかりません。

の定義を<=次のように変更できます。

その場合、私は証明することができますlem-prev'：

しかし、今は証明できませんlem-prev。

<=および/またはの両方の見出語を証明する方法はあり<='ますか？いいえの場合、それを可能にするために定義をどのように変更する必要がありますか？

追加：hammarのヘルパー補題を使用したソリューション：

決定可能等式を使用する関数について、いくつかの簡単なことを証明しようとしています。これは非常に単純化された例です。

今、私はこのようなことを証明しようとしています。ここでは、の両側_≟_が同一であることをすでに示しています。

この時点で、現在の目標は(check ds x x | x ≟ x) ≡ somethingです。それだけの場合は、のx ≟ xようなものを使用して解決しますreflが、この状況で私が思いつくことができる最善の方法は、次のようなものです。

それ自体はそれほど悪くはありませんが、より大きな証拠の真ん中でそれは混乱です。確かにこれを行うためのより良い方法があるはずですか？

密接に関連する2つの質問があります。

まず、HaskellのArrowクラスをAgdaでモデル化/表現するにはどうすればよいですか？

（次のブログ投稿では、それが可能であるはずだと述べています...）

第二に、Haskellでは、(->)は一級市民であり、もう1つの高階型であり、クラス(->)の1つのインスタンスとして定義するのは簡単です。Arrowしかし、それはAgdaではどうですか？私は間違っているかもしれませんが、Agdas->はHaskellのものよりもAgdaのより不可欠な部分であると感じてい->ます。したがって、Agdas->は高次の型、つまり、 ？Setのインスタンスにすることができる型関数を生成するものと見なすことができますArrowか？

vector-sizesが 暗黙的なままでapplyPrefixある長いベクトルの最初の部分に固定サイズのベクトル関数を適用するAgda 関数を作成しました。ヘルパー関数と一緒の定義は次のとおりです。mnksplit

applyPostfix固定サイズのベクトル関数を長いベクトルの末尾部分に適用する対称関数が必要です。

の定義がapplyPrefix既に示しているように、k-ArgumentapplyPostfixは使用時に暗黙のままにすることはできません。例えば：

を使用するときに -argument が暗黙的なままにapplyPostfixなるように実装する方法を知っている人はいますか?kapplyPostfix

私がしたことは、校正/プログラミングです:

を定義するときにその補題を使用しますapplyPostfix。

残念ながら、k補題を呼び出すために -Parameter を使用しているため、これは役に立ちませんでした:-(

k明示的であることを避けるためのより良いアイデアはありますか? 多分私はベクトルでsnoc-Viewを使用する必要がありますか?

Idrisチュートリアル、Agdaチュートリアル、および他の多くのチュートリアルスタイルのペーパーと、まだ学習していないことへの終わりのない参照を含む入門資料があります。私はこれらすべての真っ只中にいるようなもので、ほとんどの場合、数学表記と新しい用語が説明なしに突然現れることに固執しています。おそらく私の数学は最悪です:-)

依存型プログラミングにアプローチするための統制のとれた方法はありますか？Haskellを学びたいときのように、「自分自身にHaskellを教えて」から始め、Scalaを学びたいときは、Oderskyの本から始めます。Rubyの場合、変異したバグを含む奇妙なチュートリアルを読みます。しかし、私は彼らの本でアグダやイドリスを始めることはできません。彼らは私の頭上にあります。私はCoqを試してみましたが、そのすべてを証明するスタイルで立ち往生しました。アグダは巨大な数学のバックグラウンドを必要とし、イドリスは、まあ、今はそれを残しましょう！

私は静的型システムをよく理解しています。私はScalaにある程度精通しており、必要に応じてHaskellを使用できます。私は関数型パラダイムを理解し、それを日常的に使用しています。代数的データ型とGADT（実際には非常にスムーズに）を理解し、最近ラムダキューブを理解することができました。しかし、私は数学と論理の部分が不足しています。

CoList (Maybe Nat)s のみjustを考慮した sの等価性を定義したいと思います。もちろん、単に からCoList (Maybe A)に移動することはできませんCoList A。それは必ずしも生産的ではないからです。

では、私の質問は、そのような等価関係を (決定可能性に目を向けずに) どのように定義できるかということです。just無限の尾を非同等と見なすことができれば、それは役に立ちますか?

以下の@gallaisは、この関係を単純に定義できるはずだと示唆しています。

しかし、それが推移的であることを証明すると、終了チェッカーから (予想される) 問題が発生します。

nothingそこで、 @Vitusが提案したように、両側があまり曖昧でないケースを作成してみました:

transしかし、問題のあるケース(穴を残したケース) を定義する方法がわかりません。

ICFP 2012 で、Conor McBride はタイル「Agda-curious?」で基調講演を行いました。

小さなスタック マシンの実装が特徴でした。

ビデオは YouTube にあります: http://www.youtube.com/watch?v=XGyJ519RY6Y

コードもオンラインです: http://personal.cis.strath.ac.uk/conor.mcbride/ICFP12Code.tgz

runパート 5 (コードをダウンロードした場合は「Part5Done.agda」)の機能について疑問に思っています。run機能を説明する前に話が止まる。

run関数の正しい型シグネチャは何ですか? 機能はどのrunように実装する必要がありますか?

コンパイル機能については、トークの約 55 分後に説明されています。

完全なコードは、Conor の Web ページ から入手できます。