Publikation
lim+, delta+, and Non-Permutability of beta-Steps.
Claus-Peter Wirth
In: Journal of Symbolic Computation, Vol. 47, Pages 1109-1135, Academic Press, Elsevier, 2012.
Zusammenfassung
Using a human-oriented formal example proof of the (lim+) theorem, i.e. that the sum of limits is the limit of the sum, which is of value for reference on its own, we exhibit a non-permutability of beta-steps and delta+-steps (according to Smullyan's classification), which is not visible with non-liberalized delta-rules and not serious with further liberalized delta-rules, such as the delta++-rule. Besides a careful presentation of the search for a proof of (lim+) with several pedagogical intentions, the main subject is to explain why the order of beta-steps plays such a practically important role in some calculi.