Janus (可逆プログラミング言語)
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2024/09/07 09:23 UTC 版)
| パラダイム | 命令型 (手続き型), 可逆 |
|---|---|
| 登場時期 | 1982, 2007 |
| 設計者 | クリストファー・ルッツ、ハワード・ダービイ、横山 哲郎、ロバート・グリュック |
| 主な処理系 | Janus Playground |
| ウェブサイト | tetsuo |
Janusはカリフォルニア工科大学において1982年に学生のプロジェクトで設計及び実装がされた可逆プログラミング言語である[1]。2007年に、横山 哲郎とロバート・グリュックによって、この言語の操作的意味論が形式的に定められており、プログラム逆変換器及び逆変換可能な自己解釈系が実現されている[2][3]。Janusプログラム逆変換器とインタプリタはDIKUのTOPPS研究グループから自由に試すことができる[4]。別のJanus解釈系がPrologで2009年に実装された[5]。RC3研究グループにおいて最適化コンパイラが開発された[6][7]。以下は、2007年の論文に説明がされたものをまとめたものである[2]。
Janusは、構造化命令型プログラミング言語であり、ヒープ割当てなしでグローバルストア上で動作し、動的データ構造をサポートしない。可逆プログラミング言語としてJanusは順方向と逆方向の両方で決定的計算を実行する。2008年に行われたJanusの拡張は、手続きパラメータとローカル変数宣言（ローカル-非ローカル）を特徴とする[3]。さらに、Janusの親戚の言語では、リストなどの動的データ構造をサポートする[8][9]。
構文
バッカス・ナウア記法で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年の論文[2]で定められた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以上であることが求められる [4]。手続き宣言は、キーワード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に対して次のようになる、
- Janus (可逆プログラミング言語)のページへのリンク
