KnowledgeBase » 
SEMINAR
» ID = 344
Syntactic Abstraction
by Timothy G. Griffin
1987-1988
NuPrl provides a very convenient definition mechanism that is meant to capture the practice of introducing and using notational abbreviations. For example,
all <x>, <y>: <a>.<b> == all x:a.all y:a.b
An instance of the left-hand side of this defining equation
can be thought of as a convenient shorthand for the expression
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 :
- 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.
- correctness:we get a correctness proof of the definition mechanism independent of the object language.
- 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.