変数の静的有効範囲

Semantics with
Applications
(２章５節(2))
変数の静的有効範囲
変数に静的有効範囲を用いるために
状態(s)を２つの写像に書き換える。
• 変数とlocationを結びつける変数の環境(EnvV)
• それぞれのlocationに値を結びつけるstore
変数環境：変数を受け取り、locationの集合を返す
Store：下の要素（nextは次のfree locationを持っている
特殊なトークン）
簡単にするために、Loc = Z(値)ということにする。
変数の静的有効範囲
• 状態sを変数から値への単独の写像ではなく、
２つの写像 envvとstoに分けて、s=sto envv
とする。
変数xの値を求めるには、
• xに関連づけられている位置 l = envv xを求め、
• l に関連付けられている値 sto l を求める
変数xに値を割り当てるには、
• xに関連づけられている位置 l = envv xを求め、
• storeを sto l = v となるように更新する
変数宣言の静的有効範囲規則
変数環境とstoreは変数宣言によって更新されるので、
変数宣言のためのtransition system（
のところ）は
次の形に修正される。
よって次のようになる。
変数の静的有効範囲のための環境更新
変数を静的な有効範囲にするために、
procedureの環境を、procedure宣言時の変数の環境を
持つように拡張する。
procedureの環境は今までのようにprocedureの宣言
によって更新される。
拡張した環境のための環境更新は以下の通り。
変数の静的有効範囲規則(1)
命令文のtransition systemは次の形になる。
変数の静的有効範囲規則(2)
変数の静的有効範囲規則(3)
演習2.42
表2.8の自然意味論をxが値３を持つ下で演習2.38
の階乗の命令文に適用しなさい。
演習2.43
演習2.39の命令文を適用して、期待された結果が与
えられることを確かめなさい。
演習2.44
while言語の代わりの意味論が図2.8の
ass(ns)〜while(ns)
の公理と規則によって定義された。
図２のそれとこの意味論の間の等価について考察し、
証明せよ。
演習2.45
手続きが２つの call-by-value パラメータをとれるように手続き
の宣言の構文を修正せよ。
Dp ::= proc P ( x1 , x2) is S; Dp | ε
S ::= … | call p (a1,a2)
手続きの環境の要素は下の通りである。
Env p =
Pname ⇨ Var × Var × Stm × Envv × Envp
上に挙げた意味論をこの言語を処理するように修正せよ。特
にprocedureの呼び出しのための新しい規則を規定しなさい。
一つは再帰でないprocedureのために、もう一つは再帰の
procudureのために。
命令文を構成し、新しい規則をどうやって使うかを説明しなさ
い。
演習2.46
今Proc言語と相互再帰を達成する仕事を考える。
このprocedure環境は次の要素で定義される。
Env p =
Pname ⇨ Stm × Envv × Envp × Decp
これは envp p = ( S, env’v env’p, D*p) のとき
D*p はpとして同じブロックで作られた全てのprocedure環境を
含む。upd’p を次のように定義する。
upd’p (proc p is S; Dp , envv ,envp ,D*p )=
upd’p(Dp, envv,envp[p|→(S,envv,envp,D*p)],D*p)
upd’p(ε, envv,envp,D*p)=envp
演習2.46(続き)
次にupdp を次のように再定義する。
upd’p(Dp, envv,envp) = upd’p (Dp, envv,envp,Dp)
Procの意味論を同じブロックで定義されたprocudure間で相互再
帰を得るように修正しなさい。
あなた選んだ面白い命令文で新しい規則がどうやって使われる
か明らかにしなさい。
(ヒント：[call(rec)cc]が変更する必要のある唯一の規則です。関
数updpが新しい[call(rec)cc]の定義に役立つかどうか考えなさ
い)
演習2.47
次のfree locationを保持するために、storeよりむしろ変
数環境を使うような意味論の変形を考えよう。
まず、次の２つを仮定する。
Envv = Var U {next} → Loc
Store = Loc → Z
sto envvで、はじめにenvvを変数のlocationを見つけ
るために使って、stoをそのlocationの値を見つけるのに
使って求められる状態を表す。
演習2.47（続き）
図2.7の節を今置き換える。
Envv = Var∪{next} → Loc
Store = Loc → Z
意味論の２つの変形の下で違った結果を計算する命令
文を構成しなさい。適している状態から命令文を実行し、
導出木を構成することによってあなたの主張が正しいこ
とを証明しなさい。

Download Report