Accession Number:

ADA071421

Title:

Recursive Programs as Functions in a First Order Theory.

Descriptive Note:

Technical rept.,

Corporate Author:

STANFORD UNIV CALIF DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1979-03-01

Pagination or Media Count:

34.0

Abstract:

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

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE