[CakeML-dev] regexp matcher termination

Johannes Åman Pohjola pohjola at chalmers.se
Thu Mar 9 08:58:53 UTC 2017

Here's one with smart constructors, termination, and equality defined 
via normalisation in Coq:


I don't know how difficult it might be to express a similar argument in 
Konrad's setting.


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

More information about the Developers mailing list