We previously saw (Proofs and programming) that the inference rules of propositional logic are closely related to the process of type checking. The same holds here. For example, in many programming languages, we can write a sorting function that works on any type of data. It takes two arguments, a comparison function for the type and a collection (array, list, ...) of data of that type. The type of the sorting function can then be described as "for all types T , given a function of type (T and T ) → T , and data of type (collection T ), it returns data of type (collection T )". This polymorphic type-rule uses universal quantification.
Note that the details about substitutions and capture noted here arise in any kind of program that manipulates expressions with bound variables. That includes not only automated theorem provers, but compilers. To avoid such issues, many systems essentially rename all variables by using pointers or some similar system of each variable referring to its binding-site.
When people speak of proofs written by computerll , they're talking about this style of inference rule proofs.
- 983 reads
