3
$\begingroup$

I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers LF, a typed version of Martin-Lof's logical framework.

LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.

(Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)

There are five forms of judgements in LF:

enter image description here

And then he gives rules for infering judgements in LF (one and two).

In general, a specification of a type theory will consist of a collection of declarations of new constants and a collection of computation rules (usually about the new constants).

For example, sigma types can be specified by declaring the following constants:

enter image description here


I have several questions about this set up, but the most basic (and general) one is this: suppose somebody wants to define a type theory with sigma types. What are the benefits of invoking LF to define it? As far as I understand, there's a more "direct" way to define it -- for example, as in Appendix A2 of the HoTT book, where sigma types are introduced by giving rules of formation, introduction, elimination, computation (as opposed to introducing several "constants").

Also, I don't really have intuition on why one needs to single out $El(A)$; I suppose it's related to universes (see this answer), but again I don't have a strong intuition about that.

Edit: I just looked at Lungu's PhD thesis "Subtyping in signatures" written under Luo, and there constants for product types are defined and inference rules for product types are given, which makes me even more confused -- I guess I don't understand why we need to declare types like $(x:K)K'$ and $[x:K]k'$ beforehand if we eventually define expressions like $\Pi(A,B):Type$ when stating inference rules for product types.


Edit 2: Okay I think can kind of see how Luo's particular LF makes it easy to introduce Pi and Lambda in the object theory. Correct me if I'm wrong but I think the idea is that if we have these rules specified in LF and if we introduce Pi and Lambda by declaring these constants, then we don't need to postulate these rules for Pi and Lambda separately because they follow automatically from the rules for dependent products that are part of the definition of LF. And similarly for sigma types: if we want to introduce Sigma in the object theory and if we do this by declaring these constants, then the standard inference rules for sigma types will automatically follow from the rules for dependent types in LF. And if we want to introduce some new constant in the object theory, its type must have one of the following forms: $\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k)$, and then all desirable inference rules for the newly introduced constant will follow from the dependent type rules in LF.

$\endgroup$

1 Answer 1

1
$\begingroup$

What are the benefits of invoking LF to define it? As far as I understand, there's a more "direct" way to define it

The motivation for LFs (there are multiple LFs!) is that we want to specify theories without explicitly mentioning contexts, binders and substitution. The "direct" definition can be easily multiple times the size of the LF definition, and all of the extra size is just mechanically derivable boilerplate. I've recently written a small tutorial/comparison of LF-style and first-order specification for a not-too-complicated concrete type theory.

why one needs to single out El(A)

An LF needs at least a type of object-theoretic types and a family over it which represents object-theoretic terms. We need to keep the different levels in mind. The LF is itself a type theory and has type formers, but it's used as a specification language for other theories, and not as a general-purpose mathematical language. If I interpret your source right, $\mathsf{Type}$ is the type of object-theoretic types and $El$ is the type family of object-theoretic terms. A type and a type family together can be viewed as a Tarski-style universe which is closed under no type formers at all, hence the $El$ notation. I'd prefer to write $Tm$ instead of $El$ in this context.

It can be confusing when we switch between first-order specification (which mentions contexts) and second-order or higher-order (which doesn't). When introducing an LF, it is usually specified in a first-order way. The motivation here is usually that first-order specification is viewed as more basic, and we want to build our infrastructure on top of basic things. If we already have an LF, then it makes perfect sense to specify other theories inside that, including other LFs.

$\endgroup$
5
  • $\begingroup$ In what sense are we not mentioning contexts, binders and substitution when using LF? If by "binders" you mean $\Pi, \lambda, \Sigma$, then Lungu's thesis that I mentioned in the last paragraph uses Luo's LF, and she still defines $\Pi$ and $\lambda$ as constants, and the inference rules she gives still use contexts. Also, contexts are still present in the five forms of judgements of LF mentioned at the beginning. $\endgroup$
    – user1048887
    Commented Mar 26, 2023 at 15:35
  • $\begingroup$ An LF signature does not specify anything about object-theoretic binders, variables and substitutions, in a strong sense. If we work in LF, the Pi and Lambda of LF are metatheory, not object theory. We can also specify a Pi and a Lambda in an object theory, which are a) distinct from LF's Pi/Lambda b) are specified without reference to any notion of binding or context. The object-level Pi is just a symbol with a function type. $\endgroup$ Commented Mar 26, 2023 at 16:34
  • $\begingroup$ It's important to keep track of metatheory and object theory. The judgments of LF are object-theoretic when we study LF, but metatheoretic when we write a signature inside LF. It can add to the confusion that a) LFs can be specified in LFs b) object theories and LFs often have type formers in common (e.g. Pi). $\endgroup$ Commented Mar 26, 2023 at 16:37
  • $\begingroup$ If you look at my linked note, you can see that the first-order signature has formation and computation rules for contexts and substitutions (1.3) while the LF signature doesn't (2). $\endgroup$ Commented Mar 26, 2023 at 16:44
  • $\begingroup$ Thanks for your explanations. I've updated the question and added my current understanding of how the particular LF that I mentioned makes it easier to define type theories. Does what I wrote make sense? (I did look at your note, and I think I have more questions than answers about it, so in my updated I sticked to the LF that mentioned originally.) $\endgroup$
    – user1048887
    Commented Mar 26, 2023 at 17:23

You must log in to answer this question.