Mutualy遞歸函數和終止檢查

編輯Mutualy遞歸函數和終止檢查

Require Import Bool List ZArith. 
    Variable A: Type. 
    Inductive error := 
    | Todo. 
    Inductive result (A : Type) : Type := 
     Ok : A -> result A | Ko : error -> result A. 
    Variable bool_of_result : result A -> bool. 
    Variable rules : Type. 
    Variable boolean : Type. 
    Variable positiveInteger : Type. 
    Variable OK: result unit. 
    Definition dps := rules. 
    Inductive dpProof := 
     | DpProof_depGraphProc : list 
     (dps * boolean * option (list positiveInteger) * option dpProof) -> dpProof. 
    Fixpoint dpProof' (R D: rules) (p: dpProof) {struct p}:= 
    match p with 
     | DpProof_depGraphProc cs => dpGraphProc R D cs 
    end 
    with dpGraphProc (R D: rules) cs {struct cs} := 
    match cs with 
    | nil => Ko unit Todo 
    | (_, _, _, op) :: cs' => 
     match op with 
     | None => Ko unit Todo 
     | Some p2 => dpProof' R D p2 
     end 
end.

我得到一個錯誤消息說：到dpProof 遞歸調用具有等於

"p2" instead of "cs'". 
Recursive definition is: 
"fun (R D : rules) 
    (cs : list 
      (dps * boolean * option (list positiveInteger) * 
      option dpProof)) => 
match cs with 
| nil => Ko unit Todo 
| (_, _, _, Some p2) :: _ => dpProof' R D p2 
| (_, _, _, None) :: _ => OK 
end".

如果我不主要理由使用相互遞歸併使用嵌套固定點，它將合併並通過終止檢查器。這是成功結合的代碼。

Fixpoint dpProof' (R D: rules) (p: dpProof) {struct p}:= 
     match p with 
     | DpProof_depGraphProc cs => 
     match cs with 
      | nil => Ko _ Todo 
      | (_, _, _, op) :: cs' => 
      match op with 
       | None => Ko unit Todo 
       | Some p2 => dpProof' R D p2 
      end 
     end end.

我想深入瞭解它爲什麼不能通過終止檢查器？是因爲他們無法猜測爭論的減少？有沒有我可以使用相互遞歸來表達我的功能dpGraphProc什麼辦法？

而且我怎麼能寫出函數dpGraphProc，在整個列表檢查？在這裏我不知道如何使用參數cs'。

來源

2012-11-08 Quyen

你的代碼片段中有很多未聲明的標識符，並且它不包含任何在你的錯誤信息中提到的「p2」。你能否提供一個能夠完全符合上述信息的例子？ – Virgile

這次我編輯和測試代碼組合並提供錯誤。感謝您的耐心。 – Quyen

相互遞歸是要麼與單個電感數據類型或與已經在單個電感定義被定義在一起的不同感應數據類型一起使用。在你的情況，你正在使用多態數據類型PROD（對的類型），列表和dpProof之前已經被定義選項。

嵌套不動點方法沒有限制。

來源

2012-11-08 12:13:31 Yves

Mutualy遞歸函數和終止檢查

回答

相關問題