問題タブ [agda]

I'm using Emacs with agda-mode, and have written this function:

Nat, succ and * are defined to be compatible with Agda's internal definitions of natural numbers.

When I evaluate (pow 2 100000) I get a stack overflow error. However, given that the recursive call is a tail call, I would like the agda interpreter to optimize pow' into a loop.

How can I enable this optimization?

次の 2 つの例のように、型を制約できる型付きプログラミング言語はありますか?

1. Probability は、最小値 0.0 と最大値 1.0 の浮動小数点数です。

   /li>

2. 離散確率分布はマップです。ここで、キーはすべて同じタイプである必要があり、値はすべて確率であり、値の合計 = 1.0 です。

   /li>

私の知る限り、これは Haskell や Agda では不可能です。

タイプチェッカーで、特定の計算が終了することが保証されているかどうかを指定できる関数型言語はありますか? あるいは、Haskellだけでこれを行うことはできますか?

Haskellに関して、この回答では、ポスターは次のように述べています

これについての通常の考え方は、すべての Haskell 型が「リフト」されているというものです。これには ⊥ が含まれています。つまり、 だけではなくにBool対応します。これは、Haskell プログラムが終了することが保証されておらず、例外が発生する可能性があるという事実を表しています。{⊥, True, False}{True, False}

一方、アグダに関するこの論文は、次のように述べています。

正しい Agda プログラムとは、型チェックと終了チェックの両方に合格するプログラムです。

つまり、すべての Agda プログラムが終了し、BoolAgda の a は正確に に対応します{True, False}。

たとえば、Haskell では type の値を持つことができますIO a。これは、問題の値を計算するために IO が必要であることをタイプチェッカーに伝えます。Lifted a問題の計算が終了しない可能性があると主張する型を用意できますか? つまり、非終了を許可しますが、型システムで分離します。(明らかに、Agda のように、値を「確実に終了する」と「終了しない可能性がある」にのみ分けることができます) そうでない場合、これを行う言語はありますか?

これが私が理解していることです：それは任意のandRelation.Binary.PropositionalEquality.TrustMe.trustMeを取るようです、そして：xy

• xとyが真に等しい場合、refl
• そうでない場合は、 のように動作しpostulate lie : x ≡ yます。

さて、後者の場合、Agda を簡単に矛盾させる可能性がありますが、これ自体はそれほど問題ではありません。これtrustMeは、使用する証明が権威への訴えによる証明であることを意味するだけです。さらに、そのようなものを使用して を書くことはできますが、(少なくとも Cc Cn によれば) 還元されないcoerce : {A B : Set} -> A -> Bケースであることが判明するため、Haskell のセマンティック ストンピングとは実際には類似していません。coerce {ℕ} {Bool} 0unsafeCoerce

それで、私は何を恐れなければなりませんtrustMeか？一方、プリミティブの実装以外で使用する理由はありますか?

整数の割り切れる可能性について証明しようとしています。最初に、割り切れる可能性が反射的であることを証明しようとしました。

引き算で割り切れると定義したので...

...という事実を使えば簡単に思えますn-n=0:

しかし、Agda は refl でのパターン マッチを拒否します。の他の正規形が存在しなくてもn-n=0 n. 私はこれを別の関数で証明しました。という事実を利用するしかありませんn-n=0。

ノート：

• a - bによって定義されますa + (neg b)
• 私はすでに証明したn-n≡0 : (n : ℤ) → n - n ≡ zero