Extraction and verification of programs by analysis of formal proofs (Q1823656): Difference between revisions

There are various uniform constructions extracting from every constructive proof d of an existence theorem \(\exists y\) A(x,y) a program \(f_ d\) such that \(\forall x\) \(A(x,f_ d(x))\). Realizability interpretations produce \(f_ d\) which can be written in one of the popular programming languages [cf. \textit{N. Nepejvoda}, Dokl. Akad. Nauk SSSR 239, 526-529 (1978; Zbl 0392.68004)].The size of \(f_ d\) is a low degree polynomial of the size of d. Another program extraction method is normalization of d. Substituting number n for a variable x in d, normalizing and taking the final (\(\exists)\)- introduction A(n,m)/(\(\exists y)A(n,y)\) one puts \(f_ d(n)=m\). It is known [\textit{M. Hagiya}, Rubl. Res. Inst. Math. Sci. 19, 237-261 (1983; Zbl 0522.03041)] that often (for example when open assumptions are Harrop formulas) complete normalization is unnecessary; it is possible to avoid permutative reduction. The proof d can also contain non-constructive parts, if they are not used in \(f_ d\) [cf. the reviewer, Normalization of natural deductions and effectivity of classical existence (1979); English translation to appear in \textit{G. Mints}, Proof-theoretic transformations, Bibliopolis Edizioni (1989)]. It seems that the program extraction algorithm proposed by the author and producing programs in a Pascal-like language is based on the combination of these ideas with some other optimizations. It combines encoding of normalization steps corresponding to unwinding of inductions with analysis of the fine structure of the formal proof. The description is very cumbersome and attempts to give comparison with familiar proof-theoretic notions and constructions are made only for the very first steps.