弱仿射光类型化关于记法上的安全递归是完备的
Weak Affine Light Typing is complete with respect to Safe Recursion on Notation
摘要：
弱仿射轻类型化（WALT）将轻仿射线性公式作为类型分配给系统F的一个子集。WALT是多时间声音：如果一个非线性项M在WALT中有类型，那么M可以用一个多项式成本在给它一个类型的推导的维度上进行计算。评估在重写关系的任何策略下进行，该重写关系是按名称调用和按值调用的beta约简的混合。WALT削弱，即概括，概念“分层的扣除”，共同的一些光系统-这些逻辑系统，来自线性逻辑，以表征一套多项式函数-。一个较弱的分层允许定义一个组合嵌入安全递归符号（SRN）到WALT。事实证明，WALT的表现力比已知的光系统强得多。嵌入通过SRN的子系统的表示。它是通过限制SRN的合成方案只能线性使用其安全变量而得到的。一方面，这表明SRN实际上可以用更原始的结构来重新定义。另一方面，将SRN嵌入到WALT中具有以下两个显著的方面。嵌入所需的每个数据类型都是从头开始表示的，显示了WALT强大的结构证明理论根源。此外，嵌入突出了一个分层结构的正常和安全的参数，通常隐藏在世界的SRN正常/安全变量：少一个参数是“多项不可预测的”，更深，在一个正式的，证明理论的意义上，它是表示内WALT。最后，由于WALT是SRN完备的，它也是多项式时间完备的，因为SRN是。
英文摘要：
Weak affine light typing (WALT) assigns light affine linear formulae as types to a subset of lambda-terms of System F. WALT is poly-time sound: if a lambda-term M has type in WALT, M can be evaluated with a polynomial cost in the dimension of the derivation that gives it a type. The evaluation proceeds under any strategy of a rewriting relation which is a mix of both call-by-name and call-by-value beta-reductions. WALT weakens, namely generalizes, the notion of "stratification of deductions", common to some Light Systems -- those logical systems, derived from Linear logic, to characterize the set of Polynomial functions -- . A weaker stratification allows to define a compositional embedding of Safe recursion on notation (SRN) into WALT. It turns out that the expressivity of WALT is strictly stronger than the one of the known Light Systems. The embedding passes through the representation of a subsystem of SRN. It is obtained by restricting the composition scheme of SRN to one that can only use its safe variables linearly. On one side, this suggests that SRN, in fact, can be redefined in terms of more primitive constructs. On the other, the embedding of SRN into WALT enjoys the two following remarkable aspects. Every datatype, required by the embedding, is represented from scratch, showing the strong structural proof-theoretical roots of WALT. Moreover, the embedding highlights a stratification structure of the normal and safe arguments, normally hidden inside the world of SRN-normal/safe variables: the less an argument is "polyomially impredicative", the deeper, in a formal, proof-theoretical sense, it is represented inside WALT. Finally, since WALT is SRN-complete it is also polynomial-time complete since SRN is.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
