Nederpelt's calculus extended with a notion of context as a logical framework

Summary

Abstract

We define an extended version of Nederpelt's calculus which can be used as a logical framework. The extensions have been introduced in order to support the notions of mathematical definition of constants and to internalize the notion of theory. The resulting calculus remains concise and simple, a basic requirement for logical frameworks. The calculus manipulates two kinds of objects: texts which correspond to λ-expressions, and contexts which are mainly sequences of variable declarations, constant definitions, or context abbreviations. Basic operations on texts and contexts are provided. It is argued that these operations allow one to structure large theories. An example is provided.

Introduction

This paper introduces the static kernel of a language called DEVA. This language, which has been developed in the framework of the ToolUse Esprit project, is intended to express software development mathematically. The general paradigm which was followed considered development methods as theories and developments as proofs. Therefore, the kernel of the language should provide a general treatment of formal theories and proofs.

The problem of defining a generic formal system is comparable to the one of defining a general computing language. While, according to Church's thesis, any algorithm can be expressed as a recursive function, one uses higher level languages for the actual programming of computers. Similarly, one could argue that any formal system can be expressed as Post productions, but to use such a formalism as a logical framework is, in practice, inadequate.