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



On 12/18/2013 4:55 PM, Gottfried Barrow wrote:
theorem "(!!f::(nat => nat). !!a. f = (%x. f x) ==> f a = a) ==> False"
by(auto)
(*
EXAMPLE: This example, similar to yours, will be made concrete with sumXp.
*)

theorem "sumXp = (%x. sumXp x) ==> sumXp 4 = 10"

So 4 is not equal to 10, but the primary purpose was to show that nothing automatically happens with function application, such as "sumXp 4", and at most, a sequence of substitutions are made, if things are done the way I did them. Most important, maybe, is knowing that infinite recursion can't happen.

Regards,
GB




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