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.