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) |
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
Return to the
comp.compilers page.
Search the
comp.compilers archives again.