查看“︁TON记号”︁的源代码


== 合法表达式 ==
常量包含<math>0,\Omega_n</math>。

* 常量是合法表达式；
* 如果<math>a</math>和<math>b</math>是合法表达式，那么<math>C(a,b)</math>是合法表达式。

== 后缀形式 ==
对于一个合法表达式，我们删去它其中的所有<math>,</math>与<math>()</math>，并反转整个字符串，即为该表达式的后缀形式。

== 比较 ==
对于两个合法表达式，它们的大小关系等同于它们的后缀形式在字典序上的大小关系（我们认为<math>C<0<\Omega_n</math>）。

== 标准表达式 ==

* 常量是合法表达式；
* <math>C(a,b)</math>是标准表达式当且仅当：
** <math>a,b</math>是标准表达式；
** 如果<math>b</math>能表示成<math>C(c,d)</math>的形式，则<math>a\leq c</math>；
** 对于不同的版本，还有一些额外的条件，我们一般称其为 built-from-below 条件。

为了检查 built-from-below 条件，我们需要遍历某些表达式的语法树，为此，我们需要一些辅助定义：

* 位于不同位置的同类型的项被认为是不同的；
* 对于一个表达式<math>C(a,b)</math>，我们称<math>a</math>和<math>b</math>是<math>C(a,b)</math>的子项，记作<math>a,b\sqsubseteq C(a,b)</math>；
* 我们称a是b的真子项（记作<math>a\sqsubset b</math>），当且仅当<math>a\sqsubseteq b\land a\neq b</math>。

== 与序数的关系 ==
TON 中的标准表达式和序数一一对应。具体的，对于一个标准表达式<math>a</math>，如果有一系列小于它的表达式<math>b_1,b_2\cdots</math>，则<math>a</math>对应的序数为<math>b_1,b_2\cdots</math>对应的序数的上确界。

== 性质 ==

* <math>C(a,b)>b</math>；
* <math>C(a,b)</math>对<math>a,b</math>都单调递增，且对<math>a</math>连续；
* <math>C(a,b)=b+\omega^a</math>当且仅当<math>C(a,b)\geq a</math>。

== 变种 ==
以下判定条件中涉及到的项<math>x</math>默认满足<math>x\sqsubseteq a</math>。

=== Built-from-below 风格 ===
有三种 built-from-below 风格：Degrees of Reflection 风格，标准风格与 Iteration 风格（从弱到强排序）。

==== Degrees of Reflection 风格 ====
为了检查<math>C(a,b)</math>是否标准，built-from-below 条件为<math>a\prec C(a,b)</math>，其定义为：

<math>\forall x\forall y\sqsubset x(x<y<\Omega\Rightarrow</math>

Degrees of Reflection（DR）仅由 Degrees of Reflection 风格判定标准表达式。

==== 标准风格 ====
为了检查  是否标准，built-from-below 条件为 ，其定义为：

* ；
* 。

Main Ordinal Notation System（M）是一系列系统，仅由标准风格判定标准表达式，其中的  可任取  的自然数，分别对应不同的系统。

==== Iteration 风格 ====
为了检查  是否标准，我们需要找出  的语法树中所有极长的  的子项 （即，找出所有  满足 ），然后，我们按以下步骤对每个  求出对应的 ：

# 将  中的  改成 ；
# 将  改写成前缀形式（直接删去所有  和 ）；
# 删去  对应的  左侧的全部内容，并在左侧添加  使表达式合法；
# 将  重新改写回一般形式。
# 对  所有形如  的项，如果 ，就将其替换为 ，一直替换到没有这样的项；
# 执行完 1~5 步后，将现在的  记作 ；
# 记  为初始的  和  的最长公共后缀（前缀形式下）；
# 则  为最大的自然数  使得  的前缀形式形如 。

该风格的 built-from-below 条件为 对所有 ，都有 ，其定义如下：

* ；
* 。

Iteration of n-built from below (variation without 4b)（I）仅由 Iteration 风格判定标准表达式。

=== Passthrough ===
Passthrough 有三种类型：无 passthrough，-passthrough 与 -passthrough（从弱到强排序）。

==== -passthrough ====
-passthrough 可以和 Iteration 风格组合，这就是 Iteration of n-built from below（IBP）。 的定义和无 passthrough 的情况一样，但 built-from-below 条件不同：为检查  是否标准，该风格的 built-from-below 条件为 对所有 ，都有 ，其定义如下：

* 我们定义辅助函数 ：，下同；
* ；
* 。

-----passthrough 也可以和 Degrees of Reflection 风格组合，这就是 Built-from-below with Passthrough（BP）。其定义和其他变种有较大不同，见下：

合法表达式：

* 是合法表达式；
* 如果  是合法表达式，则  是合法表达式。

比较：

是最小的表达式。 当且仅当 。

标准表达式：

* 是标准表达式；
* 是标准表达式当且仅当：
** 是标准表达式；
** 如果  可以表示成  的形式，则 ；
** 该系统的 built-from-below 条件为：，其中  的定义为 。

-----passthrough 不能和标准风格组合。

==== -passthrough ====
-passthrough 可以和 Iteration 风格组合，这就是 Iteration of n-built from below (Possible extension)（IP）。其定义几乎与 IBP 一样，除了 built-from-below 条件，它变成了 对所有 ，都有 。
-----passthrough 也可以和 Degrees of Reflection 风格组合，这就是 Degrees of Reflection with Passthrough（DRP）。为检查  是否标准，built-from-below 条件为 ，其定义为
-----passthrough 还可以和标准风格组合，这就是 Main ordinal notation system (Passthrough extension)（MP）。和 Main ordinal notation system 类似，它也是一系列系统的组合。我们需要确定一个  的自然数 ，则 built-from-below 条件为 ，其定义为

* ；
* 。

=== 反射配置 ===
反射配置从底层重新定义了 built-from-below 条件。

==== 语法 ====
在反射配置下的 TON 中，表达式会出现一个新的符号 。其余部分和普通的 TON 一样。

比较和普通的 TON 类似，我们认为 。

==== 定义 ====
反射配置由两个项来定义，记作 。以下是反射配置的一个递归定义：

* ；
* ；
* 我们设 ，则：
** 若 ：；
** 若 ：；
** 若  且 ：；
** 若  且 ：。

----反射配置可以和 Degrees of Reflection 风格组合（即 Reflection configuration version of Degrees of Reflection（DRC））。为了检查  是否标准，其 built-from-below 条件为：

* 我们定义  为满足  的项 ，如果不存在这样的 ，则 ；
* 对于项 ，我们定义 。

----反射配置也可以和带 Passthrough 的 Degrees of Reflection 风格组合（即 Reflection configuration version of Degrees of Reflection with Passthrough（DRPC），注意这里不分 -passthrough 和 -passthrough）。为了检查  是否标准，其 built-from-below 条件为：
----反射配置可以和标准风格（与 -passthrough）组合，同样的，它是一系列记号的组合。你需要确定一个自然数 ，则为了检查  是否标准，反射配置和标准风格的组合（即 Reflection configuration version of Main Ordinal Notation System（MC））的 built-from-below 条件为 ，而反射配置和带 -passthrough 的标准风格的组合（即 Reflection configuration version of Main ordinal notation system (Passthrough extension)（MPC））的 built-from-below 条件为 。 的定义如下：

* ；
* ；
* 我们定义  为满足  的项 ，如果不存在这样的 ，则 ；
* ；
* 我们称 ，当且仅当 ；
* 我们称 ，当且仅当 。
{{默认排序:序数记号}}
[[分类:页面待更改]]
[[分类:记号]]