search

seanjensengrey / kiama

Automatically exported from code.google.com/p/kiama
GNU Lesser General Public License v3.0
0 stars 0 forks source link

Substitution in the example implementation of the lambda-calculus is wrong #62

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Essentially it is _not_ capture-free: 
https://code.google.com/p/kiama/source/browse/library/src/org/kiama/example/lamb
da/Lambda.scala

> What steps will reproduce the problem?

A simple test of `(\x.\y.x) y` will illustrate the problem.

> What is the expected output? What do you see instead?

The expected output should be `\z.y` (with `z` being fresh).  I did not 
actually test it, but I am almost sure the example implementation will produce 
`\y.y`.

> Please provide any additional information below.

The example implementation claims to follow Rose's \xgc, but neglected the 
"modulo ≡" (i.e., modulo α-equivalence) note in the presentation of the 
reduction rules.  You should either implement the capture-free substitution or 
be explicit the implementation consider only α-equivalent terms.  Otherwise, 
it is misleading.  Indeed, one master student I know who presented Kiama a few 
months ago in our research group was confused and confused us.

Original issue reported on code.google.com by plm....@gmail.com on 23 Jan 2014 at 9:49

GoogleCodeExporter commented 9 years ago 
Yes, of course you're right. Thanks for making the report and sorry for any 
confusion it has caused. 

I will add the renaming as soon as I am finished with another task.

Original comment by inkytonik on 23 Jan 2014 at 10:58

GoogleCodeExporter commented 9 years ago 
Revision r7ac93e401530 fixes this problem by introducing fresh variables when 
substituting inside lambda terms.

I have also added mention of this solution to the 
[https://code.google.com/p/kiama/wiki/Lambda wiki page that describes this 
example] which already mentioned Rose's Convention A.3 that required all 
variables to be unique.

Thanks again for the report.

Original comment by inkytonik on 3 Feb 2014 at 4:21

GoogleCodeExporter commented 9 years ago

Original comment by inkytonik on 9 May 2014 at 3:50