Refining Reduction in the lambda calculus Export

@misc{kamareddine-nederpelt-96, abstract = {We introduce a -calculus notation which enables us to detect in a term, more fi- redexes than in the usual notation. On this basis, we define an extended fi-reduction which is yet a subrelation of conversion. The Church Rosser property holds for this extended reduction. Moreover, we show that we can transform generalised redexes into usual ones by a process called "term reshuffling". Keywords: Item notation, Redexes, Church Rosser. Contents 1 Introduction 3 1.1 The item notation and visible redexes . . . . . . . . . . . . . . . . . . . . . . 4 1.2 The system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 Generalising redexes and fi-reduction 7 2.1 Extending redexes from segments to couples . . . . . . . . . . . . . . . . . . . 7 2.2 Extending fi-reduction and the Church Rosser theorem . . . . . . . . . . . . . 8 3 Term reshuffling 10 3.1 Partitioning terms into bachelor and well-balanced segments . . . . . . . . . . 11 3.2 The reshuffling procedure...}, author = {Kamareddine, Fairouz and Nederpelt, Rob}, citeulike-article-id = {5856227}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.6961}, journal = {Journal of Functional Programming}, keywords = {binding, cps, lambda-calculus, redexes, syntax}, number = {4}, pages = {637--651}, posted-at = {2009-09-29 23:45:24}, priority = {2}, publisher = {Cambridge University Press}, title = {Refining Reduction in the lambda calculus}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.6961}, volume = {5}, year = {1996} }

TY - ELEC ID - kamareddine-nederpelt-96 L3 - citeulike-article-id:5856227 N2 - We introduce a -calculus notation which enables us to detect in a term, more fi- redexes than in the usual notation. On this basis, we define an extended fi-reduction which is yet a subrelation of conversion. The Church Rosser property holds for this extended reduction. Moreover, we show that we can transform generalised redexes into usual ones by a process called "term reshuffling". Keywords: Item notation, Redexes, Church Rosser. Contents 1 Introduction 3 1.1 The item notation and visible redexes . . . . . . . . . . . . . . . . . . . . . . 4 1.2 The system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 Generalising redexes and fi-reduction 7 2.1 Extending redexes from segments to couples . . . . . . . . . . . . . . . . . . . 7 2.2 Extending fi-reduction and the Church Rosser theorem . . . . . . . . . . . . . 8 3 Term reshuffling 10 3.1 Partitioning terms into bachelor and well-balanced segments . . . . . . . . . . 11 3.2 The reshuffling procedure... IS - 4 JF - Journal of Functional Programming EP - 651 TI - Refining Reduction in the lambda calculus PB - Cambridge University Press VL - 5 SP - 637 KW - binding KW - cps KW - lambda-calculus KW - redexes KW - syntax AU - Kamareddine, Fairouz AU - Nederpelt, Rob PY - 1996/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.6961 ER -