Stream: Coq users

Topic: Reduce fix construct

spaceloop (Feb 08 2022 at 17:27):

Hi, how do I get a fix to reduce? Compare

Eval cbv in ((fun (_ : bool) => false)  _).
Eval cbv in ((fix f (_ : bool) := false)  _).

I have also tried using Eval cbv fix beta, hoping it would reduce according to fix- and beta-reduction as described in https://coq.inria.fr/refman/language/core/conversion.html#term-beta-reduction. I'd be very happy to know what I am doing wrong, thanks!

Gaëtan Gilbert (Feb 08 2022 at 17:29):

fix only reduces when the argument in {struct} reduces to a constructor

spaceloop (Feb 08 2022 at 17:33):

Thanks, why is that? The manual only mentions:

fix-reduction: replaces a fix with a beta-redex; recursive calls to the symbol are replaced with the fix term

Li-yao (Feb 08 2022 at 17:45):

Unfolding fix without restriction would lose the guarantee that simplification terminates.

spaceloop (Feb 08 2022 at 18:36):

That surprises me, how can there be termination issues when the argument to a fix does not reduce into a constructor? Isn't the fact that that the fixpoint is defined with structural recursion restrictive enough?

Paolo Giarrusso (Feb 08 2022 at 18:37):

Not really

Paolo Giarrusso (Feb 08 2022 at 18:37):

Just expand the body multiple times to see the problem

Paolo Giarrusso (Feb 08 2022 at 18:38):

Hm, you’d need an actually recursive function…

Gaëtan Gilbert (Feb 08 2022 at 18:39):

consider Eval cbv in (fix id n := match n with 0 => 0 | S k => id k end) _
if you reduce you get match _ with 0 => 0 | S k => (fix id n := match n with 0 => 0 | S k => id k end) k end, but you would still want to reduce the new fix application, etc, etc

Paolo Giarrusso (Feb 08 2022 at 18:40):

good example :-)

Gaëtan Gilbert (Feb 08 2022 at 18:41):

(I called that id but it's not really the identity as I decided not to write S (id k) while I was writing the thing)

Paolo Giarrusso (Feb 08 2022 at 18:41):

but S (id k) would work the same way, right?

Gaëtan Gilbert (Feb 08 2022 at 18:41):

y

spaceloop (Feb 08 2022 at 18:41):

Thanks, that makes sense

Last updated: Apr 16 2024 at 06:01 UTC