Discussion:
run recursive programs in coq
(too old to reply)
Thorsten Altenkirch
2018-11-01 11:21:17 UTC
Permalink
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.
Klaus Ostermann
2018-11-01 11:30:24 UTC
Permalink
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
Post by 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.
Peter E Schmidt-Nielsen
2018-11-01 16:09:33 UTC
Permalink
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
Post by Klaus Ostermann
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
Post by 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.
Bas Spitters
2018-11-01 16:21:23 UTC
Permalink
We have a bit of discussion on avoiding evaluation of such
propositions in section 4.4. of our paper on real number computation
here.
A trick is to wrap it in a /-abstraction. We observe that this would
not be needed if Coq evaluated propositions lazily.

Type classes for efficient exact real arithmetic in Coq
Robbert Krebbers, Bas Spitters
https://arxiv.org/abs/1106.3448
Post by Peter E Schmidt-Nielsen
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,
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
Post by Klaus Ostermann
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
Post by 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.
Li-yao Xia
2018-11-01 16:35:15 UTC
Permalink
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).
Post by Peter E Schmidt-Nielsen
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
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
Post by Klaus Ostermann
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
Post by 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.
Daniel Schepler
2018-11-01 17:25:05 UTC
Permalink
Post by Li-yao Xia
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.
Or, to put a bit of monad-type synactic sugar around it:

Definition fuelled (X : Type) : Type :=
nat -> option X.

Definition return_ {X : Type} (x : X) : fuelled X :=
fun _ => Some x.

Definition bind {X : Type} (x : fuelled X)
{Y : Type} (f : X -> fuelled Y) :
fuelled Y :=
fun fuel => match x fuel with
| Some x0 => match f x0 fuel with
| Some y0 => Some y0
| None => None
end
| None => None
end.

Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))
(x0 ident, at level 20, right associativity).

Definition recursive_call {X:Type} (x : fuelled X) :
fuelled X :=
fun fuel => match fuel with
| S fuel_pred => x fuel_pred
| O => None
end.

Definition ackermann_fuel : nat -> nat -> fuelled nat :=
fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=
match m with
| O => return_ (S n)
| S m' => match n with
| O => recursive_call (F m' 1)
| S n' =>
do x <- recursive_call (F m n');
recursive_call (F m' x)
end
end fuel.

Definition run_with_fuel {X:Type} (x : fuelled X)
(fuel : nat) :=
x fuel.

Compute (run_with_fuel (ackermann_fuel 3 3) 100)
--
Daniel Schepler
Peter E Schmidt-Nielsen
2018-11-01 22:05:59 UTC
Permalink
Good point Li-yao, I feel really silly for writing "Program Fixpoint" for
the nat-fueled version. I copied it over by analogy from the BinNat-fueled
version I tried to get to work when I saw Klaus's original suggestion to
use fuel. I got stuck on the BinNat version, and somehow had a moment of
silliness and forgot that obviously Program Fixpoint's features are
completely unnecessary with a plain nat for fuel.

Daniel's sugar for making this easier to write also looks great.

Not to hijack the thread, but I'm really curious if anyone has any leads
on getting the BinNat-fueled version (appearing below the nat-fueled one
in my gist) to work? The great thing about such a version is that you can
just past in some obscene value like 2^200 for the fuel in every case and
never worry about it, while with a nat for fuel I'm quite constrained on
how much fuel I can provide. (I figure this isn't really thread hijacking,
because I think getting a BinNat-fueled version working would basically
practically solve this issue for OP.)

I looked at the "Type classes for efficient exact real arithmetic in Coq"
paper that was linked, but I'm not sure the laziness suggested via eta
expansion solves this problem, as I'm 98% sure that the output of Program
Fixpoint actually really does need to compute through the opaque parts of
N.lt_pred_l and N.lt_wf_0, although maybe I'm missing the point.

If there were some generic mechanism that could take an opaque term and
trace all the dependencies Print Opaque Dependencies style and make a
transparent version (or somehow override the opacity) then it would
completely solve the problem...

Thanks,

-snp
Post by Daniel Schepler
Post by Li-yao Xia
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.
Definition fuelled (X : Type) : Type :=
nat -> option X.
Definition return_ {X : Type} (x : X) : fuelled X :=
fun _ => Some x.
Definition bind {X : Type} (x : fuelled X)
fuelled Y :=
fun fuel => match x fuel with
| Some x0 => match f x0 fuel with
| Some y0 => Some y0
| None => None
end
| None => None
end.
Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))
(x0 ident, at level 20, right associativity).
fuelled X :=
fun fuel => match fuel with
| S fuel_pred => x fuel_pred
| O => None
end.
Definition ackermann_fuel : nat -> nat -> fuelled nat :=
fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=
match m with
| O => return_ (S n)
| S m' => match n with
| O => recursive_call (F m' 1)
| S n' =>
do x <- recursive_call (F m n');
recursive_call (F m' x)
end
end fuel.
Definition run_with_fuel {X:Type} (x : fuelled X)
(fuel : nat) :=
x fuel.
Compute (run_with_fuel (ackermann_fuel 3 3) 100)
--
Daniel Schepler
Gaëtan Gilbert
2018-11-01 22:11:07 UTC
Permalink
Post by Peter E Schmidt-Nielsen
I'm 98% sure that the output of
Program Fixpoint actually really does need to compute through the opaque
parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing the point.
Yes, this is a known problem, see https://github.com/coq/coq/pull/7060
(which is not progressing currently, see discussion there)

Gaëtan Gilbert
Post by Peter E Schmidt-Nielsen
Good point Li-yao, I feel really silly for writing "Program Fixpoint"
for the nat-fueled version. I copied it over by analogy from the
BinNat-fueled version I tried to get to work when I saw Klaus's original
suggestion to use fuel. I got stuck on the BinNat version, and somehow
had a moment of silliness and forgot that obviously Program Fixpoint's
features are completely unnecessary with a plain nat for fuel.
Daniel's sugar for making this easier to write also looks great.
Not to hijack the thread, but I'm really curious if anyone has any leads
on getting the BinNat-fueled version (appearing below the nat-fueled one
in my gist) to work? The great thing about such a version is that you
can just past in some obscene value like 2^200 for the fuel in every
case and never worry about it, while with a nat for fuel I'm quite
constrained on how much fuel I can provide. (I figure this isn't really
thread hijacking, because I think getting a BinNat-fueled version
working would basically practically solve this issue for OP.)
I looked at the "Type classes for efficient exact real arithmetic in
Coq" paper that was linked, but I'm not sure the laziness suggested via
eta expansion solves this problem, as I'm 98% sure that the output of
Program Fixpoint actually really does need to compute through the opaque
parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing the point.
If there were some generic mechanism that could take an opaque term and
trace all the dependencies Print Opaque Dependencies style and make a
transparent version (or somehow override the opacity) then it would
completely solve the problem...
Thanks,
-snp
Post by Daniel Schepler
Post by Li-yao Xia
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.
Definition fuelled (X : Type) : Type :=
nat -> option X.
Definition return_ {X : Type} (x : X) : fuelled X :=
fun _ => Some x.
Definition bind {X : Type} (x : fuelled X)
 fuelled Y :=
fun fuel => match x fuel with
           | Some x0 => match f x0 fuel with
                        | Some y0 => Some y0
                        | None => None
                        end
           | None => None
           end.
Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))
 (x0 ident, at level 20, right associativity).
 fuelled X :=
fun fuel => match fuel with
           | S fuel_pred => x fuel_pred
           | O => None
           end.
Definition ackermann_fuel : nat -> nat -> fuelled nat :=
fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=
match m with
| O => return_ (S n)
| S m' => match n with
         | O => recursive_call (F m' 1)
         | S n' =>
           do x <- recursive_call (F m n');
           recursive_call (F m' x)
         end
end fuel.
Definition run_with_fuel {X:Type} (x : fuelled X)
 (fuel : nat) :=
x fuel.
Compute (run_with_fuel (ackermann_fuel 3 3) 100)
--
Daniel Schepler
Jean-Christophe Léchenet
2018-11-09 18:26:05 UTC
Permalink
Here is a workaround with a custom proof of well-foundedness using
"Wf_nat.well_founded_lt_compat". The drawback is that the proof of
"lt_wf" thus internally converts to "nat", and thus the computation of
"ackermann" produces a stack overflow even on small inputs. The solution
is to use "lazy" evaluation instead of "cbv".
I also understood why "Solve Obligations" did not work. You need to
start the solving tactic with "program_simplify" (or even
"program_simpl" ?) that cleans the goal a bit. This seems to be done
automatically by "Next Obligation", but not by "Solve Obligations".

Jean-Christophe

Require Import Coq.Numbers.BinNums.
Require Import Coq.NArith.BinNat.
Require Import Program.
Require Import Psatz.

Lemma lt_lt : forall n1 n2, (n1 < n2)%N -> N.to_nat n1 < N.to_nat n2.
Proof. intros; lia.
Qed.

Lemma lt_wf : well_founded N.lt.
Proof.
  apply Wf_nat.well_founded_lt_compat with (f:=N.to_nat).
  apply lt_lt.
Defined.

Ltac discharge_obligation' :=
  program_simplify;
  match goal with
  | [ H : 0%N <> _ |- _ ] => apply N.lt_pred_l; apply not_eq_sym; exact H
  | _ => apply measure_wf; apply lt_wf
  end.

Program Fixpoint ackermann_fuel' (fuel : N) (m n : nat) {wf N.lt fuel} :
nat :=
  match fuel with
  | N0 => 0 (* Default case when out of fuel. *)
  | _ =>
    match m with
    | 0 => S n
    | S m' =>
      match n with
      | 0 => ackermann_fuel' (Npred fuel) m' 1
      | S n' => ackermann_fuel' (Npred fuel) m' (ackermann_fuel' (Npred
fuel) m n')
      end
    end
  end.
Solve Obligations with discharge_obligation'.

(* Define ackermann to launch ackermann_fuel' with enough fuel to last
until the end of the universe. *)
Definition ackermann (n m : nat) := ackermann_fuel' (Npow 2 200) n m.

Fail Eval cbv in ackermann 3 3  (* Stack overflow *).
Eval lazy in ackermann 3 3 (* 61 *).
Post by Peter E Schmidt-Nielsen
Good point Li-yao, I feel really silly for writing "Program Fixpoint"
for the nat-fueled version. I copied it over by analogy from the
BinNat-fueled version I tried to get to work when I saw Klaus's
original suggestion to use fuel. I got stuck on the BinNat version,
and somehow had a moment of silliness and forgot that obviously
Program Fixpoint's features are completely unnecessary with a plain
nat for fuel.
Daniel's sugar for making this easier to write also looks great.
Not to hijack the thread, but I'm really curious if anyone has any
leads on getting the BinNat-fueled version (appearing below the
nat-fueled one in my gist) to work? The great thing about such a
version is that you can just past in some obscene value like 2^200 for
the fuel in every case and never worry about it, while with a nat for
fuel I'm quite constrained on how much fuel I can provide. (I figure
this isn't really thread hijacking, because I think getting a
BinNat-fueled version working would basically practically solve this
issue for OP.)
I looked at the "Type classes for efficient exact real arithmetic in
Coq" paper that was linked, but I'm not sure the laziness suggested
via eta expansion solves this problem, as I'm 98% sure that the output
of Program Fixpoint actually really does need to compute through the
opaque parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing
the point.
If there were some generic mechanism that could take an opaque term
and trace all the dependencies Print Opaque Dependencies style and
make a transparent version (or somehow override the opacity) then it
would completely solve the problem...
Thanks,
-snp
Post by Daniel Schepler
Post by Li-yao Xia
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.
Definition fuelled (X : Type) : Type :=
nat -> option X.
Definition return_ {X : Type} (x : X) : fuelled X :=
fun _ => Some x.
Definition bind {X : Type} (x : fuelled X)
 fuelled Y :=
fun fuel => match x fuel with
           | Some x0 => match f x0 fuel with
                        | Some y0 => Some y0
                        | None => None
                        end
           | None => None
           end.
Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))
 (x0 ident, at level 20, right associativity).
 fuelled X :=
fun fuel => match fuel with
           | S fuel_pred => x fuel_pred
           | O => None
           end.
Definition ackermann_fuel : nat -> nat -> fuelled nat :=
fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=
match m with
| O => return_ (S n)
| S m' => match n with
         | O => recursive_call (F m' 1)
         | S n' =>
           do x <- recursive_call (F m n');
           recursive_call (F m' x)
         end
end fuel.
Definition run_with_fuel {X:Type} (x : fuelled X)
 (fuel : nat) :=
x fuel.
Compute (run_with_fuel (ackermann_fuel 3 3) 100)
--
Daniel Schepler
Anton Trunov
2018-11-01 11:53:02 UTC
Permalink
Hi Thorsten,

There is a plugin written by Simon Boulier called TypingFlags:
https://github.com/SimonBoulier/TypingFlags

Best,
Anton
Post by 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.
<image001.gif>
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.
Gaëtan Gilbert
2018-11-01 11:54:35 UTC
Permalink
As far as the kernel is concerned this is possible but the syntax is not
done yet. See https://github.com/coq/coq/pull/7651

Gaëtan Gilbert
Post by 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.
Jan Bessai
2018-11-01 12:40:21 UTC
Permalink
Thorsten,

perhaps the technique presented by Larchey-Wendling and Monin at Types
2018 "Simulating Induction-Recursion for Partial Algorithms" [1] can
help you. Their trick is to use an inductively defined relation instead
of a function and later show that the relation is in fact a terminating
function. In your case you might be able to prove facts about the
relation to proceed.
Or you could have a tactic (which doesn't require any termination proof)
to infer an instance of their termination predicate D, which makes the
recursive calls proceed for the specific case you are interested in.
Also, here [2] is a larger example, where I used it to implement an
algorithm for intersection type subtyping. I can send you a paper
(accepted and to appear soon) describing the code if you are interested.

-- Jan

[1]:
https://types2018.projj.eu/wp-content/uploads/2018/06/BookOfAbstractsTYPES2018.pdf
[2]: https://github.com/JanBessai/SubtypeMachine/blob/github/Types.v
Post by 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.
--
Jan Bessai (M.Sc.)
Wissenschaftlicher Mitarbeiter

Technische Universität Dortmund
Fakultät für Informatik - Lehrstuhl 14 Software Engineering
Otto-Hahn Straße 14
D-44227 Dortmund

Tel.: +49 231-755 77 64
Fax: +49 231-755 79 36
***@tu-dortmund.de
www.tu-dortmund.de


Wichtiger Hinweis: Die Information in dieser E-Mail ist vertraulich. Sie
ist ausschließlich für den Adressaten bestimmt. Sollten Sie nicht der
für diese E-Mail bestimmte Adressat sein, unterrichten Sie bitte den
Absender und vernichten Sie diese Mail. Vielen Dank.
Unbeschadet der Korrespondenz per E-Mail, sind unsere Erklärungen
ausschließlich final rechtsverbindlich, wenn sie in herkömmlicher
Schriftform (mit eigenhändiger Unterschrift) oder durch Übermittlung
eines solchen Schriftstücks per Telefax erfolgen.

Important note: The information included in this e-mail is confidential.
It is solely intended for the recipient. If you are not the intended
recipient of this e-mail please contact the sender and delete this
message. Thank you.
Without prejudice of e-mail correspondence, our statements are only
legally binding when they are made in the conventional written form
(with personal signature) or when such documents are sent by fax.
Thorsten Altenkirch
2018-11-01 11:19:12 UTC
Permalink
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
Loading...