然而排除已使用元素是固定成本，在已使用元素會變多的情況下更是越來越大的成本。隨機抽一個，再查看有沒有撞上已經使用的位置反而更有效。但這樣做的界線到底在哪裡？

對於空間大小 $N$ 與已使用的 $U$，隨機抽一個位址命中未使用元素的機率是

假設每次抽樣互相獨立，那「抽到第 $k$ 次才第一次成功」服從幾何分布

連續 $k$ 次都失敗（選到已使用的位置）的機率是 $(1 - p)^k$，期望次數是

所以我們可以看到 $|U|$ 只佔 $N$ 一小部分時，期望次數幾乎是常數，$|U| = N/2$ 時也只是2次，跟排除法的 $O(N)$ 差距明顯。要等到 $N - |U|$ 幾乎為 $0$ 時，這才開始稱得上成本

$(1 - p)^k$ 隨 $k$ 遞減趨近 $0$，但對任何有限的 $k$ 都不等於 $0$，也就是不存在有限次數可以保證我們抽到未使用的數字。所以這裡要找的不是「幾次一定會中」，而是「願意接受多大的失敗機率」

給定可以接受的失敗機率 $\varepsilon$tr-notes 取 $10^{-9}$，我們想找出滿足 $(1 - p)^k \le \varepsilon$ 的最小 $k$

先對兩邊取 $\ln$，$\ln$ 單調遞增所以不等號方向不變

根據Logarithm power rule可以得出

$p \in (0, 1)$ 時 $\ln(1 - p) < 0$，所以同除要翻轉不等號

第二個等號來自分子分母同乘 $-1$，讓兩邊都寫成正數。取ceiling就是可拿來做嘗試次數的最小 $k$

但計算 $\ln(1/(1 - p))$ 太麻煩了，所以實作上用 $m/p$ 當上限這裡 $m = \ln(1/\varepsilon)$，而 $1/p$ 就是上面的期望次數。這個做法是因為如果把分母展開成無限級數注意收斂條件

$p \in (0, 1)$ 時每一項都是正的，因此可以看出 $\ln(1/(1 - p)) \ge p$被砍掉的高次項正好說明了高估多少

分母變大則整體變小，所以 $m / \ln(1/(1 - p)) \le m/p$，也就是 $m/p$ 大於等於 $k$ 總是成立。因此這是安全的高估，代價是最壞情況多重試幾次，但讓我們不必計算 $\ln(1 - p)$在 $p \to 1$ 時數值上也不穩，這是另一個不採用的理由

最後這個上限還要跟 $N$ 取 min。期望次數 $1/p = N/(N - |U|)$ 本身其實永遠不會超過 $N$（最壞的 $N - |U| = 1$ 時剛好等於），但 $m/p$ 可能會超過：$N - |U| < m \approx 20.7$ 時就有 $m/p > N$。既然這時候成本已經比掃過整個空間還高，應該放棄然後退回過濾再抽取的演算法

我們分析了抽取的上限是怎麼推導出來的，並且計算超過上限就退回一開始的排除法。所以最壞情況是 $O(N)$ 而不是不會停；另外空間真的滿了會直接報錯，這也是為什麼上面的分析不涉及 $p = 0$

這個演算法用在 raco tr next 的 --random 功能上

一個fediverse帳號是一個HTTP服務，要能回答這幾件事：

• /@blog：actor，帳號本身
• /@blog/inbox：別人寄東西來的地方
• /@blog/outbox、followers、following：這個帳號的公開集合
• /.well-known/webfinger：把 @blog@fedi.dannypsnl.me 這個名字換成上面那個actor的網址

這些都能用Fedify處理，因為要簽HTTP Signatures，這塊很麻煩所以要盡量復用被驗證過的程式。Actor的宣告：

builder.setActorDispatcher("/@{identifier}", async (ctx, identifier) => {
  if (identifeir !== "...") return null;
  const keys = await ctx.getActorKeyPairs(identifier);
  return new Person({
    // ...
    publicKey: keys[0].cryptographicKey,
    assertionMethods: keys.map((k) => k.multikey),
  });
})

我一開始把Actor放在 /users/blog，後來改成 /@blog。這樣會非常麻煩，因為那個id改掉之後已經追蹤的帳號手上那個id就指向一個404……

補救就要用ActivityPub自己的move功能。舊網址得回一個退休的Actor，用 successor 指向新的；新的Actor用 aliases 認領舊的，兩邊對得起來遠端才會相信。然後從舊id發一個 Move 給所有跟隨者，而且要用舊id的key id去簽

利用RSS的話，就不需要改任何現有程式。Worker用cron抓取

[triggers]
crons = ["0 0 * * *"]

item的 guid 作為識別機制：D1裡貼文的主鍵是它，Note的網址是 /@blog/notes/<addr>，前端要問互動的時候拿 location.pathname

同步功能先建立草稿，不會馬上發佈。因為第一次同步會讀到整個feed，直接發就是把站上所有文章一次丟到別人的timeline上。所以另外建立了一個用CF存取規則保護的admin頁面管理這些草稿

用Queue投遞，這裡有個坑，Queue裡的訊息是包裝過的：

const result = await workersQueue.processMessage(message.body);
if (!result.shouldProcess) { message.retry(); continue; }
await federation.processQueuedTask(env, result.message);

我原本直接把 message.body 丟給 processQueuedTask，它就永遠對不上任何一種task，然後安靜地什麼都不做

Mastodon不會自己爬你的outbox，它只顯示追蹤之後推給它的活動。所以剛追蹤的人看到的是一個空帳號。因此Follow進來時除了回Accept，還要把已經發過的文章補送給這個人：

const posts = await listPosts(ctx.data, "published");
for (const post of posts) {
  await ctx.sendActivity({ identifier: IDENTIFIER }, follower,
                         buildCreateNote(ctx, IDENTIFIER, post.addr));
}

重送本身是安全的，活動的id是從addr算出來的（/@blog/notes/<addr>#create），fediverse站點看到收過的id就不會再存一次

inbox要處理的東西其實不多

• Create 帶一個Note：回覆
• Like：讚
• Announce：轉發
• Delete、Undo：把上面存進去的刪掉

回覆只認 inReplyTo 指向我自己的Note的那些，所以一整串討論只會留下直接的reply，而不是整個討論串。那些內容屬於原本的伺服器，我這邊只知道有人對這篇文章說了什麼，剩下的點連結過去看

回覆的可見性是回覆者自己選的，跟被回覆的文章無關。私訊回覆一樣會進inbox，因為Mastodon一定會把被回覆的人列進收件人。所以存的時候要先分類：

function classifyVisibility(toIds, ccIds) {
  const pub = PUBLIC_COLLECTION.href;
  if (toIds.some((u) => u.href === pub)) return "public";
  if (ccIds.some((u) => u.href === pub)) return "unlisted";
  return "private";
}

private訊息在公開端點不應該列出

有一個公開端點 GET /interactions/:addr 可以看到這篇文章的互動，所以blog這邊用一支 interactions.js 根據 location.pathname 作為addr去問，有互動資料才顯示fediverse區塊參見部落格問題挑戰2026-08-18 · Lîm Tsú-thuàn

不受信任的HTML不應該進 innerHTML，所以先解析成一個不會執行的document，只把文字讀回來

最後是CORS。因為這個端點不吃憑證、也只回公開的資料，所以worker那邊的端點填 *

Access-Control-Allow-Origin: *

當初只是想紀錄一些學習上的問題，因為那時候看到「學東西最好的方式就是教別人」，所以就順便把筆記變成部落格

我用自己開發的靜態網站產生器tr-notes，工具的網站 https://tr-notes.srht.site/

tr-notes的起源是我使用forester的時候一直遇到breaking changes，但大抵上來說我覺得這種軟體很好用（可以讀 https://www.forester-notes.org/QHXS/index.xml 了解一下forester的一些設計理念）。所以我就開始思考怎麼用racket實現這些效果，主要技術是scribble的Text Generation跟dynamic-rerequire

就理念上來說，我用forest風格的專案目的是

• transclusion功能
• 不用特別幫檔案想名稱常青筆記的困難2025-06-10 · Lîm Tsú-thuàn 簡言之就是本體論在長期不具有可維護性，生成一個36進位的4碼數字作為位址
• 良好的數學渲染支援，包含tikz支援
• 雙向連結

另外就是tr-notes可以引入racket程式碼編寫專用功能：

• 引入dataloghttps://en.wikipedia.org/wiki/Datalog做卡片關聯查詢
• 用tree-sitter標亮程式碼區塊

曾經用過Blogger跟Hugo

通常是VSCode，因為我也寫了編輯extension

• 可以即時看到tr-notes渲染結果

• 可以用 Meta + K 搜尋卡片

• 可以用 Meta + Shift + M 插入卡片提及語法

上班的時候。主要是通過翻過去的筆記跟目前遇到的問題（來源不定）

會有很多草稿，但草稿真的很難完成

這往往隨著我最近研究的課題而變化，最近應該是

• 模擬選舉演算法
• To CPS or not to CPS：編譯理論之爭

我一直有希望加入 https://webmention.io/，但這協定會因為各種原因失效（包含但不限於cloudflare阻擋機器人讀取email），可能會看有沒有其他替代方案

跟Fediverse整合？但我還沒有研究fediverse協議的狀態

因為想要TeXmacs的所見即所得編輯功能，可能會開發一個tr-notes用的或是通用編輯器？但這畢竟也蠻麻煩的，我也不確定會不會真的動工xd

• 1978 RABBIT: A Compiler for SCHEME，據說這是最早採用CPS的編譯器
• 1992 Compiling with Continuations，Appel整理並提供了完整的ML CPS風格編譯器
• 1993 The essence of compiling with continuations，形式化並辨識出ANF，認為direct style (ANF) 在local control flow上提供了更簡單的工作方式
• 1997 A reflection on call-by-value，這篇正式的討論了direct style在什麼時候可以替代CPS編譯器
• 2007 Compiling with continuations, continued，Kennedy認為CPS在functional language上有勝過ANF或是monadic IR的地方，主要爭點就是inline會導致ANF需要renormalization
• 2017 Compiling without continuations，Haskell方認為，可以用local continuations（又稱join points）處理direct style的缺點
• 2019 Compiling with continuations, or without? whatever.，這篇認為我們需要重新考慮，用還是不用CPS取決於編譯器/語言的目標，而且join points無法讓optimizer有足夠的evaluation context資訊，導致冗餘的轉換。因此作者認為正確的問題應該是「我們需要什麼程度的CPS」，設計了direct style跟CPS optimizations都能運作的IR

ANF常被叫做administrative normal form，好像是個模糊的「把administrative redex消掉」的說法。但最好想成以下的定義：對給定的A-reductions集合，化約會得到的normal form

Lambda calculus的A-normalization可以寫成以下定義

A-reductions

化約成的A-normal form（也就是說，不斷套用A-reductions應該讓程式變成以下形式，這些形式套用A-reductions不會再化簡）

我們通常會假設綁定中涉及的變數唯一且考慮 $\alpha$-equivalence

ANF可以保證每個計算都由一系列的let序列化，並且所有operands都一定是values，從而對指令語言後端編譯是好用的表示形式。但ANF也有一些缺點

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

if0 (if0 (if0 0 0 1) 0 1)
  E1[0]
  E1[1]

if0 (if0 0 0 1)
  E2[0]
  E2[1]

if0 0
  E3[0]
  E3[1]

if0 0
  if0 0
    if0 0
      let x := 0 in LARGE
      let x := 1 in LARGE
    if0 1
      let x := 0 in LARGE
      let x := 1 in LARGE
  if0 1
    if0 0
      let x := 0 in LARGE
      let x := 1 in LARGE
    if0 1
      let x := 0 in LARGE
      let x := 1 in LARGE

begin:
  if0 V
    set! x M1
    set! x M2
  M

對於$A_2$ 規則引入的程式碼爆炸，除了直接改成用CPS，傳統方式是引入一個local continuation來處理，這種continuation常叫做join point

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

我們轉換成

let j y := LARGE
if0 (if0 (if0 0 0 1) 0 1)
  let x := 0 in j x
  let x := 1 in j x

然後以此類推，我們就不會產生重複的程式碼。然而join points也有很明顯的缺點，比如引入更多的allocation（lambda的runtime表示closure並不是免費的），並且阻止對 $j$ 的最佳化，這往往導致實務編譯器必須考慮引入相應的join points algebra去處理一系列的轉換問題

如果讓let表示monadic bind，讓return隱含在values下，那monadic form有以下commuting conversions

ANF可以定義成monadic form用associativity跟commute這兩條規則normalize的結果

Non-strict monadic evaluation contexts $E^b$

B-reductions

如果定義 $B = \{B_1, B_2, B_3\}$，那麼這組規則會確保evaluation position上的non-value會被換成value。

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

let x :=
  let y := if0 (if0 0 0 1) 0 1
  in if0 y 0 1
in LARGE

let x :=
  let z := if0 0 0 1
  in let y := if0 z 0 1
  in if0 y 0 1
in LARGE

藉由分析ANF跟monadic form的機器表示的意圖，Bowman提出了Imperative monadic form。只要我們讓

let x := a
in b

等於

set! x := a
b

的別稱。在語意上commuting conversion就不再是困擾了

set! y := {
  set! x := t
  t
}
t

等於

set! x := t
set! y := t
t

箝套的if也不再是問題

set! y := if v t1 t2
t

等於

if v
  set! y := t1
  set! y := t2
t

注意到右邊幾乎已經是指令語言可以處理的形式了

根據Imperative monadic form我們已經可以定義AB-reduction

這種方案避開了join points、編譯器不需要引入整套CPS風格、也不會造成程式碼膨脹（就像B-normalization），對stack使用最佳化（就像A-normalization）。這個做法的關鍵想法在于lexical expressions一定要在A-normalize之前先轉換成循序述句表達

AB-normalization還可以根據新的effect調整，像Bowman就展示了letregion的案例

lambda-calculus
  --> monadic form            (只有 sequencing，不碰 commuting conversion)
  --> imperative monadic form (lexical binding 降成 set!)
  --> AB-normal form          (在 statement 上做 A-normalization)

對照傳統的

lambda-calculus
  --> ANF             (sequencing + commuting conversion 一起做)
  --> code gen

傳統方法的A-normalization compiler必須寫成CPS風格（compiler自己拿一個meta-level的continuation $\kappa$ 來累積上下文），還要在target language裡處理join point的表示；而monadic版本的compiler就只是遞迴地sequence，每個子項回傳的都是可以互相組合的

這個方法有一個缺點：我們不確定AB-normal compiler能不能處理case-of-case

(if0 (if0 e 1 0) 5 6)

ANF compiler會產生 (if0 e (if0 1 5 6) (if0 0 5 6))——分支被複製了，但接著partial evaluation一步就化簡成 (if0 e 6 5)。AB-normal compiler生出的是 (let (x (if0 e 1 0)) (if0 x 5 6))，沒有複製程式碼，但也就沒辦法做同樣的化簡

Maurer等人的join point calculus 處理這個例子處理得很好，代價是引入join point。Bowman的提議是把條件位置分離成一個boolean的sublanguage，再讓一個簡單的boolean optimizer去化簡，這是Chez的做法，表示這可能這是實務上有效的方案

論文最後把幾個高效能編譯器抓出來對照，說它們早就在做AB-normalization了

• Chez Scheme：L10轉換直接把let/let跟let/if的commuting conversions轉換成imperative IR
• TIL（ML編譯器）的B-form是一個monadic form IR
• SIL（ML to Ada compiler）

用論文自己的話說就是：這些編譯器早在這個方法被辨識出來之前就使用它了

• 我們有所有集合與函數的範疇 $\text{Sets}$、所有群與群態射的範疇 $\text{Groups}$
• Monoid $M$ 的Actions可以改寫成functor $M^{op} \to \text{Sets}$（事實上這類functor有個特殊名稱，叫做presheaf）
• 拓樸空間 $X$ 的所有開集之間的包含關係構成一個category $\text{Open}(X)$
• 遺忘functor，比如 $\text{Groups} \to \text{Sets}$、$\text{Rings} \to \text{Groups}$
• Free functor，像是集合生成free groups/vector space等
• 基本群可以視為從有點拓樸到群的functor $\pi_1 : \text{Top}_* \to \text{Groups}$
• vector space對偶可以視為functor $(-)^* : \text{vect}(\mathbb{k}) \to \text{vect}(\mathbb{k})$
• 從manifold構造它的ring of smooth functions可以看成functor $C_\infty : \text{Man} \to \text{Rings}$，定義為 $$C_\infty(\mathbb{M}) := \{ f : \mathbb{M} \to \mathbb{R} \mid f \text{ is smooth}\}$$

一個category是由一些morphisms構成的，每個morphism都有頭跟尾兩個標籤（這些標籤又叫做objects），例如 $f : A \to B$ 我們畫出直線並用一個點代表 $f$

當頭尾的標籤一樣的時候，我們可以把morphisms黏起來得到另一個morphism，例如 $g : A \to B$ 而 $f : B \to C$，那 $f \circ g$ 記成

有一類特殊的morphism $1_X : X \to X$，他們的標籤頭尾都一樣，跟其他任何morphism $f$ 組合都會是 $f$（如果可以組合）。這類morphism有個特定的名稱，叫做identity morphism，而且對於該標籤 $X$ 這樣的morphism只有一個。對於這樣的morphism，我們用直線表示它可被忽略

因為我們有等式 $f \circ 1_A = 1_B \circ f = f$

Functor是範疇之間的變換，例如 $F : \mathcal{C} \to \mathcal{D}$ 可以記成

Functor必須滿足 $F(f \circ g) = F(f) \circ F(g)$，但這件事在我們目前用的string diagram表示法裡面看起來像是廢話所以就不畫了。Natural transformation是functors之間的變換，例如 $\alpha : F \Rightarrow G$ 可以記成

Natural transformation必須滿足等式 $G(f) \circ \alpha_X = \alpha_Y \circ F(f)$，稱之為naturality

用string diagram繪製之後，naturality就像是在說：我們可以把串珠在線上移來移去而不會改變意義。因此這又叫「電梯等式」，我們當然沒有必要侷限在objects跟morphisms上，所以更通用的形式是

這種string diagram的語言在Introducing String Diagrams: The Art of Category Theory裡面有更多的介紹

Example 程式作為natural transformation [631K]

2026-07-14

如果一些類型構成category，可以用functor表示參數化類型。例如我們可以定義natural transformation $\alpha : \text{Maybe} \to \text{List}$ 為

$$\begin{aligned} &\alpha_X : \text{Maybe}(X) \to \text{List}(X) \\ &\alpha_X(\text{Nothing}) &= [] \\ &\alpha_X(\text{Some}\ x) &= [x] \end{aligned}$$

或是取出List中的最大值

這是在說先結合functor還是先結合natural transformation不改變結果

一些有趣的結果A Formal Proof that the Higher Fundamental Groups are Abelian

Adjunction $L \dashv R$ 是範疇論中重要的概念，它是由一對functors $L : \mathcal{C}\to\mathcal{D}$ 跟 $R : \mathcal{D}\to\mathcal{C}$ 與一對natural transformations $\eta : 1_\mathcal{C} \Rightarrow R \circ L$ 與 $\epsilon : L \circ R \Rightarrow 1_\mathcal{D}$ 組成。注意 $1_\mathcal{D}$ 這種functor我們會乾脆不畫線

Adjunction是可以串起來的

Example Limit與colimit [50LK]

2026-07-14

每個 $D : J \to \mathcal{C}$ 有limit可以表示成diagonal functor $\Delta : \mathcal{C} \to \mathcal{C}^J$ 有right adjoint $\lim : \mathcal{C}^J \to \mathcal{C}$。$\Delta$ 定義為 $\Delta(X)(j) := X$

對偶的來說，有colimit就是$\Delta$有left adjoint $\text{colim}$

還有一些其他案例

• Forgetful functor與free functor之間構成adjunction https://ncatlab.org/nlab/show/forgetful+functor
• Galois connection是一種adjunction https://ncatlab.org/nlab/show/Galois+connection

有個跟adjunction緊密聯繫的概念是monad，我們這邊直接看adjunction如何構成monad。給定 $L \dashv R$，有以下構造

因此 $R \circ L$ 是一個monad

偏數學的案例我目前只想得到adjunction構造的monad，在電腦科學裡面monad的用途是表示程式中的effects（參考 [Moggi1991]）

張量算術可以用Penrose notation（站上的用例），此外探討string diagrams的理論跟使用string diagrams的文獻都不少，這裡我列出一些

• Diagrammatic category theory，這篇要注意的是跟我們這裡畫的圖上下相反，是從下到上的箭頭
• Promonads and String Diagrams for Effectful Categories
• The free bifibration on a functor https://noamz.org/talks/ct2026.2026.07.13.pdf

範疇論當然不是只靠一篇文章就能學會的，如果讀者有興趣的話，以下是根據不同背景我認為可能有用的學習資源

• 沒怎麼學過數學？可以考慮The Joy of Abstraction: An Exploration of Math, Category Theory, and Life
• 想要知道範疇論在各個數學領域的案例可以參考Category Theory in Context
• 想要主修範疇論？那可以考慮Handbook of Categorical Algebra
• 你是軟體工程師，希望知道直覺上怎麼運用category theory？那Category Theory for Programmers還蠻適合的，但要注意Type Theory跟Category的關係遠不是這本書說的這麼單純。另外可以考慮讀Seven Sketches in Compositionality: An Invitation to Applied Category Theory了解更廣泛的應用範疇論

只是晚上睡不著？那也可以考慮Sketches of an Elephant

fact（已知的事實）與 rule（能從事實推導新事實的規則）。先宣告一個輸入關係，代表「模組a直接相依於模組b」

// 代表 a 直接 import b
.decl depends(a: symbol, b: symbol)
.input depends

.decl 宣告關係的名字與各欄位型別（symbol 是字串，另一個常用型別是 number）。.input 表示資料從外部讀入：預設是從同名的 depends.facts 檔案，每行一筆、以 Tab 分隔。接著我們定義第一條規則：模組若被任何人相依，就是「被使用的」

.decl used(m: symbol)
used(m) :- depends(_, m).

讀法是「對任意 m，若存在 depends(_, m)，則 used(m) 成立」。:- 右邊是body（前提），左邊是head（結論），_ 是 wildcard，表示「有就好、是誰都可以」。開發者不用管理控制流程：規則評估結果是順序無關的，由引擎自己算出所有成立的結論

Datalog的威力來自join，同一個變數出現在多個atom裡時，概念上是約束成同一個，會觸發unification。比如「a透過某個中介x間接相依於b」可以寫成

.decl indirect(a: symbol, b: symbol)
indirect(a, b) :-
  depends(a, x),
  depends(x, b).

x 在兩個 depends 裡都出現，引擎就通過「a依賴的東西」和「依賴b的東西」計算a到b的間接依賴

但 indirect 只有 a -> b -> c 的情況會被辨識出來，相依是會傳遞的，不論中間隔幾層，可達性是經典的遞迴關係：transitive closure

.decl reachable(a: symbol, b: symbol)
reachable(a, b) :- depends(a, b).
reachable(a, b) :-
  depends(a, x),
  reachable(x, b).

• base case：直接相依就是可達
• induction case：a 依賴 x，x 遞迴可達的所有 b 都是 a 可達的

這裡的 reachable 只在 depends 既有的symbol之間關聯，不發明新值，可推導的fact是有限集，所以一定收斂

但保證終止不是Soufflé的通則。它有算術functor，只要規則會合成新值（如 A(i + 1) :- A(i).），domain就變成無限，會產生無窮迴圈，這種情況要自己加 i < 10 之類的條件控制

有了可達性，就能問「哪些模組是死碼」：不是從entry point可達的模組。這需要negation。先標出進入點，再定義「可從某entry到達」

.decl entry(m: symbol)
.input entry

.decl live(m: symbol)
live(m) :- entry(m).
live(m) :-
  entry(e),
  reachable(e, m).

.decl dead(m: symbol)
.output dead
dead(m) :-
  depends(m, _),
  !live(m).
dead(m) :-
  depends(_, m),
  !live(m).

!live(m) 是negation。Datalog的negation必須是 stratified（分層）的——不能有「自己依賴自己的否定」這種循環。Soufflé會把程式分層，確保 live 在被否定使用前已完全算完，!live 的語意才有良好定義

Datalog不只能推導關係，也能做聚合。例如算出每個模組「被多少人直接相依」，找出最該謹慎修改的核心

.decl fan_in(m: symbol, n: number)
.output fan_in
fan_in(m, n) :-
  used(m),
  n = count : { depends(_, m) }.

count : { depends(_, m) } 是「滿足 depends(_, m) 的fact有幾筆」。對固定的 m，引擎算出有多少個模組相依於它，綁定 n。Soufflé 也提供 max、min、sum，語法相同。聚合讓我們不必跳出Datalog就能回答「最多、最少、總共」這類問題

把上面的規則存成 deps.dl，準備一個 facts/ 目錄放輸入：depends.facts 每行一筆 模組A⟨tab⟩模組B；entry.facts 列出進入點。然後在shell中輸入

souffle deps.dl -F facts -D out

-F 指定fact目錄，-D 指定輸出目錄。每個標了 .output 的關係跑完都會出現在 out/ 下：out/dead.csv 是deadcode的清單，out/fan_in.csv 是各模組的被依賴數量

以上是直譯模式，開發時使用。資料量大、要追求速度時，可以把程式編成原生執行檔再跑

souffle -o deps deps.dl
./deps -F facts -D out

理論部分參考 On Fast Large-Scale Program Analysis in Datalog

Soufflé的心智模型很單純：我們描述「什麼成立」，引擎反覆套用推理規則直到不動點，算出所有能推導的facts

它的優勢在「對大量結構化資料反覆做join與遞迴查詢」：程式分析（points-to、call graph、taint）、相依與可達性分析、各種圖上的規則推導。當問題能轉換成「一組fact加一組蘊含式」，Soufflé就能精簡的表示邏輯，又不用損失執行速度

在桃園機場隨意吃過午餐，坐上 12:10 起飛、往日本海岸線去的班機

在降落小松之前在日本海上轉向，往陸地飛去，經過軍機場之後 16:05 降落在小松機場。小松並不大，主要都在等過海關，下了樓之後因為接駁車等待人數不少，擔心可能要再等一班，於是坐計程車去小松車站，買了類似台灣區間車的車票做到金澤站

這台火車的座椅很有趣，有一個機械結構，乘客可以把座椅調整成對向四人座，或是兩人座。飯店 checkin 完畢再去找晚餐，這時候市場已經快關了，而且很多店大排長龍，就隨便找一間吃

這天的目標是先去 ORIX 取車，然後開去千里濱凪沙道路，取車前還有一點時間，先跑去看鼓門

這一整日都陰雨綿綿，在取車之後在市區開了大概一個多小時之後來到千里濱，才發現因為海嘯的緣故，下去沙灘的道路全都封閉

前往下一個目標巖門，停好車之後，下去之前發現一隻大蜘蛛，所以就先拍了一些照片

巖門有一個比海更低的通道，漲潮的時候就無法通行，從通道看出去：

巖門園區裡面往沙灘的部分封閉。浮世繪

老鷹會在這個岩石上築巢

午餐吃能登牛富來本店，非常好吃，來到能登不要錯過

世界最長椅子：原本的椅子已經被摧毀，現在是新蓋的一座，現場有許多祈福話語

岸壁之母

附近商店裡用貝殼製作的精巧藝術

沿途的山路中有很多神社跟獨棟住宅，經過一座水庫

輪島漆芸美術館沒開，因為這樣也就跳過了輪島市，另外這裡受災也比較嚴重，不少店面都還沒有恢復，下次有機會再去看看。白米千枚田，目前景觀咖啡廳沒有營業

觀光製鹽景點，不過旅程時沒有營運

祿岡崎燈塔，現場有整修人員

青之洞窟還沒到關門時間，不過也沒有開放。他們的旅館：

瞭望台

這裏有賣超級昂貴的（靈能）石頭

晚間來到預定的小旅館 -- 珠洲温泉宝湯別館，旅館目前主要是維修工程人員住宿。由於已經比較晚了，所以詢問還能不能加訂晚餐，所以晚餐是家常料理風的炸豬排。房間就是榻榻米上面鋪棉被，這確實蠻硬的，不習慣會睡不好xd

溫泉是放到一個大約三人大小的浴池裡面，夜色從窗口透入，非常療癒

早晨工程人員已經充充上工，宝湯別館提供的早餐：

與老闆夫妻聊天得知預期修復工程需要十年。早上的風景

宝湯別館

恋路海岸 • 弁天島

因為地震的關係，見附島現在禿了一塊

九十九灣。這裡遇到一車幼稚園小朋友，結果某個小朋友跑來跟我媽擊掌之後，後面每個孩子都決定要參一咖

真脇遺跡。時間安排的關係這次是白天去的，如果真的要晚上來要注意

1. 這邊是山路而且沒燈，建議至少下午就來，然後等到晚上
2. 好像是要跟管理處申請才能過夜

樹木恐龍！

午餐來到穴水町的能登前幸寿し。因為我媽不吃生魚片，本來討論等一下另外去附近店買別的吃，店主聽了之後特地卷了一道用蔬菜做的壽司

能登鐵道

有看到里山里海號但忘了拍照了xd

接下來從能登半島進入能登島，本來想說這次不去水族館，但因為算一算時間去飯店還太早，能登島上也沒有其他有興趣的景點，所以就決定去 Notojima 水族館

地上有投影的海洋生物，有一個孩子一直追著魚的幻影大叫「魚！魚！魚！」。整備中的萬聖節活動佈置

海豹很有表演慾，只要有人錄影就會一直跑來展現自己。這裡的冰淇淋店還提醒客人不要在室外吃，不然老鷹跟海鷗會搶xd

晚上來到七尾和倉，能登樂溫泉旅館

在吃晚餐之前有點時間，就跑去拍七福神雕像。這附近有一間台灣傳統美食，下次再去和倉一定會試試看xd

目前是用 violet weave 從一個 .vt.scrbl 編譯。程式碼區塊由 violet 前處理：@vt|{…}| 的內容會被抽出、型別檢查，轉成帶標記的 HTML。其餘內容原樣交給 tr-notes

把游標移到 identifiers 上時可以看到型別；調用部分連結到它的定義；?here 這樣的 goal 會顯示 context 與 target

\universe US U

\let id(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | id A xA => xA

\let ex(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | ex A xA => id(A : universe U) -> (_ : A) -> A Auniverse U xA

\let open-goal(A : universe U) -> (_ : A) -> A (Auniverse U : Uuniverse S U) : Auniverse U -> Auniverse U \where
  <= \intro
  | open-goal A xA => ?hereA : universe U
x : A
⊢ A

id 定義，ex 內用到了 id，open-goal 留了一個 ?here goal。

現在的 <= \elim 並不處理有任何帶有非純變數參數的 elimination target，因為這會導致 eliminator 有些 case 完全沒有意義，需要引入等式去除不可及的分支。另一個辦法是讓開發者提供 motive，但那樣就沒幫助到開發者了xd

另外 lock 檔案的鎖定實現還不完整，這些實務上的限制會是接下來需要仔細處理的問題

可以看到，綁定就變成只是放一個 handler 攔截，遇到查詢就把記錄下來的值丟給 resume 跳回去

    [`(let [,x ,v] ,tm)
     (call/prompt
       go lookup-tag
       (lambda (resume x1)
         (if (eq? x x1)
             (resume (go v))
             (resume (lookup x1))))
       tm)]

但相應的，比起明確在參數中提供 env 變數的版本，我們沒辦法直接把 env 複製進 closure 就好，而是需要特地找出 free variables 並在當前的環境中找到這些變數然後複製成一個 environment。這正是 Lexical scoping與dynamic scoping的對偶的實際案例

    [`(lambda (,x) ,body)
     (define fvs (remove x (remove-duplicates (free-vars body))))
     (closure x body
              (for/list ([y fvs]) (cons y (lookup y))))]

在 application 的部分就需要把存起來的 environment 播放出來變成一系列的 handler

    [`(,f ,a)
     (define fv (go f))
     (define av (go a))
     (match fv
       [(closure x body env)
        (install-env (cons (cons x av) env) body)])]))

(struct closure (param body env) #:transparent)

(define (free-vars tm)
  (match tm
    [(? symbol? x) (list x)]
    [(? number?) '()]
    [`(+ ,@as) (append-map free-vars as)]
    [`(let [,x ,v] ,t)
     (append (free-vars v) (remove x (free-vars t)))]
    [`(lambda (,x) ,body)
     (remove x (free-vars body))]
    [`(,f ,a)
     (append (free-vars f) (free-vars a))]))

(define (install-env bs tm)
  (match bs
    ['() (go tm)]
    [(cons (cons x v) rest)
     (call/prompt
       (lambda () (install-env rest tm))
       lookup-tag
       (lambda (resume y)
         (if (eq? x y) (resume v) (resume (lookup y)))))]))

{-# OPTIONS --safe --without-K #-}
module ag-OW40 where

open import MLTT.Spartan hiding (_+_)
open import MLTT.Negation
open import MLTT.List
open import MGS.MLTT using (has-decidable-equality)
open import Integers.Type
open import Integers.Addition
open import Integers.Multiplication

首先我們建立一些單位

data Unit : 𝓤₀ ̇ where
  Meter Kilogram Second : Unit

單位的相等是可判定的

Unit-≟ : has-decidable-equality Unit
Unit-≟ Meter    Meter    = inl refl
Unit-≟ Kilogram Kilogram = inl refl
Unit-≟ Second   Second   = inl refl
Unit-≟ Meter    Kilogram = inr (λ ())
Unit-≟ Meter    Second   = inr (λ ())
Unit-≟ Kilogram Meter    = inr (λ ())
Unit-≟ Kilogram Second   = inr (λ ())
Unit-≟ Second   Meter    = inr (λ ())
Unit-≟ Second   Kilogram = inr (λ ())

整數的相等也是可判定的，TypeTopology 已經有 ℤ-is-discrete，這裡我們給它一個新名字，好跟 Unit-≟ 慣例相符

ℤ-≟ : has-decidable-equality ℤ
ℤ-≟ = ℤ-is-discrete

完整的單位簽名由一系列單位與整數組成，整數用來表示該單位的次方，比如公尺的 3 次方就是 [(Meter , pos 3)]

Units : 𝓤₀ ̇
Units = List (Unit × ℤ)

現在讓任何型別 T 都可以附帶單位，但 runtime 只存放 T

data _with-unit_ (T : 𝓤 ̇ ) (us : Units) : 𝓤 ̇ where
  Box : T → T with-unit us

接下來我們要對單位進行乘法，方法就是同單位的次方抵銷。這個合併演算法可以大致描述成

1. 要是紀錄的單位相同，就進行相加並放回清單。除非相加結果為 pos 0（也就是次方為 0），這時候就直接從清單中消去
2. 否則就繼續向後尋找可能的合併目標
3. 要是都找不到，就把自己插在最後面

*-unit : Units → Units → Units
*-unit us₁ us₂ = foldr step us₁ us₂
  where
  step : Unit × ℤ → Units → Units
  step (u , n) []             = (u , n) ∷ []
  step (u , n) ((v , m) ∷ xs) with Unit-≟ u v
  ... | inr _ = (v , m) ∷ step (u , n) xs
  ... | inl _ with ℤ-≟ (n + m) (pos )
  ...   | inl _ = xs
  ...   | inr _ = (u , n + m) ∷ xs

現在開始實現帶有單位的整數運算。相加只能跟同單位的數一起，所以打從一開始沒辦法寫錯把不同單位的數字加在一起

_+̇_ : {us : Units} → ℤ with-unit us → ℤ with-unit us → ℤ with-unit us
Box v₁ +̇ Box v₂ = Box (v₁ + v₂)
infixl  _+̇_

乘法涉及到單位的相乘（正確的處理次方抵銷問題）

_×̇_ : {us₁ us₂ : Units}
    → ℤ with-unit us₁
    → ℤ with-unit us₂
    → ℤ with-unit (*-unit us₁ us₂)
Box v₁ ×̇ Box v₂ = Box (v₁ * v₂)
infixl  _×̇_

最後來看一些範例，這裏把 3s + 3s 所以得到 6s

test-3s+3s : ℤ with-unit [(Second , pos )]
test-3s+3s = s +̇ s
  where
  s : ℤ with-unit [(Second , pos )]
  s = Box (pos )
is-6s : test-3s+3s ＝ Box (pos )
is-6s = refl

這裏把 7m³/(kg·s²) 乘上 2s，所以得到 14m³/(kg·s)

test-7m³/kg·s²×2s : ℤ with-unit ((Meter , pos ) ∷ (Kilogram , negsucc ) ∷ (Second , negsucc ) ∷ [])
test-7m³/kg·s²×2s = g ×̇ s
  where
  g : ℤ with-unit ((Meter , pos ) ∷ (Kilogram , negsucc ) ∷ (Second , negsucc ) ∷ [])
  g = Box (pos )
  s : ℤ with-unit [(Second , pos )]
  s = Box (pos )
is-14m³/kg·s : test-7m³/kg·s²×2s ＝ Box (pos )
is-14m³/kg·s = refl

不是具體的值當然也可以應用這套系統

test-*-abstract : ℤ with-unit ((Meter , pos ) ∷ (Kilogram , negsucc ) ∷ (Second , negsucc ) ∷ [])
                → ℤ with-unit [(Second , pos )]
                → ℤ with-unit ((Meter , pos ) ∷ (Kilogram , negsucc ) ∷ (Second , negsucc ) ∷ [])
test-*-abstract a b = a ×̇ b

其實上面的概念來自 Software Design for Flexibility，書中把這個技巧稱之為 layering。書中的程式長得像這樣：

(define G
  (layered-datum 6.67408e-11
    unit-layer (unit 'meter 3 'kilogram -1 'second -2)))

用我們熟悉的系統表示：

書中採用的技術對大部分語言來說都是適用的，只要能表達附註屬性在資料上就可以了。OOP 語言可能就會定義一個專有的 class 表示 layered data。這裡用標記的方式的優勢也一覽無遺，畢竟大部分語言的型別系統通常並不像上面的 Agda 有這麼強力的能力做這麼複雜的限制

我們說 $Sub\ \Gamma\ \Delta$ 是 epimorphism iff

這也導出了 term 的事實：$u[\sigma] = u'[\sigma] \Rightarrow u = u'$

一個 substitution $\sigma : Sub\ \Gamma\ \Delta$ 如果純粹由變數構成，那麼它是 renaming，記成 $\sigma : Ren\ \Gamma\ \Delta$

而且 Renaming 有以下特性

1. 如果只用到 $\Gamma$ 中的變數至多一次，那麼 $\sigma$ 是 epimorphism
2. 如果只用到 $\Gamma$ 中的變數至少一次，那麼 $\sigma$ 是 monomorphism
3. 如果只用到 $\Gamma$ 中的變數剛好一次，那麼 $\sigma$ 是 isomorphism（context 的 permutation）

Renamings 還有一個子集叫 Embeddings，是 $\Delta$ 為 $\Gamma$ 捨棄 0 到多個變數後組成的 context。

1. 每個 embedding 都是 epimorphism
2. embedding $\Gamma \to \Gamma$ 一定是 identity

想到就測試 rakka 跟 Racket coroutine thread 結果 native 還比較快XD，所以我就把 genserver 做成 Racket thread 封裝了 https://repo.dannypsnl.me/dannypsnl/erl。至於為什麼 coroutine thread 這麼快，我猜可能 CS 之後有很大改善，我之前沒有注意到這點

延續上個禮拜的工作，用手搓的 JIT 實現

1. brainfuck 編譯器
2. brainfuck JIT

racket-langserver 這個 PR 的目的是改善目前一團糟的測試體驗。現在的方式是啟動 subprocess 然後跟它的 stdio 互動，一來這意味著大量的系統資源需求，二來耦合這麼重就很難設計可以遠端連線的 server。所以第一步需要清理現在的設計，引入間接層讓測試只需要跟這個抽象部分互動就好

改善一下 racket-llvm 的文件，修復案例

如果我們同時有 $\Gamma \vdash \sigma : \Delta$ 跟 $\Delta \vdash A \text{ type}$，那我們可以對 $A$ 進行替換得到：

換句話說，我們用 $\sigma$ 完成了一個逆變，記成 $\sigma^* : Ty(\Delta) \to Ty(\Gamma)$。

用相繼式時

表示 $u$ 在 $\Gamma$ 中有類型 $A$，當然，這裡隱含的前提是 $A \in Ty(\Gamma)$。

而替換同樣可以在 term $u$ 上作用：

但我們也知道替換 $\sigma$ 也能看成一個 term，所以同樣可以對它套用替換！

這說明了替換可以結合！我們經常記成 $\gamma \circ \sigma$。

對於 $\Gamma$ 與 $A \in Ty(\Gamma)$，我們有 $\pi_A : \Gamma\triangleright A \to \Gamma$，這叫做 display map。提醒一下這個相繼式是

考慮逆變，就得到

唯一確定了一個類型，也就是說現在每個 type $A$ 都被一個某一些替換代表了。這也可以說其實我們在看 $Hom_\mathcal{C}(- , \Gamma)$ 這些 morphisms。

同理可以放到 term $u$ 上，對於

可以視為

也就是說每一個 term $u$ 都可以看成替換

對於任何 $\sigma : \Delta \to \Gamma$，我們把逆變看成 slice category 的函數 $\mathcal{C} / \Gamma \to \mathcal{C} / \Delta$，要檢查這是否是 functor，我們想要證明兩件事：保留 identity 且保留 composition。

Proof [local-5]

套上 display maps 的規範，知道逆變會產出一個 pullback：

這直接證明了 $\sigma \circ \sigma^*(id) = \sigma$，所以 $\sigma^*(id) = id_\Delta$，表示 $\sigma^*$ 保留了 identity。

要證明 composition，可以用 pullbacks 的結合知道如果 $\sigma^*(f) \circ \sigma^*(g)$ 跟 $\sigma^*(f \circ g)$ 的頂點 up to isomorphism 是同一個，因此這兩個 morphism 是一樣的，證明了也保留 composition。因此每個替換誘導出的逆變都是 functor。 □

由於一項技術的潛在用途並非其實際用途，而實際用途又取決於採用該技術的機構、機構試圖解決的問題以及機構用作衡量成功的既有指標。所以 Context Widows 認為探討 LLM 與科學的關係，等若詢問 LLM 出現之前，科學界已經運作著怎樣的體系？

我們知道當代科學界的主導是引用體系，隨著時間發展，引用體系已經改變它本要量測的對象；科學家會調整自己的行為以最佳化指標。Context Widows 也駁斥用古德哈特定律「當一個指標成為目標時，它就不再是一個好的指標」來解釋這件事，因為古德哈特定律只認為指標是問題，但 Context Widows 一文認為有問題的是需要指標才能運作的組織形式。

在這個背景下，LLM 雖然有其他的功用，卻只會加速學術界的固有邏輯：更多的發表。引用文中的話來說

LLM 並非經濟學家（一群熱衷於用貶低維度的方式來消除意義的人）所稱的科學激勵「結構」的創造者。相反，這項技術恰好出現在這樣的背景下，提供了一種更快的方式來生產系統所獎勵的成果。

同樣的，這使得我們去問：LLM 出現之前，商業運作著怎樣的體系？

在經濟學追尋公司的意義時，Milton Friedman 在 1970 年提出 The Social Responsibility of Business Is to Increase Its Profits，直譯大概就是「企業的社會責任是增加利潤」，這是當代企業的主流追求與試圖實踐的理想。這有什麼樣的後果？

Paul 有兩篇相關的 thread，很清晰的闡述了當代的企業環境

1. https://hachyderm.io/@inthehands/113603661215753448
2. https://hachyderm.io/@inthehands/115793003693199462

儘管我們大多數人都生活在現代企業地獄般的環境中，仍然無法理解大企業的運營究竟有多麼嚴重的破碎，以及它們在多大程度上依靠虛假、欺騙和胡言亂語來運作。

所以，為什麼公司部署 LLM 呢？Paul 讓我們從底線來看：XX 公司的新 AI 客服描述不存在的功能，或是叫人們去吃釘子或膠水。會怎樣嗎？嗯反正他們以前那些不幸的、缺乏訓練的、工資微薄、像泥土一樣被對待的客服人員（過去負責處理所有的客戶支援），實際上也沒有幫助人們。由於 XX 公司對吞吐量的要求如此之高，並且對問題關閉的激勵如此之大，以至於他們的客服人員帶領人們白費力氣，罵人或放棄回應。LLM 不會罵人，不會放棄回應，吞吐量極高。它在帶領人們白費力氣上「遠遠」比人類更有效率，而且有時候僅僅靠運氣，它實際上是對的！

從底線來看，部署 LLM 其實沒有那麼糟糕！所以現況其實是

商業活動為世界提供的實際價值如此之少，以至於用快速、自動化的廢話取代緩慢的人類廢話似乎是一場勝利。

所以對於採不採用 LLM，我們可以問的問題是：如果它是錯誤的，那麼重要嗎？Paul 以特斯拉為案例：特斯拉正在銷售這些「顯然」還沒有準備好迎接黃金時段的自毀汽車，它們會用事故後打不開的車門將人們困在裡面，然後將他們活活燒死。而且他們仍然在銷售大量這些東西。如果對他們來說這樣都無關緊要，那有多少虛假和危險的商業環境是可以被他們接受的？

LLM 是假的？又怎樣呢？商業也是如此。

更具體的說，LLM 會對管理層帶來什麼影響？對糟糕的組織領導人來說，讓擁有專業知識的下屬不去檢查他們的想法基本上就是成癮性藥物。那 LLM 豈不是就是不會拒絕他們任何「高妙」想法的完美下屬？這是一種強大的心理力量，促使我們快速地往採用 LLM 滑動，無關乎這是否有用。

所以同樣的，LLM 表現出的，是對既有商業實踐的加劇與加速，放大既有的功能失調。在 LLM 以前同樣有 08 年的次貸風暴，遵循一樣的系統運行規則而致。

LLM 能否有效的融入人的成長、交流與生活中？這當然是一個複雜的問題：LLM 出現之前，現代人類是怎麼成長、交流與生活的？

1. 現代的主流成長方式，是未成年人類放到學校；而成年人上網看一些什麼如何投資、如何成長的東西，比如人們會看教你如何閱讀的影片，但不會真的去閱讀。對了，老闆想要成長 — 我們就讓老闆「看見」成長。
2. 現代的主流社交方式，是在稱之為社群媒體或是社交平台（像是 threads、IG、FB）的地方對幽谷大喊，由演算法控制人們看到什麼（你很好奇為什麼 meta 好像持有前述的所有平台？這是很好的好奇）
3. 現代的主流過活方式，是必須上 8 小時以上的班，換取大概能過活的薪水，在剩餘的時間想辦法娛樂自己，我們勉強稱之為生活

LLM 會怎麼影響，要看 LLM 有哪些具體的施展位置。

1. 在學校逐漸提高效率要求的情況下，你要怎麼譴責老師：用 LLM 生成題目、改答案、規劃教學？

2. 在課業繁重的情況下，學生要怎麼不用 LLM 生成作業？尤其是成績如果能因此提高，而系統獎勵成績時？

3. 人們要怎麼分辨出 LLM 生成的留言然後避免被影響？

4. 人們要怎麼在生活壓力越來越大時不對 LLM 宣洩情感？至少它不會罵我們

5. 人們要怎麼在不因為能對 LLM 下令而被權力損傷？

   oh, I just realized: does this mean that AI gives everyone the chance of the brain damage humans get from too much power too long?

   參見 Power changes how the brain responds to others。

6. 要怎麼在搜尋引擎預設就提供 LLM 合成答案時去搜尋原始文章，確認內容？

7. 要怎麼在繁重的工作壓力下保持生活？

上述的問題，有些出自商業邏輯，有些跟我們的社會運作有關，有些是因為人類的生理能力。再次的，LLM 加劇我們的問題，但不是唯一的原因。要讓 LLM 技術不對人類造成危害，就要在這些具體的案例中找出我們的解答。

1. 監控資本主義時代 上卷: 基礎與演進/ 下卷: 機器控制力量：除了這本書本身指出的極端情況，還有數個對現況的相關看法應該一起吸收，我應該會再寫一篇文章寫這方面的感想
2. 萬事揭曉：打破文明演進的神話，開啟自由曙光的全新人類史：作者認為大眾對人類發展史的看法深受盧梭與霍布斯的遺緒影響，而考古與人類學證據足以駁斥這些觀點
3. 慈禧: 開啟現代中國的皇太后：這是在 mastodon 上看別人看很有趣就去買的書，作者盡力基於歷史證據描繪了一個與學生時代課本所述完全不同的慈禧
4. 不實在的現實：以演化為基本的公理的話，我們會推導出什麼樣的世界觀？我覺得有關聯、也很有啟發性的是訪談 Michael Levin 討論的事情
5. 勤儉魔法師的中古英格蘭生存指南、侑美與夢魘繪師、翠海的雀絲、日煉者：嚴格來說日煉者我只看了一半，不過應該很快就能看完xd
6. 裸顏（Till we have faces）：這本小說的劇情很明顯不能按照字面意思去讀，賽姬跟歐若要解釋成一個人或是兩個人都可以，而「神」的意義也明顯有多重意義，每次閱讀應該都會投射自己的人生感想進去吧xd