[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
That's right --- I did not intend any connection to other uses of the term "localization". - Frank On Tue, Mar 3, 2015 at 4:59 AM, Gabriel Scherer <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > I suspect you've been reading too much into the chosen name. I simply > understand it as making local (to each step of inference rule) something > that was global to the whole derivation -- the annoying upward dots > describing hypothetical judgments, first presented page 4 of the PDF you > link, and sometimes described as bracketing of hypotheses. It is clearly > explained as such in the lecture notes. "Localization" is a fine name in > this regard, and I would be surprised if it was related to the other uses > you mention in other ways than coincidence. > > On Tue, Mar 3, 2015 at 12:06 AM, Gershom B <[email protected]> wrote: > > > [ The Types Forum, > http://lists.seas.upenn.edu/mailman/listinfo/types-list > > ] > > > > In the course notes for Automated Theorem Proving (2004) [1], Pfenning > > describes the introduction of contexts in a Natural Deduction system as > > "Localizing Hypotheses" (see section 2.3). I cannot find many other > > examples of this terminology. Is this just a felicitous turn of phrase, > or > > is there literature that makes the connection explicit to familiar > notions > > of localization in, for example, algebraic, category-theoretic, or > > topos-theoretic settings? > > > > [1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf > > > > Thanks, > > Gershom > > > -- Frank Pfenning, Professor and Head Department of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 7019
