# 建設性度量空間的不動點定理？

Banach的不動點定理說，如果我們有一個非空的完整度量空間$A$，那麽任何均勻收縮函數$f：A \到A$它有一個唯一的固定點$\ mu（f）$。然而，這個定理的證明需要選擇公理 - 我們需要在A $中選擇一個任意元素$ a \來開始叠代$f$，得到Cauchy序列$a，f（a），f ^ 2（a），f ^ 3（a），\ ldots$。

1. 如何在建設性分析中陳述定點定理？
2. 此外，是否有對建設性度量空間的簡明引用？

## 最佳答案

Theorem: A contraction on an inhabited complete metric space has a unique fixed point.

Proof. Suppose $(M,d)$ is an inhabited complete metric space and $f : M \to M$ is a contraction. Because $f$ is a contraction there exists $\alpha$ such that $0 < \alpha < 1$ and $d(f(x), f(y)) \leq \alpha \cdot d(x,y)$ for all $x, y \in M$.

1. I was careful not to say "choose $\alpha$" and "choose $x_0$". It is common to say such things, and they just add to the confusion that prevents ordinary mathematicians from being able to tell what is and isn't the axiom of choice.

2. In the uniqeness part of the proof people often assume unnecessarily that there are two different fixed points and derive a contradiction. This way they have only managed to prove that if $u$ and $v$ are fixed points of $f$ then $\lnot\lnot (u = v)$. So now they need excluded middle to get to $u = v$. Even for classical mathematics this is suboptimal and just shows that the author of the proof does not exercise good logical hygiene.

3. In the existence part of the proof, the sequence $(x_i)$ depends on the existential witness $x_0$ we get from eliminating the assumption $\exists x \in M . \top$. There is nothing wrong with that. We do that sort of thing all the time. We did not choose anything. Think of it this way: someone else gave us a witness $x_0$ for inhabitedness of $M$, and we are free to do something with it.

4. Classically, "$M$ is inhabited" ($\exists x \in M . \top$) and "$M$ is non-empty" ($\lnot\forall x \in M . \bot$) are equivalent. Constructively, the former makes more sense and is useful.

5. Because we showed uniqueness of fixed points we actually get a fixed-point operator $\mathrm{fix}_M$ from contractions on $M$ to points of $M$, rather than just a $\forall\exists$ statement.

6. Finally, the following fixed-point theorems have constructive versions:

• Knaster-Tarski fixed-point theorem for monotone maps on complete lattices
• Banach's fixed-point theorem for contractions on a complete metric space
• Knaster-Tarski fixed-point theorem for monotone maps on dcpos (proved by Pataraia)
• Various fixed-point theorems in domain theory usually have constructive proofs
• Recursion theorem is a form of fixed-point theorem and it has a constructive proof
• I proved that Knaster-Tarski fixed-point theorem for monotone maps on chain-complete posets does not have a constructive proof. Similarly, the Bourbaki-Witt fixed-point theorem for progressive maps on chain-complete posets fails constructively. The counter-example for the later one comes from the effective topos: in the effective topos ordinals (suitably defined) form a set and the successor maps is progressive and has no fixed points. By the way, the successor map on the ordinals is not monotone in the effective topos.