Skip to main content
PRL Project

Syntactic Abstraction

by Timothy G. Griffin

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

all w,z:T.P(w,z)

can be thought of as a convenient shorthand for the expression
all w:T. all z:T.P(w,z).

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.