Re: Making C compiler generate obfuscated code

George Neuner <gneuner2@comcast.net>
Thu, 23 Dec 2010 16:08:06 -0500

          From comp.compilers

Related articles
[12 earlier articles]
Re: Making C compiler generate obfuscated code gneuner2@comcast.net (George Neuner) (2010-12-21)
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: George Neuner <gneuner2@comcast.net>
Newsgroups: comp.compilers
Date: Thu, 23 Dec 2010 16:08:06 -0500
Organization: A noiseless patient Spider
References: 10-12-017 10-12-033 10-12-035 10-12-038
Keywords: code
Posted-Date: 25 Dec 2010 16:24:46 EST

On Wed, 22 Dec 2010 11:30:48 +0000, Martin Ward <martin@gkc.org.uk>
wrote:


>On Tuesday 21 Dec 2010 at 17:25, George Neuner <gneuner2@comcast.net> wrote:
>> >Equivalence of programs is undecidable, ...
>>
>> I'm not sure that's true ... at least in theory. Turing equivalence
>> guarantees that any program can be expressed in the lambda calculus,
>> and the Church-Rosser theorem proves that two lambda expressions which
>> reduce to the same expression are equivalent.
>
>Any program which takes no input and produces no output can only
>do one of two things:
>
>(a) Terminate.
>(b) Not terminate.
>
>So such a program is equivalent to either SKIP or ABORT.
>If this equivalence were decidable, then termination would also be decidable.
>But termination is undecidable (http://en.wikipedia.org/wiki/Halting_problem).


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


"Execution" in LC is a process of continually applying the rewrite
rules to the "program" term until no more reductions can be found (a
halt) or until a fixed point (a cycle) is observed.


George


Post a followup to this message

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