6
나는 Coq로 장난하고있다. 특히, 나는 mergesort를 구현하려고 시도하고있다. 구현에서 Coq에서 Fixpoint의 제한 사항은 무엇입니까?
내 시도는
을했다 : 이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".
이러한 오류의 나의 해석은 그 리터이며, L0이없는 LS 있습니다
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.
나는이의 결과로 얻는 오류가 있습니다 그것의 머리, x, 그리고 x가없는 ls와 x 뒤에 오는 요소 (y를 호출하기로 결정한 것 같네요). 이 목록 중 하나에서 재귀하지 않고 대신 로컬로 정의 된 목록에서 재귀했습니다.
패턴 일치에서 직접 오는 것에 대해서만 재귀를 허용합니까? 그렇다면 심각한 제한이있는 것처럼 보입니다. 그 주위에 방법이 있습니까? 나는 Coq이 함수가 종료 될 것이라고 말할 수 없다고 추측하고있다. left와 right가 xs보다 작다는 것을 증명할 수있는 방법이 있습니까?
http://adam.chlipala.net/cpdt/html/GeneralRec.html
잘 설립 재귀를 읽어보십시오, 그것은 일종의에 잘 설립 재귀를 사용하여 병합을 구현