"Linear two-sorted arithmetic" (Helmut Schwichtenberg)

Bellantoni and Cook (1992) characterized the polynomial-time functions by the primitive recursion schemes, with a semicolon separating the variables into two kinds. The first ``normal'' ones control the length of recursions, and the second ``safe'' ones mark the places where substitutions are allowed. We extend this distinction to variables of higher type, and formulate a theory LRA all of whose provable recursions are polynomially bounded.
To achieve this, we need the logic to be linear and the corresponding term system LRT to have a linearity restriction on higher type safe variables (joint work with Karl-Heinz Niggl and Steve Bellantoni).

多項式時間計算可能な関数を特徴付ける Linear Atrithmetic (LA) を高階化して、Bellantori, Niggle らと LTを導入した（LAとLTの関係は、Heyting Arithmetic HA とゲーデルの T の関係と同じ）。