Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab: logical framework

Bottom of Page

1 to 12 of 12

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 28th 2012
    • (edited Nov 28th 2012)
    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeNov 30th 2012

    I expanded a bunch at logical framework, based largely on Bob Harper’s talk at IAS and the notes from it (to which I also linked).

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 2nd 2012

    Thanks!

    some basic questions:

    • after the item list of 3 kinds of LF types the statement

      this turns out to be enough for everything we need

      refers to the collection of all three items, not just the last one, right? So I have moved it out of the item context.

    • after the sentence starting with

      Once we have set up

      the next one started with “See there”. I have made that read “See (Harper)” — hopefully that’s what was meant.

    • In the section “Synthetic presentation” it starts saying “LF-type” for what previously was called “type” equipped with a warning. So I have changed these previous “types” also to “LF-types”. Okay?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeDec 2nd 2012

    Thanks. I clarified the first one a bit; you are right on the other two.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeDec 4th 2012

    Hey, these recent edits are very nice. I think that I now have an idea of what a logical framework is. I even have an inkling that the concept just might be awesome.

  6. Hello,

    I was reading this article and one paragraph struck me as odd:

    It’s worth noting that this design choice essentially renders LF incapable of representing object-theory variables in any other way than with HOAS. For ordinary usage of variables requires the ability to compare “variables” for equality and disequality, and since LF has no inductive types, we cannot define therein any type that could function as “variables” in this way.

    It definitely is possible to represent variables/contexts via first-order encodings in LF, and this is not uncommon. The point is that the substitution operation is not defined as a function (which would require an induction principle) but rather as a relation (i.e., an LF-type family).

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeNov 12th 2014

    Ok, I don’t quite understand what that means or how it solves the problem of comparing variables, but feel free to edit the page!

  8. Okay, I removed that paragraph and added a simple example about the natural numbers which I hope clarifies things. (There’s also a similar point to be made about equality, which I went ahead and added to the section “Analytic presentation”.)

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeNov 12th 2014

    Ok, thanks! I clarified a bit.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 5th 2015

    It seems to me that an “analytic presentation” of a dependent type theory (sans universes, for simplicity) inside a logical framework is rather similar to a pure type system with two sorts *\ast (for object-theory-types) and □\Box (for LF-types), with axiom *:□\ast:\Box, rules (*,□)(\ast,\Box) and/or (□,□)(\Box,\Box), and perhaps augmented with a cumulativity *≺□\ast\prec \Box. Does this make any sense?

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2015

    I un-hyperlinked “syntactic category” at logical framework, since the meaning here is different from that described at syntactic category.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 15th 2015

    I added to logical framework some more description of the universe levels and some mention of the adequacy theorem.

1 to 12 of 12

  1.