有限オートマトンCoqを定義する

Question

私はCoqを学習しています。これを正規言語理論、特に有限オートマトンの形式化に使用したいと思います。のは、次のように私はオートマトンのための構造を持っているとしましょう：

状態として誘導型である

Record automata : Type := { 
dfa_set_states : list state; 
init_state : state; 
end_state : state; 
dfa_func: state -> terminal -> state; 
}. 

：

Inductive state:Type := 
S. 

と型端子端子は、私がしようとしています

Inductive terminal:Type := 
a | b. 

です後でそれを定義することで、通常の言語の定義を一般化することができます。今のところ、{a、b}アルファベットのすべての単語である言語（a * b *）を認識するオートマトンを構築したいと考えています。誰かが（私は端末のリストとして表示される）単語を実行し、そのオートマトンがその言葉を再現するかどうかを教えてくれる固定点機能を構築する方法についてのアイデアを持っていますか？どんなアイデアや助けも大いに評価されます。

ありがとうございます。 Erick。

Answer 1

あなたは自分自身を通常の言語に制限しているので、これは非常に簡単です：折り畳みを使用するだけです。ここではサンプルです：

Require Import Coq.Lists.List. 
Import ListNotations. 

Set Implicit Arguments. 
Unset Strict Implicit. 
Unset Printing Implicit Defensive. 

Record dfa (S A : Type) := DFA { 
    initial_state : S; 
    is_final : S -> bool; 
    next : S -> A -> S 
}. 

Definition run_dfa S A (m : dfa S A) (l : list A) : bool := 
    is_final m (fold_left (next m) l (initial_state m)). 

このスニペットは状態とアルファベットのコンポーネントは、現在DFAのパラメータを入力しているという点で、あなたのオリジナルの定義から少し異なっており、その中で、私は述語と終了状態を交換しました私たちが受諾状態にあるかどうかに対応します。 run_dfa関数は、単にDFAの遷移関数を初期状態から反復し、最後の状態が受け入れ状態であるかどうかをテストします。

このインフラストラクチャを使用して、通常の言語をほとんど記述することができます。例えば、ここにa*b*を認識するためのオートマトンです：

Inductive ab := A | B. 

Inductive ab_state : Type := 
    ReadA | ReadB | Fail. 

Definition ab_dfa : dfa ab_state ab := {| 
    initial_state := ReadA; 
    is_final s := match s with Fail => false | _ => true end; 
    next s x := 
    match s, x with 
    | ReadB, A => Fail 
    | ReadA, B => ReadB 
    | _, _ => s 
    end 
|}. 

私たちは、このオートマトンは我々が期待していることを証明することができます。

Lemma ab_dfa_complete n m : run_dfa ab_dfa (repeat A n ++ repeat B m) = true. 
Proof. 
    unfold run_dfa. rewrite fold_left_app. 
    assert (fold_left (next ab_dfa) (repeat A n) (initial_state ab_dfa) = ReadA) as ->. 
    { now simpl; induction n as [| n IH]; simpl; trivial. } 
    destruct m as [|m]; simpl; trivial. 
    induction m as [|m IH]; simpl; trivial. 
Qed. 

我々はまた、それは、その言語の文字列のみを受け入れることを言う会話、そして他には何を述べることができる：ここではそれが求められた言語の文字列を受け入れることを言うの定理があります。私は証拠を残しました。それを理解することは難しいことではありません。

Lemma ab_dfa_sound l : 
    run_dfa ab_dfa l = true -> 
    exists n m, l = repeat A n ++ repeat B m. 

残念ながら、この表現ではオートマトンを実行する以外にはあまりできません。特に、オートマトンを最小化することはできず、2つのオートマトンが同等かどうかをテストすることはできません。これらの関数は、州とアルファベットのすべての要素、すなわちSとAを列挙する引数リストとしても必要です。