[CakeML-dev] regexp matcher termination

[Johannes Åman Pohjola]

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