Thu, 06 Jan 2011 15:45:23 -0500

Related articles |
---|

[14 earlier articles] |

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

Keywords: | code, theory |

Posted-Date: | 06 Jan 2011 15:50:36 EST |

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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.