Factorize Factorization

Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
Original languageEnglish
Title of host publication29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
EditorsChristel Baier, Jean Goubault-Larrecq
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages6:1-6:25
Number of pages25
DOIs
Publication statusPublished - 15 Jan 2021
Event29th EACSL Annual Conference on Computer Science Logic (CSL 2021) - Lubijana, Slovenia
Duration: 25 Jan 202128 Jan 2021

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume183

Conference

Conference29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
CountrySlovenia
CityLubijana
Period25/01/2128/01/21

Cite this