プログラミングinOCaml 練習問題3.4② ～③の答案
練習問題3.4 ②および③についても①と同様の解き方を用いる。 まずは、①で定義したオブジェクトおよび擬似関数を示す。束縛 順序対(var, val)で表す。ここで、varは変数、valは値である。部分環境 順序対(A, R)であり、[]による記法で表す。ここで、Aは同変数の束縛のクラス、RはA上の順序関係である。また、[]には宣言の新しい順に束縛が並ぶ。例: x = 3, x =1の順で宣言がなされたときの変数xの部分環境 [(x, 1), (x, 3)] 環境(全体環境) 部分環境の和クラスであり、[]と⊕とによる記法で表す。例: 変数xと変数yとが宣言された環境 [(x, 1), (x, 3)]⊕[(y, 1)]部分環境関数ℭ 変数varについての部分環境(A, R)を環境Envから抜き出す。(A, R) = ℭ(Env, var)参照関数ℜ 環境Envにおける変数varの参照。val = ℜ(Env, var)宣言関数𝔇 環境Envと宣言による束縛のクラスとから新しい環境Env'を選ぶ。Env' = 𝔇(Env, {(var₀, val₀), ..., (varₙ, valₙ)})評価関数𝔈 式exprを環境Envで評価する。val = 𝔈(expr, Env)let式の書換え規則𝔈(let var₀ = expr₀ and ... and varₙ = exprₙ in expr, Env)= 𝔈(expr, 𝔇(Env, {(var₀, 𝔈(expr₀, Env)), ..., (varₙ, 𝔈(exprₙ, Env))})関数の書換え規則𝔈(f(x, y), Env) = f(𝔈(x, Env), 𝔈(y, Env))変数の書換え規則𝔈(var, Env) = ℜ (Env, var)定数の書換え規則𝔈(val, Env) = val 次に、これらの定義を用いた練習問題3.4②, ③の答案を示す。②式の書換え 初期の環境をEnv₀とする。②の式についての評価関数𝔈は、𝔈(let x = 2 and y = 3 in (let y = x and x = y + 2 in x * y) + y, Env₀)である。Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀)), (y, 𝔈(3, Env₀))})とおくと、let式の書換え規則により、= 𝔈((let y = x and x = y + 2 in x * y) + y, Env₁)関数の書き換え規則により、= 𝔈(let y = x and x = y + 2 in x * y, Env₁) + 𝔈(y,Env₁)Env₂ = 𝔇(Env₁, {(y, 𝔈(x, Env₁)), (x, 𝔈(y + 2, Env₁))})とおくと、let式の書換え規則により、= 𝔈(x * y, Env₂) + 𝔈(y, Env₁)関数の書き換え規則により、= 𝔈(x, Env₂) * 𝔈(y, Env₂) + 𝔈(y, Env₁)変数の書換え規則により、 = ℜ(x, Env₂) * ℜ(y, Env₂) + ℜ(y, Env₁)となる。環境の導出Env₀ Env₀は空とする。Env₀ = []Env₁Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀)), (y, 𝔈(3, Env₀))})であり、𝔈(2, Env₀) = 2と𝔈(3, Env₀) = 3より、= {(x, 2), (y, 3)} ⇢ []= [(x,2)] ⊕ [(y, 3)]となる。Env₂Env₂ = 𝔇(Env₁, {(y, 𝔈(x, Env₁)), (x, 𝔈(y + 2, Env₁))})であり、𝔈(x, Env₁) = ℜ(x, Env₁) = 2と𝔈(y + 2, Env₁) = ℜ(y, Env₁) + 2 = 5 より = {(y, 2), (x, 5)} ⇢ [(x,2)] ⊕ [(y, 3)]= [(x,5), (x,2)] ⊕ [(y, 2), (y, 3)] となる。評価結果の予想 したがって、 ℜ(y, Env₁) = 3ℜ(x, Env₂) = 5ℜ(y, Env₂) = 2である。 よって、𝔈(let x = 2 and y = 3 in (let y = x and x = y + 2 in x * y) + y, Env₀)⋮= ℜ(x, Env₂) * ℜ(y, Env₂) + ℜ(y, Env₁)= 5 * 2 + 3= 13となる。変数の参照と宣言との対応 let x = 2 and y = 3 in (let y = x and x = y + 2 in x * y) + yにおける変数参照は、y = x and x = y + 2のxおよびyと、x * yのxおよびyと、yである。y = x and x = y + 2 𝔈(let y = x and x = y + 2 in x * y, Env₁)より、xおよびyの変数参照が対象とする束縛は環境Env₁に属し、その環境Env₁は、 Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀)), (y, 𝔈(3, Env₀))})である。 したがって、xについての束縛は宣言x = 2によるものであり、y + 2についての束縛は宣言y = 3によるものである。x * y 𝔈(x * y, Env₂)より、xおよびyの変数参照が対象とする束縛は環境Env₂に属し、その環境Env₂は、 Env₂ = 𝔇(Env₁, {(y, 𝔈(x, Env₁)), (x, 𝔈(y + 2, Env₁))})である。 したがって、xについての束縛は宣言x = y + 2によるものであり、yについての束縛は宣言y = xによるものである。y 𝔈(y, Env₁)より、yの変数参照に対応する宣言は、上述したy + 2での宣言と同じものである。 したがって、yについての束縛は宣言y = 3によるものである。まとめ 答え: 予想される評価結果は13である。y = xにおけるxの参照は、宣言x = 2を指す。x = y + 2におけるyの参照は、宣言y = 3を指す。x * yにおけるxの参照は、宣言x = yを指す。x * yにおけるyの参照は、宣言y = xを指す。let ... yにおけるyの参照は、宣言y = 3を指す。let x = 2 and y = 3 in (let y = x and x = y + 2 in x * y) + y③式の書換え 初期の環境をEnv₀とする。③の式についての評価関数𝔈は、 𝔈(let x = 2 in let y = 3 in let y = x in let z = y + 2 in x * y * z, Env₀)である。Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀))})とおくと、let式の書換え規則により、 = 𝔈(let y = 3 in let y = x in let z = y + 2 in x * y * z, Env₁)Env₂ = 𝔇(Env₁, {(y, 𝔈(3, Env₁))}) とおくと、let式の書換え規則により、 = 𝔈(let y = x in let z = y + 2 in x * y * z, Env₂)Env₃ = 𝔇(Env₂, {(y, 𝔈(x, Env₂))}) とおくと、let式の書換え規則により、 = 𝔈(let z = y + 2 in x * y * z, Env₃)Env₄ = 𝔇(Env₃, {(z, 𝔈(y + 2, Env₃))}) とおくと、let式の書換え規則により、 = 𝔈(x * y * z, Env₄)関数の書換え規則により、 = 𝔈(x, Env₄) * 𝔈(y, Env₄) * 𝔈(z, Env₄)変数の書換え規則により、 = ℜ(x, Env₄) * ℜ(y, Env₄) * ℜ(z, Env₄)となる。環境の導出Env₀ Env₀は空とする。 Env₀ = []Env₁ Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀))})であり、𝔈(2, Env₀) = 2より、 = {(x, 2)} ⇢ []= [(x, 2)]となる。Env₂ Env₂ = 𝔇(Env₁, {(y, 𝔈(3, Env₁))})であり、𝔈(3, Env₁) = 3より、 = {(y, 3)} ⇢ [(x, 2)]= [(x, 2)] ⊕ [(y, 3)]となる。Env₃ Env₃ = 𝔇(Env₂, {(y, 𝔈(x, Env₂))})であり、𝔈(x, Env₂) = ℜ(x, Env₂) = 2より、 = {(y, 2)} ⇢ [(x, 2)] ⊕ [(y, 3)]= [(x, 2)] ⊕ [(y, 2), (y, 3)]となる。Env₄ Env₄ = 𝔇(Env₃, {(z, 𝔈(y + 2, Env₃))})であり、𝔈(y + 2, Env₃) = ℜ(y, Env₃) + 2 = 2 + 2 = 4より、 = {(z, 4)} ⇢ [(x, 2)] ⊕ [(y, 2), (y, 3)]= [(x, 2)] ⊕ [(y, 2), (y, 3)] ⊕ [(z, 4)]となる。評価結果の予想 したがって、 ℜ(x, Env₄) = 2ℜ(y, Env₄) = 2ℜ(z, Env₄) = 4である。 よって、 𝔈(let x = 2 in let y = 3 in let y = x in let z = y + 2 in x * y * z, Env₀)⋮= ℜ(x, Env₄) * ℜ(y, Env₄) * ℜ(z, Env₄)= 2 * 2 * 4 = 16となる。変数の参照と宣言との対応 let x = 2 in let y = 3 in let y = x in let z = y + 2 in x * y * zにおける変数参照は、y = xのxと、z = y + 2のyと、 x * y * zのx, y, およびzである。y = x 𝔈(let y = x in let z = y + 2 in x * y * z, Env₂)より、xの変数参照が対象とする束縛はEnv₂に属し、そのEnv₂は、 Env₂ = 𝔇(Env₁, {(y, 𝔈(3, Env₁))})である。Env₂の宣言関数𝔇はxについての束縛を含まないので、Env₂におけるxの束縛のクラスはEnv₁のものと同一とである。そのEnv₁は、 Env₁ = 𝔇(Env₀, {(x, 𝔈(2, Env₀))})であるので、xについての束縛は宣言x = 2によるものである。z = y + 2 𝔈(let z = y + 2 in x * y * z, Env₃)より、yの変数参照が対象とする束縛はEnv₃に属し、そのEnv₃は、 Env₃ = 𝔇(Env₂, {(y, 𝔈(x, Env₂))})であるので、yについての束縛は宣言y = xによるものである。x * y * zのx 𝔈(x * y * z, Env₄)より、xの変数参照が対象とする束縛はEnv₄に属し、そのEnv₄は、 Env₄ = 𝔇(Env₃, {(z, 𝔈(y + 2, Env₃))})であるが、Env₄の宣言関数𝔇はxの束縛を含まず、さらに、Env₃についても、 Env₃ = 𝔇(Env₂, {(y, 𝔈(x, Env₂))})より、Env₃の宣言関数𝔇はxの束縛を含まない。これより、Env₄およびEnv₃におけるxの束縛のクラスはEnv₂のもの同一となる。 したがって、x * y * zにおけるxの変数参照に対応する宣言は、上述したy = xでの宣言と同じとなる。よって、xについての束縛は宣言x = 2によるものである。x * y * zのy Env₄の宣言関数𝔇はyの束縛を含まないので、yの束縛のクラスはEnv₃のものと同一である。 したがって、上述したように、yについての束縛は宣言y = xによるものである。x * y * zのz Env₄ = 𝔇(Env₃, {(z, 𝔈(y + 2, Env₃))})より、zについての束縛は宣言z = y + 2によるものである。まとめ 答え: 予想される評価結果は16である。y = xにおけるxの参照は、宣言x = 2を指す。z = y + 2におけるyの参照は、宣言y = xを指す。x * y * zにおけるxの参照は、宣言x = 2を指す。x * y * zにおけるyの参照は、宣言y = xを指す。x * y * zにおけるzの参照は、宣言z = y + 2を指す。let x = 2 in let y = 3 in let y = x in let z = y + 2 in x * y * z上記は、プログラミングinOCaml,五十嵐淳についての感想および練習問題の答案である。著作権を侵害してしまうことがないように問題文は載せていない。ただし、問題文中において、ごく短い文であって、ありふれた表現であり、それのみでは問題としての意味をなさないようなもの(例えば、"- - 1"など)は、著作物にあたらないと判断し、記述している。
