Accession Number : ADA317245
Title : Primitive Recursion for Higher Order Abstract Syntax,
Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Despeyroux, Joelle ; Pfenning, Frank ; Schurmann, Carsten
PDF Url : ADA317245
Report Date : 30 AUG 1996
Pagination or Media Count : 119
Abstract : Higher order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables in the meta-language. It leads to concise encodings, but is incompatible with functions defined by primitive recursion or proofs by induction. In this paper we propose an extension of the simply-typed lambda-calculus with iteration and case constructs which preserves the adequacy of higher-order abstract syntax encodings. The well-known paradoxes are avoided through the use of a modal operator which obeys the laws of S4. In the resulting calculus many functions over higher-order representations can be expressed elegantly. Our central technical result, namely that our calculus is conservative over the simply-typed lambda-calculus, is proved by a rather complex argument using logical relations. We view our system as an important first step towards allowing the methodology of LF to be employed effectively in systems based on induction principles such as ALF, Coq, or Nuprl, leading to a synthesis of currently incompatible paradigms.
Descriptors : *COMPUTATIONAL LINGUISTICS, *OBJECT ORIENTED PROGRAMMING, RECURSIVE FUNCTIONS, MAPPING, SYNTAX.
Subject Categories : Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE