coq - 定义有限自动机 Coq

Question

我正在学习 Coq，我想用它来形式化正则语言理论，特别是有限自动机。假设我有一个自动机结构如下:

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

其中 state 是归纳类型:

Inductive state:Type :=
S.

终端的类型是

Inductive terminal:Type :=
a | b.

我正在尝试定义它，以便稍后我能够概括任何常规语言的定义。现在，我想构建一个自动机来识别语言 (a * b *)，它是 {a,b} 字母表中的所有单词。有没有人知道如何构建某种固定点函数来运行单词(我将其视为终端列表)并告诉我该自动机是否识别该单词？任何想法/帮助将不胜感激。

提前致谢，埃里克。

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.

不幸的是，除了运行自动机之外，我们对这种表示无能为力。特别是，我们不能最小化自动机，测试两个自动机是否等价等。这些函数还需要将枚举状态和字母类型的所有元素的列表作为参数，S 和 A.