Recursive Programs as Functions in a First Order Theory.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1979
Accession Number
ADA071421

Entities

People

  • John McCarthy
  • Robert Cartwright

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Arithmetic
  • Artificial Intelligence
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Equations
  • Language
  • Logic
  • Mathematical Logic
  • Number Theory
  • Programming Languages
  • Recursive Functions
  • Set Theory
  • Theorems
  • Theory Of Computation

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.