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"
EXAMPLE: This example, similar to yours, will be made concrete with
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and