Failing to halt and going into an infinite loop are not the same thing.
I’d appreciate some explanation on that, to see if you’re saying something I haven’t heard before or if we’re talking past each-other. I don’t just include while(true); under “infinite loop”, I also include infinitely-expanding recursions that cannot be characterized as coinductive stepwise computations. Basically, anything that would evaluate to the \Bot type in type-theory counts for “infinite loop” here, just plain computational divergence.
I think that what Joshua was talking about by ‘infinite loop’ is ‘passing through the same state an infinite number of times.’ That is, a /loop/, rather than just a line with no endpoint.
although this would rule out
(some arbitrary-size int type) x = 0;
while(true){
x++;
}
on a machine with infinite memory, as it would never pass through the same state twice. So maybe I’m still misunderstanding.
No. These aren’t “loops” in any meaningful sense of the word. Failing to halt and going into an infinite loop are not the same thing.
I’d appreciate some explanation on that, to see if you’re saying something I haven’t heard before or if we’re talking past each-other. I don’t just include
while(true);under “infinite loop”, I also include infinitely-expanding recursions that cannot be characterized as coinductive stepwise computations. Basically, anything that would evaluate to the\Bottype in type-theory counts for “infinite loop” here, just plain computational divergence.I think that what Joshua was talking about by ‘infinite loop’ is ‘passing through the same state an infinite number of times.’ That is, a /loop/, rather than just a line with no endpoint. although this would rule out (some arbitrary-size int type) x = 0; while(true){ x++; } on a machine with infinite memory, as it would never pass through the same state twice. So maybe I’m still misunderstanding.
Ok. By that definition, yes these are the same thing. I don’t think this is a standard notion of what people mean by infinite loop though.