引数渡し機構を拡張した可逆プログラミング言語の可逆性の保証
2010SE199 新海由侑

2010SE237 田中秀明

指導教員：横山哲郎

1

はじめに

2.2

Jensen’s Device

Jensen’s Device とは，命令型プログラミング言語 Al現在，提案されている可逆命令型プログラミング言語
では，高水準プログラミング言語に通常は備わっている gol60 において提案された総和を求める計算を行うプログ
表現力を高めるための機構が備わっていない．可逆命令 ラムである．文献 [4] においても，Jensen’s Device を参照
型プログラミング言語のひとつである Janus[1][2][3] には， し，文献中で用いられている．Jensen’s Device は，名前引数渡し機構が提案されているが，不十分であると考え 渡しのもつ力を最大限生かすような構造をしており，名られる点がある．たとえば，提案されている Janus には， 前渡しを実装していないプログラミング言語では記述す
変数名と記憶場所との対応関係を表す環境という概念が ることができない．
導入されていない．これにより，可逆性を保ったまま引3 環境記憶域モデルを適用した可逆プログラ数を渡すとき，実引数が変数に限定されるため，一般にミング言語用意すべき変数が増えてしまう．ここで，可逆性とは，任
我々は，Janus に環境記憶域モデルを適用した．環境意の状態において，その直前と直後の状態がそれぞれ一意に定まることをいう．また，可逆プログラミング言語 γ :: Vars ∪ {next} ∪ Cons * Lvals ∪ Vals は変数 x, nextとは，そのプログラムが必ず可逆性をもつような言語設 または定数 c と左辺値 l または値 v とを対応付ける部分関数である：
計がなされているプログラミング言語である．
(
我々は本研究において，環境の概念を追加した Janusl0
if x0 = x00の引数渡し機構を提案し，その可逆性を証明する．これ
x(γ[x 7→ l ]) =xγ otherwise
により，変数に加えて，実引数として式を渡すことができるようになり，一般に変数の数を減らすことができる．
γ の一番右側が必ず [next 7→ ·] になるようにすることで，また，環境の導入に伴い，配列を連続的に扱うことがで可逆な意味規則にしている．なお，next は現在使用されきるようになる．ている記憶域の次に使用されていない記憶域を指す特別
引数渡し機構を拡張した Janus で，実引数として式を渡な変数名である．記憶域 σ :: Lvals * Vals は左辺値 l とすプログラムを実現し，現在提案されている Janus によ
値 v を対応付ける部分関数であり，後置演算子 [l, v1 , v2 ] ::るプログラムとの比較を行う．現在提案されている JanusStores * Stores は，記憶域の記憶場所 l にある値 v1 をでは，可逆性を保ったまま式を渡すことができない．こv2 に更新する：
れに対して，我々の提案する Janus では，引数として式を渡すことによって変数の数を減らし，表現力の高いプ(σ[l0 7→ v 0 ])[l, v1 , v2 ]ログラム記述に繋げることができる．
(σ[l0 7→ v2 ]if l0 = l and v 0 = v1
=2 関連研究(σ[l, v1 , v2 ])[l0 7→ v 0 ] otherwise
2.1 Janus
この演算子には必ず逆関数が存在する：
前述のような不十分な点は存在するが，Janus は我々の研究におけるアイデアを試す可逆プログラミング言語と[l, v1 , v2 ]−1 = [l, v2 , v1 ]して適した特性を備えている．以下に Janus が備える主ここで，環境記憶域モデルを適用した Janus の構文の要な特性を 4 つ紹介する．第 1 に，Janus は，可逆であることの形式的証明がなされており，非可逆なプログラ 一部を紹介する．本稿で取り扱う構文領域を図 1, 意味領ムを記述することはできない．これにより，答えを返し 域を図 2, 構文規則を図 3, 操作的意味論を図 4 に示す．
た任意のプログラムの可逆性が必ず保証される．第 2 に， まず，操作的意味論における式と文の判断についてのJanus では同一のプロシージャを順，逆の両方向に実行 説明を記す．ただし，e は式，Γ はプロシージャ名とプロできる．第 3 に，Janus では可逆性を保つために構文に シージャ本体を対応させる関数である．式の評価は，対していくつかの条件や制約が設けられているが，これγ, σ `expr e ⇒ v
らによってプログラマの意図しないゴミ情報が発生することのないように設計がされている．なお，ゴミ情報とで表され，環境 γ, 記憶域 σ において，式 e の評価値が v
は，プログラムに期待される本来の出力以外に発生するになることを意味する．文の実行は，出力のことである．第 4 に，Janus は汎用的な可逆プログラミング言語である．
γ, σ `Γstmt s ⇒ γ, σ 0s ∈ Stmse ∈ Expsp ∈ Procsx ∈ Varsd ∈ Vdecs
q ∈ PIdst ∈ Typec ∈ Consct ∈ CallTypes∈ ModOps⊗ ∈ Ops

d ::= x | x[c]t ::= ints ::= x = e | x[e] = e |if e then s else s fi e |local t x = e s delocal t x = e |call q(e) | uncall q(e) | · · ·e ::= c | x | x[e] | e ⊗ ec ::= -2147483648 | · · · | 2147483647::= + | - | ^⊗ ::= | * | / | · · ·ct ::= val | name | refp ::= procedure q(ct d) s

図 1 構文領域v ∈ Valsl ∈ Lvalsx ∈ Varsγ ∈ Envs
σ ∈ StoresΓ ∈ Pmapsξ ∈ Substs=======Z32
N{ a, b, ... }Vars ∪ {next} ∪ Cons * Lvals ∪ Vals
Lvals * Vals
PIds * Procs
Stms → Stms

図 3 構文規則
図 2 意味領域xγ = llσ = v1 γ, σ[l, v1 , undef ] `expr e ⇒ v v2 = [[ ]](v1 , v)γ, σ `stmt x =e ⇒ γ, σ[l, v1 , v2 ]γ, σ `expr e1 6⇒ 0 γ, σ `Γstmt s1 ⇒ γ, σ 0γ, σ 0 `expr e2 6⇒ 0γ, σ `Γstmt if e1 then s1 else s2 fi e2 ⇒ γ, σ 0γ, σ `expr e1 ⇒ 0 γ, σ `Γstmt s2 ⇒ γ, σ 0γ, σ 0 `expr e2 ⇒ 0γ, σ `Γstmt if e1 then s1 else s2 fi e2 ⇒ γ, σ 0

AssVarIfTrue

IfFalseγ, σ `expr e ⇒ v
γ[x 7→ l][next 7→ new (l)], σ[l, undef , v] `Γstmt s ⇒ γ[x 7→ l][next 7→ new (l)], σ 0γ, σ 0 `expr e0 ⇒ v 0γ[next 7→ l], σ `Γstmt local t x = e s delocal t x = e0 ⇒ γ[next 7→ l], σ 0 [l, v 0 , undef ]Γ(q) = procedure q(val y) s γ, σ `expr e ⇒ v γ, σ 0 `expr e ⇒ v
γ[y 7→ l][next 7→ new (l)], σ[l, undef , v] `Γstmt s ⇒ γ[y 7→ l][next 7→ new (l)], σ 0γ[next 7→ l], σ `Γstmt call q(e) ⇒ γ[next 7→ l], σ 0 [l, v, undef ]LocMemCallValΓ(q) = procedure q(ref y) s xγ = l γ[y 7→ l], σ `Γstmt s ⇒ γ[y 7→ l], σ 0
CallRefγ, σ `Γstmt call q(x) ⇒ γ, σ 0
Γ(q) = procedure q(name y) s γ, σ `Γstmt s[e/y] ⇒ γ, σ 0
CallNameγ, σ `Γstmt call q(e) ⇒ γ, σ 0
図 4 操作的意味論

γ, σ 0 `Γstmt call q(e) ⇒ γ, σUncallγ, σ `Γstmt uncall q(e) ⇒ γ, σ 0で表され，環境 γ, 記憶域 σ において，文 s を実行すると，記憶域 σ 0 に更新されることを意味する．なお，判断は文献 [5] のように記述することもできる．ある文 s がγ, σ `stmt s ⇒ γ, σ 0 ∧ γ, σ `stmt s ⇒ γ, σ 00 =⇒ σ 0 = σ 00を満たすとき，その文 s は前方決定性があるといい，γ, σ 0 `stmt s ⇒ γ, σ ∧ γ, σ 00 `stmt s ⇒ γ, σ =⇒ σ 0 = σ 00の評価値と一致していなければならず，不一致の場合は実行時エラーとなる．これが，局所変数ブロックに可逆性をもたせるための条件である．もし，定義から解放の間で局所変数の値が変更されていた場合，逆実行の際の初期値が断定できない．そこで，このような条件を加えている．なお，逆実行の際の初期値は delocal によって与えられ，local によって条件付きで解放が行われる．

4

可逆プログラミング言語における引数渡し

既存の言語では実引数と仮引数を結合するために，様々を満たすとき，その文 s は後方決定性があるという．また，ある文 s に前方決定性と後方決定性があるとき，そ な引数渡しの方法が用いられている．可逆プログラミン
グ言語においては，引数渡し機構によって非可逆とならの文 s は可逆性をもつという．
まず，規則 AssVar で表現される変数代入について記 ないように，制約を加える必要もある．本研究では，一す．一般的な命令型プログラミング言語で用いられてい 般的に用いられている値渡し，参照渡し，名前渡しにつる代入をそのまま可逆プログラミング言語に適用するこ いて Janus で実現した．
値渡しは実引数の評価値を仮引数に渡す引数渡しの方とはできない．なぜなら，代入は情報を上書きする操作であり，代入後の値を知ることができず，非可逆となって 法であり，規則 CallVal によって表現されている．値しまうためである．そこで，Janus では代入操作を加算 渡しの場合，仮引数と実引数で割り当てられる記憶場所
代入 +=, 減算代入 -=, 排他的論理和代入 ^= に限定してい が異なり，プロシージャを抜けたときに仮引数に割り当る．また，代入の左辺の式に出現する変数 x の左辺値と てられた記憶場所が解放される．このため，仮引数の値同じ左辺値に対応付けられている変数は，右辺の式に出 が何であったかが分からなくなり，一般に非可逆となる．
現してはならないという制約を加えている．これは，出 そこで，プロシージャを抜ける際の仮引数 y が実引数 e の力値から入力値を計算できない記述を避けるために設け 評価値 v に対応付けられていない場合，構文エラーとなられている．たとえば，x -= x のような代入文を記述す るようにした．このような記述をする必要はあるが，こることはできない．この代入文に相当する C 言語の代入 の制限によって可逆な値渡しを実現することができた．
参照渡しは実引数の左辺値を仮引数に渡す引数渡しの文 x -= x; では，変数 x の値に依らず，代入文実行後の変数 x の値は 0 となる．計算結果の 0 という値から，変 方法であり，規則 CallRef で表現されている．参照渡
数 x の元々の値は知りえない．したがって，この代入文 しの場合，仮引数が実引数の値を間接参照するため，仮は後方決定性を持たず，可逆であるとはいえない．この 引数の値の変更が実引数の値にも反映されることになる．
名前渡しは実引数の式を仮引数に渡す引数渡しの方法
ような記述をした場合，実行時エラーとなる．
次に，規則 IfTrue と規則 IfFalse で表現される条件 であり，規則 CallName で表現されている．名前渡しで分岐について記す．一般的な命令型プログラミング言語 は，呼び出されたプロシージャ内の仮引数は実引数のテの条件分岐文との違いは，アサーションが加えられてい キストがそのまま置換される．また，プロシージャ呼出る点である．アサーションとは必ず満たすべき条件を意 し文には，呼び出されたプロシージャの仮引数が実引数味し，条件分岐文においては，条件分岐文を抜けるとき に置換されたテキストがそのまま置換される．このために満たすべき条件として用いられている．これによって， 仮引数の値の変更が，そのまま実引数の値の変更となる．
ただし，参照渡しや名前渡しによって引数を渡す場合，逆実行の際にも真と偽のどちらに分岐するのかが一意に定まるため，可逆性をもつことになる．構文としては，if 複数の仮引数に同じ実引数が渡されることを制限する必に続く式 e1 の評価値が真であれば then に続く文 s1 を， 要がある．これは，この行為によってエイリアシングが偽であれば else に続く文 s2 を実行する．なお，Janus 発生し，エイリアシングによって非可逆となる可能性がでは真を非 0, 偽を 0 としている．その後，アサーション あるためである．非可逆となる具体的な例を，図 5 に示である fi に続く式 e2 が評価されることになる．式 e1 を す．なお，ここでは参照渡しで引数が渡されているもの
真で通過していれば式 e2 も真となるとき，式 e1 を偽で とする．プロシージャsub は，引数として 2 つの整数 a通過していれば式 e2 も偽となるときのみ条件分岐文を抜 と b を受け取り，a を左辺値として，b を減算代入するプ
け，これを満たさない場合は実行時エラーとなる．なお， ロシージャである．ここで問題となるのが，sub の呼び
逆実行の際は fi で条件を与えて分岐を行い，if をアサー 出しにおいて，仮引数 a と b の両方に，実引数として同じ x の左辺値を渡している点である．これは，プロシーションとして機能させている．
最後に，規則 LocMem で表現される局所変数ブロック ジャsub の仮引数 a と b が，同じ x の記憶場所を参照しについて記す．一般的な命令型プログラミング言語と違 ていることを意味している．つまり，プロシージャsub 内い，Janus では割り当てられた局所変数について条件付 の演算 a -= b における左辺値 a も，右辺値 b も，x としきで解放を行う．具体的には，local x=e と記述すると， て計算が行われている．これは 3 章で示した代入におけ局所変数 x が定義され，式 e の評価値が初期値として格 る問題と同様に，非可逆となることになる．
納される．その後，delocal x=e0 という記述によって， なお，Janus では uncall によってプロシージャを逆呼
局所変数 x が解放される．このとき，局所変数 x は式 e0 出しすることができる．これについては，どの呼出し方procedure sub(ref a, ref b)
a -= bcall sub(x, x)procedure factorial(val n, val tmp1, ref a)
if n = 1
then a += tmp1
else call factorial(n-1, tmp1*(n-1), a) fi n = 1

図 5 エイリアシングの問題が発生する例
図 7 環境記憶域モデルの Janus で記述したプログラム法に対しても規則 Uncall で実現することができている．
また，これらの引数渡し機構を応用することによって，3 よって，実引数として変数だけでなく，式を渡すことも種類の引数渡し方法の組み合わせ自由な複数引数渡しも 可能となった．また，配列を連続的に扱うことも可能となった．さらに，値渡し，参照渡し，名前渡しをそれぞれ実現可能である．
可逆化し，Janus で実現した．これにより，これらの引数5 可逆性の証明
渡し方法を場合によって使い分けることができるように
我々は，導出木に対する構造帰納法を用いて，環境記 なった．また，これら 3 種類の引数渡し方法の組み合わ憶域モデルを適用した Janus のすべての文が前方後方決 せ自由な複数引数渡し機構を実現することができた．こ定性をもつことを証明し，以下の定理 1 を得た．これに れらの成果として，一般に変数の数を減らすことができるようになった．また，状態モデルの Janus では記述不よって，Janus の可逆性を保証することができた．
可能なJensen’s Device のようなプログラムを記述できる
定理 1 Janus のすべての文が可逆性をもつ．
ようにもなった．以上の結果より，我々の提案によってまた，定理 1 と局所的な逆文の生成によって，逆プロJanus の表現力は向上したといえる．
グラムを常に生成可能であるため，Janus は可逆プログ
また，我々は，環境記憶域モデルの Janus についてのラミング言語であるといえる．
可逆性を保証した．これにより，3 種類の引数渡し方法の可逆化に成功したことが確認できた．また，本稿で提案
6 おわりにする Janus についても，同一のプロシージャにおいて呼現在の Janus と我々の提案する Janus についての比較出しと逆呼出しが可能である．プロシージャ逆呼出しのを具体的なプログラムを用いて行った．整数 n の階乗を規則の前提に，プロシージャ呼出しの判定を用いること求めるプロシージャfactorial を，文献 [1] で提案されては，プログラミング言語全体を注意深く可逆に設計している Janus で記述したものが図 6 である．なお，a は階はじめてできることである．さらに，Janus は汎用的な可乗の計算結果が格納される変数であり，tmp1, tmp2 は計逆プログラミング言語であるため，別の可逆プログラミ算過程を一時的に保存する変数である．また，n の初期値ング言語にも本研究の成果を適用することが可能である．
は 1 以上に限定し，tmp1 の初期値は n が，a の初期値は今後の課題としては，本稿で表現力を向上させた Janus0 が与えられるものとする．このプログラムを，我々の提に対して，一般的な命令型プログラミング言語で用いら案する Janus では図 7 のように記述可能である．変数だれている機構を更に可逆化し，導入することが挙げられ
けでなく，場合に応じて式を実引数に記述できるようにる．たとえば，副作用をもたない標準ライブラリ関数や，なった．この例では，プロシージャ本体の行数が 8 行かスタックなどが考えられる．
ら 4 行になり，変数も 1 つ減らすことができている．

procedure factorial(n, tmp1, a)
local tmp2 = tmp1*(n-1)
if n = 1
then a += tmp1
else n -= 1
call factorial(n, tmp2, a)n += 1fi n = 1
delocal tmp2 = tmp1*(n-1)
参考文献[1] Yokoyama, T., Axelsen, H.B. and Glück, R.: Principles of a Reversible Programming Language, Proc.
Computing frontiers, pp.43–54, ACM (2008).
[2] Yokoyama, T. and Glück, R.: A Reversible Programming Language and its Invertible Self-Interpreter,
Proc. Partial evaluation and semantic-based program
manipulation, pp.144–153, ACM (2007).

[3] Lutz, C.: Janus: a time-reversible language. Letterto R. Landauer (1986).
[4] Dijkstra, E.W.: Letter to the Editor: Defense of ALGOL 60, Communications of the ACM, Vol.4, No.11,
図 6 状態モデルの Janus で記述したプログラム
pp.502–503 (1961).
我々は，Janus に環境記憶域モデルを適用し，引数渡し [5] 田中秀明，新海由侑，横山哲郎：引数渡し機構をもつ機構の拡張を提案した．新たに左辺値を定義したことに可逆プログラミング言語の可逆性（to be published）．