通过线性逻辑(长版)在Call-by-Name和Calculi 中按Call-Val-Val-cal-cal-cal-cal-cal-cal-cal-cal-cal-clookic(长版) (Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version))

In each variant of the lambda-calculus, factorization and normalization are two key-properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the lambda-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV. The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

翻译：在每一种羊羔计算模型中,系数化和正常化是表明如何计算结果的两种关键特性。我们没有分别证明呼唤名(CbN)和呼唤量(CbV)变量的系数化/正常化,而是只证明一次,在爆炸计算模型中(由线性逻辑和分包CbN和CbV启发的羊羔计算模型的延伸),然后我们通过翻译将结果转换为CbN和CbV的系数化/正常化。这种方法是稳健的:在向操作员扩展计算器和额外规则以建模一些额外的计算特征时,它仍然坚持不变。