유한 오토 마타 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 *라는 언어를 인식하는 오토 마타를 만들고 싶습니다. 누구나 단어를 실행하는 고정 점 기능을 빌드하는 방법에 대한 아이디어가 있습니까 (터미널 목록으로 볼 수 있음). 자동 작성 기능이 해당 단어를 재구성하는지 여부를 알려주십시오. 모든 아이디어/도움이 크게 평가됩니다.

미리 감사드립니다. 에릭.

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의 전환 함수를 초기 상태에서 시작하여 단순히 반복 한 다음 마지막 상태가 수락 상태인지 여부를 테스트합니다.

이 인프라를 사용하여 일반 언어를 거의 설명 할 수 있습니다.

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 
|}. 

우리는이 기계적으로 우리가 무엇을 기대한다는 것을 증명할 수있다 : 예를 들어, 여기 a*b*을 인식 자동 장치입니다. 우리는 또한 그 언어의 문자열 및 아무것도를 수용하는 것을 말한다 역을 명시 할 수

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을 열거하는 인수 목록을 취해야합니다.