[remexre]

For straight-line code, something like

    %2 <- foo %0 %1
    ...

is effectively equivalent to

    (foo %0 %1 (lambda (%2)
      ...)

Phis are sorta modeled inversely:

    %1:
        %2 <- const 0
        br %5
    %3:
        %4 <- const 1
        br %5
    %5:
        %6 <- phi [%1 -> %2, %3 -> %4]
        ...

becomes:

    (letrec ((%1 () (const 0 (lambda (%2) (%5 %2))))
             (%3 () (const 1 (lambda (%4) (%5 %4))))
      (%5 (%6) ...))
      ...)

The nice thing on paper about both of these is that you've broken every computation down into nice nameable bits; if you want to do some analysis (e.g. abstract interpretation) over the programs, you can store intermediate results as a map from names (like %4) to values.

The traditional downside of CPS is that requiring lambdas be nested in order for things to be in scope can make some program transformations require "reshuffling" terms around in a way SSA doesn't require.

The "cps soup" [0] approach used in Guile fixes this, but your terms look like they violate lexical scoping rules!

[0]: https://wingolog.org/archives/2015/07/27/cps-soup