[CakeML-dev] regexp matcher termination
Ramana.Kumar at cl.cam.ac.uk
Thu Mar 9 07:12:27 UTC 2017
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?
More information about the Developers