# HG changeset patch # User urbanc # Date 1315857021 0 # Node ID 061b32d78471703041a5a1074b8af8cff86871bb # Parent 47446f111550d20b46c8e0ac8115c14197f6032e a final polishing before submitting later this week diff -r 47446f111550 -r 061b32d78471 Journal/Paper.thy --- a/Journal/Paper.thy Thu Sep 08 15:08:02 2011 +0000 +++ b/Journal/Paper.thy Mon Sep 12 19:50:21 2011 +0000 @@ -427,7 +427,7 @@ regular expressions. This theorem gives necessary and sufficient conditions for when a language is regular. As a corollary of this theorem we can easily establish the usual closure properties, including complementation, for - regular languages. We use the continuation lemma \cite{Rosenberg06}, + regular languages. We use the Continuation Lemma \cite{Rosenberg06}, which is also a corollary of the Myhill-Nerode Theorem, for establishing the non-regularity of the language @{text "a\<^isup>nb\<^isup>n"}.\medskip @@ -2398,8 +2398,8 @@ equational system is set up. We have the $\lambda$-term on our `initial state', while Brzozowski has it on the terminal states. This means we also need to reverse the direction of Arden's Lemma. We have not found anything - in the literature about our way of proving the first direction of the - Myhill-Nerode Theorem, but it appears to be folklore. + in the `pencil-and-paper-reasoning' literature about our way of proving the + first direction of the Myhill-Nerode Theorem, but it appears to be folklore. We presented two proofs for the second direction of the Myhill-Nerode Theorem. One direct proof using tagging-functions and another using partial diff -r 47446f111550 -r 061b32d78471 Journal/document/root.bib --- a/Journal/document/root.bib Thu Sep 08 15:08:02 2011 +0000 +++ b/Journal/document/root.bib Mon Sep 12 19:50:21 2011 +0000 @@ -15,7 +15,7 @@ author = {L.~H.~Haines}, title = {{O}n {F}ree {M}onoids {P}artially {O}rdered by {E}mbedding}, journal = {Journal of Combinatorial Theory}, - year = {1996}, + year = {1969}, volume = {6}, pages = {94--98} } diff -r 47446f111550 -r 061b32d78471 Literature/Slind --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Literature/Slind Mon Sep 12 19:50:21 2011 +0000 @@ -0,0 +1,165 @@ +A student who is attempting to prove the pumping lemma for regular +languages came across the following problem. Suppose a DFA is +represented by a record <| init ; trans ; accept |> where + + init : 'state + trans : 'state -> 'symbol -> 'state + accept : 'state -> bool + +Execution of a DFA on a string: + + (Execute machine [] s = s) + (Execute machine (h::t) s = Execute machine t (machine.trans s h)) + +Language recognized by a machine D: + + Lang(D) = {x | D.accept (Execute D x D.init)} + +These are all accepted by HOL with no problem. In then trying to define +the +set of regular languages, namely those accepted by some DFA, the +following +is natural to try + + Regular (L:'symbol list -> bool) = ?D. L = Lang(D) + +But this fails, since D has two type variables ('state and 'symbol) but +Regular is a predicate on 'symbol lists. So the principle of definition +rejects. + +So now my questions. + +1. Is there a work-around (other than not attempting to define Regular, + or defining regularity through some other device, like regular +expressions). + +2. I'm aware that examples of this kind have cropped up from time to +time, + and I'd like to hear of any others you've encountered. + +Thanks, +Konrad. + + + +----------------------------------------- +Hi Konrad, + +| Regular (L:'symbol list -> bool) = ?D. L = Lang(D) +| +| But this fails, since D has two type variables ('state and 'symbol) but +| Regular is a predicate on 'symbol lists. So the principle of definition +| rejects. + +This is a classic case where adding quantifiers over type variables, as +once suggested by Tom Melham, would really help. + +| 2. I'm aware that examples of this kind have cropped up from time to +| time, and I'd like to hear of any others you've encountered. + +The metatheory of first order logic (this is close to Hasan's example). +In the work I reported at TPHOLs'98 I wanted to define the notion of +"satisfiable" for first order formulas, but this cannot be done in the +straightforward way you'd like. See the end of section 3 of: + + http://www.cl.cam.ac.uk/users/jrh/papers/model.html + +| 1. Is there a work-around (other than not attempting to define Regular, +| or defining regularity through some other device, like regular +| expressions). + +You could define it over some type you "know" to be adequate, such +as numbers (Rob) or equivalence classes of symbol lists (Ching Tsun). +Then you could validate the definition by proving that it implies +the analogous thing over any type. In first-order logic, this was +precisely one of the key things I wanted to prove anyway (the +downward Loewenheim-Skolem theorem) so it wasn't wasted effort. + + |- (?M:(A)model. M satisfies p) ==> (?M:(num)model. M satisfies p) + +Where "A" is a type variable. That's an abstraction of the actual +statement proved, which is given towards the end of section 4. + +John. + +----------------------------------------------------- + +On Apr 21, 2005, at 1:10 PM, Rob Arthan wrote: +>> +>> So now my questions. +>> +>> 1. Is there a work-around (other than not attempting to define +>> Regular, +>> or defining regularity through some other device, like regular +>> expressions). +> +> I was going to say: instantiate 'state to num in the definition - +> after all, DFAs only have finitely many states so the states can +> always be represented by numbers. + +Good idea. + +> +> But your student's definitions don't captured the tiniteness +> requirement. And they need to! As things stand every language L is +> regular via the machine with states being lists of symbols and with +> +> init = [] +> trans st sym = st @ [sym] +> accept = L + +Good example, sorry about my shoddy presentation: I gave an overly +simplified +version. A better version would be something like the following: + +Hol_datatype `dfa = <| states : 'a -> bool ; + symbols : 'b -> bool ; + init : 'a ; + trans : 'a->'b->'a ; + accept : 'a -> bool |>`; + + Define + `DFA(M) = + FINITE M.states /\ + FINITE M.symbols /\ + ~(M.states = {}) /\ + ~(M.symbols = {}) /\ + M.accept SUBSET M.states /\ + M.init IN M.states /\ + !(a:'symbol) (s:'state). + a IN M.symbols /\ s IN M.states ==> (M.trans s a) IN +M.states`; + + +Define `(Exec D [] s = s) /\ + (Exec D (h::t) s = Exec D t (D.trans s h))`; + +Define `Lang D = {x | D.accept (Exec D x D.init)}`; + +(* Urk! *) + +Define `Regular L = ?D::DFA. L = Lang D`; + +> +> if you take account of finiteness properly, then instantiating 'state +> to num will give the right answer.; And it gives another proof +> opportunity! (Namely to prove that the instantiated definition is +> equivalent to the definition you really wanted). + +That's a nice bit of spin: a proof opportunity! + +> +>> +>> 2. I'm aware that examples of this kind have cropped up from time to +>> time, +>> and I'd like to hear of any others you've encountered. +>> +> +> Free algebraic structures provide a vast set of examples. +> +> +Very interesting. Can you give some specific examples? + +Thanks, +Konrad. +