--- /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.
+