Questions tagged [fixpoint]

In mathematics, a fixed point (sometimes shortened to fixpoint, also known as an invariant point) of a function is an element of the function's domain that is mapped to itself by the function. That is to say, c is a fixed point of the function f(x) if and only if f(c) = c. A set of fixed points is sometimes called a fixed set.

Filter by
Sorted by
Tagged with
1 vote
2 answers

Defining a Recursive Function decreasing on one argument with < and another structurally

I want to define a function which decreases in one argument using < and on another structurally. What is the least painful way to do this? Among the many options (Function, Program Fixpoint, ...
Agnishom Chattopadhyay's user avatar
0 votes
1 answer

Coq simpl failing to do beta reduction in this fixpoint expression

I have ...
Agnishom Chattopadhyay's user avatar
3 votes
1 answer

Is unguarded fixpoint reduction consistent?

In Coq, there are two restrictions on fixpoints to retain normalization: Recursive calls can only be done on structurally smaller arguments, enforced by a guard condition during type checking; and ...
ionchy's user avatar
  • 906