查看“︁iBLP”︁的源代码

== 记号简介 ==
无限基本Laver图案(Infinite Basic Laver Pattern)是由test_alpha0的记号Basic Laver Pattren改造而来。IBLP目前尚不理想，还存在许多的坏图案，test_alpha0规定其极限表达式为(1,0)1(2,1,0)1(3,2,1,0)2(4,3,2)1(5,4,3,2)2(6,5,4)1。尽管如此，IBLP仍然被认为是目前最强的记号。本页面介绍的规则对应[https://hypcos.github.io/notation-explorer/ NE]上的DEN2。

== 定义 ==

=== 定义1 （IBLP） ===
一个IBLP是一个四元组<math>A=(n,(A_1,\dots,A_n),(l_1,\dots,l_n),(M_1,\dots,M_n))</math>，

其中：

<math>(1)n\in\N</math>。

<math>(2)</math>对每个<math>i\in\{1,\dots,n\}</math>，<math>A_i</math>是严格递增的非负整数序列，满足<math>\mathrm{len}(A_i)\geq2\text{且}\max(A_i)=i</math>。

<math>(3)</math>对每个<math>i\in\{1,\dots,n\}</math>，步长<math>l_i\in \N</math>。

<math>(4)</math>对每个<math>i\in\{1,\dots,n\}</math>，标记集合<math>M_i\subseteq A_i</math>

约定所有编号从 1 开始；<math>A_i[k]</math> 表示第 ''k'' 个元素，<math>A_i[-j]=A_i[\mathrm{len}(A_i)-j+1]</math>表示倒数第 ''j'' 个元素。

=== 定义2 （长行、中等行、短行） ===
行 <math>i</math> 称为长行若<math>\mathrm{len}(A_i)>2l_i</math>，称为中等行若<math>\mathrm{len}(A_i)=2l_i</math>，称为短行若 <math>\mathrm{len}(A_i)<2l_i</math>。

=== 定义3 （零图案、后继图案、极限图案） ===
若 ''n'' = 0，称 ''A'' 为零图案。若 <math>n>0\text{且}\mathrm{len}(A_n)=2\text{且}\min(A_n)=0</math>，称 ''A'' 为后继图案。否则称 ''A'' 为极限图案。

=== 定义4 （行比较键） ===
令<math>A_i=(A_1<a_2<\dots<a_m)\text{且}L=l_i</math>。定义保留序列

<math>K_i=\begin{cases}(a_1,a_2,\dots,a_m),&L\leq1;\\(a_1,a_{L+1},a_{L+2},\dots,a_m),&2\leq L\leq m;\\(a_1,a_2,\dots,a_m),&L\geq2\text{且}m<L.\end{cases}</math>

定义行键为<math>\overleftarrow{K_i}</math>（即<math>K_i
</math>逆序，从大到小）。

=== 定义5 （IBLP的大小比较） ===
给定两个 ''IBLP'' <math>A\text{、}B</math>，从 <math>i=1</math> 起逐行比较其

行键<math>\overleftarrow{K_i(A)}\text{与}\overleftarrow{K_i(B)}</math> 的字典序；第一处不同决定大小。若前<math>\min(n_a,n_b)</math>行都相等，则行数较小者更小。

=== 定义6 （一行的根<math>p(i)</math>） ===
对<math>i\in\{1,\dots,n\}</math>，定义<math>p(i)=A_i[-(l_i+1)]</math>.

=== 定义7 （传递序列<math>tr_i(j)</math>） ===
固定行 ''i''。若<math>j=A_i[k](1\leq k\leq\mathrm{len}(A_i))\text{且}k\geq l_i</math>，定义阈值 <math>\theta=A_i[k-l_i]</math>。令 <math>t_0=j</math>，并在<math>t_m>\theta\text{且}p(t_m)\text{有定义}</math>时令 <math>t_{m+1}=p(t_m)</math>。若存在最小 <math>m>0</math>使<math>t_m=\theta</math>，则定义<math>tr_i(j)=(t_0,t_1,\dots,t_m)</math>''，''否则称 <math>tr_i(j)</math> 无定义。若 <math>k\leq l_i</math>，亦称无定义。

=== 定义8 （部分函数<math>f_A</math>） ===
设 ''A'' 非零且有至少1行。令 <math>a_1=A_n[1]=\min(A_n)\text{，}L=l_n\text{，}p=p(n)=A_n[-(L+1)]</math>。定义部分函数 <math>f_A:\N\rightharpoonup\N</math>：

<math>(1)</math>若<math>x<a_1</math>，则<math>f_A(x)=x</math>；

<math>(2)</math>若<math>x=A_n[k]\text{且}x<p\text{且}k+L\leq\mathrm{len}(A_n)</math>，则<math>f_A(x)=A_n[k+L]</math>；

<math>(3)</math>若<math>x\geq p</math>，则<math>f_A(x)=x+n-p</math>；

<math>(4)</math>其余情形 <math>f_A(x)</math> 无定义。

=== 定义9 （copy 的行与步长） ===
设 ''A'' 行数为<math>n\geq1</math>，令 <math>p=p(n)</math>。若 copy 过程中出现 <math>f_A(x)</math> 无定义，则<math>copy(A)</math>无定义。否则定义 <math>A'=copy(A)</math> 行数为 <math>n'=2n-p</math>，满足：

<math>(1)</math>对<math>1\leq i\leq n-1\text{：}A_i'=A_i\text{，}l_i'=l_i\text{，}M_i'=M_i</math>；

<math>(2)</math>对每个<math>i\in\{1,\dots,n-p+1\}</math>，令源行<math>\sigma=p+i-1</math>，目标行<math>\tau=n-1+i</math>''i''，定义<math>A_\tau'=\mathrm{sort}(\{f_A(x)|x\in A_\sigma\})\text{，}l_\tau'=l_\sigma</math>，要求<math>\forall x\in A_\sigma\text{，}f_A(x)\text{有定义}</math>。

=== 定义10 （copy的标记过滤） ===
延续上一定义。对目标行<math>\tau</math>中元素<math>x\in A_\tau'</math>，令

<math>y\in A_\sigma</math>为其唯一来源（即 <math>f_A(y)=x</math>）。则 <math>x\in M_\tau'</math> 当且仅当：

<math>y\in M_\sigma</math>，并且满足下列之一：

* <math>tr_\sigma(y)</math>有定义且<math>tr_\sigma(y)[-2]\geq p</math>；
* 令<math>y_0</math>为<math>tr_\sigma(y)</math>中首次出现的<math><p</math>的元素（等价于“最大的
<math><p</math>的元素”）。要么<math>y_0<a_1</math>；要么存在 ''k'' 使<math>y_0=A_n[k]\text{且}k+L\leq\mathrm{len}(A_n)\text{且}A_n[k+L]\in M_n</math>，并且若 ''x'' 在 <math>A_\tau'</math>中的位置  为 ''q''（从 1 开始），则当 <math>q+1-l_\sigma\geq1</math> 时需满足<math>A_\tau'[q+1-l_\sigma]\leq a_1.</math>

=== 定义11 （E(A,0)） ===
若 ''A'' 非零且 ''n ≥'' 1，则 ''E''(''A,'' 0) 为删除最后一行后的图案（行数变为 ''n −'' 1，其余行、步长、标记保持不变）。

=== 定义12 （''E''(''A, m'')的copy阶段 (''m≥1)''） ===
设A是极限图案。令<math>A^{(0)}=A</math>。若第一次<math>copy(A^{(0)})</math> 无定义，则称 ''A'' 为坏图案并定义<math>E(A,m)=E(A,0)</math>。否则定义

<math>A^{(1)}=copy(A^{(0)}),A^{(2)}=copy(A^{(1)}),\dots,A^{(m)}=copy(A^{(m-1)})</math>,

并令<math>B=E(A^{(m)},0)</math>

接下来对B做补全，初始行号 <math>r=n</math>（这里 ''n'' 为原始 ''A'' 的行数）。补全过程允许使用临时记录映射 <math>\rm Rec</math>（行号 <math>\mapsto</math> 有限序列），结束后丢弃。

=== 定义13 （标记补全） ===
固定当前行 ''r''。令<math>\mathcal{B}=\{b\in M_r|b\in A_r\}</math>并按升序枚举其元素<math>b_1<b_2<\dots<b_k</math>（该集合在本轮开始时冻结，新产生标记不加入本轮）。对每个 <math>b_i</math>依次：

<math>(1)</math>若 <math>tr_i(b_i)</math>无定义则跳过；

<math>(2)</math>令<math>t=tr_r(b_i)[-2]</math>。若<math>\mathrm{Rec}(t)</math>不存在或为空则跳过，否则记 <math>s=\mathrm{Rec}(t)</math>；

<math>(3)</math>若对所有<math>j=3,4,\dots,\mathrm{len}(tr_r(b_i))</math>都有<math>tr_r(b_i)[-j+1]+1\in A_{tr_r(b_i)[-j]}</math>，那么把s 及<math>b_i+1,b_i+2,\dots,b_i+\mathrm{len}(s)</math> 加入 <math>A_r</math>，并重新排序去重使

之严格递增。更新标记：''s'' 中元素不标记，<math>b_i+1,b_i+2,\dots,b_i+\mathrm{len}(s)</math> 全标

记，其余标记保留（按上述规则修正）。更新步长：<math>l_r=l_r+len(s)</math>。

=== 定义14 （原生补全） ===
固定当前行 ''r''。若<math>A_r</math>为长行，则原生补全不执行并返回 0。否则令<math>p_r=p(r)=A_r[-(l_r+1)]\text{，}a=A_r[-l_r]</math>.

构造序列 ''s''：令 <math>u_0=a</math>，并在<math>A_{u_m}[-2]</math> 存在且 <math>>p_r</math> 时令 <math>u_{m+1}=A_{u_m}[-2]</math>并把 <math>u_{m+1}</math> 追加到 ''s''，直至无法继续。令 <math>t=\mathrm{len}(s)</math>。若 <math>t=0</math> 返回 0；若<math>t>0</math>，令 <math>\mathrm{Rec}(r)=s</math> 并继续：

<math>(1)</math>在 ''r'' 后插入 ''t'' 行，使原本行号 <math>>r</math> 的行号整体加 ''t''；

<math>(2)</math> 仅对原本行号 <math>>r</math>的那些行，在其中把所有 <math>>r</math> 的元素加 ''t''，并同步

标记集合，步长不变；

<math>(3)</math>令旧行及旧步长为 <math>A_r^{old},l_r^{old}</math>。将旧行替换为 ''t'' + 1 行：

<math>A_{r+t}=\mathrm{sort}(A_r^{old}\cup s\cup\{r+1,r+2,\dots,r+t\})\text{，}l_{r+t}=l_r^{old}+t</math>.

标记规则：除s和r+t外均标记。

<math>(4)</math>对<math>i=t,t-1,\dots,1</math>，由<math>A_{r+i}</math>构造 <math>A_{r+i-1}</math>：删除元素<math>r+i</math>，并删除元素 <math>A_{r+i}[-l_{r+i}]</math>，去除<math>r+i-1</math> 的标记，并令 <math>l_{r+i-1}=l_{r+i}-1</math>。

<math>(5)</math>'''中等行例外：'''若<math>i=t</math> 且 ''<math>A_r^{old}</math>''为中等行，则在构造 <math>A_{r+i-1}</math> 时不删除 <math>A_{r+i}[-l_{r+i}]</math>且不减步长（令 <math>l_{r+i-1}=l_{r+i}</math>），但仍删除 <math>r+i</math> 并去除<math>r+i-1</math> 的标记。

原生补全返回t。

=== 定义15 （补全主循环(用于 ''E''(''A, m''))） ===
令初始<math>r=n</math>（''n'' 为原始 ''A'' 的行数）。当 ''r'' 不超过当前 ''B'' 的行数时循环：先对行 ''r'' 执行标记补全，再执行原生补全得到 ''t''，然后更新 <math>r=r+t+1</math>。当 ''r'' 越界时补全结束，丢弃 <math>\rm Rec</math>，所得 ''B'' 即为<math>E(A,m)</math>。
[[分类:记号]]