Janus (時間可逆コンピューティング プログラミング言語)

#構文

代入が可逆であるためには、左辺の変数が代入の両辺の式に現れないことが要求される。（配列のセル代入は代入の両側に式を持つことに注意）。

スワップ（<x>"<=>"<x>）は可逆である。

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

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

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

#例

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 を求めることができる。