在 Hacker News 上看到選擇公理

沒想到會在 Hacker News 的首頁上看到這麼硬核的主題,選擇公理 (Axiom of choice,通常縮寫成 AC):「What is the Axiom of Choice?」,對應的討論在「What is the Axiom of Choice? (jaydaigle.net)」。

出自「xkcd: Set Theory

應該是大一教集合論的時候學到的,算是一個非常重要的公設,雖然的確有些數學系統是可以假定 AC 不成立,但用起來會不太好用,主要是因為「對於集合 S,取出任意一個元素」這類用法太常出現,在沒有 AC 的情況下這件事情就不一定能操作了...

我們目前常用的數學一般是建立在 Zermelo-Fraenkel Set Theory (ZF) 這個公理系統加上 AC,簡寫變成 ZFC。而 AC 在集合論常常會被拿出來說明,主要還是因為在歷史上花了不少力氣才證明 ZF 與 AC 的相對協調性 (ZF 與 AC 不衝突),以及 ZF 與 AC 獨立性 (ZF 無法推導出 AC)。

有了 AC 後就會再解釋連續統假設 (Continuum hypothesis,簡稱 CH),也就是 \mathbb{N}2^{\mathbb{N}} 之間存不存在一個集合 S 使得 |\mathbb{N}| < |S| < |2^{\mathbb{N}}|

然後再打臉一次,說明 ZFC 與 CH 的協調性 (ZFC 與 CH 不衝突),與獨立性 (ZFC 無法推導出 CH)。

當時學的時候的確是很頭痛,不過現在回頭看倒是覺得很有趣:在數學上你可以證明「某個敘述無法被證明」,這點應該是以前沒想過的...

User-Agent 的淘汰提案

看到廢除更新 User-Agent 字串的提案:「Intent to Deprecate and Freeze: The User-Agent string」。

一方面是 User-Agent 裡面太多沒用的假資料 (像是每一家都是 Mozilla),另外 User-Agent 會帶出一些隱私問題 (辨識資訊)。

目前的提案是希望改用 User-Agent Client Hints (UA-CH) 取代 User-Agent 的功能,把預定義好的東西透過對應的 HTTP header 傳遞。

Chromium 的計畫是在 M81 (stable 版預定在 2020 年三月中釋出) 先 deprecate navigator.userAgent,所以有存取時 web console 上會出現警告。而 M83 (2020 年六月初) 則是不再更動 user agent 字串 (鎖住)。到了 M85 (2020 年九月中) 則是統一 desktop 的 user agent 字串,並且盡可能統一 mobile 上的字串。

另外裡面也有整理了其他瀏覽器的意願:

Edge: Public support

Firefox: Public support for freezing the UA string - “freezing the User Agent string without any client hints—seems worth-prototyping”

Safari: Shipped to some extent. Safari has attempted to completely freeze the UA string in the past, without providing an alternative mechanism. That got a lot of pushback, which resulted in somewhat reverting that decision. Nowadays, their UA string seems frozen, other than updates to the OS version and the browser major version.

雖然不是完全都同意,但看起來應該有機會在今年陸陸續續搞定...