User:NathFR76

Hi! My name is Nathan.

I created **Thutus**, a diagonalization of the SKI calculus, and its associated function \(T(n)\).

This page describes the system, its rewrite rules, and the lower bounds currently known for \(T(n)\).

THUTUS — Function T(n)

Thutus is a combinatorial rewriting system whose syntax and expression application follow the SKI calculus.

1. Alphabet

For each integer n ≥ 1, the available alphabet is: L₁, L₂, ..., Lₙ.

2. Initial expression

The initial expression contains exactly n occurrences of symbols. Parentheses do not count toward the size.

3. Arity

Each symbol Lₖ has between 1 and k−1 arguments, with the exception of L₁, which always follows the rule: L₁x → x.

The arguments x, y, z, etc., may be arbitrarily complex expressions.

4. Rewriting rules

The rules for each symbol are chosen prior to execution and remain fixed throughout the execution.

For each symbol Lₖ, the right-hand side of its rule contains between 1 and k occurrences of arguments, excluding parentheses.

Arguments may be reused, rearranged, nested, or deleted.

Examples: L₄xy → x(y(xx)) L₄xyz → z(xy)

5. Reduction and termination

At each step, a rule may be applied to any reducible occurrence, as in the SKI calculus.

An expression terminates when it reaches a normal form—that is, when no further rules can be applied. Expressions that diverge do not contribute to the maximum.

6. Definition of T(n)

T(n) is the maximum number of symbols in the final normal form, taken over all initial expressions of size exactly n and all admissible Thutus rule systems.

The available alphabet is L₁, ..., Lₙ. The rules are chosen at the outset, must satisfy the aforementioned constraints, and remain fixed throughout the execution.

And actually few value for T(n):

T(0) = 0

T(1) = 1

T(2) = 1

T(3) = 4

T(4) ≥ 522

T(5) ≥ 1814

T(6) or higher can encode BCKW system so:

T(6) ≥ 2^256*6-1

T(7) ≥ 2^^^17

T(8) ≥ 2^^^2^^^17

T(9) ≥ 2^^^^^2^^^^2^^^17

T(10) ≥ f_ω+1(2^^6/2-1)

T(15) ≥ f_ω^(2^^18-1)(2)

And for T(1) to T(5) result: T(1) = 1

A

T(2) = 1

AB B

T(3) = 4

Initial: (L2 (L3 L3)) Rules:

 L1 (1 args) -> x1
 L2 (1 args) -> (x1 x1)
 L3 (2 args) -> (x1 (x1 x2))

L3 (L3 (L3 L3))

T(4) ≥ 522

Initial: (L3 (L3 (L4 L4))) Rules:

 L1 (1 args) -> x1
 L2 (1 args) -> (x1 x1)
 L3 (1 args) -> ((x1 x1) x1)
 L4 (3 args) -> ((x1 x2) (x2 x3))

Normal form: ((L4 ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4))))))))) ((L4 ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4)))))))) ((L4 ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4))))))) ((L4 ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4)))))) ((L4 ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4))))) ((L4 ((L4 (L4 L4)) ((L4 L4) (L4 L4)))) ((L4 ((L4 L4) (L4 L4))) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 ((L4 (L4 L4)) ((L4 L4) (L4 L4)))) ((L4 ((L4 L4) (L4 L4))) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4)))))) ((L4 ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L4 L4))))) ((L4 ((L4 (L4 L4)) ((L4 L4) (L4 L4)))) ((L4 ((L4 L4) (L4 L4))) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 ((L4 (L4 L4)) ((L4 L4) (L4 L4)))) ((L4 ((L4 L4) (L4 L4))) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) ((L4 (L4 L4)) ((L4 L4) (L ... [truncated]

T(5) ≥ 1814

Initial: (L3 ((L3 L4) (L4 L5))) Rules:

 L1 (1 args) -> x1
 L2 (1 args) -> x1
 L3 (1 args) -> (x1 (x1 x1))
 L4 (2 args) -> (x1 (x2 (x1 x2)))
 L5 (4 args) -> x4

Normal form: (((L5 ((L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))) ((L5 (L4 (L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))))) ((L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))) (L5 (L4 (L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))))))))) (L4 (L5 ((L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))) ((L5 (L4 (L5 (L5 (((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))) (L5 ((L5 (L4 (L4 L5))) (L5 ((L5 (L4 (L4 L5))) (L5 (L5 (L4 (L4 L5))))))))))))) ((L5 (L5 (((L5 (L4 (L4 L5))) ... [truncated]

This bound for T(4) and T(5) is from a python program but T(4) and T(5) is probably higher than this bound and this bound is verified by SKI Interpreter (https://dallaylaen.github.io/ski-interpreter/)