Re: [isabelle] Infinitely recursive lambda expression or not?



Le Sat, 14 Dec 2013 13:24:49 +0100, Lawrence Paulson <lp15 at cam.ac.uk> a écrit:

On 14 Dec 2013, at 12:17, Yannick <yannick_duchene at yahoo.fr> wrote:

Why is f(False) not False ? If it's built with False only and only disjunctions, where could True comes from?

Or else may be my interpretation is wrong: I see it as an infinite sequence like “x ∨ x ∨ x ∨ x ∨ x ∨ …”.

I’m afraid that’s your mistake. Such expressions simply don’t make sense.

Larry Paulson

I agree opinion may vary about the sense, I mainly had the hope this won't be unsound.

I will go another way, reformulating some expressions, using a garde, to avoid this case. The question was still interesting to me.

Thanks again for the comments.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.