Janus (可逆プログラミング言語)

Janus

パラダイム	命令型 (手続き型), 可逆
登場時期	1982, 2007
設計者	クリストファー・ルッツ、ハワード・ダービイ、横山 哲郎、ロバート・グリュック
主な処理系	Janus Playground
ウェブサイト	tetsuo.jp/ref/janus.html

Janusはカリフォルニア工科大学において1982年に学生のプロジェクトで設計及び実装がされた可逆プログラミング言語である。2007年に、横山 哲郎とロバート・グリュックによって、この言語の操作的意味論が形式的に定められており、プログラム逆変換器及び逆変換可能な自己解釈系が実現されている。Janusプログラム逆変換器とインタプリタはDIKUのTOPPS研究グループから自由に試すことができる。別のJanus解釈系がPrologで2009年に実装された。RC3研究グループにおいて最適化コンパイラが開発された。以下は、2007年の論文に説明がされたものをまとめたものである。

Janusは、構造化命令型プログラミング言語であり、ヒープ割当てなしでグローバルストア上で動作し、動的データ構造をサポートしない。可逆プログラミング言語としてJanusは順方向と逆方向の両方で決定的計算を実行する。2008年に行われたJanusの拡張は、手続きパラメータとローカル変数宣言（ローカル-非ローカル）を特徴とする。さらに、Janusの親戚の言語では、リストなどの動的データ構造をサポートする。

構文

バッカス・ナウア記法でJanusの構文を定める。Janusプログラムは、1つ以上の変数宣言の並びと、それに続く1つ以上の手続き宣言の並びである：

<program> ::= <v-decl> <v-decls> <p-decl><p-decls>
 <v-decls> ::= <v-decl> <v-decls> | ""
 <p-decls> ::= <p-decl> <p-decls> | ""

ここで，2007年の論文で定められたJanusは0個以上の変数を許すが、空のストアから始まるプログラムは空のストアを生成する。何もしないプログラムは明らかに逆変換可能であり、応用上興味深いところは見当たらない。変数宣言は、変数か1次元配列を定義する：

<v-decl> ::= <v> | <v> "[" <c> "]"

変数宣言は型情報を持たないことに注意せよ。これは、Janusではすべての値（およびすべての定数）が非負の32ビット整数であるためで、すべての値は0から232 - 1 = 4294967295の間になる。しかし、TOPPSにあるJanusインタプリタは、2の補数32ビット整数を使用するため、すべての値は-231 = -2147483648 から 231 - 1 = 2147483647 の間になることに注意せよ。すべての変数は0に初期化される。配列のサイズに理論的な制限はないが、TOPPSにあるJanusインタプリタでは配列のサイズは1以上であることが求められる 。手続き宣言は、キーワードprocedureと、それに続く一意な手続き識別子と文から構成される：

<p-decl> ::= "procedure" <id> <s>

プログラムのエントリーポイントはmainという名前の手続きである。そのような手続きが存在しない場合は、プログラムテキストの最後の手続きがエントリポイントになる。文とは、代入、スワップ、if-then-else、ループ、手続き呼出し、手続き逆呼出し、スキップ、または文の並びのことである：

<s> := <x> <mod-op> "=" <e> | <x> "[" <e> "]" <mod-op> "=" <e>｜ <x> "[" <e> "]
     | <x> "<=>" <x>
     | "if" <e> "then" <s> "else" <s> "fi" <e>
     | "from" <e> "do" <s> "loop" <s> "until" <e>
     | "call" <id> | "uncall" <id
     | "skip"
     <s> <s>

代入が可逆であるためには、左辺の変数が代入の両辺の式に現れないことが要求される。(配列のセル代入は代入の両側に式を持つことに注意)。 スワップ(<x> "<=>" <x>)は可逆である。

条件式が可逆であるためには、テスト（"if"のあとの<e>）とアサーション（"fi"のあとの<e>）の両方を用意する。意味論としては、then節の実行前にテストが成立しなければならず、その後にアサーションが成立しなければならない。逆に、else節の実行前にはテストが成立してはならず、else節の実行後にはアサーションが成立してはならない。逆プログラムでは、アサーションがテストになり、テストがアサーションになる。(Janusの値はすべて整数なので、0は偽を表すという通常のC言語的な意味論が適用される)。

ループを可逆にするために、同様にアサーション("from"の後の<e>)とテスト("until"の後の<e>)を用意する。このセマンティクスは、アサーションはループに入るときだけ、テストはループから出るときだけ成立しなければならないというものである。逆プログラムでは、アサーションがテストになり、テストがアサーションになる。"loop"の後に<e>を追加することで、テストが偽と評価された後に処理を実行することができる。 この処理では、アサーションがその後に偽でありつづけることを保証するものでなければならない。手続きの呼出しは、手続きの文を順方向に実行する。手続きの逆呼出しは、手続きの文を逆方向に実行する。手続きにはパラメータがないので、変数の受け渡しはすべてグローバル・ストア上の副作用によって行われる。

式は、定数（整数）、変数、インデックス付き変数、バイナリ演算のアプリケーションである：

<e> ::= <c> | <x> | <x> "[" <e> "]" | <e> <bin-op> <e>

Janus（および TOPPSがホストするJanus インタプリタ）の定数については、すでに前述した。

二項演算子は以下のいずれかで、C言語と同様のセマンティクスを持つ：

<bin-op> ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="

修正演算子は二項演算子のサブセットであり、すべてのvに対して次のようになる、$\lambda v'.\oplus \left(v',v\right)$が双射、したがって逆が得られるものである。 ここで、$\oplus$は修正演算子である：

<mod-op> ::= "+" | "-" | "^"

逆関数はそれぞれ"-"、"+"、"^"である。 代入された変数が代入の両側の式に現れないという制約により、Janusの推論システムが前方決定論的および後方決定論的であることを証明することができる。

意味論

Janus言語は1982年にカリフォルニア工科大学で考案された。その後の研究で、自然意味論と表記的意味論の形で言語意味論が形式化された。純粋に可逆的なプログラミング言語の意味論も、メタレベルで可逆的に扱うことができる。

例

n>2、i=n、x1=1、x2=1 について、n番目のフィボナッチ数を求めるJanus プロシージャ fib を書く。

procedure fib
	from i = n
	do
	x1 += x2
	x1 <=> x2
	i -= 1
	until i = 2

このプロシージャの実行が完了した時、x1 は(n-1)番目のフィボナッチ数となり、x2はn番目のフィボナッチ数となる。i はn から2 までのイテレータ変数である。i はすべての繰り返しの中で１ずつ減少するので、仮定(i = n）が真となるのは最初の繰り返しの前だけである。(i=2)が真になるのは、ループの最後の繰り返しの後だけである（n>2 と仮定する）。次に示すプロシージャ呼び出しの前の初期化を仮定すると、x2 に4 番目のフィボナッチ数が得られる。

i n x1 x2
procedure main
	n += 4
	i += n
	x1 += 1
	x2 += 1
	call fib

なお、n≦2、特に負の整数を扱えるようにするには、mainプロシージャに工夫が必要である。fib の逆プロシージャは以下のようになる。

procedure fib
	from i = 2
	do
	i += 1
	x1 <=> x2
	x1 -= x2
	loop
	until i = n

このように、Janusプログラムは、ループのテストとアサーションが入れ替わり、文の順序が逆転し、ループ内のすべての文が逆になる局所的な逆変換によって変形することができる。x1 を(n-1)番目、x2 をn番目のフィボナッチ数とするとき、逆プログラムを用いてn を求めることができる。