Skip to main content

Questions tagged [fixed-points]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
5 votes
0 answers
126 views

Accessible Reference for Guarded Recursion

I am looking for an accessible reference that explains the concept of guarded recursion. Some things I have in mind are: How is guarded recursion defined syntactically? Why do the greatest- and least-...
Agnishom Chattopadhyay's user avatar
3 votes
1 answer
127 views

Can the initial algebra of a 2-variable polynomial functor be computed on the diagonal?

Given a polynomial functor $F$, its initial algebra is denoted by $\mu X.F(X)$. Now, if $F$ is a 2-variable polynomial functor, $Y \mapsto \mu X.F(X,Y)$ turns out to be functorial and we can, again, (...
sparusaurata's user avatar
3 votes
0 answers
82 views

Generalizing Quines: Outputting an Arbitrary Function of Source Code

​​A Quine is a (non-empty) program $P$ that takes no inputs and returns its own source code $\langle P\rangle$ as the only output. For a function $f$ (with appropriate domains and range) define an $f$-...
Pooya Farshim's user avatar
4 votes
1 answer
189 views

Computing an approximate root of a two-dimensional monotone function

Let $f$ be a Lipschitz-continuous function from the square $[-1,1]^2$ to itself, satisfying the following conditions: For all $y\in [-1,1]$: $~~~~f(-1,y)_1\leq 0\leq f(1,y)_1$, and $f(x,y)_1$ is ...
Erel Segal-Halevi's user avatar
0 votes
1 answer
212 views

Fixed-point combinator on arithmetic functions

The question is about this Racket program: ...
Cyker's user avatar
  • 779
4 votes
1 answer
145 views

Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

This question extends my inquiry from a previous post [0]. Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
jpt4's user avatar
  • 111
2 votes
0 answers
101 views

Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?

Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
jpt4's user avatar
  • 111
8 votes
4 answers
553 views

Type theory and fixed points of datatypes

For the purposes of this question, say that a datatype is a type constructor with one type parameter (this is sometimes called a type operator). In Haskell, we can define a fixed point ...
Ilk's user avatar
  • 920
9 votes
0 answers
207 views

Is it known how much computation a fixed-point combinator gets you?

It is well-known that the SKI combinators are enough to get universal computation, though the original version of combinatory calculus used BCKW. However, it is possible to get a fixed-point ...
David Roberts's user avatar
3 votes
1 answer
356 views

Fixed points of fixed-point combinator?

A fixed point f of a fixed-point combinator would be a function that has itself as a fixed point: f(f) = f. The only such ...
GeoffChurch's user avatar
9 votes
0 answers
253 views

Which version of KAKUTANI does lie in PPAD?

The seminal paper of Papadimitriou [1] claims that the computational search problem KAKUTANI is $\mathbf{PPAD}$-complete. Unfortunately, there are very few details. Many other papers and surveys cite ...
Daniil Musatov's user avatar
7 votes
1 answer
299 views

The originator of the fixed point theorem for DCPOs

Pataraia proved in "A constructive proof of Tarski’s fixed-point theorem for dcpo's", presented in the 65th Peripatetic Seminar on Sheaves and Logic, in Aarhus, Denmark, November 1997 that in a ...
user avatar
0 votes
1 answer
84 views

Solving recurrence [closed]

Let $f(x) = 3/2 - \sqrt{2 - 8x^2}$. I am interested in the recurrence $Y_0 = 0$ and $Y_{i+1} = f(Y_i) = f(f(Y_{i-1})) = ... = f(f(f(f(... f(0) ...))))$. A quick plot shows that $Y_i$ converges to $1/6$...
Chris's user avatar
  • 79
1 vote
0 answers
100 views

Deciding reachability under iterated independent polynomial mapping

For any $1\leq i\leq m$, $f_i: \mathbb{Q}\rightarrow \mathbb{Q}$ is a polynomial mapping over $x_i$, where $\mathbb{Q}$ is the set of rationals. For $\vec{a}_0=(a_1, \cdots, a_m)\in \mathbb{Q}^m$, we ...
Liam_math's user avatar
7 votes
0 answers
231 views

Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
Neel Krishnaswami's user avatar