5 ms·
> representation that is invariant under program equivalence is this even computable at all (leaving aside the complexity theoretic issues)?
by 0xBABAD00C 8y ago
> representation that is invariant under program equivalence
is this even computable at all (leaving aside the complexity theoretic issues)?
- DannyBee 8y agoNo, 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.
- fmap 8y agoThat 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.