Extraction of Efficient Programs in $I\Sigma_1$-arithmetic

TL;DR

This paper presents a method to extract efficient primitive recursive programs from $Ioldsymbol{ ext{-}}oldsymbol{ ext{Sigma}}_1$-proofs within a logical framework, bridging proof theory and program extraction.

Contribution

It introduces extraction proofs that enable the extraction of efficient primitive recursive programs from $oldsymbol{ ext{Pi}}_2$-specifications in $Ioldsymbol{ ext{-}}oldsymbol{ ext{Sigma}}_1$-arithmetic.

Findings

Extraction proofs produce programs as efficient as hand-coded ones.

Programming constructs align exactly with proof rules, ensuring computational content.

Extension of $Ioldsymbol{ ext{-}}oldsymbol{ ext{Sigma}}_1$-proofs for program extraction.

Abstract

Clausal Language (CL) is a declarative programming and verifying system used in our teaching of computer science. CL is an implementation of, what we call, $\mathit{PR}{+}I\Sigma_1$ paradigm (primitive recursive functions with $I\Sigma_1$-arithmetic). This paper introduces an extension of $I\Sigma_1$-proofs called extraction proofs where one can extract from the proofs of $\Pi_2$-specifications primitive recursive programs as efficient as the hand-coded ones. This is achieved by having the programming constructs correspond exactly to the proof rules with the computational content.