User:NathFR76
Hi! My name is Nathan.
And i made Thutus function
Thutus calculus
Thutus is a combinatorial rewriting system whose syntax and expression application follow the SKI calculus.
- 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₁ x1 → x1. The arguments x1, x2, x3, 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₄ x1 x2 → x1 (x2 (x1 x1)) L₄ x1 x2 x3 → x3 (x1 x2)
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) (also written as Ξ₀T) 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.
Champions for T(n) / Ξ₀T
| n | Value | Champion Initiate Term | Champion Rule |
|---|---|---|---|
| 0 | = 0 | ||
| 1 | = 1 | L1 | L1 x1 -> x1 |
| 2 | = 1 | L1L2 | L1 x1 -> x1
L2 x1 -> x1 x1 |
| 3 | = 4 | L2(L3L3) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 x2 -> x1 (x1 x2) |
| 4 | ≥ 522 | L3(L3(L4L4)) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 -> (x1 x1) x1 L4 x1 x2 x3 -> x1 x2 (x2 x3) |
| 5 | ≥ fω+1(2^^6/2) | L1(L2(L4(L5L3)) | L1 x1 -> x1
L2 x1 -> x1 x1 L3 x1 x2 -> x1 (x1 x2) L4 x1 x2 -> x2 (x2 x1) L5 x1 x2 x3 -> x3 x2 x1 |
| ... | |||
| 15 | > fω2^^18-1(2) | L4L4(L5(L4L6)(L6(L6L5(L5L5(L4L6)))(L5(L6L5)))) | L1 x1 -> x1
L2 x1 -> x1 L3 x1 x2 -> x1 L4 x1 x2 -> x1 x2 x2 L5 x1 x2 x3 -> x1 x3 x2 L6 x1 x2 x3 -> x1 (x2 x3) L7 x1 -> x1 L8 x1 -> x1 L9 x1 -> x1 L10 x1 -> x1 L11 x1 -> x1 L12 x1 -> x1 L13 x1 -> x1 L14 x1 -> x1 L15 x1 -> x1 |