lambda calculus proof help - General

I have been stuck this "simple" proof for multiple reading sessions now and I just want to move on

untyped_lambda.pdf

theorem 2.16, part 3

I just don't understand how "e exists by confluence", where's the diamond!

Ah - I guess you can use transitivity of $r^\star$ on $c \to_r b \to_r^\star d$ to create $c \to_r^\star e$?

thinking about it more, I don't understand why that $e$ is even there in the first place. $a\to_{r^*}d$ and $c\to_{r^*}d$, that should be QED :thinking:

It's an inductive step where result for $d$ is hypothesis?

So that $d = a$ in 1. inductive case according to base case

I think you're right and that's a copy-paste mistake

You mean as in $e$ is not needed?

yeah

It's not just that it's not needed, but the sentence "e exists by confluence" is not true.

It exists in the second branch of the proof because it completes the diamond (d <- b -> c) but in the third branch the arrows are not in the right direction (d <- b <- c).

:angry:

@Mason Mackaman Have you tried emailing Helmut? Not only would he appreciate the tip-off, you'd also get what should've been Part 3 of the proof.

@Kim-Ee Yeoh oh do they list an email? I've found 3 mistakes so far and I'm only on page 18. regarding the proof, I think I already know the correction.

oh, yep, email right at the top :+1:

I'll shoot him an email after I finish

The email is on the very first page of the document, albeit in a smaller font: Helmut Brandl (firstname dot lastname at gmx dot net)

I actually found the github repo for the pdf, so I'll be using that