為什麼需要 domain theory？遞迴的數學表示 [math-28UX]

2023-12-09 · Lîm Tsú-thuàn

一般的 OCaml 函數可以寫成

let f x y z = ...

一個直覺的想法是：每個型別都解釋成一個可數集合，該型別的 term 解釋成這個集合的元素。但有些函數會用到自己本身，例如整數階乘函數

let rec fac n =
  if n = 0
  then 1
  else n * fac(n-1)

它的值是什麼呢？答案是

μ(x:int→int).λ(n:int).{1(n=0)n×x(n−1)(n≠0)\mu (x : int \to int). \lambda (n : int). \begin{aligned} \begin{cases} 1 &\quad &(n = 0) \\ n \times x(n-1) &\quad &(n \ne 0) \end{cases} \end{aligned}

μ\mu 中的 xx 就是 fac 自己，把原始 OCaml 程式中的 fac 換成 xx 即可。問題是集合論沒有辦法充分解釋這個運算，具體來說，集合解釋不滿足 PCF 的 Adequacy theorem。

Theorem Adequacy (充分性定理) [math-CFN7]

2023-12-09

If MM is closed term of ground type and C⟦M⟧=C⟦V⟧\mathcal{C}\llbracket M \rrbracket = \mathcal{C}\llbracket V \rrbracket for a value VV, then M⇓VM \Downarrow V.

對一個形式系統來說，需要證明一個假定的 model 確實能表現系統的特徵，所以才需要證明這個定理。參考 computational adequacy

一般來說，只考慮構造與操作規則的話，可以記成下面這樣

Definition Rules of μ\mu [math-TMY9]

2023-12-09

Typing [local-0]

Γ,x:t⊢M:tΓ⊢μ(x:t).M:t\frac{ \Gamma, x : t \vdash M : t }{ \Gamma \vdash \mu (x : t) . M : t }

Operational (Big step) [local-1]

[μ(x:t).M/x]M⇓Vμ(x:t).M⇓V\frac{ [\mu(x:t).M/x] M \Downarrow V }{ \mu(x:t).M \Downarrow V }

但我們想要知道在數學上可以用什麼物件表示運算子 μ\mu，也就是指稱語意 (denotational semantic)，我先定義一個這個目標需要達成的等式。

基本的約束 [math-2C9J]

2023-12-09

解釋 (interpretation)

⟦Γ▹μ(x:t).M:t⟧ρ\llbracket \Gamma \triangleright \mu(x:t). M : t \rrbracket\rho

必須是一個能滿足下面等式的 ⟦t⟧\llbracket t \rrbracket 元素 dd

d=⟦Γ,x:t▹M:t⟧(ρ[x↦d])d = \llbracket \Gamma, x:t \triangleright M : t \rrbracket(\rho[x \mapsto d])
註：ρ\rho 在後面講到語意解釋時會定義

問題是我們怎麼知道存在這麼一個元素呢？由於不動點定理，使得我們有動機把 ⟦t⟧\llbracket t \rrbracket 解釋成 cpo，把計算解釋成 monotone function 再套用不動點定理。從而得到一個合理的定義：least fixed point 即是 μ\mu 的表示物件。

Definition C⟦e⟧\mathcal{C}\llbracket e \rrbracket 的解釋 [math-SSSU]

2023-12-09

Notation [local-0]

這裡採用 x↦vx \mapsto v 表示數學中的函數，xx 是輸入 vv 是輸出；但 ρ[x↦d]\rho[x \mapsto d] 則是指 ρ\rho 中的 xx 被替換成 dd

在開始之前我們需要大概了解 C⟦x⟧\mathcal{C}\llbracket x \rrbracket 這個解釋的定義。

  • 當 tt 是型別，則 C⟦t⟧\mathcal{C}\llbracket t \rrbracket 是一個 cpo
  • 當 s,ts, t 是型別，則 C⟦s→t⟧\mathcal{C}\llbracket s \to t \rrbracket 是一個連續函數，domain 是 C⟦s⟧\mathcal{C}\llbracket s \rrbracket 而 codomain 是 C⟦t⟧\mathcal{C}\llbracket t \rrbracket
  • ρ\rho 是一個 Γ\Gamma-環境，幫每個 Γ\Gamma 中的變數 xx 定義一個 ρ(x)∈C⟦Γ(x)⟧\rho(x) \in \mathcal{C}\llbracket \Gamma(x) \rrbracket，Γ(x)\Gamma(x) 是一個型別
  • C⟦Γ▹M:t⟧ρ∈C⟦t⟧\mathcal{C}\llbracket \Gamma \triangleright M : t \rrbracket\rho \in \mathcal{C}\llbracket t \rrbracket，要解釋成三種情形
    • C⟦Γ▹x:t⟧ρ=ρ(x)\mathcal{C}\llbracket \Gamma \triangleright x : t \rrbracket\rho = \rho(x)

      需要 ρ\rho 函數的部分，當我們在程式語言中寫下 let f : T = M 時，就在 ρ\rho 這個部分函數中加入了 f=Mf = M 的定義，注意到 ρ\rho 是部分函數，因為也可能被問到未綁定的變數 zz，這時候 ρ(z)=⊥\rho(z) = \bot

    • C⟦Γ▹λ(x:s).M:s→t⟧ρ=(d↦C⟦Γ,x:s▹M:t⟧(ρ[x↦d]))\mathcal{C}\llbracket \Gamma \triangleright \lambda (x : s). M : s \to t \rrbracket\rho = (d \mapsto \mathcal{C}\llbracket \Gamma, x : s \triangleright M : t \rrbracket(\rho[x \mapsto d]))

      為程式函數找一個數學函數作為解釋

    • C⟦Γ▹M(N):t⟧ρ=(C⟦Γ▹M:s→t⟧ρ)(C⟦Γ▹N:s⟧ρ)\mathcal{C}\llbracket \Gamma \triangleright M(N) : t \rrbracket\rho = (\mathcal{C}\llbracket \Gamma \triangleright M : s \to t \rrbracket\rho)(\mathcal{C}\llbracket \Gamma \triangleright N : s \rrbracket\rho)

      直接調用作為解釋的數學函數

Definition μ\mu 的解釋結果 [math-IG9K]

2023-12-09

μ\mu 本身的公式倒沒有很複雜

C⟦Γ▹μ(x:t).M:t⟧ρ=fix(f)\mathcal{C}\llbracket \Gamma \triangleright \mu(x:t). M : t \rrbracket\rho = \text{fix}(f)

其中數學函數 ff 是

d↦C⟦Γ,x:t▹M:t⟧ρ[x↦d]d \mapsto \mathcal{C}\llbracket \Gamma, x : t \triangleright M : t \rrbracket \rho[x \mapsto d]

但我們怎麼確認 fix(f)\text{fix}(f) 的存在？我們已經知道 C⟦t⟧\mathcal{C}\llbracket t \rrbracket 是 cpo。根據不動點定理我們知道只要再證明 ff 是連續函數即可；接著根據下面的定理我們可以知道這能夠套用到任意來自 ground type 的 functional 上

Proposition (cpo)-continuous function space is a cpo [math-LVSY]

2023-12-10

If DD and EE are cpo, then the continuous function space

[D→E]={f:D→E∣f is continuous} [D \to E] = \{ f : D \to E \mid f \ \text{is continuous} \}

is a cpo under the pointwise order.

再來就可以選擇 least fixed point 作為 fix(f)\text{fix}(f) 的解釋

⨆n∈ωdn\bigsqcup_{n \in \omega}d_n

其中

  • d0=⊥⟦t⟧d_0 = \bot_{\llbracket t \rrbracket}
  • dn=C⟦Γ,x:t▹M:t⟧ρ[x↦dn−1]d_n = \mathcal{C}\llbracket \Gamma, x : t \triangleright M : t \rrbracket\rho[x \mapsto d_{n-1}]

不過這條鏈 dnd_n 不需要是唯一的，只要對任何一條都能這樣推理即可。

要證明函數 d↦C⟦Γ,x:t▹M:t⟧ρ[x↦d]d \mapsto \mathcal{C}\llbracket \Gamma, x : t \triangleright M : t \rrbracket\rho[x \mapsto d] 對所有 Γ\Gamma-環境 ρ\rho 都成立有點麻煩，需要歸納所有的語法構造，所以這裡就跳過。或許哪天我會寫這部分，不過有興趣的讀者可以先參考 Gunter 的書的第四章，或是自己根據 PCF 這個 metalanguage 進行證明。Sterling 的演講 Synthetic Domains in the 21st Century 也是很好的資源。