So, for some years I’ve been stuck unable to figure out delta computing. I use the symbol because it looks similar on my phone to the symbol I want. But here, I will use in place of .

The small delta means difference between two programs is a program that when applied to the program produces another program that can takes any input, , of to produce , a result that is equivalent to the second program run on the same input and environment such that for some useful definition of . This is the program difference(pd) between two programs.

The large delta the gives us the program differential operator(PD). produces a function that can produce the change in when a pd of its argument is offered . That is: where the RHS partial evaluations are performed by partially specifying just the parameter and leaving the rest free.

An understanding of a pair of pd operator allows for reversible change if is an appropriately typed identity function. A single is an irreversible change. For one example, reading from a true random number generator would be an irreversible program. Inside the realm of a computer, simply reading an input from outside of the computer is an irreversible program within the computer, because it cannot affect the unpressing of the key. Even though outside of the computer we may know the reverse state of the “no” is the question“are you sure” from “rm -rf /“, the computer cannot know that for sure with its own faculties. That is to say, you cannot either, even if you are inside the computer and has access to just the computer memories and interfaces. Invertible pairs are intuitive, such as .

Our accessible realm of compute in an execution is therefore an accumulation of: (an initial state, irreversibly computed outputs, and the compute graph of reversible deltas) By modeling information this way, we can explicitly consider more general changes of states as well as give rise to a framework for understanding, interacting and developing software programs more effectively.

p.s. Btw, these ideas can be equally well expanded into operational and denotational semantics, each with their own idiosyncrasies.

p.p.s. Can we circumvent first order logic by currying functions instead of using ? Elsewhere I have worked out the reparameterization to achieve . One of several example of this kind of reparameterization would be each LHS and RHS now is requested to takes two parameters typed for and yields a function that computes the pd of when it’s parameter changes from one to the second. To achieve the first order approximation effect of derivation in ordinary calculus on reals, all we need is to specify a loose , the first order equivalence, and so on. There are also sub-first-order equivalences such as: having at least same number of characters in the program code, that they are in the same language, etc. First order equivalence should minimally be a program having sufficiently compatible (-ly typed) input and outputs. Subsequently higher order equivalences include progressively more and more identical runtime behaviors or progressively more matching meaning. Here, again is another example of why presently described paradigm is beneficial: for example if a program is stochastic, how do we determine if another program is equivalent to it other than that the code is identical? By isolating the irreversible compute of receiving (from identical) external entropy, the remaining program can be evaluated in the order using conventional . Further higher order equivalence may require that they have same runtime/memory/resource complexities. Which, btw, inspires an ordering that requires all equivalences and then at the level require LHS to be better than RHS—such as lower runtime complexity, etc. The details of all these developments are documented more fully elsewhere.

p.p.p.s. Where is this headed? Well, aside from modeling the universe, one possibility is to achieve truly symbolic differentiation and do back-prop on program code. One can ask, for the PD to a program’s unit test wrt the program. We then pass in the pair (false,true) to arrive at the program (code) mutator that can repairs the input program to produce a program that causes the unit test to pass, after which we use higher ordering to search for a better program.

One can dream…