[CakeML-dev] regexp matcher termination

[Konrad Slind]

Rosu and Viswanathan:

http://fsl.cs.illinois.edu/FSL/papers/2003/rosu-viswanathan-2003-rta/rosu-viswanathan-2003-rta-public.pdf


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

> 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/coqua
>>> nd2011.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/bac29aae/attachment.html>