PyRWhile

A Python implementation of the Reversible While language (R-WHILE).

R-WHILE is a minimalist reversible programming language where all data is represented as binary trees. It is r-Turing complete, meaning it can express any reversible computation.

Features

• Interpreter — tree-walking evaluator with reversible store semantics
• Program inversion — automatic generation of inverse programs
• Macro expansion — with support for inverse macros (INV-M)
• Online specializer — partial evaluation with support for partial values
• Program ↔ Data encoding — program-to-data and data-to-program conversion
• Self-interpreter (ri.rwhile) — R-WHILE written in R-WHILE
• Inverse self-interpreter (qi) — qi = inv(ri)
• Futamura projections — all three levels of compilation by specialization
• smn theorem — reversible currying via program transformation
• Step counting — verification of linear-time self-interpretation
• Inverse composition — 4-path input recovery theorem
• Exhaustive bijection verification — injectivity, inverse correctness, equivalence
• Kleene fixed point — self-inverse programs, involution, semantic fixed points

Installation

pip install -e .

Requires Python 3.10+ and Lark.

Usage

# Run a program
pyrwhile examples/reverse.rwhile examples/list123.val

# Generate inverse program
pyrwhile -inverse examples/reverse.rwhile

# Program-to-data encoding
pyrwhile -p2d examples/reverse.rwhile

# Expand macros
pyrwhile -exp examples/minus.rwhile

Language Overview

R-WHILE programs have the structure:

read X;
  <commands>
write Y

Data Types

Type	Syntax	Description
nil	nil	Empty tree
atom	'a, 'hello	Named leaf node
cons	(A . B)	Binary tree node

Commands

Command	Syntax	Description
Reversible assignment	X ^= E	XOR-based update
Reversible replacement	Q <= R	Structural data exchange
Conditional	if E then C else D fi F	Reversible if with entry/exit tests
Loop	from E do C loop D until F	Reversible loop with entry/exit tests
Macro call	M(X, Y, ...)	Invoke macro M

Testing

pip install pytest
python -m pytest tests/ -v

208 tests covering the interpreter, inversion, specialization, Futamura projections, smn theorem, step counting, inverse composition, bijection verification, and Kleene fixed points.

References

1. T. Yokoyama, R. Glück. A Reversible Programming Language and its Invertible Self-Interpreter. Proc. ACM SIGPLAN PEPM, pp. 144–153, 2007. DOI
2. R. Glück, T. Yokoyama. A Minimalist's Reversible While Language. IEICE Trans. Inf. & Syst., E100-D(5), pp. 1026–1034, 2017. DOI
3. R. Glück, T. Yokoyama. A Linear-Time Self-Interpreter of a Reversible Imperative Language. Computer Software, 33(3), pp. 108–121, 2016. DOI

License

MIT