[TYPES] preterms

[Jay Sulzberger]

On Mon, 5 Feb 2018, Jay Sulzberger wrote:

>
> 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".

Ah, Andrew Pitts is also one of the authors of the theory of
nominal sets.  My error in attributing nominal sets, as she is
spoke today, is due to my too quick reading of the ncatlab page.

  http://www.cl.cam.ac.uk/teaching/1314/L23/lectures/lecture-1.pdf

And I have failed entirely to answer your questions about when
were "preterms" formally introduced.

ad troubles with scopes of names: See "upward funarg problem".  I
remember at least one Lisp of the 1960s whose interpreter and
compiler would disagree on what certain programs should do.

   http://archive.computerhistory.org/resources/access/text/2012/08/102746453-05-01-acc.pdf

And I have heard that the great 1928 textbook on logic of
D. Hilbert and W. Ackermann also had some difficulty with one of
the scope rules, and that the difficulty was close to the funarg
difficulty.

   https://en.wikipedia.org/wiki/Principles_of_Mathematical_Logic
   [page was last edited on 26 June 2017, at 00:02]

oo--JS.


>
>  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.
>
>