About redextape

Watch the Church–Turing thesis happen.

redextape compiles one small program, written in a little imperative and functional language, into both a lambda-calculus term and a Turing machine, and runs the two side by side. The λ view reduces the term one redex at a time; the Turing-machine view steps the machine across its tapes; an assembly view shows the register-assembly program the machine is lowered from. Every leg steps forwards and backwards, and a position in one can be linked to the same point of the program in the others.

Nothing is simulated for show. The reducer and the machine are real, and each answer is decoded from the model's own final state — so what you watch is the computation itself, not a native run with an animation laid over it. The test suite holds every backend to the others on every commit.

The name

redex — a reducible expression, the atom of lambda-calculus reduction — plus tape, the Turing machine's. Read aloud it is “red tape”.

This build

dev build, from the source at github.com/Davey-Hughes/redextape.

Licence

redextape is free software under the GNU General Public License, version 3 only. The libraries and fonts it ships keep their own licences, listed on the licences page.