This page provides a list of identities that can be used to rewrite expressions preserving semantics. Each provides a reference to the proof of the identity. =~= denotes strong equivalence in the semantics and =~~= denotes weak equivalence.

Everything needs to be checked. Especially the lines without a proof reference.

#### Table of Contents

## Syntactic Identities#

Syntactic identities are those whose restrictions are purely syntactic and do not need to know anything about sites used or other properties of the expressions. These identities are taken from Prof. Misra's book primarily but also other sources.Misra (Ch. 3) states that all the identities proved for the asynchronous case also hold for the synchronous case. This should be the case, however a proof would be good to have.

Identity | Proof |
---|---|

Parallel | |

f | g =~= g | f | Misra ch 3 |

f | stop =~= f | Misra ch 3 |

f | (g | h) =~= (f | g) | h | Misra ch 3 |

Sequence | |

stop >x> f =~= stop | Misra ch 3 |

f >x> (g >y> h) =~= (f >x> g) >y> h if x is not free in h | Misra ch 3 |

signal >x> f =~~= f if x is not free in f | Misra ch 3 |

f >x> x =~~= f | Misra ch 3 |

Pruning | |

f <x< stop =~= f if x is not free in f | Misra ch 3 |

f <x< g =~= f <x< (stop <x< g) =~= f | (stop <x< g) if x is not free in f | Misra ch 3 |

(f <x< g) <y< h =~= (f <y< h) <x< g if x is not free in h and y is not free in g and x and y are distinct | Misra ch 3 |

Otherwise | |

(f ; g) ; h =~= f ; (g ; h) | Misra ch 3 |

stop ; g =~~= g | Misra ch 3 |

g ; stop =~~= g | Misra ch 3 |

Misc | |

(f | g) >x> h =~= (f >x> h) | (g >x> h) | Misra ch 3 |

(f | g) <x< h =~= (f <x< h) | g if x is not free in g | Misra ch 3 |

(f >y> g) <x< h =~= (f <x< g) >y> g if x is not free in g and x and y are distinct | Misra ch 3 |

(f ; g) <x< h =~~= (f <x< h) ; g if g does not refer to x | ??? |

S(..., stop, ...) =~~= stop where S is a site | ??? |

## Semantic Identities#

Semantic identities are those that are restricted by the properties of the expression that may depend on the sites used.

Identity | Proof |
---|---|

f <x< n =~= [x := stop].f | n if n is silent | Misra ch 3 |

n >x> f =~= n if n is silent | ??? |

There are two properties that make pruning (f <x< g) different than sequence (g >x> f). First, pruning terminates g when it publishes. Second, pruning allows f to execute while waiting for x to be bound (late binding of x). We can imagine two steps between these. They would only be used in cases where a normal pruning operator would have the same semantics. They can be thought of as pruning with optimization annotations.

- g >x>| f (late-sequence) which late binds x but does not terminate g although it does ignore publications after the first. This is only late binding.
- f <x<$ g (strict-pruning) which terminates g when it publishes but does not start f until x is bound. This is only termination.

Identity | Proof |
---|---|

f <x< g =~= f <x<$ g if f is side-effect free | |

f <x< g =~= f <x<$ g if f is strict on x | |

(f | h) <x< g =~= (f | h) <x<$ g if h is strict on x and f is side-effect free (This subsumes the above 2 lines) | TODO |

f <x< g =~= g >x>| f if g is resilient or terminating (This holds generally because there is no guarantee when g will be terminated even in the left expression, so as long as it eventually terminates the guarantees are met) | TODO |

g >x>| (f | h) =~= g >x> (f | h) if h is strict on x, f is side-effect free and g publishes at most once (This implies 2 identities similar to the top 2 lines) | TODO |

f <x<$ g =~= g >x> f if g is resilient or terminating and g publishes at most once (allowed because termination timing is not guaranteed) | TODO |

These identities may not hold in the synchronous case. This is because timing of publications is not taken into account. However, even the synchronous semantics do not guarantee any order, so delaying some publications would just select a specific and allowed scheduling.