|[14 earlier articles]|
|Re: Making C compiler generate obfuscated code email@example.com (Walter Banks) (2010-12-21)|
|Re: Making C compiler generate obfuscated code firstname.lastname@example.org (glen herrmannsfeldt) (2010-12-21)|
|Re: Making C compiler generate obfuscated code email@example.com (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 firstname.lastname@example.org (George Neuner) (2010-12-23)|
|Re: Making C compiler generate obfuscated code email@example.com (2011-01-04)|
|Re: Making C compiler generate obfuscated code firstname.lastname@example.org (George Neuner) (2011-01-06)|
|From:||George Neuner <email@example.com>|
|Date:||Thu, 06 Jan 2011 15:45:23 -0500|
|Organization:||A noiseless patient Spider|
|References:||10-12-017 10-12-033 10-12-035 10-12-038 10-12-042 11-01-019|
|Posted-Date:||06 Jan 2011 15:50:36 EST|
On Tue, 04 Jan 2011 12:19:18 +0100, firstname.lastname@example.org (Torben Fgidius
>George Neuner <email@example.com> 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
>There is no conflict here: Equivalence of lambda terms is undecidable.
I think it depends on which calculus you're working in.
>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.
Actually I'm talking about alpha equivalence: e.g., \x.x <==> \y.y
Identical form modulo variable names.
>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.
AFAIK, for the _untyped_ lambda calculus, head normal forms are not an
issue and you can prove or disprove alpha equivalence of forms by
recursive substitution and applicative order reduction until no more
substitutions or reductions are possible and then examining the
Happy to be proven wrong though. References?
Return to the
Search the comp.compilers archives again.