[TYPES] Localizing Hypotheses?

[Frank Pfenning]

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 <gabriel.scherer at gmail.com>
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 <gershomb at gmail.com> 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