Coinductive combinatory and lambda reduction systems

Question

SK combinators and the lambda-calculus are inductively-defined reduction systems. A nice online lambda-calculus interpreter is at https://lambdacalc.dev/

Question: what happens if instead of inductively defining reductions, we do so coinductively. This would correspond to the same derivation rules, but now we allow cyclic derivations (ones that loop).

Does this lead to anything interesting -- or do the systems perhaps become trivial in that everything reduces to everything else?

Thank you.

p.s. A coinductive reduction relation (having derivations that may be cyclic) is not the same thing as an inductive relation that admits a term that reduces to itself. These are two orthogonal concepts.

• sparusaurata: Notice that a coinductive reduction relation is also not the same thing as a reduction relation whose derivations may be cyclic: the latter would be the regular fragment of the former.

Answer 1

On the λ-calculus side, an infinitary λ-calculus has been introduced quite a while ago, as the result of the introduction of:

• converging infinite sequences in first-order rewriting [DKP'91]
• strongly converging infinite sequences in first-order rewriting [KKSV'95]
• strongly converging infinite β-reduction sequences of infinitary λ-terms, aka infinitary λ-calculus [KKSV'97]

This is summarised for instance in [Terese, chap. 12].

All this work is done in a topological setting, but it was later noticed that it can be equivalently presented coinductively: infinitary λ-terms are built coinductively just as λ-terms are built inductively, and strongly converging β-reduction sequences between such terms are equivalent to an infinitary closure of the β-reduction [EP'13], defined coinductively by: $$ \frac{M \to^* x}{M \to^\infty x} \qquad \frac{M \to^* λx.P \quad P \to^\infty P'}{M \to^\infty λx.P'} \qquad\frac{M \to^* PQ \quad P \to^\infty P' \quad Q \to^\infty Q'}{M \to^\infty P'Q'} $$

A general, abstract correspondence between topologically and coinductively presented infinitary rewriting is provided in [EHHPS'18]. Maybe this is what you want to look at to get a general notion of "coinductive rewriting relation". (It is summarised, slightly extended and related to λ-calculus in the preliminary [CS'25], longer version hopefully to appear.)

By the way, notice that a notion of infinitary combinatory reduction systems has also been introduced in [KS'11].

I'm not quite sure this is what you're looking for but if so I'd be glad to develop on whichever details or references you're interested in!