2

私は Agda を初めて使用し、Decidable関数とDec型を理解するために助けが必要です。

私は一次論理述語を定義しようとしていますが、ある種のブール値を証明してエンコードしたいと考えています。これを行う方法は Dec タイプを使用することです..

今、私が知る限り、これを行うには、すべての論理演算子をセット型ではなく決定可能な型に再定義する必要があります。そうするために、私はそれを新しい型に埋め込んだのです。これは、and 演算子に対して行った方法です。

data _∧_ (A B : Set) : Set where 
   _&_ : A → B → A ∧ B 

Dec∧ : {A B : Set} → A ∧ B → Dec (A ∧ B) 
Dec∧ A∧B = yes (A∧B)

それはそれを行う方法ですか、それとも別の方法がありますか？

次に、この演算子を使用して Nat 値の関係を定義したいので、次のようにしました。

_◆_ : ℕ → ℕ → Dec∧ (Rel ℕ lzero) (ℕ → Set) 
x ◆ y = (0 < x) ∧ (x ² ≡ 2 * y ²)

しかし、これは型エラーを与えます..

論理ステートメントを証明するためにそれを使用するチュートリアルまたは例に誰かが私Decを案内してくれれば幸いです..

4

1 に答える 1

1

基本的に決定可能な述語は、有限時間で終了し、それが真であるという証明とともに yes を返すか、否定の証明とともに no を返すアルゴリズムを持つ述語です。たとえば、2 つの自然数ごとに、それらが等しいか等しくないかを証明できます。

あなたが書いたものはタイプチェックではありません。関数は Dec (Rel ℕ lzero) (ℕ → Set) を返す必要があります。最初の引数は正しいですが、2 番目の引数は正しくありません。これは、\x -> 2 * x のような関数でなければなりません。

PS私にとって、この機能は意味がありません。それを使って何を達成したいですか？

于 2014-03-13T22:57:46.737 に答える