Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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).
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?
Thanks. I clarified the first one a bit; you are right on the other two.
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.
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).
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!
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”.)
Ok, thanks! I clarified a bit.
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?
I un-hyperlinked “syntactic category” at logical framework, since the meaning here is different from that described at syntactic category.
I added to logical framework some more description of the universe levels and some mention of the adequacy theorem.
1 to 12 of 12