Constructing recursion operators in intuitionistic type theory (Q1094421)

The paper consists of counterparts, in the Type Theory (TT) considered, of material in the standard intuitionistic literature (evidently not familiar to the author nor to the people he consulted according to p. 354). Viewed this way, the principal open problem, on relations between recursion and induction in TT, is purely technical since they are well known for standard systems. On the other hand these technicalities distract from the main (cl)aim, on p. 325, the use of TT for automatic theorem proving, as follows. TT is a universal system (for a certain part of mathematics) corresponding to set theory (for the ordinary kind). Even though electronic computation and mathematical reasoning - in fancy jargon, electronic and biological data processing - differ in many ways, there are compelling parallels, at least, on the general level of this paper. The fiasco of the New Maths and Bourbaki's verdict on set- theoretic foundations (le côté le moins intéressant, tacitly, for effective mathematics) provide object lessons from experience with that other universal system, which are neglected in the paper. Reviewer's note. Contemporary axiomatic mathematics offers also positive object lessons for automation, alias organization: a relatively small number of modules \((=\) basic structures and their axioms), which can be combined to handle a relatively large number of situations. Those modules were extracted from extensive experience with substantial mathematics, not imposed for ideological reasons.