5
$\begingroup$

Question (short and simple version):
Can anyone suggest a very short SK combinator expression with a ridiculously long, but still terminating, reduction path (ignoring loops)?

Question (longer version):
I note that my question above seems closely related to the study of Busy Beaver functions. If we define BB_SK(n) to be the length of the longest terminating SK combinator reduction -- we might have to fix a reduction strategy, or declare that we ignore loops -- amongst all SK combinator terms of length at most n, then we can rephrase my question in more mathematical generality as asking: what if anything is known about BB_SK(n)?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

The lambda term (λ 1 1) (λ 1 (1 (λ λ 1 2 (λ λ 2 (2 1))))) requires a number of reduction steps exceeding Graham's number [1], and translates to the following SK term:

S (S K K) (S K K) (S (S K K) (S (S K K) (K (S (K (S (K (S S (K (K (S (S (K S) K) (S K K)))))) (S (S K K)))) K))))

Generally, all the lower bounds on BBλ [2] translate to lower bounds on your BB_SK.

[1] https://github.com/tromp/AIT/blob/master/fast_growing_and_conjectures/melo.lam

[2] https://oeis.org/A333479

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.