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 n

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.