7

私はCoqをいじっています。具体的には、マージソートを実装して、それが機能することを証明しようとしています。

実装の私の試みは次のとおりでした：

Fixpoint sort ls :=
match ls with
| nil => nil
| cons x nil => cons x nil
| xs =>
  let (left, right) := split xs nil nil
  in merge (sort left) (sort right)
end.

この結果として私が得るエラーは次のとおりです。

Error:
Recursive definition of sort is ill-formed.
In environment
sort : list nat -> list nat
ls : list nat
x : nat
l : list nat
y : nat
l0 : list nat
left : list nat
right : list nat
Recursive call to sort has principal argument equal to "left" instead of
one of the following variables: "l" "l0".
Recursive definition is:
"fun ls : list nat =>
match ls with
| nil => nil
| x :: nil => x :: nil
| x :: _ :: _ =>
    let (left, right) := split ls nil nil in merge (sort left) (sort right)
end".

これらのエラーの私の解釈は、lとl0は、頭のないls、x、xのないls、およびxの後の要素（yと呼ぶことにしたと思います）です。私がこれらのリストの1つで再帰せず、代わりにローカルで定義されたリストで再帰したのは気が狂っています。

パターンマッチから直接得られるものにのみ再帰することは許可されていますか？はいの場合、これは厳しい制限のようです。それを回避する方法はありますか？Coqは関数が終了することを認識できないと思います。左右がxsよりも小さいことを証明する方法はありますか？

4

1 に答える 1

10

一般的な再帰に関するCPDTの章では、その特定の問題のみを扱っていることがわかりました。

http://adam.chlipala.net/cpdt/html/GeneralRec.html

十分に根拠のある再帰と呼ばれるセクションを読んでください。これは、十分に根拠のある再帰を使用してマージソートを実装し、Coqの終了チェッカーが満足できるようにします。

Functionまたはを使用してその問題を解決する他の方法があるかもしれませんがProgram Fixpoint、十分に根拠のある再帰について読んでも害はないと思います。

于 2012-12-10T11:45:34.923 に答える