fix(LambdaCalculus): change from rename to swap in alpha equivalence

[SamuelSchlesinger]

This PR fixes a bug in alpha equivalence where one could prove the Church encoded true is alpha-equivalent to Church-encoded false. To fix it, I switched over to a swap based dynamics which IIUC is how other formalizations have done it without De Bruijn indices. Leaves an example so it can't happen again and to explain why it works that way.

[SamuelSchlesinger]

Oh I see that there are some other PRs up to do more comprehensive things here. Happy to close this if those are preferred, but something surgical to fix the issue seems reasonable if those will take some time to get in.

[chenson2018]

This seems likely to be superceded by #458, right? I'd appreciate more eyes there even if it's just limited to this issue.

[SamuelSchlesinger]

This seems likely to be superceded by #458, right? I'd appreciate more eyes there even if it's just limited to this issue.

Yeah, if that got in it would definitely supercede this. I just took a look but it looks like I'd need a bit more time to wrap my head around that one.

[chris-anto-froeschl]

This seems likely to be superceded by #458, right? I'd appreciate more eyes there even if it's just limited to this issue.

Yeah, if that got in it would definitely supercede this. I just took a look but it looks like I'd need a bit more time to wrap my head around that one.

I didn't look into the details of the old implementation pre #458 but my PR showing #741 equivalence between a renaming and a swap approach would be relevant here. My swap implementation is almost like yours except for being implemented as a special case of permutations.

I also intend to look into the test examples the upcoming days and add some to #741 .

[SamuelSchlesinger]

Yes, yours is one of the PRs I noticed right after I pushed this up! After some reading it seems that #458 is pretty far along, I am going to close this so we don't cause unnecessary thrash there.