Abstract
Rewriting is a foundation for the operational theory of programming languages. The process of rewriting describes the computation of a result (typically, a normal form), with lambdacalculus being the paradigmatic example for rewriting as an abstract form of program execution. Taking this view, the execution of a program is formalized as a specific evaluation strategy, while the general rewriting theory allows for program transformations, optimizations, parallel/distributed implementations, and provides a base on which to reason about program equivalence.
In this talk, we discuss what happens when the notion of termination is asymptotic, that is, the result of computation appears as a limit, as opposed to reaching a normal form in a finite number of steps.
 Example 1. A natural example is probabilistic computation. A probabilistic program P is a stochastic model generating a distribution over all possible outputs of P. Even if the termination probability is 1 (almost sure termination), that degree of certitude is typically not reached in a finite number of steps, but as a limit. A standard example is a term M that reduces to either a normal form or M itself, with equal probability 1/2. After n steps, M is in normal form with probability 1/2 + 1/(2²) + … + 1/(2ⁿ). Only at the limit this computation terminates with probability 1.
 Example 2. Infinitary lambdacalculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambdacalculi provide several other relevant examples.
Instances of asymptotic computation are quite diverse, and moreover the specific syntax of each system may be rather complex. In the talk, we present asymptotic rewriting in a way which is independent of the specific details of each calculus, and we provide a toolkit of prooftechniques which are of general application. To do so, we rely on Quantitative Abstract Rewriting System [Claudia Faggian, 2022; Claudia Faggian and Giulio Guerrieri, 2022], building on work by Ariola and Blom [Ariola and Blom, 2002], which enrich with quantitative information the theory of Abstract Rewriting Systems (ARS) (see e.g. [Terese, 2003] or [Baader and Nipkow, 1998]). ARS are indeed the core of finitary rewriting, capturing the common substratum of rewriting theory and term transformation, independently from the particular structure of the objects. It seems then natural to seek a similar foundation for asymptotic computation. The issue is that the arguments relying on finitary termination do not transfer, in general, to limits (a game changer being that asymptotic termination does not provide a wellfounded order): we need to develope an opportune formalization and suitable proof techniques.
The goal is then to identify and develop methods which only rely on the asymptotic argument  abstracting from structure specific to a setting  and so will apply to any concrete instance. For example, in infinitary lambda calculus, the limit is usually a (possibly infinite) limit term, while in probabilistic lambda calculus, the limit is a distribution over (finite) terms. The former is concerned with the depth of the redexes, the latter with the probability of reaching a result. The abstract notions of limit and of normalization subsumes both, and so abstract results apply to either setting.
BibTeX  Entry
@InProceedings{faggian:LIPIcs.CSL.2023.1,
author = {Faggian, Claudia},
title = {{Asymptotic Rewriting}},
booktitle = {31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
pages = {1:11:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772648},
ISSN = {18688969},
year = {2023},
volume = {252},
editor = {Klin, Bartek and Pimentel, Elaine},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/17462},
URN = {urn:nbn:de:0030drops174621},
doi = {10.4230/LIPIcs.CSL.2023.1},
annote = {Keywords: rewriting, probabilistic rewriting, confluence, strategies, asymptotic normalization, lambda calculus}
}
Keywords: 

rewriting, probabilistic rewriting, confluence, strategies, asymptotic normalization, lambda calculus 
Collection: 

31st EACSL Annual Conference on Computer Science Logic (CSL 2023) 
Issue Date: 

2023 
Date of publication: 

01.02.2023 