[FOM] regular expressions

[Adam Kolany]

Vaughan Pratt wrote:
> Adam Kolany wrote:
>   
>> I am sorry for possibly trivial questions:
>>     1. Is the problem of equality of languages given by two regular
>> expresions equal decidable?
>>     2. Is there a (decidable) formal system for proving the above
>> equalities?
>>     

>> ....
>>     

>> For Proposition 1, take an infinite tree T all of whose vertices are of 
>> out-degree the cardinality s of the alphabet S.  All are of in-degree 1 
>> save the root vertex which is of in-degree zero.  There are no 
>> leaves---all paths are infinite.
>>
>> Label the s edges leaving each vertex of T with the respective s letters 
>> of S.
>>
>>     
...
...
>> Now associate to every vertex v of T the language w\L defined as the set 
>> of those words x in S* such that wx is in L, where w is the word 
>> labeling v per the above procedure.  Call two vertices with labels v and 
>> w *equivalent* when v\L = w\L, that is, when the two subtrees with 
>> respective roots v and w are made equivalent automata by taking the 
>> respective subtree's root to be the start state in each case.  (The 
>> final states remain marked as originally.)
>>
>> One can show that the automaton obtained by identifying equivalent 
>> vertices is the final automaton A_L in the category of all deterministic 
>> automata accepting L.  It has the further property that *any* automaton 
>> accepting L can be turned into the final one by identifying states (the 
>> sense in which it is final).  This is crucial for the last stage of the 
>> construction in Proposition 2.
>>
>>     

Thanks again for answering my question.
One little question:
In the definition of A_L however, we use an infinite structure, which
cannot be used in any algorithm.
Can the automaton A_L be obtained in a more straigthforward way?
....

regards, Adam