The Coq mailing list

[raffaello.giulietti AT supsi.ch]

On 08/06/17 14:52, Beta Ziliani wrote:
> 
> 
> On Thu, Jun 8, 2017 at 9:42 AM, Dominique Larchey-Wendling
> <dominique.larchey-wendling AT loria.fr
> <mailto:dominique.larchey-wendling AT loria.fr>>
>  wrote:
> 
>     Le 08/06/2017 à 14:38, 
> raffaello.giulietti AT supsi.ch
>     
> <mailto:raffaello.giulietti AT supsi.ch>
>  a écrit :
>     > Hello,
>     >
>     > consider the following z function
>     >
>     > Fixpoint z (n: nat): nat := 0 * z n.
>     >
>     > which Coq accepts with the usual notification "decreasing on 1st 
> argument".
> 
>     I suppose that during type-checking, Coq performs some kind of reduction
>     and sees that 0 * z n reduces to 0 (definition of mult) ... hence there
>     is no recursive sub-call.
> 
>     On the contrary, the following fails
> 
>     Fixpoint z (n: nat): nat := z n * 0.
> 
> 
> 
> Exactly. The other day, Gil Hur pass me an example of this. The official
> answer AFAIK is that "Coq is not Strongly Normalizing, but it is Weakly
> Normalizing. That is ---together with the property of Uniqueness of
> Normal Forms--- for every reduction scheme either it terminates in THE
> normal form of the term, or it loops forever. And, for soundness, that's
> good enough".
> 
> 

Structurally, I see no *surface* difference between 0 * z n and z n * 0,
so I would expect Coq to accept either both or none. But of course, if
Coq also looks up the definition of the multiplication, then there is a
deeper structural difference and I can understand the different behaviors.

Further, I had the vague impression that the typing system of Coq was
conceived to guarantee strong normalization. Evidently, I'm wrong.

Thanks
Raffaello