Refining reduction in the lambda calculus

F. Kamareddine, R.P. Nederpelt

Research output: Contribution to journalArticleAcademicpeer-review

11 Citations (Scopus)


We introduce a ¿-calculus notation which enables us to detect in a term, more ß-redexes than in the usual notation. On this basis, we define an extended ß-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’.
Original languageEnglish
Pages (from-to)637-651
Number of pages24
JournalJournal of Functional Programming
Issue number4
Publication statusPublished - 1995


Dive into the research topics of 'Refining reduction in the lambda calculus'. Together they form a unique fingerprint.

Cite this