A normal form for a chaotic combinator term?

19 Views Asked by At

Here is the term: $M M C$, where $M = S (S S) S$, which involves the combinators $C = λxλyλz((xz)y)$ and $S = λxλyλz((xz)(yz))$. What does $M M C$ reduce to, under β-equivalence? Or ... if its β-reduction sequences are all infinite (as they appear to be) ... what infinitary combinator expression does it unfold into, in the limit? An example of a term that is β-equivalent to $M M C$ is $a f_{18} \left(f_{17} g_{17} f_{18} f_{18} ⋯ f_{18} a\right)$, where $a = S (S M) C$, $f_0 = C (S C) a$, $g_n = C f_n$ and $f_{n+1} = S g_n$, for all $n = 0, 1, 2, 3, ⋯$, where the $f_{18} f_{18} ⋯ f_{18} ⋯$ consist of $17$ $f_{18}$'s and the trailing "⋯" indicates there's a lot more that follows, past this.

Edit: I found an inductive sequence for normal order that establishes normal order reduction is infinite. Let $a = S (S M) C$. Then $M M C ⇒ ⋯ ⇒ a f_0 ⋯$, and for each $n = 0, 1, 2, ⋯$, $a f_n ⇒ ⋯ ⇒ a f_{n+1} ⋯$, where the trailing $⋯$'s consists of 6 additional arguments (for $M M C$ and $a f_0 ⋯$) or 4 additional arguments (for $a f_n$ and $a f_{n+1} ⋯$).

I'll leave it open for others to find their own inductive proofs.