Janus (可逆プログラミング言語)のソースを表示

{{Infobox programming language
| name                   = Janus
| logo                   = 
| year                   = 1982, 2007
| designer               = クリストファー・ルッツ、ハワード・ダービイ、横山 哲郎、ロバート・グリュック
| developer              =
| paradigm               = [[命令型プログラミング|命令型]] ([[手続き型プログラミング|手続き型]]), [[可逆計算|可逆]] 
| latest release version =
| latest release date    = 
| latest test version    =
| latest test date       =
| implementations        = [http://topps.diku.dk/pirc/?id=janusP Janus Playground]
| typing                 = 
| influenced_by          = 
| dialects   = 
| platform   = 
| license    = 
| website    = {{URL|http://tetsuo.jp/ref/janus.html}}
| file_ext   = 
}}

'''Janus'''は[[カリフォルニア工科大学]]において1982年に学生のプロジェクトで設計及び実装がされた[[可逆計算|可逆]]プログラミング言語である<ref>{{Cite web | author=Christopher Lutz | title=Janus: a time-reversible language | year=1986 | url=http://tetsuo.jp/ref/janus.html|accessdate=2024-07-22}}</ref>。2007年に、横山 哲郎とロバート・グリュックによって、この言語の[[操作的意味論]]が形式的に定められており、[[プログラム逆変換器]]及び逆変換可能な[[w:en:self-interpreter|自己解釈系]]が実現されている<ref name="diku">{{Cite journal| author1=Tetsuo Yokoyama | author2=Robert Glück | year=2007 | title=A reversible programming language and its invertible self-interpreter | journal=Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation | publisher=ACM | location=New York, NY, USA| pages=144-153 | doi=10.1145/1244381.1244404}}</ref><ref name="janus2">{{cite book |last1=Yokoyama |first1=Tetsuo |last2=Axelsen |first2=Holger Bock |last3=Glück |first3=Robert |title=Proceedings of the 5th conference on Computing frontiers |chapter=Principles of a reversible programming language |date=5 May 2008 |pages=43–54 |doi=10.1145/1366230.1366239|isbn=978-1-60558-077-7 |s2cid=14228334 }}</ref>。Janusプログラム逆変換器と[[インタプリタ]]は[[w:en:DIKU|DIKU]]の[[w:en:TOPPS (research group)|TOPPS研究グループ]]から自由に試すことができる<ref name="interpreter">{{Cite web|url=http://topps.diku.dk/pirc/janus-playground/|title = Janus Extended Playground|accessdate=2024-07-22}}</ref>。別のJanus解釈系が[[Prolog]]で2009年に実装された<ref>{{Cite web|url=http://www.complang.tuwien.ac.at/adrian/revcomp|title=A reversible interpreter|accessdate=2024-07-22}}</ref>。RC3研究グループにおいて最適化コンパイラが開発された<ref>{{Cite web|url=https://git.thm.de/thm-rc3/release|title=RC3: Reversible Computing Compiler Collection|accessdate=2024-07-22}}</ref><ref>{{cite journal |last1=Deworetzki |first1=Niklas |last2=Kutrib |first2=Martin |last3=Meyer |first3=Uwe |last4=Ritzke |first4=Pia-Doreen |title=Optimizing Reversible Programs |journal=Reversible Computation |date=2022 |volume=13354 |pages=224–238 |doi=10.1007/978-3-031-09005-9_16}}</ref>。以下は、2007年の論文に説明がされたものをまとめたものである<ref name="diku" />。

Janusは、[[構造化プログラミング|構造化]][[命令型プログラミング|命令型]]プログラミング言語であり、ヒープ割当てなしでグローバルストア上で動作し、動的データ構造をサポートしない。可逆プログラミング言語としてJanusは順方向と逆方向の両方で決定的計算を実行する。2008年に行われたJanusの拡張は、手続きパラメータとローカル変数宣言（ローカル-非ローカル）を特徴とする<ref name="janus2" />。さらに、Janusの親戚の言語では、リストなどの動的データ構造をサポートする<ref>{{cite journal |last1=Glück |first1=Robert |last2=Yokoyama |first2=Tetsuo |title=A Linear-Time Self-Interpreter of a Reversible Imperative Language |journal=Computer Software |volume=33 |issue=3 |pages=3_108-3_128 |doi=10.11309/jssst.33.3_108 |url=https://doi.org/10.11309/jssst.33.3_108}}</ref><ref>{{cite journal |last1=Glück |first1=Robert |last2=Yokoyama |first2=Tetsuo |title=Reversible computing from a programming language perspective |journal=Theoretical Computer Science |date=2023 |volume=953 |pages=113429 |doi=10.1016/j.tcs.2022.06.010 |doi-access=free }}</ref>。

==構文==
[[バッカス・ナウア記法]]でJanusの構文を定める。Janusプログラムは、1つ以上の変数宣言の並びと、それに続く1つ以上の手続き宣言の並びである：
<syntaxhighlight lang=bnf>
<program> ::= <v-decl> <v-decls> <p-decl><p-decls>
 <v-decls> ::= <v-decl> <v-decls> | ""
 <p-decls> ::= <p-decl> <p-decls> | ""
</syntaxhighlight>
ここで，2007年の論文<ref name="diku"/>で定められたJanusは0個以上の変数を許すが、空のストアから始まるプログラムは空のストアを生成する。何もしないプログラムは明らかに逆変換可能であり、応用上興味深いところは見当たらない。変数宣言は、変数か1次元配列を定義する：
<syntaxhighlight lang=bnf>
<v-decl> ::= <v> | <v> "[" <c> "]"
</syntaxhighlight>
変数宣言は型情報を持たないことに注意せよ。これは、Janusではすべての値（およびすべての定数）が非負の32ビット整数であるためで、すべての値は0から232 - 1 = 4294967295の間になる。しかし、TOPPSにあるJanusインタプリタは、2の補数32ビット整数を使用するため、すべての値は-231 = -2147483648 から 231 - 1 = 2147483647 の間になることに注意せよ。すべての変数は0に初期化される。配列のサイズに理論的な制限はないが、TOPPSにあるJanusインタプリタでは配列のサイズは1以上であることが求められる <ref name="interpreter"/>。手続き宣言は、キーワードprocedureと、それに続く一意な手続き識別子と文から構成される：
<syntaxhighlight lang=bnf>
<p-decl> ::= "procedure" <id> <s>
</syntaxhighlight>
プログラムのエントリーポイントはmainという名前の手続きである。そのような手続きが存在しない場合は、プログラムテキストの最後の手続きがエントリポイントになる。文とは、代入、スワップ、if-then-else、ループ、手続き呼出し、手続き逆呼出し、スキップ、または文の並びのことである：
<syntaxhighlight lang=bnf>
<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>
</syntaxhighlight>

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

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

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

式は、定数（整数）、変数、インデックス付き変数、バイナリ演算のアプリケーションである：
<syntaxhighlight lang=bnf>
<e> ::= <c> | <x> | <x> "[" <e> "]" | <e> <bin-op> <e>
</syntaxhighlight>
Janus（および [[TOPPS (research group)|TOPPS]]がホストするJanus インタプリタ）の定数については、すでに前述した。

二項演算子は以下のいずれかで、[[C言語]]と同様のセマンティクスを持つ：
<syntaxhighlight lang=bnf>
<bin-op> ::= "+" | "-" | "^" | "*" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="
</syntaxhighlight>

修正演算子は二項演算子のサブセットであり、すべてのvに対して次のようになる、<math>\lambda v'.\oplus\left(v',v\right)</math>が双射、したがって逆が得られるものである。 ここで、<math>\oplus</math>は修正演算子である：
<syntaxhighlight lang=bnf>
<mod-op> ::= "+" | "-" | "^"
</syntaxhighlight>
逆関数はそれぞれ<code>"-"</code>、<code>"+"</code>、<code>"^"</code>である。
代入された変数が代入の両側の式に現れないという制約により、Janusの推論システムが前方決定論的および後方決定論的であることを証明することができる。

==意味論==
Janus言語は1982年に[[カリフォルニア工科大学]]で考案された。その後の研究で、自然意味論と表記的意味論の形で言語意味論が形式化された<ref>{{cite journal |last1=Paolini |first1=Luca |last2=Piccolo |first2=Mauro |last3=Roversi |first3=Luca |title=A Certified Study of a Reversible Programming Language |date=2018 |pages=7:1-7:21 |doi=10.4230/LIPIcs.TYPES.2015.7|journal=Proc. 21st International Conference on Types for Proofs and Programs (TYPES 2015).
}} </ref>。純粋に可逆的なプログラミング言語の意味論も、メタレベルで可逆的に扱うことができる。

==例==
n>2、i=n、x1=1、x2=1 について、n番目の[[フィボナッチ数]]を求めるJanus プロシージャ <code>fib</code> を書く。
<pre>
procedure fib
	from i = n
	do
	x1 += x2
	x1 <=> x2
	i -= 1
	until i = 2
</pre>
このプロシージャの実行が完了した時、<code>x1</code> は(n-1)番目のフィボナッチ数となり、<code>x2</code>はn番目のフィボナッチ数となる。<var>i</var> は{{Var|n}} から2 までのイテレータ変数である。<var>i</var> はすべての繰り返しの中で１ずつ減少するので、仮定(<code>i = n</code>）が真となるのは最初の繰り返しの前だけである。(<code>i=2</code>)が真になるのは、ループの最後の繰り返しの後だけである（{{Var|n}}>2 と仮定する）。次に示すプロシージャ呼び出しの前の初期化を仮定すると、<code>x2</code> に4 番目のフィボナッチ数が得られる。
<pre>
i n x1 x2
procedure main
	n += 4
	i += n
	x1 += 1
	x2 += 1
	call fib
</pre>
なお、n≦2、特に負の整数を扱えるようにするには、mainプロシージャに工夫が必要である。fib の逆プロシージャは以下のようになる。
<pre>
procedure fib
	from i = 2
	do
	i += 1
	x1 <=> x2
	x1 -= x2
	loop
	until i = n
</pre>
このように、Janusプログラムは、ループのテストとアサーションが入れ替わり、文の順序が逆転し、ループ内のすべての文が逆になる局所的な逆変換によって変形することができる。{{Var|x1}} を(n-1)番目、{{Var|x2}} をn番目のフィボナッチ数とするとき、逆プログラムを用いて{{Var|n}} を求めることができる。

==References==
{{Reflist}}

[[Category:プログラミング言語]]
[[Category:可逆計算]]