Light affine lambda calculus and polytime strong normalization
Light affine lambda calculus and polytime strong normalization
复制标题
轻仿射 lambda 演算和多时间强归一化
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
K. Terui
中科院分区：
文献类型：
--
作者：
K. Terui
光线线性逻辑（LLL）及其变体，直觉的光仿射逻辑（iLAL）是Poly Time Computitation的逻辑。所有多项式时间函数均可通过这些逻辑的证据来表示（通过证明 - 程序通信），相反，有一种特定的减少（切除）策略，该策略将给定的证据归一化（后者是后者）很可能被称为多时间“弱”归一化定理）。在本文中，我们介绍了一个未经类似的术语演算，称为“光仿射lambda cyculus”（/spl lambda // sub la/），将光逻辑的基本思想推广到一个无限制的框架中。这是对 /spl lambda /-calculus的简单修改，并具有iLal作为类型分配系统。然后，在这种广义的环境中，我们证明了多个降低策略：任何还原策略都会在多项式数量的还原步骤中及其在多项式时间中及其在多项式数量中归一化/spl lambda // sub la/enter（固定深度）（固定深度） 。
Light linear logic (LLL) and its variant, intuitionistic light affine logic (ILAL), are logics of polytime computation. All polynomial-time functions are representable by proofs of these logics (via the proofs-as-programs correspondence), and, conversely, that there is a specific reduction (cut-elimination) strategy which normalizes a given proof in polynomial time (the latter may well be called the polytime "weak" normalization theorem). In this paper, we introduce an untyped term calculus, called the light affine lambda calculus (/spl lambda//sub LA/), generalizing the essential ideas of light logics into an untyped framework. It is a simple modification of the /spl lambda/-calculus, and has ILAL as a type assignment system. Then, in this generalized setting, we prove the polytime "strong" normalization theorem: any reduction strategy normalizes a given /spl lambda//sub LA/ term (of fixed depth) in a polynomial number of reduction steps, and indeed in polynomial time.