Re: Making C compiler generate obfuscated code

George Neuner <gneuner2@comcast.net> writes:




> It is true that termination, in general, is undecidable ... but that
> doesn't invalidate Church-Rosser equivalence.
>
> The lambda calculus is based on term rewriting. Church-Rosser
> equivalence is based on pattern matching of lambda terms. By applying
> the rewrite rules for term expansion, substitution and reduction, if
> two different terms can be rewritten to be in the same pattern form -
> modulo variable names - then they are considered equivalent. It
> doesn't matter what the terms "mean" or what they might do if
> "executed".


There is no conflict here: Equivalence of lambda terms is undecidable.


Equivalence (more specifically beta equivalence), as you say, is defined
by saying that two terms t1 and t2 are equivalent if there is a term t3
such that t1 => t3 and t2 => t3, where => is the (reflective and
transitive) reduction relation. But if t1 or t2 both are without normal
forms, you can not decide their equivalence by comparing a finite number
of terms. Hence, equivalence is only semi-decidable.


There are various other ways to define equivalence of lambda terms
that attempt to equivalate more terms, such as all terms that have no
head normal form or weak head normal form. But these are also
undecidable. You can define equivalences that equate fewer terms and
which are decidable, but these are not useful as program equivalence.
Alpha equivalence and eta equivalence springs to mind.


Torben

Return to the comp.compilers page.
Search the comp.compilers archives again.