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.