Compiler Output as a Programming Tester in Ontology

This chapter is focused on the application of the COC (the criterion of ontological commitment) to the \(\lambda \) -calculus and the formulation of the functional ontology that underlies it. As the theory \(\lambda \) is an equational theory, then we can use either Martin’s metalinguistic approach (see Chap. 8 ) or Anderson’s definition of the existential quantifier in the object-language of the \(\lambda \) -calculus. In both cases, then the \(\lambda \) -calculus is exclusively committed (ontologically) with \(\lambda \) -terms. The ontological reduction implemented by the functional ontology  of the \(\lambda \) -calculus (for both logic and programming) is, then, the following: no abstract objects other than (Curried) monadic functions are needed for science. This powerful functional ontology is more economical than the set-theoretical ontology described by Quine. Moreover, the “Strachey-Quine example” illustrates, in a very effective way, the intersubjective nature of functional ontology. The example shows that using the COC, the programming language ALGOL is ontologically committed to real numbers because they behave like quantified (bound) variables. In contrast, procedures (the ALGOL term for functions) are not admitted in its ontology because they do not behave like quantified variables at all. Two specific lines of code (provided by Strachey) show this difference in the ontology of ALGOL.