<div dir="ltr">Share away, Scott. Two other approaches that might work, not sure they have been mentioned. Grigori Rosu <div>has a paper on using extended regexps for runtime verification and he </div><div>shows a bound on the max size of a derivative. The other was done in the</div><div>context of RockSalt where Gang Tan, I think, used some techniques from </div><div>partial derivatives (of regexps) to prove termination. Like Rosu I think</div><div>this was a measure on the size of regexps. I will dig up the papers/links</div><div>when I get to work.</div><div><br></div><div>Alternatively, the current definition of the compiler as a partial function works, although</div><div>it's slower than need be since the domain check has to be proved.</div><div>If the definition of the compiler is rephrased a bit then one can </div><div>prove that (roughly)</div><div><br></div><div>   compiler r = SOME dfa ==> regexp_lang(r) = dfa_lang(dfa)</div><div><br></div><div>and then the domain check is subsumed and doesn't have to be </div><div>explicitly redone.</div><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Mar 9, 2017 at 4:18 AM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I put my thoughts on the termination problem on the internal wiki. I don’t want to publicise them, partially because they include an email from Konrad, and I haven’t asked his permission to share.<br>
<span class="HOEnZb"><font color="#888888"><br>
Scott<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
> On 2017/03/09, at 10:09, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br>
><br>
> This looks like it is formalising Brzozowski’s proof. Traytel and Nipkow have some nice papers along these lines too.<br>
><br>
> It might not be too bad to lose the extra smart constructors. You get bigger DFAs, which was very bad for Konrad’s application, but probably doesn’t matter for the grep application. Alternately, re-normalising might not be bad either as the regexps probably won’t get too big.<br>
><br>
> Scott<br>
><br>
>> On 2017/03/09, at 08:58, Johannes Åman Pohjola <<a href="mailto:pohjola@chalmers.se">pohjola@chalmers.se</a>> wrote:<br>
>><br>
>> Here's one with smart constructors, termination, and equality defined via normalisation in Coq:<br>
>><br>
>> <a href="http://www.diku.dk/hjemmesider/ansatte/henglein/papers/coquand2011.pdf" rel="noreferrer" target="_blank">http://www.diku.dk/<wbr>hjemmesider/ansatte/henglein/<wbr>papers/coquand2011.pdf</a><br>
>><br>
>> I don't know how difficult it might be to express a similar argument in Konrad's setting.<br>
>><br>
>> /Johannes<br>
>><br>
>> On 2017-03-09 09:27, Scott Owens wrote:<br>
>>> I don’t think it’s an easy problem. As far as I know, there is no known proof of termination with the smart constructors, unless you want to re-normalise the expressions before testing equality, and I do know that several people have spent some time thinking about it without getting the solution.<br>
>>><br>
>>> If you get rid of the smart constructors, except for ACI for OR, then you can use Brzozowski’s proof. I don’t know how hard that would be to mechanise.<br>
>>><br>
>>> Scott<br>
>>><br>
>>>> On 2017/03/09, at 07:12, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
>>>><br>
>>>> Hi all,<br>
>>>><br>
>>>> Just checking: is there any chance we might get the termination proof<br>
>>>> for the regular expression matcher done within a week or two? I heard<br>
>>>> it's a very hard problem that people have already sunk a lot of time<br>
>>>> into, so my guess is no. However, this means our top-level spec for<br>
>>>> grep will have an annoying clunky assumption.<br>
>>>><br>
>>>> I guess another way to ask the question: Should I invest time in the<br>
>>>> termination proof or in making the termination assumption prettier?<br>
>>>><br>
>>>> Cheers,<br>
>>>> Ramana<br>
>>> ______________________________<wbr>_________________<br>
>>> Developers mailing list<br>
>>> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>>> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
>><br>
>><br>
>> ______________________________<wbr>_________________<br>
>> Developers mailing list<br>
>> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</div></div></blockquote></div><br></div>