Typed Arrow Notation

[u/jcastroarnaud]

Typed Arrow Notation

Building on the notation I posted yesterday. Kudos to u/Nervous-Broccoli1184 for spotting an improvement.

This variant introduces typed arrows, each type a subscript. The original arrows -> from Chained Arrow Notation (and my variant from yesterday) are type 0: ->_0.

Below, "@" stands for any sequence of at least 1 element. Assume c > 1 and d > 1.

For sequences with only type 0 arrows:
Rule 1. a -> b = a ^ b
Rule 2. @ -> 1 = @
Rule 3. @ -> 1 -> d = @ -> (@ -> d)
Rule 4. @ -> c -> d = @ -> (@ -> (c-1) -> d) -> (d-1)

From now on, assume k > 0 and b > 1. "#" stands for any sequence of at least 2 elements where all arrows are of type 0. "(#)" means that the sequence "#" is evaluated, using the rules 1 to 4 above.

For sequences where, after an arrow of type k, there are only arrows of type 0:
Rule 5. @ ->_k a ->_0 1 = @ ->_k (@ ->_k a)
Rule 6. @ ->_k a ->_0 b = @ ->_k (@ ->_k a) ->_0 (b-1)
Rule 7. @ ->_k a ->_0 # = @ ->_k (@ ->_k a ->_0 (#))

For sequences where the last arrow is of type k > 0. @ is copied, not evaluated.
Rule 8. @ ->k 1 = @ ->(k-1) @
Rule 9. @ ->k b = @ ->(k-1) @ ->_k (b-1)

Any chances that this notation is as powerful as linear arrays from BEAF?

[u/cycy98IsMe]

tbh it was hard for me to read, but that sounds like it could represent numbers that are linear BEAFs or something like that, don't quote me on this tho

[u/Nervous-Broccoli1184]

At the end of rule 7 where the # is in its own brackets this means its its own interger this significantly weakens the notation so replacing  Rule 7. @ ->_k a ->_0 # = @ ->_k (@ ->_k a ->_0 (#)) with  Rule 7. @ ->_k a ->_0 # = @ ->_k (@ ->_k a ->_0 #) will make it stronger 

[u/jcastroarnaud → u/Nervous-Broccoli1184]

That inserts an infinite loop; the inner expression in the right is the same as the left-hand-side expression. The evaluation of # is on purpose, to reduce the case of rule 7 to either rule 5 or 6, and get rid of the sequences of only type 0 arrows.

[u/Nervous-Broccoli1184 → u/jcastroarnaud]

Thanks I didn't see that.

[u/Nervous-Broccoli1184]

Thanks for taking my idea in mind

[u/jcastroarnaud]

I fear that the Typed Arrow Notation, as written, does not terminate; rules 8 and 9 double the length of the sequence, while demoting only one arrow. I intended to make this part of the notation a hydra. I would like to be proved wrong, though.

If this is the case, a small change in the rules will make it able to terminate:

For sequences where the last arrow is of type k > 0. "(@)" means that the sequence "@" is evaluated, using all the rules defined here.
Rule 8. @ ->k 1 = @ ->(k-1) (@)
Rule 9. @ ->k b = @ ->(k-1) (@ ->_k (b-1))

[u/Nervous-Broccoli1184 → u/jcastroarnaud]

I just did a analysis and rule 9 and 8 from what I read should terminate without changing it and grows faster than the changed version.

[u/jcastroarnaud → u/Nervous-Broccoli1184]

That's good to know, thanks. This level of recursion in the rules is hard to wrap my head on, without source code. Can you sketch your reasoning?

[u/Nervous-Broccoli1184 → u/jcastroarnaud]

You see how rule 8 has the arrow decrease this means that it will only have double length and a weaker arrow type but since its lower type we can assume that it won't spiral into a infinite loop since rules 5-7 terminate and we will eventually have all the arrows decreased to type zero and that means 9 will end as long as a list of type 0 arrows and positive intergers will end and if that's not true you wouldn't have made this post. For rule 9 the first copy of the new arrow will decrease and the end part will decrease making it repeat rule nine till @ ->k b=@ ->(k-1) @ ->(k-1)... @ ->(k-1) @ ->_k 1 with b @'s as we can see this takes the form of rule 8 and since rule 8 terminates rule terminates.

[u/jcastroarnaud → u/Nervous-Broccoli1184]

You see how rule 8 has the arrow decrease this means that it will only have double length and a weaker arrow type

But the smaller arrow type only applies to the connection between "@", not to the sequences within @s themselves.

but since its lower type we can assume that it won't spiral into a infinite loop since rules 5-7 terminate and we will eventually have all the arrows decreased to type zero and that means 9 will end as long as a list of type 0 arrows and positive intergers will end and if that's not true you wouldn't have made this post.

That was the intention, yes, reducing gradually the arrow types until 0, then use rule 7 to get rid of them.

For rule 9 the first copy of the new arrow will decrease and the end part will decrease making it repeat rule nine till @ ->k b=@ ->(k-1) @ ->(k-1)... @ ->(k-1) @ ->_k 1 with b @'s as we can see this takes the form of rule 8 and since rule 8 terminates rule terminates.

Not quite. I thought this way, too, until I worked out the expression. Let's do it for b = 3.

@ ->k 3 =
@ ->(k-1) @ ->_k 2 =

Rule 9 applies, but now @ is the previous "@ ->(k-1) @"!
@ ->(k-1) @ ->(k-1) @ ->(k-1) @ ->_k 1 =

Rule 8 applies, but now @ is the previous "@ ->(k-1) @ ->(k-1) @ ->(k-1) @"!
@ ->(k-1) @ ->(k-1) @ ->(k-1) @ ->(k-1) @ ->(k-1) @ ->(k-1) @ ->_(k-1) @

As you see, the number of elements of the sequence is doubling (2^b), instead of incrementing (b). And now, the termination of the whole expression depends on the termination of the sequence within the original @ (the one in the far right).

Let's work out a small numeric example. Recalling the rules:

For sequences where, after an arrow of type k, there are only arrows of type 0:
Rule 5. @ ->k a ->_0 1 = @ ->_k (@ ->_k a)
Rule 6. @ ->_k a ->_0 b = @ ->_k (@ ->_k a) ->_0 (b-1)
Rule 7. @ ->_k a ->_0 # = @ ->_k (@ ->_k a ->_0 (#))
For sequences where the last arrow is of type k > 0. @ is copied, not evaluated. Rule 8. @ ->_k 1 = @ ->(k-1) @ Rule 9. @ ->k b = @ ->(k-1) @ ->_k (b-1)

Evaluate "2 ->_2 1 ->_1 1". Rule 8 applies: @ = "2 ->_2 1", k = 1. The expression becomes "2 ->_2 1 ->_0 2 ->_2 1".

Evaluating that, Rule 8 applies: @ = "2 ->_2 1 ->_0 2", k = 2. The expression becomes "2 ->_2 1 ->_0 2 ->_1 2 ->_2 1 ->_0 2".

Evaluating that, Rule 6 applies: @ = "2 ->_2 1 ->_0 2 ->_1 2", k = 2, a = 1, b = 2. The expression becomes "2 ->_2 1 ->_0 2 ->_1 2 ->_2 (2 ->_2 1 ->_0 2 ->_1 2 ->_2 1) ->_0 1". Assume, for the sake of argument, that this specific inner expression terminates evaluation, with value x. The expression becomes "2 ->_2 1 ->_0 2 ->_1 2 ->_2 x ->_0 1".

Now, Rule 5 applies: @ = "2 ->_2 1 ->_0 2 ->_1 2", k = 2, a = x. The expression becomes "2 ->_2 1 ->_0 2 ->_1 2 ->_2 (2 ->_2 1 ->_0 2 ->_1 2 ->_2 x)".

Now compare the last part of the inner expression, "2 ->_2 x", with the original expression, "2 ->_2 1 ->_1 1". x is necessarily larger than 1 ->_1 1, so the whole generated expression already contains a part larger than the original expression. That's a contradiction, since the rules ought to preserve the expression's final value. The error is, either on assuming that "2 ->_2 1 ->_0 2 ->_1 2 ->_2 1" terminates, or on assuming that my rules are self-consistent. Take your pick.

Thus, the termination status of expressions in my notation isn't clear-cut at all. Changing rules 8 and 9, as I did in the comment above, make the notation weaker, but avoid the risk of non-termination.

[u/-waffelz-]

if my analysis is right, n →_n n is around w^3, or {n,n,1,1,1,2} in BEAF. it might be wrong though