Как я могу убедить Coq, что моя функция на самом деле рекурсивная?

Question

Я пытаюсь написать программу на Coq для анализа относительно простой контекстно-свободной грамматики (один из типов скобок), и мой общий алгоритм заключается в том, чтобы синтаксический анализатор потенциально возвращал остаток строки. Например, разбор "++]>><<" должен вернуться CBTerminated [Incr Incr] ">><<" и затем, скажем, синтаксический анализатор, который анализирует "[++] >><<", сможет подобрать ">><<" и продолжить с этим.

Очевидно, что строка меньше, но убедить Coq в этом - другое дело. Это дает мне ошибку

Рекурсивное определение 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

Рассматривали ли вы использование обоснованной рекурсии? Стандартная библиотека Coq имеет ряд полезных комбинаторов для определения функций над обоснованными отношениями. Ссылка 1 показывает две техники (обоснованную рекурсию и монаду) для общей рекурсии.

Другой метод, который также очень полезен в контексте Agda, - это так называемый метод Бове-Капретты, который определяет индуктивный предикат, который имитирует граф вызовов определенной функции.

Coq также имеет команду Function, которую можно использовать для определения более общих рекурсивных функций. Всякий раз, когда мне нужно было определить неструктурно-рекурсивные функции, я использовал обоснованную рекурсию.

Надеюсь, что это поможет вам.