coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] wasting natural fuel is costly
- Date: Wed, 16 Dec 2020 20:31:10 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f174.google.com
- Ironport-phdr: 9a23:SozaOBaiJVKmD2+xR+PDrJD/LSx+4OfEezUN459isYplN5qZrsyybnLW6fgltlLVR4KTs6sC17OJ9fmxAidZvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txjdu80YjIdtN6o8yAbCr2dVdehR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDM/7WrZiNF/jLhDrRyvpxJx3ZPaboKSOvVxYqzTcsgXRXZDU8tLSyBMGJ+wY5UJAuEcPehYtY79p14WoBewBwmsA+Xvyj5LhnDo2a01zfouHBrJ3AwlBd0OsXDUoM/pO6cVVOC5wrTDwDLBb/NR3zf96YvIfQ4lof6SQ719asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRm44YylDK+CpnzYopOdC1SEx2bNC4HZZfqy2XN5Z6TM0+T2xsuSs0yr4LtICncCUW1Zkr2RzSZuCafoWG4h/tWuCcKip7inJ9YL+zmQq+/Ey6xuD/VsS4ykhGojRbntXWq3wA1RPe5tCZRvZ84kutxDOC2x3X5+5YJE05mqvWJ4I9zrM1i5YevkfOEyrylUj1kqObdkAp9+q15OTpbLXro5GcOJFohg7gN6kjlNCwDOUlPgUIQmOV4/6z1Kf58k38WLhKjuM5kq3esJ3CIMQUvK+5AwtM3oY66BazEi6q0NoFkXQFI19JYh2Hj4/uO1HBJPD3E+2zjEirkDdu3/zGP7vhDYvRLnXbjrvtYbJw51RfxQcz19xT+YxYBq8bLP7uWEL8u8TUDhojPAy1x+bnBs991oQbWW+XAK+ZN6XSsV6L5u0xJ+mDepEatS3yK/gg/fHujHs5lUUBcqmu2JsbcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9fIKdHvwIdSjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3Rr2caspTi19Vx6uD7mhQ79DgyBMOYmSnZTWZyn2AFQzI79K96qE15jFyE1P4r0LRjCdVP6qYRAU8BPpnGwrkiUoGgakf6Zt6MDW2ebJCjCDA1QMg2xoZXMUl4EtSmyBvE2njzWuJHp/mwHJUxt5nk8T3xKsJ6kSiU0aAgixw/QZIKOzT52uhw8A/cA4OPmEKcxf7zKfYsmRXV/WLG9lKg+VlCWVcpA6rAVHEbIEDRqIah6w==
I have a recursive Gallina function that uses a nat-typed fuel arg to
guarantee termination. In cases where the function terminates prior to
running out of fuel, I've found that larger than necessary fuel args
are very costly. For example, with a fuel value of 100, the function
takes 30 times longer than if the fuel value is 10 (neither runs out of
fuel, all other args are the same). In both cases, the computation was
done with vm_cast_no_check. Nothing is done with the fuel arg other
than the usual "match fuel with 0 => done | S n => loop n"
recursion idiom.
I guess this is probably due to the overhead of nats in Gallina. But
it is still surprising to me, considering that if I wrote a function to
traverse the first 8 links in a list, I wouldn't expect it to take 30
times longer with a 100-element list than a 10-element list.
Is there a way around this? I'd like to use a constant fuel value
that is plenty large enough, without having to compute one from the
function's arguments that is just barely large enough.
- [Coq-Club] wasting natural fuel is costly, jonikelee AT gmail.com, 12/17/2020
- Re: [Coq-Club] wasting natural fuel is costly, Jason Gross, 12/17/2020
- Re: [Coq-Club] wasting natural fuel is costly, Clément Pit-Claudel, 12/17/2020
- Re: [Coq-Club] wasting natural fuel is costly, jonikelee AT gmail.com, 12/17/2020
- Re: [Coq-Club] wasting natural fuel is costly, Jason Gross, 12/17/2020
- Re: [Coq-Club] wasting natural fuel is costly, jonikelee AT gmail.com, 12/17/2020
Archive powered by MHonArc 2.6.19+.