私の機能が実際に再帰的であることをCoqにどのように納得させることができますか？

Question

私は比較的シンプルな文脈自由文法（括弧の1つのタイプ）を解析するためにCoqにプログラムを書こうとしています。私の一般的なアルゴリズムはパーザが潜在的に残りの文字列を返すことです。たとえば、"++]>><<"を解析すると、CBTerminated [Incr Incr] ">><<"が返され、 "[++] >> < <"を解析するパーサーは、 ">> < <"を取得してそれを続行できます。

明らかに文字列は小さくなりますが、そのことを確信させることは別の問題です。それは私にエラーを与えている

parseHelperの再帰的な定義が悪いです。 [...] parseHelperへの再帰呼び出しは、 "rest"の ではなく、 "rest"に等しい主な引数を持っています。私が想定し

は、道でrest' < inputそれはrest < inputと確信していますということを納得していないことを意味しています。 （<は「より小さい」を意味します）。

私はスキップする文字の数を返すと考えていましたが、それはやや控えめで不必要なものです。

Require Import Coq.Strings.String. 
Require Import Coq.Strings.Ascii. 
Require Import Coq.Lists.List. 
Require Import ZArith. 

Open Scope char_scope. 
Open Scope list_scope. 

Notation " [ ] " := nil (format "[ ]") : list_scope. 
Notation " [ x ] " := (cons x nil) : list_scope. 
Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope. 

Inductive BF := 
    | Incr : BF 
    | Decr : BF 
    | Left : BF 
    | Right : BF 
    | In : BF 
    | Out : BF 
    | Sequence : list BF -> BF 
    | While : BF -> BF. 

Inductive BF_Parse_Result := 
    | UnmatchedOpen 
    | EOFTerminated (u : list BF) 
    | CBTerminated (u : list BF) (rest : string). 

Definition bind (val : BF) (onto : BF_Parse_Result) := 
    match onto with 
     | UnmatchedOpen => UnmatchedOpen 
     | EOFTerminated values => EOFTerminated (cons val values) 
     | CBTerminated values rest => CBTerminated (cons val values) rest 
    end. 

Fixpoint parseHelper (input : string) : BF_Parse_Result := 
    match input with 
     | EmptyString => EOFTerminated nil 
     | String first rest => 
      match first with 
       | "+" => bind Incr (parseHelper rest) 
       | "-" => bind Decr (parseHelper rest) 
       | "<" => bind Left (parseHelper rest) 
       | ">" => bind Right (parseHelper rest) 
       | "," => bind In (parseHelper rest) 
       | "." => bind Out (parseHelper rest) 
       | "]" => CBTerminated nil rest 
       | "[" => 
        match parseHelper rest with 
         | UnmatchedOpen => UnmatchedOpen 
         | EOFTerminated _ => UnmatchedOpen 
         | CBTerminated vals rest' => 
          bind (While (Sequence vals)) (parseHelper rest') 
        end 
       | _ => parseHelper rest 
      end 
    end. 

Answer 1

well-founded recursionとお考えですか？ Coqの標準ライブラリには、よく確立された関係上の関数を定義するための一連の有用なコンビネータがあります。参照1は、一般的な再帰のための2つの手法（よく知られた再帰とモナド）を示しています。

Agdaのコンテキストでも非常に有用なその他の手法は、定義された関数のコールグラフを模倣する帰納的述語を定義する、いわゆるBove-Capretta methodです。

Coqには、より一般的な再帰関数を定義するために使用できるFunctionコマンドもあります。非構造的再帰関数を定義する必要があるときはいつでも、私は十分に確立された再帰を使いました。

これがあなたに役立つことを願っています。