Recursive Programs as Functions in a First Order Theory.
STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Pure Lisp style recursive function programs are represented in a new way by sentences and schemata of first order logic. This permits easy and natural proofs of extensional properties of such programs by methods that generalize structural induction. It also systematizes known methods such as recursion induction, subgoal induction, inductive assertions by interpreting them as first order axiom schemata. We discuss the metatheorems justifying the representation and techniques for proving facts about specific programs. We also give simpler version of the Goedel-Kleene way of representing computable functions by first order sentences. Author
- Computer Programming and Software