Janus (programming language)
|This article needs additional citations for verification. (July 2013)|
The name Janus refers to at least two computer programming languages or partial descriptions of possible computer programming languages:
Concurrent Constraint Programming
|Paradigm(s)||concurrent constraint logic|
|Designed by||Ken Kahn and Vijay A. Saraswat|
|Major implementations||(none available)|
Janus is a computer programming language partially described by K. Kahn and Vijay A. Saraswat in "Actors as a special case of concurrent constraint (logic) programming", in SIGPLAN Notices, October 1990. Janus is a concurrent constraint language without backtracking.
Janus models concurrency through the use of bag channels. Code that needs to send a message to a process does so by constraining a bag to be the union of another bag and the singleton bag of the message. The other bag is then available to be constrained for sending subsequent messages.
The process receives the message by matching the bag to a pattern that says it is the union of some singleton and some other bag. The logic of the bag channels produces a property shared by the actor model, namely that the order of arrival of the messages is not guaranteed. However, unlike actors in the actor model, processes in Janus can pass around their "mailboxes" so to speak, in the form of bags, and can hold more than one. This ability to pass mailboxes around and hold more than one is inherited in computer programming language ToonTalk, which is influenced by Janus.
Janus, the programming language, is named after Janus, the two-faced Roman god, because every logical variable in Janus has as its two "faces", two aspects that can be passed as arguments. These are called the asker and the teller. These represent, respectively, the right to ask the value of the variable (or some characteristic of the value) and the right to tell the value (or to tell some constraint on what the value can be). The asker and teller aspects can be passed around as arguments independently of each other. Neither right implies the other right. The syntax of the language prevents copying a teller or exercising it more than once. Logical contradiction is statically prevented, according to Kahn and Saraswat.
|Designed by||Christopher Lutz, Howard Derby, Tetsuo Yokoyama, and Robert Glück|
|Appeared in||1982, 2007|
Janus is also the name of a time-reversible programming language written at Caltech in 1982. The operational semantics of the language were formally specified, together with a program inverter and an invertible self-interpreter, in 2007 by Tetsuo Yokoyama and Robert Glück. A Janus inverter and interpreter is made freely available by the TOPPS research group at DIKU. The below summarises the language presented in the 2007 paper.
Janus is an imperative programming language with a global store (there is no stack or heap allocation). Janus is a reversible programming language, i.e. it supports deterministic forward and backward computation by local inversion.
We specify the syntax of Janus using Backus-Naur Form.
A Janus program is a sequence of one or more variable declarations, followed by a sequence of one or more procedure declarations:
<program> ::= <v-decl> <v-decls> <p-decl> <p-decls> <v-decls> ::= <v-decl> <v-decls> | "" <p-decls> ::= <p-decl> <p-decls> | ""
Note, Janus as specified in the 2007 paper, allows zero or more variables, but a program that starts with an empty store, produces an empty store. A program that does nothing is trivially invertible, and not interesting in practice.
A variable declaration defines either a variable or a one-dimensional array:
<v-decl> ::= <v> | <v> "[" <c> "]"
Note, variable declarations carry no type information. This is because all values (and all constants) in Janus are non-negative 32-bit integers, so all values are between 0 and 232-1=4294967295. Note however, that the Janus interpreter hosted by TOPPS uses regular two's complement 32-bit integers, so all values there are between -231=-2147483648 and 231-1=2147483647. All variables are initialized to the value 0.
There are no theoretical bounds to the sizes of arrays, but the said interpreter demands a size of at least 1, and at most 4000.
A procedure declaration consists of the keyword
procedure, followed by a unique procedure identifier and a statement:
<p-decl> ::= "procedure" <id> <s>
The entry point of a Janus program is a procedure named main. If no such procedure exists, the last procedure in the program text is the entry point.
A statement is either an assignment, a swap, an if-then-else, a loop, a procedure call, a procedure uncall, a skip, or a sequence of statements:
<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> | "skip" | <s> <s>
For assignments to be reversible, it is demanded that the variable on the left-hand side does not appear in the expressions on either side of the assignment. (Note, array cell assignment has an expression on both sides of the assignment.)
A swap is trivially reversible.
For conditionals to be reversible, we provide both a test (the
"if") and an assertion (the
"fi"). The semantics is that the test must hold before the execution of the then-branch, and the assertion must hold after it. Conversely, the test must not hold before the execution of the else-branch, and the assertion must not hold after it. In the inverted program, the assertion becomes the test, and the test becomes the assertion. (Note, Since all values in Janus are integers, the usual C-semantics that 0 indicates false are employed.)
For loops to be reversible, we similarly provide an assertion (the
"from") and a test (the
"until"). The semantics is that the assertion must hold only on entry to the loop, and the test must hold only on exit from the loop. In the inverted program, the assertion becomes the test, and the test becomes the assertion. An additional
"loop" allows to perform work after the test is evaluated to false. The work should ensure that the assertion is false subsequently.
A procedure call executes the statements of a procedure in a forward direction. A procedure uncall executes the statements of a procedure in the backward direction. There are no parameters to procedures, so all variable passing is done by side-effects on the global store.
An expression is a constant (integer), a variable, an indexed variable, or an application of a binary operation:
<e> ::= <c> | <x> | <x> "[" <e> "]" | <e> <bin-op> <e>
The constants in Janus (and the Janus interpreter hosted by TOPPS) have already been discussed above.
A binary operator is one of the following, having semantics similar to their C counterparts:
<bin-op> ::= "+" | "-" | "^" | "+" | "-" | "/" | "%" | "&" | "|" | "&&" | "||" | ">" | "<" | "=" | "!=" | "<=" | ">="
The modification operators are a subset of the binary operators such that for all v, is a bijective function, and hence invertible, where is a modification operator:
<mod-op> ::= "+" | "-" | "^"
The inverse functions are
The restriction that the variable assigned to does not appear in an expression on either side of the assignment allows us to prove that the inference system of Janus is forward and backward deterministic.
We write a Janus procedure fib to find the nth Fibonacci number, for n>2, i=n, x1=1, and x2=1:
procedure fib from i = n do x1 += x2 x1 <=> x2 i -= 1 until i = 2
Upon termination, x1 is the (n-1)th Fibonacci number and x2 is the nth Fibonacci number. i is an iterator variable that goes from n to 2. As i is decremented in every iteration, the assumption (
i = n) is only true prior to the first iteration. The test is (
i = 2) is only true after the last iteration of the loop (assuming i > 2).
Assuming the following prelude to the procedure, we end up with the 4th Fibonacci number in x2:
i n x1 x2 procedure main n += 4 i += n x1 += 1 x2 += 1 call fib
Note, our main would have to do a bit more work if we were to make it handle n≤2, especially negative integers.
The inverse of fib is:
procedure fib from i = 2 do i += 1 x1 <=> x2 x1 -= x2 loop until i = n
As you can see, Janus performs local inversion, where the loop test and assertion are swapped, the order of statements is reversed, and every statement in the loop is itself reversed. The reverse program can be used to find n when x1 is the (n-1)th and x2 is the nth Fibonacci number.
- Christopher Lutz. Janus: a time-reversible language. 1986. Letter to R. Landauer. http://tetsuo.jp/ref/janus.html.
- Tetsuo Yokoyama and Robert Glück. 2007. A reversible programming language and its invertible self-interpreter. In Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation (PEPM '07). ACM, New York, NY, USA, 144-153. http://doi.acm.org/10.1145/1244381.1244404