Re: Making C compiler generate obfuscated code

torbenm@diku.dk (Torben Ęgidius Mogensen)
Tue, 04 Jan 2011 12:19:18 +0100

          From comp.compilers

Related articles
[13 earlier articles]
Re: Making C compiler generate obfuscated code gneuner2@comcast.net (George Neuner) (2010-12-21)
Re: Making C compiler generate obfuscated code walter@bytecraft.com (Walter Banks) (2010-12-21)
Re: Making C compiler generate obfuscated code gah@ugcs.caltech.edu (glen herrmannsfeldt) (2010-12-21)
Re: Making C compiler generate obfuscated code martin@gkc.org.uk (Martin Ward) (2010-12-22)
Re: Making C compiler generate obfuscated code DrDiettrich1@aol.com (Hans-Peter Diettrich) (2010-12-22)
Re: Making C compiler generate obfuscated code gneuner2@comcast.net (George Neuner) (2010-12-23)
Re: Making C compiler generate obfuscated code torbenm@diku.dk (2011-01-04)
Re: Making C compiler generate obfuscated code gneuner2@comcast.net (George Neuner) (2011-01-06)
| List of all articles for this month |

From: torbenm@diku.dk (Torben Ęgidius Mogensen)
Newsgroups: comp.compilers
Date: Tue, 04 Jan 2011 12:19:18 +0100
Organization: SunSITE.dk - Supporting Open source
References: 10-12-017 10-12-033 10-12-035 10-12-038 10-12-042
Keywords: code, theory
Posted-Date: 04 Jan 2011 11:22:40 EST

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



Post a followup to this message

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