The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

If you're using fuel it is fairly easy to make it structurally 
decreasing with a simple Fixpoint because fuel can just decrease by 1, 
instead of using a Program and proving decreasingness with respect to lt.

Li-yao

---

Fixpoint ackermann_fuel (fuel : nat) (m n : nat) : nat :=
  match fuel with
  | 0 => 0 (* Ran out of fuel! Give a default value of 0. *)
  | S fuel =>
    match m with
    | 0 => S n
    | S m' =>
      match n with
      | 0 => ackermann_fuel fuel m' 1
      | S n' => ackermann_fuel fuel m' (ackermann_fuel (pred fuel) m n')
      end
    end
  end.

Compute (ackermann_fuel 100 3 3).


On 11/1/18 12:09 PM, Peter E Schmidt-Nielsen wrote:
> Using a fuel quantity seems like a reasonable solution whenever you can 
> easily produce a default value when you run out of fuel. Here's an 
> example of performing this transformation generically on a recursive 
> function, using a nat to track the fuel:
>
> https://gist.github.com/petersn/361c40b3394a3ad9721b738ac61d48b1
>
> Of course, if we switched to using a binary number for the fuel then we 
> could trivially just pass in 2^300 for the fuel and get a definition 
> which won't run out of fuel before the heat death of the universe.
>
> However, some library theorems (N.lt_pred_l and N.lt_wf_0) are opaque, 
> blocking the binary version in the above gist from computing. I'm 
> wondering if anyone more experienced here knows if there're some 
> transparent versions elsewhere I don't know about, or if I'm missing 
> something silly?
>
> -snp
>
> On Thu, 1 Nov 2018, Klaus Ostermann wrote:
>
> > It's maybe not particularly elegant or sophisticated, but what about
> > just adding "fuel" as an additional argument
> > and initializing with a sufficient amout of fuel?
> >
> > Klaus
> >
> >
> > Am 01.11.18 um 12:21 schrieb Thorsten Altenkirch:
> > > Is there a way to run possibly non-terminating programs in the coq
> > > type checker. In Agda you can just switch off the termination checker.
> > >
> > >
> > >
> > > I think this is useful if you want to use something whose termination
> > > you haven't yet proven but want to exploit reduction.
> > >
> > >
> > >
> > > Hence it is not enough to add the assumption that it terminates as an
> > > axiom because this won't reduce.
> > >
> > > Thorsten
> > >
> > > This message and any attachment are intended solely for the addressee
> > > and may contain confidential information. If you have received this
> > > message in error, please contact the sender and delete the email and
> > > attachment.
> > >
> > > Any views or opinions expressed by the author of this email do not
> > > necessarily reflect the views of the University of Nottingham. Email
> > > communications with the University of Nottingham may be monitored
> > > where permitted by law.