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