The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

On 29/02/2016 21:20, 
"coq-club-request AT inria.fr
 on behalf of Jonathan
Leivent" 
<coq-club-request AT inria.fr
 on behalf of 
jonikelee AT gmail.com>
wrote:

>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.

I don¹t think any ³trick² is necessary, one uses a monad as for other
computational effect as well.

The slides by Tarmo
https://www.cs.ox.ac.uk/ralf.hinze/WG2.8/22/slides/tarmo.pdf
are a nice summary and build on earlier work by Venanzio Capretta
http://arxiv.org/pdf/cs/0505037.pdf

Using quotients we can encapsulate the weak bisimulation - however one
needs the axiom of countable choice, see
http://jmchapman.github.io/papers/quot_delay.pdf
However, it turns out that this is not necesssary if one uses Higher
Inductive Types, or more precisely Quotient Inductive Types.

>
>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.

Indeed. In any case *strong* normalisation isn¹t really the issue but
normalisation should hold.

>
>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.

There are no cardinality issues when reasoning about non-terminating
programs afaik.

Thorsten


>
>-- 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
>>>
>>>
>





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 send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.