解釋 (interpretation) ⟦Γ▹μ(x:t).M:t⟧ρ\llbracket \Gamma \triangleright \mu(x:t). M : t \rrbracket\rho[[Γ▹μ(x:t).M:t]]ρ 必須是一個能滿足下面等式的 ⟦t⟧\llbracket t \rrbracket[[t]] 元素 ddd d=⟦Γ,x:t▹M:t⟧(ρ[x↦d])d = \llbracket \Gamma, x:t \triangleright M : t \rrbracket(\rho[x \mapsto d])d=[[Γ,x:t▹M:t]](ρ[x↦d]) 註：ρ\rhoρ 在後面講到語意解釋時會定義