[CakeML-dev] regexp matcher termination

[Konrad Slind]

Share away, Scott. Two other approaches that might work, not sure they have
been mentioned. Grigori Rosu
has a paper on using extended regexps for runtime verification and he
shows a bound on the max size of a derivative. The other was done in the
context of RockSalt where Gang Tan, I think, used some techniques from
partial derivatives (of regexps) to prove termination. Like Rosu I think
this was a measure on the size of regexps. I will dig up the papers/links
when I get to work.

Alternatively, the current definition of the compiler as a partial function
works, although
it's slower than need be since the domain check has to be proved.
If the definition of the compiler is rephrased a bit then one can
prove that (roughly)

   compiler r = SOME dfa ==> regexp_lang(r) = dfa_lang(dfa)

and then the domain check is subsumed and doesn't have to be
explicitly redone.

Konrad.


On Thu, Mar 9, 2017 at 4:18 AM, Scott Owens <S.A.Owens at kent.ac.uk> wrote:

> 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
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170309/59d810a4/attachment.html>