Light affine lambda calculus and polynomial time strong normalization |
| |
Authors: | Kazushige Terui |
| |
Institution: | (1) National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, 101-8430 Tokyo, Japan |
| |
Abstract: | Light Linear Logic (LLL) and Intuitionistic Light Affine Logic (ILAL) are logics that capture polynomial time computation. It is known that every polynomial time function can be represented
by a proof of these logics via the proofs-as-programs correspondence. Furthermore, there is a reduction strategy which normalizes
a given proof in polynomial time. Given the latter polynomial time “weak” normalization theorem, it is natural to ask whether
a “strong” form of polynomial time normalization theorem holds or not. In this paper, we introduce an untyped term calculus,
called Light Affine Lambda Calculus (λLA), which corresponds to ILAL. λLA is a bi-modal λ-calculus with certain constraints, endowed with very simple reduction rules. The main property of LALC
is the polynomial time strong normalization: any reduction strategy normalizes a given λLA term in a polynomial number of reduction steps, and indeed in polynomial time.
Since proofs of ILAL are structurally representable by terms of λLA, we conclude that the same holds for ILAL.
This is a full version of the paper 21] presented at LICS 2001. |
| |
Keywords: | Light logics Lambda calculus Polynomial time |
本文献已被 SpringerLink 等数据库收录! |
|