I've recently discovered the existence of infinitary lambda calculus, or infinite lambda calculus, and am interested but unclear about some of its properties.
So what is infinitary lambda calculus and how is it different compared to conventional lambda calculus? What are the benefits of infinitary lambda calculus over conventional lambda calculus?
What is infinitary λ-calculus?
In one sentence: it is λ-calculus with (possibly) infinite(ly deep) terms, and (possibly) infinite β-reductions. Notice that finite terms and reductions are also infinitary ones!
If you have done a bit of λ-calculus, you probably already know some infinitary λ-terms: the Böhm trees, a notion on infinite normal form introduced by Barendregt. For instance, the Böhm tree of any fix-point combinator $Y$ is $\lambda f.fff\dots$ (an infinite sequence of $f$). The infinitary λ-calculus formalizes this idea that $Y \longrightarrow_{\beta}^{\infty} \lambda f.fff\dots$.
It was first defined in Kennaway et al. (1997) using a topological definition: infinite terms are limits of Cauchy sequences of finite terms, and the infinitary reduction is defined by sequences of β-reductions enjoying a strong convergence property. Later, it was reformulated into an elegant coinductive definition (Endrullis and Polonsky 2013). If you want a survey on the subject, see Chapter 6 of the recent Barendregt-Manzonetto Satellite.
(I keep this answer very short since I don't know exactly what you are expecting, feel free to add comments so that I can precise my answer.)
How is it different compared to conventional lambda calculus? What are the benefits of infinitary lambda calculus?
Normalization. — Still, the infinitary λ-calculus is not normalizing; for instance, $\Omega$ has no infinitary normal form. But there are more normalizable terms than in the finitary setting (e.g. $Y$).
Confluence. — The confluence property is broken. However, introducing a variant of the β-reduction (the β$\bot$-reduction, which reduces all “problematic” terms to a constant $\bot$ in one step) is sufficient to retrieve confluence. (There is a precise definition of “problematic”, see the literature about meaningless sets of λ-terms. The precise result is: the infinitary β-reduction modulo some meaningless set is confluent, see Czajka 2020.)
This variant is also normalizing: in the “general” infinitary λ-calculus, for any term $M$ we have $M \longrightarrow_{\beta\bot}^{\infty} \mathrm{BerT}(M)$ its Berarducci tree (Berarducci 1996, a refinement of Böhm trees), which is in normal form. If you're interested in Böhm trees, there is a slightly different infinitary λ-calculus (called 001-infinitary) where $M \longrightarrow_{\beta\bot}^{\infty} \mathrm{BT}(M)$ for all $M$ (see the seminal paper by Kennaway et al., or Cerda and Vaux Auclair 2022 for a coinductive presentation).
The main benefit here is to extend the benefits of Böhm trees: give an account of the computational behavior of terms that do not normalize. In very vague words: once you excluded some meaningless programs (like $\Omega$), you obtain programs that do not necessarily terminate but still compute something, and have a meaning (like $Y$). Think of a program computing the decimals of $\pi$: it is not terminating but it has a “limit output”, namely $\pi$.
(About this notion of meaning, Barendregt writes: “It is proposed that [the unsolvable] terms represent the notion of undefined. [...] This class should be considered as the meaningless terms.”)
