TtT (Terms to Transducers)

A tool for web browsers (http://koko-m.github.io/TtT/) that simulates execution of transducers generated by the Memoryful GoI framework.

This tool is developed using Firefox 39 on Mac OS X; currently it is not tested on other browsers.

What is TtT?

Given a lambda-term with probabilistic choice operators (choose (p) M N), the Memoryful GoI framework generates its translation to a transducer. A transducer, that is here a "probabilistic" Mealy machine, is depicted as a diagram. This tool simulates execution of the resulting transducer by showing how a token moves around the diagram with updating information it carries.

Usage

1. Enter a term, or type ";ex" to select one from 13 examples.
2. Click the start button.

A diagram can be zoomed by scrolling and moved by dragging. Clicking the "centering" button clears zoom and move. Animation can be paused/resumed by either clicking pause/resume button or clicking a diagram.

Modes of Animation

Normal Mode

A token moves on wires. You can adjust its speed by moving the range bar or increasing/decreasing the number.

Skip Mode

A token skips from ports to ports. This mode can be toggled by a button.

Frame-by-Frame Mode

A token moves on wires extremely slowly. This mode can be also toggled by a button.

Accepted Terms

This tool adopts the following Scheme-like grammar. Characters after ';' are ignored.

<var> := {variables}
<nat> := {natural numbers}
<prob> := {real numbers in the unit interval [0,1]}
<expr> ::= <var>  # variables
         | <nat>  # natural numbers
         | *      # the unit value
         | (lambda (<var>) <expr>)     # abstraction
         | (rec (<var> <var>) <expr>)  # recursion
         | (<expr> <expr>)             # application
         | (choose (<prob>) <expr> <expr>)
           # probabilistic choice
           ## the left term executed with probability <prob>
           ## the right term executed with probability 1 - <prob>
         | (car <expr>) | (cdr <expr>) | (cons <expr> <expr>)
           # pairs (product types)
         | (inl <expr>) | (inr <expr>)
         | (match <expr> ((inl <var>) <expr>) ((inr <expr>) <expr>))
           # pattern match (coproduct types)
         | (+ <expr> <expr>)
           # summation (arithmetic primitive)

What You Can See

A transducer, depicted as a diagram, that corresponds the input term.

• Each transducer has input/output ports depicted as blue circles with identification numbers.
• Dashed boxes in a diagram represents countably many copies of their internal transducers.
• Bold boxes with name like choose(0.4) perform probabilistic choices and remember the results by using internal states, or memories. For each copy, if exists, one of the following 3 states are assigned: DEFAULT, LEFT and RIGHT. You can see contents of a memory by putting the cursor in these boxes. For example 0:RIGHT -:DEFAULT shows that only the 0-th copy is in the state RIGHT (i.e. the copy chose the right internal transducer), while the others are in DEFAULT (i.e. in initial states).

A token, depicted as a red circle, moving around and updating its information at ports.

• Information like {0} shown in the left indicates on which copy the token is.
• Information like <42,137> shown in the right indicates the actual data.

Log messages that show how the token moves and how its information changes.

• Lines like enter/exit M indicate the token enters/exits a transducer that corresponds to a term M at the leftmost input/output port (i.e. the left bottom/top blue circle of a white rectangle with name M).
• Lines like enter/exit M at x indicate the token enters/exits a transducer that corresponds to the term M at the input/output port with name x. Here x is a free variable that possibly occurs in M.
• Lines like {0} dd<42,137> at 2(H:1) indicate a token of information {0} and dd<42,137> passes by a port of identification number 2. Expressions like (H:1) represents what kind of computation (i.e. update of the token's information) occurs.
• Lines like ==== PROBABILISTIC CHOICE (0.1) LEFT ==== indicate a probabilistic choice is performed and the left transducer is chosen. Lines like ==== STATE LEFT ==== indicate the current state LEFT is looked up.

For More Information

Developers

• Koko Muroya
• Toshiki Kataoka for the previous LOLA 2014 version

References

• Naohiko Hoshino, Koko Muroya and Ichiro Hasuo. Memoryful Geometry of Interaction: from coalgebraic components to algebraic effects. In CSL-LICS 2014. [acm | preprint pdf]
• Koko Muroya, Toshiki Kataoka, Ichiro Hasuo and Naohiko Hoshino. Compiling effectful terms to transducers: prototype implementation of memoryful Geometry of Interaction (preliminary report). Short abstract presented at LOLA 2014. [pdf]
• Koko Muroya, Naohiko Hoshino and Ichiro Hasuo. Memoryful GoI with recursion (preliminary report). Short abstract presented at LOLA 2015. [pdf]

Special Thanks

Daisuke Sakamoto for his useful advice on visualization.

License

This tool is licensed under the MIT License. It includes Processing.js and PEG.js that are also under the MIT License. See LICENSE for details.