[CakeML-dev] regexp matcher termination

[Scott Owens]

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