Thumbnail
Access Restriction
Open

Author Aehlig, Klaus ♦ Joachimski, Felix
Source CiteSeerX
Content type Text
Publisher Springer-Verlag
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Natural Topology ♦ Coalgebraic Setting ♦ Repetition Rule ♦ Non-wellfounded Term ♦ Primitive Recursive Normalization Function ♦ Normal Form ♦ So-called Repetition Rule ♦ Void Constructor ♦ Continuous Normalization ♦ Much Simpler ♦ Syntactical Property ♦ Untyped Coinductive Calculus ♦ Proof Theory
Description Proc. 11 th CSL 2002 (Edinburgh), volume 2471 of Lecture
This work aims at explaining the syntactical properties of continuous normalization, as introduced in proof theory by Mints, and further studied by Ruckert, Buchholz and Schwichtenberg. In an extension of the untyped coinductive -calculus by void constructors (so-called repetition rules), a primitive recursive normalization function is de ned. Compared with other formulations of continuous normalization, this de nition is much simpler and therefore suitable for analysis in a coalgebraic setting. It is shown to be continuous w.r.t. the natural topology on non-wellfounded terms with the identity as modulus of continuity. The number of repetition rules is locally related to the number of -reductions necessary to reach the normal form (as represented by the B ohm tree) and the number of applications appearing in this normal form.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article