BNFスタイル定義の定義前に識別子を使用する

Question

BNF文法を定義するにあたっては、文法が「転送」となるように、定義する前に事柄を使用するのが一般的です。

これをcoqでどうやって行うことができますが、それでもバッファを通過することができますか？

Answer 1

Coqでは、バッファという概念はあらかじめ定義されていないので、あなたが意味することを理解するのは非常に難しいです。それでも、BNF文法を定義するときに使用できる、Look-aheadの可能性を与えるCoqの2つの側面があります。

再帰関数定義では、複数の再帰関数を同時に導入できます。

型定義は、いくつかの誘導型を同時に導入することができます。

どちらの場合でも、定義されている最初のオブジェクトは、定義される前の2番目のオブジェクトを参照できます。

ここに2つの例があります。最初の例は再帰関数です。

Fixpoint even (n : nat) : bool := 
    match n with 
    0 => true 
    | S p => negb(odd p) 
    end 
with odd (n : nat) : bool := 
    match n with 
    0 => false 
    | S p => negb (even p) 
    end. 

あなたは、それが定義される前に、機能evenが機能oddを参照していることを、この例では、参照してください。

ここで2番目の例があります。私はBNFのあなたの主導的な隠喩に固執しようとします。文法の記述は帰納的述語として与えることができます。ここでは、加算、乗算、および自然数だけを含む算術式の文法を使った小さな例を示します。

Require Import String Ascii Arith. 

Definition digit (c : ascii) : bool := 
    (nat_of_ascii "0" <=? nat_of_ascii c) && 
    (nat_of_ascii c <=? nat_of_ascii "9"). 

Fixpoint number (s : string) : bool := 
    match s with 
    | String c EmptyString => digit c 
    | String c tl => digit c && number tl 
    | EmptyString => false 
    end. 

Inductive Exp1 : string -> Prop := 
    plus : forall x y, Exp2 x -> Exp1 y -> Exp1 (x ++ "+" ++ y) 
| inj2 : forall x, Exp2 x -> Exp1 x 
with 
    Exp2 : string -> Prop := 
    times : forall x y, Exp3 x -> Exp2 y -> Exp2 (x ++ "*" ++ y) 
| inj3 : forall x, Exp3 x -> Exp2 x 
with 
    Exp3 : string -> Prop := 
| num : forall x, number x = true -> Exp3 x 
| inj1 : forall x, Exp1 x -> Exp3 ("(" ++ x ++ ")"). 

この文法の説明では、指定された式が文法を尊重することが証明できます。

Lemma example : Exp1 "3+2*(5*4)". 
Proof. 
apply (plus "3" "2*(5*4)"). 
    apply inj3. 
    apply num; reflexivity. 
apply inj2. 
apply (times "2" "(5*4)"). 
    apply num; reflexivity. 
apply inj3, (inj1 "5*4"), inj2, (times "5" "4"). 
    apply num; reflexivity. 
apply inj3, num; reflexivity. 
Qed. 

これはパーサーについての説明ではありません。これはもう一つの運動です。

あなたの質問はとても簡潔で、私はこれが答えかどうか分からない。