User:Alemagno12/Translation maps for SSS: Difference between revisions
Jump to navigation
Jump to search
Content added Content deleted
Alemagno12 (talk | contribs) m (Formatting) |
Alemagno12 (talk | contribs) No edit summary |
||
| Line 1: | Line 1: | ||
Here are some |
Here are some translation maps between SSS and BM2.3, alongside their proofs. |
||
For a BM2.3 or SSS expression X, o<sub>BM2.3</sub>(X) or o<sub>SSS</sub>(X) is the order type of all possible standard expressions below it under expansion; for BM2.3, this is guaranteed to be an ordinal by [https://arxiv.org/abs/2307.04606 <nowiki>[Yto2023]</nowiki>]. ES is the empty string/matrix, + is string/matrix concatenation, X*k = X+X+X+...+X k times for some natural number k, and > is ordering by expansion. |
|||
TODO: Prove that lexicographic ordering is equivalent to expansion for SSS. This is already proven for BM2.3 in <nowiki>[Yto2023]</nowiki> |
|||
== Up to \(\varepsilon_0\) == |
== Up to \(\varepsilon_0\) == |
||
<b>Lemma 1.</b> Assume that o<sub>SSS</sub>(X) = o<sub>BM2.3</sub>(X') and o<sub>SSS</sub>(Y) = o<sub>BM2.3</sub>(Y') for some standard X,X',Y,Y'. Then, o<sub>SSS</sub>(X+(0)+Y) = o<sub>BM2.3</sub>(X'+Y'). |
|||
Define a function Prune : Term(SSS) -> Term(SSS) inductively as follows: |
|||
* Prune(ES) = ES |
|||
<i>Proof.</i> By induction on Y. Zero and successor cases are trivial. For the limit case, let Z < Y and o<sub>SSS</sub>(Z) = o<sub>BM2.3</sub>(Z'). |
|||
* Prune((A,0)) = (Prune(A),0) |
|||
* Prune((A,0,B,1)) = (Prune(A),0,B), where B >= 1 |
|||
* BM2.3 does not have any "stop at the leftmost element if you can't find the bad root" condition, so the bad root of X'+Z' is the bad root of Z', and o<sub>BM2.3</sub>(X'+Z') = sup<sub>n<ω</sub>(o<sub>BM2.3</sub>(X'+exp(Z',n))). |
|||
* Otherwise, Prune(A) doesn't exist. |
|||
* For SSS, if the second bad root check finds a bad root in Z, the bad root of X+(0)+Z is the bad root of Z. If it does not find a bad root, then since the first bad root must be at least (0,1) and every standard expression starts with 0, (0)+Z = (0,0)+W for some W < (0,1) <= bad root; |
|||
Define a function Shift : Term(PrSS) -> Term(PrSS) inductively as follows: |
|||
* Shift(ES) = ES |
|||
* Shift((A,k)) = (Shift(A),k+1) |
|||
i.e. Shift(A) is the result of adding 1 to all the elements in A. |
|||
WIP |
|||
Define a function Map : Term(SSS) -> Term(PrSS) inductively as follows: |
|||
* Map(ES) = ES |
|||
* Map((A,0)) = (Map(A),0) |
|||
* Map((0,A)) = I'll finish this later, also maybe a more algorithmic approach would be better? E.g first turn all (0,1^k)s into (k)s, then add inbetween elements |
|||
Latest revision as of 05:41, 13 November 2023
Here are some translation maps between SSS and BM2.3, alongside their proofs.
For a BM2.3 or SSS expression X, oBM2.3(X) or oSSS(X) is the order type of all possible standard expressions below it under expansion; for BM2.3, this is guaranteed to be an ordinal by [Yto2023]. ES is the empty string/matrix, + is string/matrix concatenation, X*k = X+X+X+...+X k times for some natural number k, and > is ordering by expansion.
TODO: Prove that lexicographic ordering is equivalent to expansion for SSS. This is already proven for BM2.3 in [Yto2023]
Up to \(\varepsilon_0\)[edit | edit source]
Lemma 1. Assume that oSSS(X) = oBM2.3(X') and oSSS(Y) = oBM2.3(Y') for some standard X,X',Y,Y'. Then, oSSS(X+(0)+Y) = oBM2.3(X'+Y').
Proof. By induction on Y. Zero and successor cases are trivial. For the limit case, let Z < Y and oSSS(Z) = oBM2.3(Z').
- BM2.3 does not have any "stop at the leftmost element if you can't find the bad root" condition, so the bad root of X'+Z' is the bad root of Z', and oBM2.3(X'+Z') = supn<ω(oBM2.3(X'+exp(Z',n))).
- For SSS, if the second bad root check finds a bad root in Z, the bad root of X+(0)+Z is the bad root of Z. If it does not find a bad root, then since the first bad root must be at least (0,1) and every standard expression starts with 0, (0)+Z = (0,0)+W for some W < (0,1) <= bad root;
WIP