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.
5 questions
2
votes
1
answer
105
views
Type annotation of fixpoint combinator intereferes with Lean4's strictness
As many people already know, it's not possible to implement a Y combinator in a strict language using the following combinator $\mathsf{M},\,\mathsf{W}$ where
$$
\...
- 23
4
votes
2
answers
481
views
How does Coq guess `i` is decreasing?
As far as I know, fix must be called with a decreasing argument.
In the following code, i is the decreasing argument of ...
- 363
1
vote
2
answers
111
views
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, ...
- 1,502
0
votes
1
answer
144
views
3
votes
1
answer
99
views
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
...
- 1,026