totality

0熱

1答えて

I have the following definition for terms : Require Import Coq.Arith.Arith. Require Import Coq.Lists.List. Require Import Coq.Strings.String. Import ListNotations. Definition VarIndex:Type := n

1熱

1答えて

引数を減らす（とどのようなプログラム不動点である）

には、次の固定点を考えてみましょう：それは減少不動点を推測することはできませんので Require Import Coq.Lists.List. Import ListNotations. Inductive my_type: Type:= | Left: my_type | Right: my_type . Fixpoint decrease (which: my_type) (

0熱

2答えて

この再帰関数は合計ではありませんか、コンパイラはそれを証明できませんか？それを合計で書き直すには？

次のコードを提示：私は他のいくつかの方法でこのコードを再書かれているが、イドリスは合計としてそれを認識することができません TotalityOrWhat.idr:17:3: TotalityOrWhat.parseDriver, parseDriver' is possibly not total due to recursive path TotalityOrWhat.parseDriver

7熱

1答えて

CoqのProgram FixpointとFunctionの違いは何ですか？

これらは同じ目的を果たしているようです。私が今まで気づいた1つの違いは、は{measure (length l1 + length l2) }のような複合尺度を受け入れますが、はこれを拒否しているように見え、{measure length l1}を許可します。 Program Fixpointは、厳密にはFunctionより強力ですか、さまざまな用途に適していますか？

1熱

1答えて

この機能がREPLをハングアップするのはなぜですか？

Test-Driven Development with Idrisの第9章には、以下のデータタイプとremoveElem機能があります。 import Data.Vect data MyElem : a -> Vect k a -> Type where MyHere : MyElem x (x :: xs) MyThere : (later : MyElem x xs)

7熱

1答えて

コックSIMPL

はProgram Fixpointのための戦術simplようなものはありますか？特に、次のような些細な声明をどのように証明できますか？明らかに Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n' => S (bla n') end. Lemma obvious: forall n, bla

3熱

2答えて

Coqのベストプラクティス：相互再帰は、一つだけの機能は、構造的に型指定されていないラムダ計算のために、次のおもちゃの表現を考えてみましょう

が減少している。 Require Import String. Open Scope string_scope. Inductive term : Set := | Var : string -> term | Abs : string -> term -> term | App : term -> term -> term. Fixpoint print (term : term

7熱

1答えて

Idrisが物事が完全ではないと思ったら、Idrisは証明のために使用できますか？

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issuesと述べている：は、第二に、現在の実装では、これまでのところ、それに入れ限られた努力があったので、まだそれは機能がされていない合計であると考えている場合もあります。まだあなたの証明のためにそれに頼らないでください！これは、Idris

2熱

1答えて

イドリス：全体のチェックが失敗したナット

のために再実装fromIntegerしようとしたとき、私は次のコードを持っている： module Test data Nat' = S' Nat' | Z' Num Nat' where x * y = ?hole x + y = ?hole fromInteger x = if x < 1 then Z' else S' (fromInteger

10熱

1答えて

Agdaにはどのようなサイズの種類がありますか？

アグダのサイズの種類は何ですか？ MiniAgdaについての論文を読もうとしましたが、以下の点で進めませんでした：なぜデータ型はそのサイズよりも一般的ですか？私が知る限り、サイズは誘導木の深さです。データ型がサイズに対して共変するのはなぜですか？< = j - > T_i < = T_j？ >と#のパターンは何を意味していますか？