An arithmetic for polynomial-time computation

DOI10.1016/J.TCS.2006.03.019MaRDI QIDQ2500489zbMATH OpenOpenAlexFDO

Authors Helmut Schwichtenberg

Publication date 16 August 2006

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2006.03.019

zbMATH Keywords

linear Heyting arithmeticpolynomial-timeramification

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Review text

Constructive proofs theoretically allow for the extraction of correct programs for specifications. This paper is concerned with the feasibility of such methodology. The author defines a restriction of Heyting arithmetic which has the property that all extracted codes are efficient. These restrictions concern the ranges of the terms and the like.

Recommendations

• An arithmetic for non-size-increasing polynomial-time computation
• A weak constructive second-order arithmetic with extraction of algorithms computable in polynomial time
• scientific article; zbMATH DE number 1848310
• A new “feasible” arithmetic
• Extraction and verification of programs by analysis of formal proofs

Cites work

• A new recursion-theoretic characterization of the polytime functions
• A new “feasible” arithmetic
• A syntactical analysis of non-size-increasing polynomial time computation
• An arithmetic for non-size-increasing polynomial-time computation
• Bounded arithmetic for NC, ALogTIME, L and NL
• Elementary arithmetic
• Higher type recursion, ramification and polynomial time
• scientific article; zbMATH DE number 4059391 (Why is no real title available?)
• scientific article; zbMATH DE number 65741 (Why is no real title available?)
• scientific article; zbMATH DE number 176200 (Why is no real title available?)
• scientific article; zbMATH DE number 176206 (Why is no real title available?)
• scientific article; zbMATH DE number 512774 (Why is no real title available?)
• scientific article; zbMATH DE number 512786 (Why is no real title available?)
• scientific article; zbMATH DE number 2079048 (Why is no real title available?)
• scientific article; zbMATH DE number 1848310 (Why is no real title available?)
• scientific article; zbMATH DE number 2110623 (Why is no real title available?)
• scientific article; zbMATH DE number 2242587 (Why is no real title available?)
• Light linear logic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The realm of primitive recursion
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(10)

• Quantum implicit computational complexity
• Extraction and verification of programs by analysis of formal proofs
• An arithmetic for non-size-increasing polynomial-time computation
• Correctness, explanation and intention
• An abstract approach to stratification in linear logic
• Build your own clarithmetic. I: Setup and completeness
• scientific article; zbMATH DE number 1848310 (Why is no real title available?)
• Complexity Analysis by Rewriting
• Introduction to clarithmetic. I
• A weak constructive second-order arithmetic with extraction of algorithms computable in polynomial time

This page was built for publication: An arithmetic for polynomial-time computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2500489)