Generalize "compositional congruence" beyond circuits
Created by: joaopizani
From @joaopizani on March 28, 2015 18:22
If not in definition, at least in type.
For equality "up to simulation" we cannot define the usual congruence law, but we can define a constrained version that uses a zipper-like representation. This is effectively a congruence law over compositional functions, i.e, functions that only "prepend" the two subtrees in a common "context".
We should generalize this concept to work on datatypes other than Circuit.
Copied from original issue: joaopizani/piware#33