search

hbr / Lambda-Calculus

Some papers on "Lambda Calculus"
23 stars 4 forks source link

Fix proof #3

Closed ursi closed 3 years ago

ursi commented 3 years ago

It looks like there was a copy-paste error here. I believe this is the correct proof.

hbr commented 3 years ago

Thanks for the issue. However I cannot understand why the proof needs a fix.

The cases 2 and 3 are completely symmetrical. Only the direction is reversed b <- c instead of b -> c. I.e. either both cases need a fix or none of them.

Why do you think that the proof is wrong?

ursi commented 3 years ago

Well you're saying "e exists by confluence", i.e. r* is a diamond, but given the direction of the arrows, I don't understand how that applies - the arrows don't make a diamond. Also, why is the e even needed in the first place? The d alone is an element that exists such that r*(a, d) and r*(c, d), which is what we're trying to prove, no?

hbr commented 3 years ago

You are right and I am wrong. Sorry for not understanding your point initially.

Thanks for all your comments.

Regards Helmut

ursi commented 3 years ago

no problem! thank you for this free resource!