[CakeML-dev] regexp matcher termination

[Konrad Slind]

Here's the pointer to the RockSalt stuff.

https://github.com/gangtan/CPUmodels/blob/master/x86model/Model/Recognizer.v

Termination lemma is around line 1256.


On Thu, Mar 9, 2017 at 8:25 AM, Konrad Slind <konrad.slind at gmail.com> wrote:

> 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/43290274/attachment-0001.html>