[CakeML-dev] regexp matcher termination

Scott Owens S.A.Owens at kent.ac.uk
Thu Mar 9 10:18:47 UTC 2017


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.

Scott

> On 2017/03/09, at 10:09, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> 
> This looks like it is formalising Brzozowski’s proof. Traytel and Nipkow have some nice papers along these lines too.
> 
> 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.
> 
> Scott
> 
>> On 2017/03/09, at 08:58, Johannes Åman Pohjola <pohjola at chalmers.se> wrote:
>> 
>> Here's one with smart constructors, termination, and equality defined via normalisation in Coq:
>> 
>> http://www.diku.dk/hjemmesider/ansatte/henglein/papers/coquand2011.pdf
>> 
>> I don't know how difficult it might be to express a similar argument in Konrad's setting.
>> 
>> /Johannes
>> 
>> On 2017-03-09 09:27, Scott Owens wrote:
>>> 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.
>>> 
>>> 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.
>>> 
>>> Scott
>>> 
>>>> On 2017/03/09, at 07:12, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
>>>> 
>>>> Hi all,
>>>> 
>>>> Just checking: is there any chance we might get the termination proof
>>>> for the regular expression matcher done within a week or two? I heard
>>>> it's a very hard problem that people have already sunk a lot of time
>>>> into, so my guess is no. However, this means our top-level spec for
>>>> grep will have an annoying clunky assumption.
>>>> 
>>>> I guess another way to ask the question: Should I invest time in the
>>>> termination proof or in making the termination assumption prettier?
>>>> 
>>>> Cheers,
>>>> Ramana
>>> _______________________________________________
>>> Developers mailing list
>>> Developers at cakeml.org
>>> https://lists.cakeml.org/listinfo/developers
>> 
>> 
>> _______________________________________________
>> Developers mailing list
>> Developers at cakeml.org
>> https://lists.cakeml.org/listinfo/developers
> 
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers



More information about the Developers mailing list