MATH.12:4.4 - Determine which computation the argument supports

Inspect every operation on which the returned data depends. Is it supplied? Does it return on the permitted inputs? Can the case distinctions be decided? Finite composition of terminating operations gives an obtaining procedure; recursion needs its stated termination argument.

A proof step that invokes a classical choice of an element does not, by that invocation alone, give an executable choice procedure. Retain the existence result and either obtain a construction for that step or use another proof that supplies one. Classical reasoning can still justify a separately defined computable function.

Suppose a finite list is supplied together with a terminating test P and a proof that some listed element passes. Test the elements in order and return the first that passes. The list makes the search finite, and the proof rules out exhaustion without a result. For [2,5,8] and P(n)=(n>6), this returns 8 after three tests. The existence proof may use classical reasoning: the returned data comes from the search.

For a formalized proof, inspect the system’s actual rules for data and proofs. In Lean, for example, an existential proposition in Prop is not a data-bearing dependent pair whose witness a program may simply project. A value packaged in a data type with a proof of its property can retain its data while compilation erases the proof. Choice used to manufacture the data is a separate computational issue.

The chosen logic and evaluation rules determine the proof-to-computation correspondence. General recursion can describe a computation that never returns; its type alone need not establish the requested terminating construction. An ordinary proof narrative also needs its object-producing steps recovered before it provides that construction.