Solve the halting problem for S combinatory logic

Question

Background

Combinatory logic is a system where a term is written using a finite set of combinators and function application between terms, and reduction rules are defined for each combinator. The well-known S and K combinators have the following reduction rules:

$$ \begin{aligned} S\;x\;y\;z & \overset{S}{\implies} x\;z\;(y\;z) \\ K\;x\;y & \overset{K}{\implies} x \end{aligned} $$

A term is in normal form when no reduction is possible. A term has a normal form if a series of reductions applied to it gives a normal form. The halting problem in combinatory logic is essentially about determining whether a term has a normal form.

It is known that any lambda calculus expression can be converted to an expression in SK combinatory logic, and therefore the halting problem for SK combinatory logic is undecidable. However, neither K nor S alone has such property, and it turns out that the halting problem for each of them is decidable. But K is too trivial (it always terminates), so we turn to S.

A paper titled The Combinator S, by Johannes Waldmann, describes how to decide if a term in S combinatory logic has a normal form. Theorem 55 is the main result, and the regular tree grammar is also presented in Appendix 2.

Examples

The expression \$S(SS)(SS)S\$ halts in two steps:

$$ \begin{aligned} S(SS)(SS)S & \overset{S}{\implies} SSS(SSS) \\ & \overset{S}{\implies} S(SSS)(S(SSS)) \\ \end{aligned} $$

But the two expressions \$S(SS)(SS)(S(SS)(SS))\$ and \$SSS(SSS)(SSS)\$ can be proven to be non-halting, as shown in the paper linked above.

Challenge

Solve the halting problem for S combinatory logic.

In this system, a term is simply a binary tree where each leaf represents S and each internal node represents application. You may take the input using any suitable structure that can directly represent the term, such as

• a binary tree data type,
• a nested array,
• or a string representation using parentheses (e.g. S(SS)(SS)(SS) or (((S(SS))(SS))(SS))) or in prefix notation (e.g. @@@S@SS@SS@SS).

For output, you can choose to

1. output truthy/falsy using your language's convention (swapping is allowed), or
2. use two distinct, fixed values to represent true (affirmative) or false (negative) respectively.

Standard code-golf rules apply. Shortest code in bytes wins.

Answer 1

Charcoal, 264 260 257 235 bytes

⊞υθＦυＦ⊖ＬιＦι⊞υλＦ⮌υＦ⊖Ｌι⊞ι⍘§⁺§⪪”}∨M.⁶C¬²2´#±³¹⊗Ｉ↧β.|eBＴXmê�…⊟→⁼‹Ｒ$➙≧→↧ÀZLq);p↶⁷b⬤Jⅈ⁺7ς⧴Wn7bＺpïＸ|.➙Ｋ!μ…⁼@|v‹℅↨Ｓθ？mＹ,ＫＶ}⟧⎇Φ/◨7⁹¶↧πºwT～B0⁸!✳[➙↘↨cjf^{Ｍg‽bQⅉ→↥Za？↶⁶⊖J↘Ｄ⁻D⟲σ7r⬤？φ'⟦6f▷M↖¡[i⌊⊟\2ν｜¶x2;¹±＆~⁴K∨ρ‽↨⌕ＨMν(T‖β→⁵ⅈÞ↑«…i⊟Ｄ»”0⊟⊟ι×Cφ⊟⊟ιφ›³⁸⊟θ

Try it online! Link is to verbose version of code. Takes input as a nested array where S is represented by [0] so e.g. S(SS) is represented by [[[0], [[0], [0]]]] (note that an extra set of []s is required to input an array to Charcoal since it accepts an array of arguments). Explanation: Based on the look-up table on p. 16 of http://www.cs.ru.nl/~henk/BEKW.pdf but with the values translated to make the resulting table more compressible.

⊞υθＦυＦ⊖ＬιＦι⊞υλ

Perform a breadth-first traversal to collect all of the nodes.

Ｆ⮌υＦ⊖Ｌι

Loop through the non-leaf nodes in reverse order. This effectively produces a depth-first traversal.

⊞ι⍘§⁺§⪪”...”0⊟⊟ι×Cφ⊟⊟ιφ

Turn the node into a leaf by replacing its children with the value from the compressed lookup table.

›³⁸⊟θ

If the value is still less than 38 then the expression halts.

The following rearrangement of the table values is used as this places as many 38s at the bottom of each column as possible. These are then discarded from the compressed string and reconstructed afterwards.

Rearranged  Original
         0   0
        20   1
        19   2
         3   3
         4   4
        16   5
        17   6
         7   7
         1   8
        18   9
         2  10
         9  11
         5  12
        10  13
        12  14
         8  15
        13  16
        14  17
        15  18
        21  19
         6  20
        11  21
        24  22
        23  23
        25  24
        28  25
        27  26
        22  27
        26  28
        35  29
        37  30
        32  31
        30  32
        33  33
        36  34
        34  35
        29  36
        31  37
        38  ∞

Answer 2

Jelly, 248 bytes

Œœżs2Œṙ$€}¥/F^Ị$;0xȷ¤s36
“ƙŀṂƒḂʂŻ⁷Ȧ¿ẏƑ<ọṭẹọ\Ṿ!µɗ⁻ȥƭĊƊġȯ;ŻxḂøCFO)1ɲŒṅ€+ṪʂU-Ɲ¿Ụ£þ^¶ ẹZ361PHc&ẓḟẉẹ⁴Ƒ@G⁶W6ṭ⁽A2K%Ṿ{ẉȯaỊ;ṆẊ:ḄtJ&ß>r³ɲȮ=Ŀ⁼ıɗt¦ÄɦñṙÇ⁹]ḷṡ⁸\]*<f6<U⁷ƲṬðẸG¬db⁾ƭɠ⁹S®w|XƈẎḤ⁴Ȯ⁺2BæƤḋ§Ḷọapæ4%ỊḞḟ¬v⁴ṇW^ŀ$ƈİƥX÷Ð{ṛƈ⁼T4\®ZṆ’b39ṣ0µṪ’s2;"Ç;€0
,߀ŒḊ’$¿œị¢ʋ/

Try it online!

A full program that takes a single argument consisting of a list of S terms. S is represented by 1, and the parentheses are represented using nested lists. For example, \$S(SS)(SS)(S(SS)(SS))\$ becomes [1, [1, 1], [1, 1], [1, [1, 1], [1, 1]]].

Returns 0 for inputs that do not halt and a positive integer (which is regarded as truthy by Jelly) for ones that halt.

This uses a rearranged version of the table found by @Neil for his answer. Most of the work and the bytes were spent on optimally compressing this table from a 38 x 38 table of numbers from 1 to 38 down to 231 bytes. The code that actually solves the problem is a mere 13 bytes (not counting the newline that separates the two).

Explanation

Helper link 1

Expand the run-length encoded segments and append lots of zeros before splitting into 36-length rows. Takes a single argument that alternates between integers to be used as is and run-length encoded runs of integers.

Œœ                          | Split into lists of the odd-indexed and even-indexed members of the original argument
          ¥/                | Reduce using the following:
  ż                         | - Zip with the following:
        €}                  |   - For each member of the right-hand argument (i.e. the even-indexed members of the original list):
   s2                       |     - Split into twos
     Œṙ                     |     - Run-length decode
            F               | Flatten
             ^Ị$            | Xor with whether the numbers are <=1 (effectively turns 1s to 0s)
                ;0xȷ¤       | Append 1000 zeros
                     s36    | Split into lists of length 36
                        ;€0 | Append 0 to each

Helper link 2

Niladic link that generates the look-up table to reduce a pair of S terms

“ƙ…Ṇ’               | Large integer
     b39            | Convert to base 39
        ṣ0          | Split at zeros
          µ         | Start a new monadic chain
           Ṫ        | Tail (which holds the first two cells for each row)
            ’       | Reduce by 1
             s2     | Split into twos
               ;"Ç  | Concatenate zipped to the result of calling helper link 2 on the other members of the list generated in the first part of this link

Main link

Takes an S expression as its argument and returns 0 for non-halting and a positive integer for halting.

           ʋ/ | Reduce using the following:
,             | - Pair
   ŒḊ’$¿      | - While depth >1:
 ߀           |   - Recursively call the current link for each member of the pair
        œị¢   | - Multidimensional index into the look-up table generated by helper link 2