Polynomially graded logic I. A graded version of system T

摘要

An investigation is made of a logical framework for programming languages which treats requirements on computation resources as part of the formal program specification. Resource bounds are explicit in the syntax of all programs. In a programming language based on this approach, compliance of a program with imposed resource bounds would be assured by verifying the syntactic correctness using a compiler with a static type checking feature. The principal innovation is the introduction of systems of logical inference, called polynomially graded logics. These logics make resource bounds part of every proposition and every deduction. The sample calculus presented is a restriction of Godel's system T to polynomial time resources. It is proved that the numerical functions representable in this calculus are exactly the PTIME functions.