PRL Seminars

NuPrl provides a very convenient definition mechanism that is meant to capture the practice of introducing and using notational abbreviations. For example,

An instance of the left-hand side of this defining equation

The problem with the NuPrl mechanism is that it does not treat definition instances as "first-class" citizens in the land of terms. For example, Substitution into an instance may induce a cascade of unwanted definition expansions because the mechanism does not keep track of the "binding structure" of an instance.

I will start with a "calculus of expressions" - a simple typed lambda-calculus for representing terms of a given object language in the style of Martin-Lof, the Edinburgh Logical Framework, and others. On top of this I will build the machinery for what I call "syntactic abstraction" which is meant to capture at an abstract level the essence of notational abbreviation. I will then attempt to convince you that it really really works.

The advantages of this approach are :

1. generality: we can account for a definition mechanism in any language representable in the calculus of expression. The approach could be applied to the implementation of language- based editors for programming languages.
2. correctness:we get a correctness proof of the definition mechanism independent of the object language.
3. ease of implementation: the approach suggests a method of automatically generating the implementation of the syntactic component (term representation, routines for calculating free variables, substitution, alpha-conversion, and the definition mechanism) for systems like Nuprl given only a high-level specification of the object language.