Stream: Beginner Questions

Topic: How to prove the complement automaton in below way

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 14:29):

I am trying to construct the complement regexp.

First, I construct the NFA automaton, the definition of neg1 automaton takes an automaton and changes its accepts states. I thought it's a straightforward idea.

However, I was stuck by the last lemma, accepts_neg1. Any help would be appreciated. 

type_synonym ('a,'s) na = "'s * 'a set * ('a ⇒'s ⇒ 's set) * ('s ⇒ bool)"

primrec delta :: "('a,'s)na ⇒ 'a list ⇒ 's ⇒ 's set" where
"delta A []    p = {p}" |
"delta A (a#w) p = Union(delta A w ` next A a p)"

definition
 accepts :: "('a,'s)na ⇒ 'a list ⇒ bool" where
"accepts A w = (∃q ∈ delta A w (start A). fin A q)"

definition
 step :: "('a,'s)na ⇒ 'a ⇒ ('s * 's)set" where
"step A a = {(p,q) . q : next A a p}"

primrec steps :: "('a,'s)na ⇒ 'a list ⇒ ('s * 's)set" where
"steps A [] = Id" |
"steps A (a#w) = step A a  O  steps A w"


lemma steps_append[simp]:
 "steps A (v@w) = steps A v  O  steps A w"
by(induct v, simp_all add:O_assoc)

lemma in_steps_append[iff]:
  "(p,r) : steps A (v@w) = ((p,r) : (steps A v O steps A w))"
apply(rule steps_append[THEN equalityE])
apply blast
done

lemma delta_conv_steps: "⋀p. delta A w p = {q. (p,q) : steps A w}"
by(induct w)(auto simp:step_def)

lemma accepts_conv_steps:
 "accepts A w = (∃q. (start A,q) ∈ steps A w ∧ fin A q)"
by(simp add: delta_conv_steps accepts_def)

type_synonym 'a bitsNA = "('a, nat list)na"

definition
neg1 :: "'a bitsNA ⇒ 'a bitsNA" where
"neg1 = (λ(ql,vl1,dl,fl). (ql, vl1, dl, λs. ¬ fl s))"

lemma fin_neg1[iff]:
"⋀L. fin (neg1 L) q = (¬ fin L q)"
  apply(simp add:neg1_def)
  done
lemma start_neg1[iff]:
"⋀L. start (neg1 L) = start L"
  apply (simp add:neg1_def)
  done
lemma step_neg1[iff]:
"⋀L p. (p, q)∈ step (neg1 L) a = ((p, q) ∈ step L a)"
  apply(simp add:neg1_def step_def)
  done



lemma steps_neg1[iff]:
"⋀L p. (p, q)∈ steps (neg1 L) w = ((p, q) ∈ steps L w)"
  apply(induct w)
   apply simp
  apply simp
  apply force
  done

lemma accepts_neg1: accepts (neg1 L) w ⟹ (¬ accepts L w)"
apply (simp add: accepts_conv_steps)
  apply(induct w)
  apply simp
  sorry

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 14:35):

I just think the way is to universal parameter in the state q, but I don't know how to solve it.

view this post on Zulip Maximilian Schäffeler (Jun 05 2023 at 14:55):

What is you definition of next?

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 15:08):

definition start :: "'a * 'b * 'c * 'd ⇒ 'a" where "start A = fst A"
definition alp :: "'a * 'b * 'c * 'd ⇒ 'b" where "alp A = fst(snd(A))"
definition "next" :: "'a * 'b * 'c * 'd ⇒ 'c" where "next A = fst(snd(snd(A)))"
definition fin :: "'a * 'b * 'c * 'd ⇒ 'd" where "fin A = snd(snd(snd(A)))"

view this post on Zulip Mathias Fleury (Jun 05 2023 at 17:49):

Please remove the useless ⋀L p.

view this post on Zulip Mathias Fleury (Jun 05 2023 at 17:50):

And the proof goes through once you realize that you have to generalize over p and q
wrong lemma

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 18:22):

Once remove the L and p, the steps lemma couldn't pass easily

view this post on Zulip Mathias Fleury (Jun 05 2023 at 18:23):

I though a little bit more about it and it is unclear to me if this holds because NFA means that you could have two paths one reaching a final a state and one reaching a non-final state. So negation would still accept the word.

 lemma "accepts (neg1 L) [w] ⟹ (¬ accepts L [w])"
(*
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
  L = ([], {}, λx xa. {[0], []}, UNIV - {[]})
  w = a⇩1
*)

view this post on Zulip Mathias Fleury (Jun 05 2023 at 18:23):

Not sure if the counter-example is correct

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 18:28):

My NFA includes the initial state, alphabet, transition states and accept states.

The transition rules take one alphabet and one state, the state is denoted in a list, then return a list set, like the atom automaton below,

definition
  "atom"  :: "'a ⇒ 'a set ⇒ 'a bitsNA" where
"atom a vs = ([2],vs,
            λb s. if s=[2] ∧ b=a ∧ a : vs then {[3]} else {[1]},
            λs. case s of [] ⇒ False | left#s ⇒ (left#s) = [3])"

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 18:29):

There is no counterexample in my script. 

Testing conjecture with Quickcheck-exhaustive...
Quickcheck ran out of time
Quickcheck found no counterexample.

I don't know exactly.

view this post on Zulip Mathias Fleury (Jun 05 2023 at 18:30):

I replace the path w by a path of length 1 [w]

view this post on Zulip Hongjian Jiang (Jun 05 2023 at 18:34):

Ahh, I see. From the counterexample, the negation of L cound just accept empty list. That's the inital state and any input character.

Last updated: Apr 27 2024 at 20:14 UTC