一千萬個為什麽

搜索

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

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

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

我問的原因是我想構建一個System F模型,其中類型還包含度量結構(以及其他內容)。在建設性集理論中,我們可以制作一系列$ U $,這樣$ U $在產品,指數和$ U $ -indexed系列下關閉是非常有用的,這使得很容易給出一個模型系統F.

如果我可以烹飪類似的建設性超參數空間系列,那將是非常好的。但是,由於在構造集合理論中加入選擇使其成為經典,顯然我需要更加小心定點定理,也可能是其他東西。

最佳答案

當存在“事物”的集合並且為每個“事物”選擇一個元素時,使用選擇公理。如果集合中只有一件事,那就不是選擇的公理。在我們的例子中,我們只有一個度量空間,我們在其中“選擇”一個點。因此,這不是選擇的公理,而是消除存在量詞,即我們假設$ \在A中存在x \。 \ phi(x)$和我們說“讓$ x \ in A $是這樣的$ \ phi(x)$”。不幸的是,人們經常說“選擇 $ x \ in A $這樣的$ \ phi(x)$”,然後看起來像是選擇公理的應用。

作為參考,這是Banach不動點定理的建設性證明。

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$.

假設$ u $和$ v $是固定點$ f $。然後我們得到$$ d(u,v)= d(f(u),f(v))\ leq \ alpha d(u,v)$$,它跟隨$ 0 \ leq d(u,v) \ leq(\ alpha - 1)d(u,v)\ leq 0 $,因此$ d(u,v)= 0 $和$ u = v $。這證明$ f $最多有一個固定點。

它仍然是證明一個固定點的存在。因為$ M $有人居住,所以M $中存在$ x_0 \。通過$$ x_ {i + 1} = f(x_i)遞歸定義序列$(x_i)$。$$我們可以通過歸納證明$ d(x_i,x_ {i + 1})\ leq \ alpha ^ i \ cdot d(x_0,x_1)$。由此可見,$(x_i)$是Cauchy序列。因為$ M $已完成,序列的限制為$ y = \ lim_i x_i $。由於$ f $是一個收縮,它是統一連續的,所以它與序列的限制通勤:$$ f(y)= f(\ lim_i x_i)= \ lim_i f(x_i)= \ lim_i x_ {i + 1} = \ lim_i x_i = y。$$ 因此$ y $是$ f $的固定點。 QED

備註:

  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.

現在這比你要求的信息要多得多。

轉載註明原文: 建設性度量空間的不動點定理?