I guess that depends on what you mean by equivalence between CPS and SSA.
My prefered form is basic blocks with arguments. Where the final jump has parameters it passes to it's destination blocks.
That form has a 1-1 equivalence with SSA and I find it much easier to reason about. Every SSA algorithm I have looked at so far works just fine on the representation. Plus there is none of the annoying transforming into and out of SSA.
If you omit the mucking about with return closures in CPS what is left is basic blocks with arguments.
To see basic blocks with arguments as a form of SSA just see every basic block argument as a phi function, and the callers parameters that feed into that argument as the other end of the sources of the phi function.
Just from your description I think your pizlo special SSA is actually a form of basic blocks with arguments. What I don't see from your description is why Upsilon and phi aren't combined into a single notion (What I would call an incoming block parameter).
Nit: the correspondence between phi-SSA and basic block arguments is not one to one. With block arguments, you can jump to the same block with different arguments depending on a condition. You can’t do that in SSA without adding new blocks.
What is Upsilon? It sounds like something that figures out the value coming into a block, which I would call a basic block argument.
How does Upsilon know which values from other basic blocks it could receive? That information is critical for transformations like constant propagation, and register allocation.
Upsilon doesn't know anything about basic blocks. It's just an assignment.
Upsilon uses an SSA value, and assigns to a Phi. The use of an SSA value is just a normal SSA use.
The assignment to the Phi is special, and follows Static Single Use law.
In practice, you'll want to either have all Phis know about the Upsilons that refer to them, or you'll want to have a handy analysis that tells you about the Upsilons that refer to Phis. This part is no different from how your SSA form will either have user tracking (like LLVM IR) or an analysis that tells you the users.
Isn't it supposed to be ANF ("A-normal form") rather than full CPS? That looks a bit closer to what you're talking about re: basic blocks w/ arguments.
My prefered form is basic blocks with arguments. Where the final jump has parameters it passes to it's destination blocks.
That form has a 1-1 equivalence with SSA and I find it much easier to reason about. Every SSA algorithm I have looked at so far works just fine on the representation. Plus there is none of the annoying transforming into and out of SSA.
If you omit the mucking about with return closures in CPS what is left is basic blocks with arguments.
To see basic blocks with arguments as a form of SSA just see every basic block argument as a phi function, and the callers parameters that feed into that argument as the other end of the sources of the phi function.
Just from your description I think your pizlo special SSA is actually a form of basic blocks with arguments. What I don't see from your description is why Upsilon and phi aren't combined into a single notion (What I would call an incoming block parameter).