Asymptotic Rewriting (Invited Talk)

Author Claudia Faggian

Thumbnail PDF


  • Filesize: 353 kB
  • 2 pages

Document Identifiers

Author Details

Claudia Faggian
  • IRIF, CNRS - Université de Paris Cité, F-75013 Paris, France

Cite AsGet BibTex

Claudia Faggian. Asymptotic Rewriting (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


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 lambda-calculus 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 lambda-calculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambda-calculi 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 proof-techniques 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 well-founded 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Models of computation
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Lambda calculus
  • rewriting
  • probabilistic rewriting
  • confluence
  • strategies
  • asymptotic normalization
  • lambda calculus


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Zena M. Ariola and Stefan Blom. Skew confluence and the lambda calculus with letrec. Annals of Pure and Applied Logic, 117(1):95-168, 2002. URL:
  2. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL:
  3. Claudia Faggian. Probabilistic rewriting and asymptotic behaviour: on termination and unique normal forms. Log. Methods Comput. Sci., 18(2), 2022. URL:
  4. Claudia Faggian and Giulio Guerrieri. Strategies for asymptotic normalization. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, volume 228 of LIPIcs, pages 17:1-17:24. Schloss Dagstuhl, 2022. URL:
  5. Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar