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

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

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

  • $\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]))$

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

  • $\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)$

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