coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Clément Pit-Claudel <cpitclaudel AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] wasting natural fuel is costly
- Date: Thu, 17 Dec 2020 11:19:45 -0500
- Authentication-results: mail3-smtp-sop.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:hDhyrBbUbD5qL0r8xqmBnSf/LSx+4OfEezUN459isYplN5qZrsu7bnLW6fgltlLVR4KTs6sC17OJ9fmxAidZucfJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRe7oR/MusQSj4ZuJbs9xgfNr3BVZ+lY2GRkKE6JkR3h/Mmw5plj8ypRu/Il6cFNVLjxcro7Q7JFEjkoKng568L3uxbNSwuP/WYcXX4NkhVUGQjF7Qr1UYn3vyDnq+dywiiaPcnxTbApRTSv6rpgRRH0hCsbMTMy7XragdJsgq1FvB2hpgR/w4/Kb4GTKPp+Zb7WcdcDSWZcQspdSylND4WhZIUNEuUBJ/5VoYf9qVUQsBWwBgujBO3oxDBHmnD40rY30/g4EQzcwAAtBc4CvXbSod7oNKkSS+e1zKzQwDnNbfNW3jH96InLch8/pfGDQ6x/fNHeyUkqDQzFj1GQpZb5MDOS0+QBvXWQ4u1iVeKojW4nqgJxrSarxsgylIbEnY0VylXe+iV4xIY5P8G3SEl+YdO9FpZbqi6VOZdsTMw4X2FopDg1yqcAuZOjYCUG1pYqyhHBZvGFcoWG7BLtWfqRLDp8mn9oeayyiguy/ES81+HxV9e43UhXoydbndTAqm4A2RLP58WETvZw/kGs0iuM2QDL8uxIP1w4mK7BJ5MiwrM8jIQfvVrdEiPshUn7jqCbel069uWp9+jrf7DrqoKYOoBojwzzPaUjltCjDek9LwQDUWmW9OG82bH//kD2XbBHg/0yn6nXvpDXIMobqbC2DgJU14sv9RayACm639kegHIJNkhKeAidgIjsI1zOIO73DfO4g1m0lTdk3fHGPrn4DpXULXjPja7tfbhg50Nexwc/199f55VTCrEOJPL8RFX9u8DfDh88KwC0wuDnB8th1o4GR26DHquUPLnRvFKI/O4jPfeAaJEPtDrgKfUo6ObijXojll8ceamp04EXaHe9Hvl+IUWZZnzsgtYCEWgUugoxUvLlhUaNUT5WfXmyXqY86isnB4KhCIfPXpqtj6CZ3CenAp1WYXhLBUyLEXfxbomLR/MMaD+JLcJ6iTwFVb2hS5c72h20tQ/6zaBnLuvO9SECu5Ljzos92+qGvhWz8DFyE4yl0n3IZGV9g28FQ3di17h+vUd5w0qP3KxQjPlRFNgV7PRMBFQUL5nZmqZ4DNbzWQ/Fc9qhR1OvQ9HgCjY0BJplwdgIYkVwH9ivph/G1iuuRbQSkurYV9QP7qvA0i2pdI5GwHHc2fxk1gF+G5YdBSidnqd6sjPrKcvJnkGezfj4cK0d2GvU9z7GwzPR4AdXVwl/VaiDVncaNBOP/IbJo3jaRrrrMowJdw5IyMqMMKxPM4S7glBPRfOlM9PbMTvoxzWAQC2Qz7bJV7LEPn0H1XyEWkcBmgEXu32BMFpmCw==
My bad. There is something else going on in the recursive function.
It passes the recursive call as a continuation, which is being called
more often than I thought, and is running until out of fuel in some
cases even though the outer recursion doesn't.
I wish there was an easy way to debug Gallina code.
Thanks anyway to Jason and Clément for the suggestions.
On Wed, 16 Dec 2020 21:41:36 -0500
Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:
> On 12/16/20 8:31 PM, jonikelee AT gmail.com wrote:
> > 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).
>
> What if you pass much larger fuel values, like 10000?
>
> > 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.
>
> The 30x factor is surprising, but a small difference wouldn't be
> entirely unexpected for large constants, since they have to be
> constructed. Try replacing 100 with (Nat.of_uint 100%uint), or
> passing 10000 as the fuel (which will automatically get interpreted
> as (Nat.of_uint 10000%uint)):
>
> Fixpoint collatz (fuel: nat) (start: positive) :=
> match fuel with
> | O => false
> | S fuel =>
> match start with
> | xO x => collatz fuel x
> | xI _ => collatz fuel (start * 3 + 1)
> | xH => true
> end
> end.
>
> Require Import Decimal.
>
> Time Compute (collatz 50 150). 0s
> Time Compute (collatz 2000 150). 0.006s
> Time Compute (collatz 5000 150). 0.021s
> Time Compute (collatz 10000 150). 0s (w/ warning)
>
>
>
- [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+.