### Dan Piponi

Shared publicly -When we use mutable variables we abandon referential transparency. However, in some cases we preserve another property that I'm going to call coreferential transparency.

First I'll show an example of this property at work and then I'll show why I call it coreferential transparency.

Here's a fragment of C code (call it fragment 1):

B += D

C += D

A += 2*C

B += C

Suppose the variable C is never used after this. Then the final update to C can be eliminated leaving:

B += D

// Deleted line

A += 2*C

B += C

However, this code clearly doesn't have the same effect because A and B are now updated with a different C. We can fix this by writing (fragment 2):

B += D

A += 2*D // new line

B += D // new line

A += 2*C

B += C

So we can eliminate updates to variables if we patch up subsequent uses of that variable. I'm hoping you can see how to generalise this result for yourself. It gives a way to replace certain lines of code with others without changing any behaviour. It's more useful in reverse because it allows you to shorten code in a way that's analogous to common subexpression elimination. You could imagine this being a pattern in a peephole optimization [1] pass.

So why do I call this coreferential transparency?

I've discussed a few times before that given code to compute linear (as in linear algebra) functions, you can easily transform it to code to compute the "transpose" operation [2].

If you start with the code:

C = 2*A+B

D = B+C

and apply the transpose transform you get fragment 1 above.

If you apply referential transparency to C you can transform it to the equivalent code:

C = 2*A+B

D = B+2*A+B

Apply the transpose transform to this code and you get fragment 2.

So the thing I call coreferential transparency corresponds to transposition of referential transparency.

I've no idea if it's a useful property, but it's there.

[1] https://en.wikipedia.org/wiki/Peephole_optimization

[2] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.159.4990&rep=rep1&type=pdf

First I'll show an example of this property at work and then I'll show why I call it coreferential transparency.

Here's a fragment of C code (call it fragment 1):

B += D

C += D

A += 2*C

B += C

Suppose the variable C is never used after this. Then the final update to C can be eliminated leaving:

B += D

// Deleted line

A += 2*C

B += C

However, this code clearly doesn't have the same effect because A and B are now updated with a different C. We can fix this by writing (fragment 2):

B += D

A += 2*D // new line

B += D // new line

A += 2*C

B += C

So we can eliminate updates to variables if we patch up subsequent uses of that variable. I'm hoping you can see how to generalise this result for yourself. It gives a way to replace certain lines of code with others without changing any behaviour. It's more useful in reverse because it allows you to shorten code in a way that's analogous to common subexpression elimination. You could imagine this being a pattern in a peephole optimization [1] pass.

So why do I call this coreferential transparency?

I've discussed a few times before that given code to compute linear (as in linear algebra) functions, you can easily transform it to code to compute the "transpose" operation [2].

If you start with the code:

C = 2*A+B

D = B+C

and apply the transpose transform you get fragment 1 above.

If you apply referential transparency to C you can transform it to the equivalent code:

C = 2*A+B

D = B+2*A+B

Apply the transpose transform to this code and you get fragment 2.

So the thing I call coreferential transparency corresponds to transposition of referential transparency.

I've no idea if it's a useful property, but it's there.

[1] https://en.wikipedia.org/wiki/Peephole_optimization

[2] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.159.4990&rep=rep1&type=pdf

10

13 comments

" but linear logic has little to do with linear types afaict, so there may be more to say here."

What? Types in linear logic are terms of linear logic in the same way traditional types are terms in constructive* logic.

For one example: https://www.cs.cmu.edu/~fp/papers/concur10.pdf

https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwj1ovz06eDPAhVDQyYKHZQ-BHcQFggeMAA&url=https%3A%2F%2Fwww.cs.cmu.edu%2F~fp%2Fpapers%2Fconcur10.pdf&usg=AFQjCNHAphMfLHiF0VbsVOxsUTG8_apfVw&sig2=babMKku_ntixY3C8LHxDFg

What? Types in linear logic are terms of linear logic in the same way traditional types are terms in constructive* logic.

For one example: https://www.cs.cmu.edu/~fp/papers/concur10.pdf

https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwj1ovz06eDPAhVDQyYKHZQ-BHcQFggeMAA&url=https%3A%2F%2Fwww.cs.cmu.edu%2F~fp%2Fpapers%2Fconcur10.pdf&usg=AFQjCNHAphMfLHiF0VbsVOxsUTG8_apfVw&sig2=babMKku_ntixY3C8LHxDFg

Add a comment...