Re: Making C compiler generate obfuscated code

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


>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.


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
resultant forms.




Happy to be proven wrong though. References?
George

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