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

Question

には、次の固定点を考えてみましょう：それは減少不動点を推測することはできませんので

Require Import Coq.Lists.List. 
Import ListNotations. 

Inductive my_type: Type:= 
| Left: my_type 
| Right: my_type 
. 

Fixpoint decrease (which: my_type) (left right: list my_type) : list my_type := 
match which with 
| Left => 
    match left with 
    | [] => [] 
    | a::tl => decrease a tl right 
    end 
| Right => 
    match right with 
    | [] => [] 
    | a::tl => decrease a left tl 
    end 
end. 

コックは、以下の不動点を拒否（時にはleftリストは、時にはそれが、その頭を失いright）。

このanswerは、Program Fixpointを使用し、{measure ((length left)+(length right))}を指定することでこれを解決できることを示しています。

私の質問は以下のとおりです。

• 定期FixpointとProgram Fixpointの違いは何ですか？
• 減少する引数を通常のFixpointに明示することはできますか？
• Next Obligationの目標は？

Answer 1

• コックにおけるFixpointコマンドが終了を確実にするために、構造再帰をチェックコックのfixプリミティブを使用して再帰関数を構築します。これはCoqの唯一の再帰であり、他のすべての手法は最終的には何種類かのfixになります。

  Program Fixpointは、Programの機能で、わずかに拡張された言語で定義を記述してから、Coq定義にコンパイルすることができます。 Program Fixpointは任意の再帰関数を受け取り、関数が終了することを示す適切な証明義務を生成し（各再帰サブコール上の引数のいくつかの尺度を減少させることによって）、定義および終了証明を構造的に引数を減少させるCoq定義にパッケージ化する。それが基本的には魔法のように聞こえるが、CPDTはこの種のエンコーディングをどのように行うのかをよく説明している。 Fixpoint decrease (which: my_type) (left right: list my_type) {struct right} : list my_type：

• はい、あなたは明示的、構造的が減少している引数を指定する{struct arg}注釈を追加することができます。あなたの関数は一般的にいずれの引数も構造的に減少させないので、これはあなたの例にとっては役に立ちません。すべてのプリミティブfix構造体にはstructアノテーションがありますが、Fixpointと書くとCoqは自動的にアノテーションを自動的に推論できます。あなたがProgram FixpointでNext Obligationから目標の2種類を取得

  Nat.add = 
      fix add (n m : nat) {struct n} : nat := 
      match n with 
      | 0 => m 
      | S p => S (add p m) 
      end : nat -> nat -> nat 
  

• ：たとえば、ここにNat.addだ最初の各下位呼び出しが小さく引数があること（measureを使用して、「小さな」はNATを上<を使用して定義される）と、第2 「より小さい」関係が十分に確立されていること。これは、小さくて小さなオブジェクトの無限に降順のシーケンスはありません。私はなぜProgram FixpointがNat.ltのために自動的にこれをしないのか分からない。 Programには、より一般的な再帰よりも多くの機能があるため、作成する定義に応じて、これらの機能に関連する他の目標も生成できます。