[TYPES] preterms

[Jay Sulzberger]

On Sun, 4 Feb 2018, Stefan Ciobaca <stefan.ciobaca at gmail.com> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> Could anyone help me with a reference to when the concepts of
> preterm/preproof/pretype were first introduced, or what counts as
> acceptable definitions of preterms?
>
> Unfortunately, google is not too helpful when searching for the terms above.
>
> Thanks!
>
> Stefan Ciobaca

I believe that the book by M. H. B. Sorenson and P. Urzyczyn

   Lectures on the Curry-Howard Isomorphism (May 1998 not final version)

which, I think, is at

   http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf

has a definition on page 2 of Chapter 1.

The "nominal sets" of M. J. Gabbay are part of, and also an
extension of, one explication explication of the passage from
"preterms" to "terms".

   https://ncatlab.org/nlab/show/nominal+set

I think before "preterms", mathematicians did not completely
explicitly distinguish between terms and preterms.  There were
just lambda expressions, and then an "equivalence" between terms,
terms which we now call preterms.  The equivalence classes of the
equivalence relation, all now admit, are the actual terms of the
lambda calculus.  Of course, also in near branches of
mathematics, we must, on occasion, distinguish "formulae" and
"formulae up to careful renaming of bound variables".  It is
clear that the absolute binary opposition of "free" vs "bound"
variables is just the most simple case of the general situation:
as we reason, or program, we impose conditions on the objects of
our attention, and so in our notations, we will have partly bound
and partly un-bound names of things.

oo--JS.