Let me first rewrite this code to an equivalent but more readable version:
fun max(x,y) = if x > y then x else y
fun goodMax(nil) = 0
| goodMax(x::nil) = x
| goodMax(x::xs) = let val y = goodMax(xs) in max(x,y) end
Now we can consider how evaluation of goodMax([3,4,5])
proceeds: conceptually, it will be reduced to an answer by repeatedly substituting the respective branch of the function definition(s):
goodMax([3,4,5])
= goodMax(3::[4,5])
= let val y = goodMax([4,5]) in max(3, y) end
= let val y = goodMax(4::[5]) in max(3, y) end
= let val y = (let val y' = goodMax([5]) in max(4, y') end) in max(3, y) end
= let val y = (let val y' = goodMax(5::nil) in max(4, y') end) in max(3, y) end
= let val y = (let val y' = 5 in max(4, y') end) in max(3, y) end
= let val y = max(4, 5) in max(3, y) end
= let val y = (if 4 > 5 then 4 else 5) in max(3, y) end
= let val y = 5 in max(3, y) end
= max(3, 5)
= if 3 > 5 then 3 else 5
= 5
I have renamed the y
in the inner invocation to y'
for clarity.