3

我正在学习 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} 字母表中的所有单词。有没有人知道如何构建某种定点函数来运行单词（我将其视为终端列表）并告诉我该自动机是否识别该单词？任何想法/帮助将不胜感激。

在此先感谢，埃里克。

4

1 回答 1

4

因为您将自己限制在常规语言中，所以这很简单：您只需要使用折叠即可。这是一个示例：

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。

于 2017-05-12T18:53:49.550 回答