これらは同じ目的を果たしているようです。私が今まで気づいた1つの違いは、は{measure (length l1 + length l2) }のような複合尺度を受け入れますが、はこれを拒否しているように見え、{measure length l1}を許可します。CoqのProgram FixpointとFunctionの違いは何ですか？
Program Fixpointは、厳密にはFunctionより強力ですか、さまざまな用途に適していますか？
これは完全なリストではないかもしれないが、それは私がこれまでに発見したものです：
Program Fixpointメジャーが複数の引数を見ることができます。Functionは、fooへのコールをそのRHSで書き換えるために使用できる補題を作成します（foo_equation）。 Coq simpl for Program Fixpointのような問題を避けるために非常に便利です。Functionは、fooという再帰呼び出しの構造に沿って誘導を実行するための補題をfoo_indと定義できます。繰り返しになりますが、証明書の中でtermination引数を効果的に繰り返さずにfooについての事を証明するのにも非常に便利です。Program Fixpointは、ネストされた再帰をサポートするように誘惑される可能性があります。https://stackoverflow.com/a/46859452/946226を参照してください。これはなぜProgram Fixpointがdefine the Ackermannの場合でもFunctionが機能しない場合があります。また、Ackermann関数を 'Function'で定義することは不可能ですが、' Program Fixpoint' [それはできます]（https://stackoverflow.com/questions/10292421/error-in-defining-ackermann-in-coq） 。 –
お返事ありがとうございました。 –
ちなみに、[Coq v8.7ロードマップ]（https://github.com/coq/roadmaps/blob/master/text/roadmap-8.7.md#implementation-cleanups）は、実装が合併する。 –
これは良い質問です。詳しい知識が必要な人はSO AFAIKを読んでいないので、詳しい回答が必要な場合はCoqのgitterに行くことをおすすめします。関数とプログラムの実装は、異なる人物や異なるコンテキストで行われていました。実際、その機能セットは厳密には他のもののサブセットではありません。新しい「Equations」プラグインで両方をマージする計画がありますが、多くの進歩があったとしても、8.7ではそれは起こりません。つまり、将来のCoqリリースとの互換性を気にするならば、通常はプログラムを使う方が良いと思います。 – ejgallego