[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Mon, 5 Feb 2018, Jay Sulzberger wrote:
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".
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.
