寻观「标准库」之书。
寻观「编译器核心」之「编译步骤」之「求值正则变换」之「统一正则数据」之书。

「：文言：整参入而整数出，无外效方可复用；无外效非必终。汉语：输入须为已验证SSA，且调用处另外证明所有实参都是整数。本分析独立重建整数与布尔种类，不信任结果类型标签；拒绝分配、内存访问、除法与未知操作。结论是条件性的无外部副作用和整数返回，不保证终止，不允许将调用提前到原本不执行的路径。：」
「纯整查函」乃化「字符串」而化「正则模块」而（「或可有」于「正则函数」）也。
「纯整查函」者会「名」而会「诸函」而
  鉴「诸函」而
    有「罄」则「可无」
    或有（「缀」于「函」于「余」）则
      若「串相等」于「名」于（「函」中「零」）则「可有」于「函」否则「纯整查函」于「名」于「余」
也。

「验纯整函数」乃化「正则模块」而化「正则函数」而「爻」也。
「验纯整函数」者会「候选」而会「函」而
  若「或者」
    于（「大于」于（「函」中「四」）于「二五六」）
    于（「大于」于（「长度」授以「整数」于（「函」中「二」））于「八」）则
      「阴」
  否则
    虑「种」者「新数组引用」授以「整数」于「零」于（「函」中「四」）
    而
    虑「好」者「新引用」授以「爻」于「阳」而
    虑「无」者
      「态射」授以「整数」授以「有」
      于（「函」中「二」）
      于（会「号」而「写数组引用」授以「整数」于「种」于「号」于「一」）
    而
    虑「取」者
      （化「正则原子」而「整数」也会「值」而鉴「值」而
          有（「正则局部」于「号」）则
            「读数组引用」授以「整数」
            于「种」于「号」
          或有（「正则整数」于「数」）则「一」
          或有（「正则爻」于「爻值」）则「二」
          或有「其他」则「零」
      ）
    而
    虑「诸整」者
      （化（「列」于「正则原子」）而「爻」也会「参」而「全部符合」授以「正则原子」
        于（会「值」而「等于」于（「取」于「值」）于「一」）于「参」
      ）
    而
    虑「运种」者
      （化「正则操作」而化（「列」于「正则原子」）而「整数」也会「术」而会「参」而鉴「术」而
          有（「正则原语」于「名」）则（
            若「非」于（「且」于（「等于」于（「长度」授以「正则原子」于「参」）于「二」）于（「诸整」于「参」））则
              「零」
            否则
              鉴「名」而
                有『豫言_整数加』则「一」
                或有『豫言_整数减』则「一」
                或有『豫言_整数乘』则「一」
                或有『豫言_整数相等』则「二」
                或有『豫言_整数大于』则「二」
                或有「其他」则「零」
          ）
          或有「正则调用」则（
            鉴「参」而
              有（「缀」于（「正则函数引用」于「名」）于「余」）则（
                鉴（「纯整查函」于「名」于「候选」）而
                  有（「可有」于「往」）则
                    若「且」
                      于（「等于」于（「长度」授以「正则原子」于「余」）于（「长度」授以「整数」于（「往」中「二」）））
                      于（「诸整」于「余」）则
                        「一」
                    否则
                      「零」
                  或有「可无」则「零」
              ）
              或有「其他」则「零」
          ）
          或有「其他」则「零」
      ）而
    递归虑「察段」其化「正则区域」而「整数」者会「段」而
      鉴「段」而
        有（「正则段」于「令们」于「终」）则（
          虑「无」者
            「态射」授以「正则指令」授以「有」
            于「令们」
            于（会「令」而鉴「令」而
              有（「正则运算」于「号」于「类」于「术」于「参」）则（
                虑「果」者「运种」于「术」于「参」
                而
                虑「无」者
                  若「等于」于「果」于「零」则「写引用」于「好」于「阴」否则「元」
                而
                「写数组引用」授以「整数」于「种」于「号」于「果」
              ）
              或有（「正则如果」于「号」于「类」于「条件」于「阳体」于「阴体」）则（
                虑「无」者
                  若「等于」于（「取」于「条件」）于「二」则「元」否则「写引用」
                    于「好」于「阴」
                而
                虑「阳种」者「察段」于「阳体」
                而
                虑「阴种」者「察段」于「阴体」
                而
                虑「果」者
                  若「等于」于「阳种」于「阴种」则「阳种」否则「零」
                而
                虑「无」者
                  若「等于」于「果」于「零」则「写引用」于「好」于「阴」否则「元」
                而
                「写数组引用」授以「整数」于「种」于「号」于「果」
              ）
              或有「其他」则
                「写引用」于「好」于「阴」）
          而
          鉴「终」而
            有（「正则产出」于「值」）则「取」于「值」
            或有「其他」则（虑「无」者「写引用」于「好」于「阴」而「零」）
        ）
    而
    虑「果」者「察段」于（「函」中「三」）而
    「且」于（「读引用」于「好」）于（「等于」于「果」于「一」）
也。

「：文言：候选自全而削，互递同验，未定则尽拒。汉语：求封闭的整数函数集合，删除含未知操作的函数及所有依赖者；支持互递归。达到迭代预算仍未收敛则返回空集，不发布暂定证明。调用者不得单独把一次验纯整函数的假设检查当作最终证明。：」
「求纯整闭包」乃化「正则模块」而「正则模块」也。
「求纯整闭包」者会「诸函」而
  递归虑「收」其化「整数」而化「正则模块」而「正则模块」者会「轮」而会「候选」而
    若「大于」于「轮」于「三二」则
      「罄」
    否则
      虑「余」者
        「滤」授以「正则函数」
        于（会「函」而「验纯整函数」于「候选」于「函」）于「候选」
      而
      若「等于」于（「长度」授以「正则函数」于「余」）
      于（「长度」授以「正则函数」于「候选」）则「余」
      否则
        「收」于（「加」于「轮」于「一」）于「余」
  而
  「收」于「零」于「诸函」
也。
