轻型逻辑分层记法的安全递归
Safe Recursion on Notation into a Light Logic by Levels
摘要：
我们嵌入安全递归记法（SRN）到轻仿射逻辑的水平（LALL），来自逻辑L4。LALL是一个直观的演绎系统，具有多项式时间割消策略。嵌入允许将SRN的每个项t表示为LALL中的证明网族|t| ^l。族中的每个证明网|t| ^l在其位长度由整数l限制的参数上模拟t。嵌入基于两个关键特征。一种是LALL中的递归类型，它将Scott二进制数字（即Scott单词）编码为证明网。斯科特词代表t的参数，而不是更标准的丘奇二进制数。此外，嵌入利用LALL从L4继承的段落框的“模糊”边界来“自由”复制t的参数，特别是安全的参数。最后，|t| ^l的类型取决于用于定义t的复合和递归方案的数量，即t的结构复杂度。此外，|t| ^l的大小是l中的多项式，其次数取决于t的结构复杂度。因此，这项工作使SRN所依赖的谓词递归理论原则和基于Light Linear Logic的证明理论原则（称为/分层/）更加接近。
英文摘要：
We embed Safe Recursion on Notation (SRN) into Light Affine Logic by Levels (LALL), derived from the logic L4. LALL is an intuitionistic deductive system, with a polynomial time cut elimination strategy. The embedding allows to represent every term t of SRN as a family of proof nets |t|^l in LALL. Every proof net |t|^l in the family simulates t on arguments whose bit length is bounded by the integer l. The embedding is based on two crucial features. One is the recursive type in LALL that encodes Scott binary numerals, i.e. Scott words, as proof nets. Scott words represent the arguments of t in place of the more standard Church binary numerals. Also, the embedding exploits the "fuzzy" borders of paragraph boxes that LALL inherits from L4 to "freely" duplicate the arguments, especially the safe ones, of t. Finally, the type of |t|^l depends on the number of composition and recursion schemes used to define t, namely the structural complexity of t. Moreover, the size of |t|^l is a polynomial in l, whose degree depends on the structural complexity of t. So, this work makes closer both the predicative recursive theoretic principles SRN relies on, and the proof theoretic one, called /stratification/, at the base of Light Linear Logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
