Lambda the Ultimate

Reversible computations are interesting, but many plain functions don't have a unique reversable inverse. Of the top of my hat, abs, square, and (bitwise) or have at least two or many inverses and will be problematic to handle. In short, this programming language can't handle many simple arithmetic calculations. Dead on arrival.

So the reverse is non-determinisitic? Going in reverse could result in the set of possible precursory states.

Say 9=square(x), what is/was the value of x? 3 or -3? Worse, say 7=x|y, what are/were the values of x and y? The state space of reverse possible answers easily explodes on even simple programs.

No doubt most people and the authors are aware of it, but I imagine most reversible programs are not that interesting.

It may be a nice toy language to explore a very restricted subset of programs, but I gather that's about it.

Is that even the main problem? The challenge is inverting effects, not pure functions. So "y = square(x)", x is still hanging around after y is computed...it is not forgotten. But see my other comment for how we could try and deal with this if we wanted to use functions to forget values by inverting them.

I imagine most reversible programs are not that interesting.

It may be a nice toy language to explore a very restricted subset of programs, but I gather that's about it.

Reversible computation becomes a lot more practical if we make a distinction between information which is required by our algorithm and information which is required for reversibility. Here's an example of addition which returns a pair of its algorithmic result and its reversibility information:

plus 0 n = (n, 0)
plus (S n) m = let (rec, rev) = plus n m in
                   (S rec, S rev)

Notice that the reversibility information we create is always the same as the argument information we destroy.

Also notice that this is basically a form of state monad; we can implement it something like this:

instance Monad (Reversible a) where
  return x = (x, [])
  (x, r) >>= f = let (result, rev) = f x in (result, rev ++ r)

In the same way that the state monad lets us write imperative-looking code which is actually pure, this lets us write irreversible-looking programs which are actually reversible.

I've previously mentioned a generic (but inefficient) way to make any function reversible.

But in this case, you've just reinvented instruction tracing. The idea about a "reversible language" is that no state is transparently allocated to enable reversibility. Reversibility can be implemented for any language as long as you allow for tracing or checkpointing.

Instruction tracing records the initial state and the sequence of operations that mutates it. This approach looks like it stores the difference in information content between points. Tracing can only simulate reversibility (i.e. there is at least an extra linear cost to replay the portion of the program before the the step in time), where-as this approach would allow the single step to be executed backwards ignoring the rest of the (earlier) steps.

The idea about a "reversible language" is that no state is transparently allocated to enable reversibility.

That seems to be a strange definition as it limits the language to totally information preserving problems. Surely a more general use of the term would require some sort of hidden state? For example proposed quantum algorithms use junk state in their qubits to avoid the destruction of information.

That seems to be a strange definition as it limits the language to totally information preserving problems. Surely a more general use of the term would require some sort of hidden state? For example proposed quantum algorithms use junk state in their qubits to avoid the destruction of information.

That's my thinking. A reversible language sounds like all of our algorithms must be inherently reversible, but as programmers we can always work around the language and follow a convention that some information is 'junk'. That way we can write irreversible algorithms in a reversible language by scattering around some junk-handling boilerplate. The language doesn't need to distinguish between 'real' and 'junk', it's up to us to be disciplined. Then we can normalise our interfaces, eg. using (real, junk) pairs, and hide the boilerplate using monads or macros.

That's the situation I described above, which can be done in a completely reversible language with no language support other than higher-order functions or macros. The point about turning irreversible functions into reversible ones was meant as an existence proof that we can use junk information to make any function reversible, not a pragmatic approach to implementation ;)

Let's put it this way: how much about a procedure can you forget after the call so that it can be "uncalled"? The more junk you keep around after the call, the more burdened the procedure caller with forgetting or propagating the junk. Its a fascinating problem, and from what I can tell in this post, it might be proven to be unsolvable in general (junk just accumulates necessarily for most interesting procedures).

Janus avoids the issue by not having any encapsulated variables (all variables are arguments or globals).

Let's put it this way: how much about a procedure can you forget after the call so that it can be "uncalled"? The more junk you keep around after the call, the more burdened the procedure caller with forgetting or propagating the junk. Its a fascinating problem, and from what I can tell in this post, it might be proven to be unsolvable in general (junk just accumulates necessarily for most interesting procedures).

The Physicist in me says we run everything forwards to produce a result, we copy it, then we run everything backwards. This lets us perform arbitrarily complex computations for no more energy than the cost of copying the result (which could be as small as one bit), and gives a natural way to consume the junk.

The Computer Scientist in me says that we can treat junk in a similar way to types: use it as input to a theorem prover which checks properties of the code. We can then erase the junk at compile time and get a regular program. As you say, tracking junk is probably undecidable, which means there's a never-ending wealth of information to mine.

A random thought which also springs to mind is the potential connection between reversible computing (minimal energy requirements), computational complexity (maximum time required) and the energy/time uncertainty principle. That might be something for me to think about this weekend :)

I'm not big on energy conversation (its not just a good idea, its the law), but I wonder if we can learn about the complexity of our procedures by how much junk must be preserved to preserve reversibility? Perhaps in the future we will train new programmers to minimize the junk produced by their procedures so that they are easier to debug.

Measuring information destruction in procedures is actually a really interesting idea, and not too far from the code I'm writing at the moment. Give me a few months :) and I'll come back with some results.

This I find a solution which falls in the category: Let's raise the bar so high that we can only cross it by walking underneath it.

Of course you can expand, and make reversible, any function by expanding it with argument 'tracing'. But then you changed the function, I agree with Sean that that is better handled by the language, and I would like to point out that the class of functions which are reversible without change is rather small. The latter fact indicates to me that you better have some substantial gain somewhere else before people will flock to writing reversible algorithms.

I still think that the language is interesting to research what happens when you program with reversible functions, but it looks like (even from your examples) that that is the sole interesting feature of it. Noone will write production code in it until there is some advantage to writing reversible functions, and at the moment there isn't.

Reversible functions are related to data provenance. For example, in the field of scientific research, it is important for results to be reproducible. For that, you need to be able to trace big datasets and transformations on them in much detail, or even better - to be able to reverse computations, if possible.
Next to that, scientific software must also be of high - production quality - standard. So I argue that there is an advantage in writing reversible functions, and that similar concepts are already being used in production settings (think colliders).

Data provenance is a well-defined term on which you don't elaborate, scientific software is so broad and vague you leave me clueless, I have no idea how collider software looks like, it certainly is a small niche in the ocean of scientific software written, but you could elaborate on that.

You skip between the vague, general, and abstract and underspecified niche software so wildly that I have no idea what you are talking about.

Give me a specific example where it is used and I might agree, your post is very unconvincing.

Btw. My personal experience with software written by scientists is that it is mostly certainly not up to par with high-reliability software written in industry. Mostly it is spaghetti code rushed by someone getting a PhD. Certainly you don't refer to that kind of software?

I didn't care to elaborate on data provenance exactly because it is a well-defined term. But yes, I guess my post was all over the place.

Anyway, I've seen software written by scientists, used to conduct experiments. And yes, they were generally not of good quality. But I argue that they *must* be of good quality, otherwise how would one trust the scientific outcome?

To be honest, I've never seen any collider software. But I do know that they deal with huge huge amounts of distributed data. My gut feeling says that reversible computations (where possible) might be an efficient way to provide data provenance on such datasets (instead of using traces).
It is not just in the scientific domain where data provenance is needed. For instance, in the bank domain (where I work) it is getting more and more important. For some background information, see: A Survey of Data Provenance Techniques.

I believe reversibility is one of the key properties to achieve data provenance in practice. I'm developing a programming language that has (scaleable) first-class reversibility (next to being retroactive).

Indeed, provenance is a key application of reversible computation. (There's no need to distinguish trace-based approaches from other reversible computational models.) Dynamic program slicing is another application, although perhaps related to provenance.

In incremental computation, such as self-adjusting computation, change propagation usually relies on reversibility to navigate to affected parts of the computation. Perhaps this is similar to what happens in Spread.

Yet another application is updateable views, such as database views and GUIs. Witness the growing body of work on lenses, bidirectional transformations, etc.

I find the more you think about it, the more implausible the idea of *irreversible* computation starts to sound. Consider a distributed setting, and suppose the subsystem of interest is an external computation which we lack the means or authority to re-execute in a debugger, or run with tracing enabled. Then there are simply no prospects for debugging or otherwise dynamically analysing that subsystem all, unless we suppose that it somehow maintains its computational history.

In incremental computation, such as self-adjusting computation, change propagation usually relies on reversibility to navigate to affected parts of the computation. Perhaps this is similar to what happens in Spread.

I have never relied on reversibility in any of the incremental programming systems I've built; I just found it much harder to "undo" than to "redo" (aka damage, repair). Most of the reactive programming languages I've looked at are similar, but then the self-adjusting computation work has never been vigorously compared to FRP work. And of course, for live programming, reversing is quite impossible since the code can change randomly.

Yet another application is updateable views, such as database views and GUIs. Witness the growing body of work on lenses, bidirectional transformations, etc.

True, I just read something this week to that affect. Lenses haven't gone very far yet in practice, but the field is fascinating.

Consider a distributed setting, and suppose the subsystem of interest is an external computation which we lack the means or authority to re-execute in a debugger, or run with tracing enabled. Then there are simply no prospects for debugging or otherwise dynamically analysing that subsystem all, unless we suppose that it somehow maintains its computational history.

We have a whole group in my team who focus on logging in distribute systems. Much of the time travel work comes out of the systems community, not the PL community, for this very reason (not to mention checkpointing etc...).

"And of course, for live programming, reversing is quite impossible since the code can change randomly.".
Unless you treat code as data and track their dependencies, just as with data.

Yes, that's what we do, but no, I wouldn't consider that "reversing" the code. Rather, its tracing dependencies and then re-executing the code (in its current state) when the code or its dependencies have changed.

Changing code creates an alternative 'branch' of execution, at point where the code has changed. This 'change' of code can be reversed (go back to the branching point).

That is definitely one way that might work. But I find "undoing" everything to be too much hassle, you need to do a ton of tracing to make it worse, and you have to "delay" your change until you can finish reversing. Other problems:

• What if you have a syntax/semantic error? You'll have to wait to reverse/redo until you are in a good state. What if you have a dynamic error? Part of the trick to live programming is dealing with transient errors in a way that doesn't destroy the good state of the whole program.
• You wind up undoing a lot of stuff that probably hasn't changed anyways. By just tracing dependencies and dynamically replaying things until your program stabilizes, you can actually save a lot of work compared to going back.

Consider traces, data and code to be immutable data structures. Every computational step creates a new branch/version of the whole system. Using versions, it's impossible to 'destroy' the good state of whole program.
A computational step can be the replacement of a value in a trace, which spawns another branch of execution (retroactively). It could be that the alternative branch end ups in a state, exactly similar to a state in another branch of execution. At that point, the subsequent states will be know and can be shared.
Checking whole system states (past and present) on equality requires fast O(1) equality checks. I've developed a confluent uniquely represented purely functional data structure that has this property.

Too much work and too complex, though our solutions overlap a lot.

Right now I re-execute the computation and basically compare its result to the last one: undo any effects/dependencies that are no longer done/used, install new effects/dependencies that were not done/used previously; conserve good state when in an error state. I've built UI, parsing, type checking, execution components on a framework that only takes 426 lines of C# code to implement (770 when a few core collections are included).

Unfortunately you can't use "redo" to emulate "undo" the presence of effects. In self-adjusting computation, effects are revocable and "undo" an integral part of the semantics. (There is an issue of how to integrate such a system into a larger system that doesn't support revocable effects; one way to make progress on this issue is to make it less relevant, by making more computational systems reversible.)

As far as I know, FRP tends not to be very incremental. Streams of values model time-indexed state, but when the values being carried by the stream are structured (e.g. trees), there is no fine-grained information about how that structure is changing. At each tick, you get a new tree. I'm not aware of any work that looks at this, but I'd very interested to hear of any. (I've wondered whether there needs to be some kind distributivity of streams over the carrier type, so that at some level a Stream (Tree A) is also a Tree (Stream A).

Logging is all well and good, but if you leave something out of the log that turns out to be important later, then you're out of options, unless you're able to rely on re-execution to reconstruct the missing history. To avoid this problem logging has to be "complete", which is another way of saying that execution has to be lossless.

Yes, I've noticed that much of the work on omniscient debugging, execution mining, etc is "systems" rather than "PL". I'm a bit troubled by "systems" as a research methodology, but nevertheless it exists and that's where the work has for the most part taken place. Hopefully that will change.

[dup]

Unfortunately you can't use "redo" to emulate "undo" the presence of effects.

Perhaps we are picking at what we mean by "undo." In my current live programming system, an effect is revoked (undone) if it is not repeated on a node clean that involves replaying its code. There are arguments on why that is "undo" or "redo," I like to think of it as something more like garbage collection. In no case can I compute a nice invertable or delta function that can avoid the replay step.

As far as I know, FRP tends not to be very incremental. Streams of values model time-indexed state, but when the values being carried by the stream are structured (e.g. trees), there is no fine-grained information about how that structure is changing.

We could distinguish between pure (continuous) and non pure (discrete) FRP work. Ingo Maier's scala.react (a discrete form of FRP) definitely does not re-compute an entire tree on each tick. Perhaps Leo could chime in about Flapjax and his recent work.

To avoid this problem logging has to be "complete", which is another way of saying that execution has to be lossless.

The more common problem with logs for distributed systems these days is that they are too big (the info is there, but you can't find it), not that they aren't big enough (the info is not there).

I'm a bit troubled by "systems" as a research methodology, but nevertheless it exists and that's where the work has for the most part taken place. Hopefully that will change.

The systems people are incredibly pragmatic and their work has to scale and be efficient to be taken seriously; correct is less important than usable. I see PL working on the same problems with less success if they don't embrace similar methods.

> In my current live programming system, an effect is revoked (undone)
> if it is not repeated on a node clean that involves replaying its
> code. There are arguments on why that is "undo" or "redo," I like to
> think of it as something more like garbage collection.

In a model of update where you re-execute from scratch, that sounds reasonable. I'm not sure how you would incrementalise this without introducing some notion of undo, though. (Just think of "undo" as incremental garbage collection.)

> In no case can I compute a nice invertable or delta function
> that can avoid the replay step.

Surely it's technical feasible. Otherwise there will never be a scalable version of live programming, where the update time is bounded by the size of the execution delta. (And I don't know how one would achieve this other than via a trace, as per self-adjusting computation. Although SAC doesn't allow arbitrary code changes.)

In a model of update where you re-execute from scratch, that sounds reasonable. I'm not sure how you would incrementalise this without introducing some notion of undo, though. (Just think of "undo" as incremental garbage collection.)

You divide your computations into nodes that can be replayed independent of other nodes (i.e. they save their input context from parent). So you don't have to re-execute from scratch, and you have a grain of re-execution that is coarser than an instruction. However, in a simple system, re-executing from scratch works well enough also, though you have to worry about continuity in the UI you are using to display your results.

urely it's technical feasible. Otherwise there will never be a scalable version of live programming, where the update time is bounded by the size of the execution delta.

There are a lot of other points in the design space that are much more scalable, as I talked about above. I guess it depends on what you mean by "trace"? Tracing dependencies, sure! Tracing individual instructions? Not necessary.

Consider how UI rendering caches rendering results from scene graph sub-trees. Or how transactions can be aborted with some rollback.

The more common problem with logs for distributed systems these days is that they are too big (the info is there, but you can't find it), not that they aren't big enough (the info is not there).

I disagree. I routinely have both problems at once.

We can solve the problem for many plain functions in two ways:

• Arguments of a non-invertable function cannot be forgotten since they can't be reconstructed. Even c = a + b has the problem that either a or b can be forgotten, but not both. Forgetting (the opposite of define) probably needs to be an explicit operation in a reversible language. Even reassignment is a form of forgetting (the old value), though we get lucky with naturally invertible procedures like increment-in-place.
• The answer produced must be expressive enough to reproduce the arguments. So rather than square be num -> num, it could be num -> (num, sign). This doesn't seem as workable as the first solution, it really can't deal with multi-argument functions very well.

I would love to tackle this problem someday if I have time, but I am also a firm believer in replay rather than invert as a practical solution.

Re. your earlier point about effects, one of the key points of the Information Effects paper is that effectful functions and lossy functions are essentially the same thing. To "forget" information about an argument _is_ a computational effect. Effects seem "irreversible" only because we are considering things from the vantage point of an open system.

An alternative to making an effectful function directly reversible therefore is to embed it in an environment such that the two systems combined are closed and reversible. The effects are interactions with the environment, which gains the information lost by the subsystem. This is how I understand Tailspin and also approaches to reversibility based on traces. Along similar lines, it's been shown that you can embed an irreversible cellular automaton in a reversible one with the same number of dimensions, and that a reversible Turing machine can simulate a reversible one, etc.

Can you elaborate on what you have in mind when you say "replay rather than invert as a practical solution"? (I read "replay" as forward execution, and "invert" as backward execution, so I'm curious as to how they can both be a solution to the same problem.)

A lot, if not most, verification tools allow for forward and backward reasoning over a program simply by the reasoning formalism used over programs. A number of state exploration tools, such as SMV, explicitly reason backward given particular logical formulae to satisfy.

In short, reasoning backward is usually a given property of a large number of formalisms. More specifically, in the Hoare logic example you gave there is nothing holding you from reasoning backward in the first place.