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

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

μ\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 不需要是唯一的，只要對任何一條都能這樣推理即可。