The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Le 29/02/2016 22:20, Jonathan Leivent a écrit :
> I thought that the fuel trick works only for some non-terminating 
> programs, not all.  Or, to say it another way, I thought that the set 
> of all programs, including those that don't terminate, is too "big" to 
> be able to express them all in a language where all functions 
> terminate, regardless of the trick used.
Isn't it the opposite way? The set of all programs, including 
non-terminating ones, is recursively enumerable while the set of all 
terminating programs is not.

Frédéric.

> To further demonstrate my naiveté, I thought that Coq's coinduction 
> was there just to address such cases.  But I guess, based on this 
> thread, that coinduction and such doesn't prevent strong normalization 
> after all.
>
> Maybe strong normalization doesn't do any such damage - as I'm just 
> thinking in terms of an old undergraduate computability course.  Or, 
> maybe it doesn't matter because all interesting properties of 
> interesting programs can be expressed and reasoned about in Coq even 
> if it is strongly normalizing.
>
> -- Jonathan
>
> On 02/29/2016 03:39 PM, Benoît Viguier wrote:
> > @Jonathan,
> > For non terminating functions (such as a program interpreter semantic,
> > virtual machine simulations...), We recurse on a kind of fuel.
> >
> > Fixpoint execution (fuel:nat) (program:state -> state) (s:state) := 
> > match
> > fuel with
> > | 0 => state
> > | S f => execution f program (program s)
> > end.
> >
> > Then you will need to prove that there exist enought fuel to execute 
> > fully
> > your program.
> >
> > Kind regards.
> >
> >
> > 2016-03-01 4:42 GMT+09:00 Jonathan Leivent 
> > <jonikelee AT gmail.com>:
> >
> > > Forgive my type-theory naiveté, but shouldn't we want some part of 
> > > Coq to
> > > not be strongly normalizing, so that it is possible to express and 
> > > reason
> > > about non-terminating functions?
> > >
> > > -- Jonathan