构造性算术中基于证明提取的数论算法——Minlog中的实现与形式化

《Annals of Pure and Applied Logic》：Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives

　　

摘要：研究人员在构造性数学(constructive mathematics)与证明辅助工具Minlog框架下，基于Curry-Howard对应(即程序提取program extraction)，将经典数论谓词(divisibility、primality等)重新形式化为具计算意义的构造性公式，并从已证明定理中提取出可执行的数论算法——包括整除性测试、最大公约数(Greatest Common Divisor, gcd)、Fermat因式分解(Fermat factorization)及素数判定(primality test)。研究表明，借助正二进制数(positive binary numbers, P)及其区间套算子(ν-operator, PosMonMax)可实现比传统自然数一元编码更高效的算法：二进制Stein gcd算法时间复杂度为O(max(poslog(p),poslog(q))2)，优于自然数Euclidean算法的O(max(n,m))；基于ν-operator的下取整平方根(PosSqrt ?√p?)配合快速迭代版本(FastSqrt)可高效支撑因数分解。所有定义、引理及主定理均于Minlog内完全形式化并机械验证正确性(soundness theorem)，证实程序提取可自严格构造性证明直接产出经形式化保证的正确算法实现。

本文发表于《Annals of Pure and Applied Logic》，针对构造性逻辑与证明辅助系统Minlog中数论算法形式化及程序提取(program extraction)的研究空白，指出现有数论算法多基于经典逻辑或非形式化实现，缺乏从构造性证明中提取并保证正确性的系统方法；而传统自然数 unary 表示导致提取算法效率低下。研究人员以Minlog为平台，重新定义自然数与正二进制数(positive binary numbers, P)上的基本运算(有界存在量词?^<、最小元算子μ_<(NatLeast)、单调极大算子ν(PosMonMax))，给出下取整/上取整平方根(PosSqrt ?√p?、NatSqrt ?√n?)、整除关系(NatDiv/PosDiv定义为gcd(p,q)=p)、最大公约数(Euclidean gcd于N、二进制Stein gcd于P)及其Bézout等式的形式证明，进而从合数存在性证明中提取Fermat因式分解算法、从素数特征命题提取试除法及最小因子素数判定算法，所有提取代码经Minlog展开为Haskell并附运行耗时实测。关键结论为：正二进制数表示配合区间套算子ν可使gcd达二次复杂度、平方根达拟三次复杂度，显著优于自然数版本；提取算法与手工实现等价且经Minlog内置可靠性定理(soundness theorem)保证正确。

主要关键技术方法如下：① 有界存在量词?^<n(ExBNat)与?^≤p(ExBPos)及最小元搜索算子μ_<n(NatLeast)，将非计算性弱存在转化为计算性存在；② 正二进制数(P)上的单调极大/区间套算子ν(PosMonMax)，以O(poslog(p)/2+1)步二分逼近满足单调布尔函数wf(q)的最大p；③ 平方根双定义——自然数上取整NatSqrt ?√n?(μ-算子)与正二进制数下取整PosSqrt ?√p?(ν-算子)及快速迭代版FastSqrt；④ 整除性PosDiv定义为gcd(p,q)=p，gcd于N用Euclidean递归、于P用Stein算法(S₀/S₁尾剥离+相减)；⑤ 从"合数??a,b. n=a·b ∧ 1<a≤b<n"构造性证明提取Fermat因数分解，从"素数?只有1与n整除n"提取试除与最小素因子判定。

研究结果总结如下：

3. Basic Definitions（第3节基本定义）：定义自然数上有界存在量词?^<n、正二进制数上有界存在量词?^≤p、最小搜索算子μ_<n(NatLeast)及正二进制数区间套/单调极大值算子ν(PosMonMax)。通过Lemma 4证明μ-算子可将非计算性弱存在?^nc转为计算性存在?^cr。给出自然数上取整平方根NatSqrt ?√n?（定义5）与正二进制数下取整平方根PosSqrt ?√p?（定义6，ν-算子）、快速迭代平方根FastSqrt（定义7），并证Lemma 6–8表明PosSqrt与FastSqrt等价且满足m·m≤p<m+1·m+1。

4. Divisibility and Greatest Common Divisor（第4节整除与最大公约数）：定义自然数整除NatDiv为?l<n+1. l·m=n（定义8），正二进制数整除PosDiv(p|q) := gcd(p,q)=p（定义11）。自然数gcd用经典Euclidean递归（定义9），正二进制数gcd用Stein算法——偶数Strip S₀后缀剥离、奇数时作差（定义10）。证Lemma 9给出NatDiv?乘积等价，Lemma 11给出PosDiv?乘积等价，Lemma 12–13证整除为偏序且具有加/乘保持性，Lemma 14证gcd同时整除两元且被任一公因子整除（最大性），Theorem 1–2证N与P上的Bézout型线性组合等式（无负数，移项至同侧）。

5. Formal Proofs and Program Extraction for Elementary Number Theory（第5节基础数论形式证明与程序提取）：形式化证明"n为合数 ? ?a,b. 1<a≤b<n ∧ n=a·b"，从该构造性证明提取Fermat因式分解算法(et(M)=λn. let s=FastSqrt(n); loop x from s down to 2 ... ); 形式化"素数 ? ?k. 1<k<n → ?(k|n)"，提取试除素数判定及最小素因子求解算法。给出Minlog中完整proof term M及其提取Haskell代码，实测NatDiv判除耗时为线性、Stein gcd万位数字<1 s、PosSqrt万位可行而FastSqrt受内存限制。

6. Discussion / Conclusion（第6节讨论与结论）：译文——"研究人员展示了如何在Minlog中基于构造性证明之程序提取开发数论算法形式化库。借由正二进制数(P)表示及高效区间套算子ν，所得算法（Stein gcd、基于ν的平方根、Fermat分解、试除素数判定）较自然数一元表示版本显著更高效。所有算法源自经形式验证的构造性证明，其正确性由Minlog可靠性定理保证——提取项et(M)满足realizer predicate A^r(et(M))。未来工作含扩展至模算术、中国剩余定理及概率素数测试之提取。库已开源发布。"