[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Sun, 4 Feb 2018, Stefan Ciobaca <[email protected]> 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.
