That was a poor choice of words. Models of lambda calculus are invariant under beta-eta conversion, which is what I meant by program equivalence, but which is not the same thing as contextual equivalence.

Thus you get a representation invariant under computation. This remains decidable when you consider only normalizing programs as in STLC or related subsystems.

No, it isn't. It's clearly undecidable.

Herbrand equivalence is the best you can do (in general) if you are trying to say whether two variables have the same values at the same program points.

If you are willing to be probablistically correct you can do better, but you will get wrong answers (and not know they are wrong) That is likely okay for this application.