People who code: we want your input. Take the Survey

# Tag Info

## Hot answers tagged fixed-point

13

Any form of recursion or iteration in programming is actually a fixed point. For instance, a while loop is characterized by the equation while b do c done ≡ if b then (c ; while b do c done) which is to say that while b do c done is a solution W of the equation W ≡ Φ(W) where Φ(x) ≡ if b then (c ; x). But what if Φ has many fixed points? Which one ...

10

Putting it very simply, a fixed point is a point that, when provided to a function, yields as a result that same point. The term comes from mathematics, where a fixed point (or fixpoint, or "invariant point") of a function is a point that won't change under repeated application of the function. Say that we have function $f(x) = 1/x$. For $x = 2$ we get ...

6

Here is the intuition: least fixed points help you analyze loops. Program analysis involves executing the program -- but abstracting away some details of the data. This is all good. The abstraction helps the analysis go faster than actually running the program, because it allows you to ignore aspects you don't care about. For instance, that's how ...

6

As Discrete Lizard points out, there exist more than one "fixed point theorem." The one you're mentioning makes sense in terms of topology and geometry, but you're right to realize that it does not apply to programming languages. It turns out, though, that a more general notion of continuity, called Scott Continuity, can give you something that is ...

5

$\newcommand{\fix}{\mathsf{fix}}$ $\newcommand{\fold}{\mathsf{fold}}$ $\newcommand{\map}{\mathsf{map}}$ Here is, I believe, how one would use parametricity to prove your last lemma. I'm going to rework some stuff slightly for my own understanding. We have: $$C = ∀ r. (F r → r) → r$$ with $F$ functorial. We have: $$\fix : F C → C$$ corresponding to your ...

5

The fixed point theorem you are mentioning is the Brouwer fixed-point theorem. It is possible that there is some way to give a topology to computer programs and use homotopy theory to derive the existence of a fixed point, but a way to do this does not immediately spring to mind. Your objections do not completely make sense in the language of topology: A ...

4

Formal definition: a fixed point of a function $g : D \rightarrow D$ is an element $d : D$ such that $(g \ d) = d$ (source: Design Concepts in Programming Languages, p. 167). Make it simple: a fixed point is simply a solution to the equation $f(x) = x$. Intuitively: say $D = [0, 1]$. Then, imagine the unit square and its diagonal (which is the line $y = x$...

3

Your second question first. The context of your question is called descriptive complexity theory. In this context, I would suggest the book Finite Model Theory by Heinz-Dieter Ebbinghaus and Jörg Flum. As far as I recall it thoroughly covers both logics and their connection to P, respectively NP. Now to your first question. Of course, as soon as both ...

3

The recursion theorem only applies to admissible programming languages. A programming language $P$ is admissible if it satisfies the following three properties, with respect to some reference programming language $U$: The problem of simulating a $P$-program on an input $x$ is r.e. There is a computable transformation $f$ which, given a $P$-program, outputs ...

3

Let $x$ be the real number you wish to convert. We will assume without loss of generality that $0 \le x < 1$. Form the Dedekind-completeness of the order on $\mathbb{R}$, it follows that $x$ can be (almost) uniquely written as $$x = \sum_{h=1}^{\infty} 2^{-h} \alpha_h$$ where $a_h \in \{ 0, 1\}$ for all $h$. Now observe that: $$2x = \sum_{h=1}^{\... 2 Suppose Q is a join semilattice. Define g:Q \to Q by$$g(x) = f(x) \sqcup q.Then \text{fix} \; g is equal to the least fixpoint of q,f(q),f^2(q),\dots. So, at least for cpo's that form a join semilattice, you can indicate it pretty naturally using existing notation -- there's not a strong need to invent a new notation (though you could of ... 2 Your code converts a fixed-point number into its value. It also works for converting a fixed-point number to a rational number, for example. A fixed-point number of the form 16.16 consists of 32 binary digits, the first 16 to the left of the decimal dot, the second 16 to its right. When you insert the decimal dot, you are dividing by 2^{16} = 65536. ... 1 In this case, the notation F^n denotes iterated composition, that is, repeatedly applying the function F, for n iterations: F^0(x) = x. F^1(x) = F(x). F^2(x) = F(F(x)). F^3(x) = F(F(F(x))). F^4(x) = F(F(F(F(x)))). F^5(x) = F(F(F(F(F(x))))). And so on. There are two common ways to define function iteration inductively: \begin{align} F^0(x)... 1 No, they are not constructed, to avoid having fixed point because it will not leverage extension attack, as of now, even making counter of lenght equal to some weak hash is infeasible and preimage attack is hard (otherwise we would call it compression, not hashing). As of today, there are methods for collisions finding, and for SHA 256 for finding fixed ... 1 There was a misunderstanding in regards to the evaluation algorithm/minimal model. The derivation of new values is atomic e.g.: step 1: p = {} q = {} step 2: p = r q = r In step 2 p and q only see the value that each other had at step 1(the old value). I thought p and q would have access to the value of the current step and thus, the order of ... 1 Start by reading the research literature on this topic. There's a large number of published papers that discuss how to quantize the weights or intermediate values used in deep learning. For instance, here are a few papers: https://arxiv.org/abs/1412.7024, https://arxiv.org/abs/1605.06402, https://arxiv.org/abs/1612.01064, https://arxiv.org/abs/1701.08978 ... 1 Note that, in general, there might not be such a fixed point. E.g. \begin{array}{l} f : \mathbb{N}_\bot \to \mathbb{N}_\bot\\ f(\bot) = \bot\\ f(\lfloor n\rfloor) = \lfloor n + 1\rfloor \end{array}  is the standard denotation of the lazy lambda calculus function $\lambda n.\ n+1$. It is Scott-continuous. Its least fixed point is $\bot$ -- actually, ...

Only top voted, non community-wiki answers of a minimum length are eligible