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

Janus は1982 年にCaltechで書かれた時間可逆プログラミング言語です。^[1]この言語の操作的意味論は、プログラム インバータと可逆自己インタープリタとともに、2007 年に横山哲夫と Robert Glück によって正式に仕様化されました。^{[2] [3] Janus インバータとインタープリタは、} DIKUのTOPPS 研究グループによって無料で提供されています。^[4]別の Janus インタープリタは2009 年にPrologで実装されました。^[5]最適化コンパイラは RC3 研究グループで開発されました。^{[6] [7]}以下は、2007 年の論文で発表された言語の概要です。^[2]

Janus は、ヒープ割り当てなしでグローバル ストア上で動作し、動的データ構造をサポートしない構造化命令型プログラミング言語です。可逆プログラミング言語として、Janus は前方と後方の両方向で決定論的な計算を実行します。Janus の拡張機能には、プロシージャ パラメータとローカル変数宣言 (local-delocal) があります。^[3]さらに、Janus の他のバリアントは、リストなどの動的データ構造をサポートしています。^{[8] [9]}

Janus の構文はBackus-Naur 形式を使用して指定します。

Janus プログラムは、1 つ以上の変数宣言のシーケンスと、それに続く 1 つ以上のプロシージャ宣言のシーケンスで構成されます。

<プログラム>  ::=  < v-decl >  < v-decls >  < p-decl >  < p-decls > 
< v-decls >  ::=  < v-decl >  < v-decls > | ""
 < p-decls >  ::=  < p-decl >  < p-decls > | ""

2007 年の論文^[2]で指定されている Janus では、 0 個以上の変数が許可されますが、空のストアで始まるプログラムは空のストアを生成します。何もしないプログラムは簡単に可逆であり、実際には興味深いものではありません。

変数宣言は、変数または 1 次元配列のいずれかを定義します。

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

変数宣言には型情報が含まれていないことに注意してください。これは、Janus のすべての値 (およびすべての定数) が負でない 32 ビット整数であるため、すべての値は 0 から 2 ³² − 1 = 4294967295 までの範囲にあるためです。ただし、TOPPSによってホストされる Janus インタープリタは、通常の2 の補数の32 ビット整数を使用するため、すべての値は -2 ³¹ = -2147483648 から 2 ³¹ − 1 = 2147483647までの範囲にあることに注意してください。すべての変数は値 0 に初期化されます。

配列のサイズには理論的な制限はないが、上記のインタープリタは少なくとも1のサイズを要求している。^[4]

プロシージャ宣言は、キーワードprocedure、それに続く一意のプロシージャ識別子、およびステートメントで構成されます。

< p-宣言>  ::= "プロシージャ" < id >  < s >

Janus プログラムのエントリ ポイントは、 という名前のプロシージャですmain。そのようなプロシージャが存在しない場合は、プログラム テキスト内の最後のプロシージャがエントリ ポイントになります。

ステートメントは、代入、スワップ、if-then-else、ループ、プロシージャ呼び出し、プロシージャ呼び出し解除、スキップ、またはステートメントのシーケンスのいずれかです。

< s >  := < x >  < mod-op > "=" < e > | < x > "[" < e > "]" < mod-op > "=" < e > 
     | < x > " < = > " < x > 
     | "if" < e > "then" < s > "else" < s > "fi" < e > 
     | "from" < e > "do" < s > "loop" < s > "until" < e > 
     | "call" < id > | "uncall" < id >
     | 「スキップ」
     | < s >  < s >

代入を可逆的にするには、左側の変数が代入のどちらの側の式にも現れないことが要求されます。(配列セル代入では、代入の両側に式があることに注意してください。)

スワップ ( <x> "<=>" <x>) は簡単に元に戻すことができます。

条件文を可逆的にするために、テスト( <e>after "if") とアサーション( <e>after )の両方を提供します"fi"。セマンティクスは、then ブランチの実行前にテストが成立し、then ブランチの実行後にアサーションが成立する必要があるというものです。逆に、 else ブランチの実行前にテストが成立してはならず、else ブランチの実行後にアサーションが成立してはなりません。反転したプログラムでは、アサーションがテストになり、テストがアサーションになります。(Janus のすべての値は整数であるため、0 が偽を示すという通常の C セマンティクスが採用されています。)

ループを可逆的にするために、同様にアサーション ( <e>after "from") とテスト ( <e>after "until") を提供します。セマンティクスは、アサーションはループに入るときにのみ保持され、テストはループから出るときにのみ保持される必要があるというものです。反転されたプログラムでは、アサーションがテストになり、テストがアサーションになります。追加の<e>after により、"loop"テストが false と評価された後に作業を実行できます。作業により、アサーションがその後 false になることが保証されます。

プロシージャ呼び出しは、プロシージャのステートメントを順方向に実行します。プロシージャの呼び出し解除は、プロシージャのステートメントを逆方向に実行します。プロシージャにはパラメーターがないため、すべての変数の受け渡しはグローバル ストアの副作用によって行われます。

式は、定数 (整数)、変数、インデックス付き変数、または二項演算の適用です。

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

Janus (およびTOPPSがホストする Janus インタープリター) の定数については、すでに上で説明しました。

二項演算子は次のいずれかであり、C の対応する演算子と同様の意味を持ちます。

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

修正演算子は、すべての v に対して、全単射関数であり、したがって可逆であるような二項演算子のサブセットです。ここで、 は修正演算子です。 ${\displaystyle \lambda v'.\oplus \left(v',v\right)}$${\displaystyle \oplus}$

< mod-op >  ::= "+" | "-" | 「＾」

逆関数はそれぞれ、、、"-"です。 "+""^"

代入先の変数が代入のどちらの側の式にも現れないという制約により、Janus の推論システムが前方および後方決定論的であることを証明できます。

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

n>2、i=n、x1=1、x2=1 の場合、 n番目のフィボナッチ数fibを見つけるためのヤヌス手順を記述します。

手順の嘘
    i = n より
    する
        x1 += x2
        x1 <=> x2
        私 -= 1
    i = 2 になるまで

終了時には、x1は ( n −1) 番目のフィボナッチ数であり、x2は n^番目のフィボナッチ数です。iはnから2 までの反復変数です。iは反復ごとに減分されるため、仮定 ( i = n) は最初の反復の前でのみ真になります。テスト is ( i = 2) は、ループの最後の反復の後でのみ真になります ( n > 2 と仮定)。

手順の前提として次のことを想定すると、 の 4 番目のフィボナッチ数が得られますx2。

x1 x2で
手順メイン
    4 + = 4 です
    私 += n
    x1 += 1
    x2 += 1
    嘘をつく

注意: n≤2、特に負の整数を処理できるようにするには、メインでもう少し作業を行う必要があります。

の逆はfib次のようになります。

手順の嘘
    i = 2 から
    する
        私 += 1
        x1 <=> x2
        x1 -= x2
    ループ
    i = n になるまで

ご覧のとおり、Janus プログラムはローカル反転によって変換できます。ローカル反転では、ループ テストとアサーションが入れ替わり、ステートメントの順序が逆になり、ループ内のすべてのステートメント自体が逆になります。逆プログラムを使用すると、x1が (n-1)^番目で​​ x2 がn^番目のフィボナッチ数である場合にn を見つけることができます。