but let’s rather branch the discussion of that list to its own thread.
]]>I found the slides
useful. I am getting now a sense of that system of “layers of foundational structure” that I am after. At least parts of it starts out as follows (please comment; I have put this into an entry layers of foundations, but just so as to have it somewhere, let’s develop it):
natural deduction logical framework for dependent types (and including a type of types hierarchy at this stage or later)
add dependent product type formation rule $\to$ pure type system
add rules for introducing inductive types $\to$ calculus of inductive constructions
specify the rules for the inductive types empty type, dependent sum type, identity type $\to$ intensional dependent type theory
add uniqueness of equality-axiom $\to$ extensional dependent type theory
consider setoid types $\to$ intuitionistic predicative set theory
add univalence-axiom and rules for introducing higher inductive types $\to$ homotopy type theory
add cohesion-axiom $\to$ cohesive homotopy type theory
David,
I see what you mean and would entirely agree. But the reason I feel like pushing this nevertheless is that it seems to me that in view of a bit of natural deduction/type theory, there will not actually be “too much sand”. That’s what motivates me. I don’t like sand either.
At the moment my impression is that we have a pretty sandless and rather beuatiful meta-foundation if we take
a natural-deduction “framework”
with just the FIEC-rules for dependent product pre-specified
and with the rule how to add inductive types.
In fact, if I understand correctly, then this is what Coq implements. Maybe I should just say “Calculus of inductive Constructions” for this, I am not sure yet if I understand that term enough, though.
Then from there for instance
get set theory by defining setoids and adding some foundational axioms, as desired;
get homotopy type theory by adding a univalent type of types
etc.
The point being that all these “get xyz” work by naturally adding stuff within the above framework. And also it seems plausible that the intersection of all “xyz” that one wants is that framework. So then this would be the sufficient and necessary meta-foundations. And it would be as elegant as it is rich and sand-free.
It seems to me.
]]>I can see that it would be interesting to know of a framework in which all kinds of formal system can be set, but it wouldn’t last too long for me. Like set theory containing “too much sand” (Weyl). I’d want to know what there is to be said about the conceptual power of specific formal systems. And then how they throw light on the success of earlier formal systems.
So now we have a good sense of why set theory was so successful. For example, $Sets$ belongs to many different 2-categories, allowing it to play the role of dualizing object in very many ways.
]]>There is a recent blog post by Andrej Bauer roughly related to parts of the above discussion, or at least it is through the lense of a comment/question that I posted. Now Neel Krishnaswami kindly points me to Giovanni Sambin’s “Basic Logic”.
Right now I have -2 minutes to look at this. But I’ll try to come back to it later.
]]>It looks like Mike invented ‘FIEC’ in #86.
]]>The main reference for Coq is the Coq site. On there you can find the standard library, which includes very early on the module that defines these data types.
But I’m still not sure that Coq without this module is quite what you want in a logical framework. This includes a little more than knowing what a FIEC definition would be, it also includes a specification (at least implicitly) of which FIEC definitions are valid. (And also which coinductive FEIC definitions are valid.) So all of the (co)inductive types are implicitly there, much as the number $3$ is implicitly there in any definition of the system of natural numbers, even if you haven’t yet written down a definition of $3$ itself.
]]>By the way: FEIC is an Irish verb. (Ask Finn for details!)
]]>Wow, thanks for that answer, Toby. That feels like I am now getting feedback on a bunch of further points.
Didn’t you invent ‘FIEC’
I don’t think so. Instead I was wondering why I had to keep saying “the 4-step formation/introduction/elimination/computation rule” without having a term for it. I would have thought this goes by some official term.
at least Coq has a level (before reading in the basic inductive and coinductive types) where there are general types (indeed universes of them) but only the dependent product among the usual type constructors.
Ah, that’s interesting. Where do you get that info from? Do you have some pointers? How is it that there is only the dependent product? So the dependent sum is then realized as an inductive type, is that it?
Can we say the only non-inductive type constructor that we need is dependent product? Would that be right? Is everything else we need obtaininable by combinations of that and inductive types?
the machinery is already there to define inductive and coinductive types too; it just hasn’t read in the definitions yet
Well, but this is precisely what I am after. The “logical framework”, if that’s what it’s called, which “just hasn’t read in the definitions yet” for type constructors.
Again, if you could point me to where you have all this information from, I’d be grateful.
]]>Could you remind me what FEIC stands for?
Didn’t you invent ‘FIEC’? ‘FEIC’ is the same, only emphasising elimination over introduction.
I got then confused whether Calculus of Constructions is just about props or about general types. Does the general type theoretic CoC only have the dependent product?
I’m not sure what officially counts as the CoC, but at least Coq has a level (before reading in the basic inductive and coinductive types) where there are general types (indeed universes of them) but only the dependent product among the usual type constructors.
However, it’s not really true that $\forall$ is the only type constructor at this level, since the machinery is already there to define inductive and coinductive types too; it just hasn’t read in the definitions yet.^{1} But this just means that Coq is already more than the CoC.
This is probably why the others say that you can’t remove the (co)inductive types from Coq by removing a module, while I’m sure that there is a module defining these types that you could remove if you wanted to. Because even without that module, the user can still construct their own (co)inductive types. ↩
Maybe the word that I am after is calculus of constructions?
I don’t think so.
Yes, after reading up on it, I saw this. The wealth of terminology can be a bid forbidding to the outsider. Could you remind me what
FEIC
stands for?
The CoC’s single type operator $\forall$
That made me wonder concerning the “caterpillar type theory” that I was asking about here (as in: how many legs can we remove so that it can still walk). I got then confused whether Calculus of Constructions is just about props or about general types. Does the general type theoretic CoC only have the dependent product?
]]>Re the technical problem of creating sequence calculus when there was already sequent calculus: HowTo.
(And right now the cache bug has struck the former.)
]]>Kind of obsolete, now, but …
Maybe the word that I am after is calculus of constructions?
I don’t think so.
On the pro side: IIRC (and in contrast to what others may have implied), the CoC is hard-wired in Coq more deeply than the full calculus of inductive and coinductive constructions, so this may be the answer to the question of what we get when we remove the type definitions from Coq; it is what we get when we remove the definitions of the basic inductive and coinductive type definitions.
But on the con side: The CoC’s single type operator $\forall$ is still given by FIEC. It’s unusual in that it’s a negative type, unlike than the positive inductive types (although the less commonly used coinductive types are also negative); that is, E is more basic than I (so FEIC instead of FIEC?). But it’s still a type operator.
]]>Ulrik (or Mike or anyone),
can you point me to a place in the literature on logical frameworks where inductive types are also discussed?
]]>After the information Ulrik and Mile kept giving me finally penetrated my skull, I am now reading
In section 3.2 there I find something related to #92, #93 above
Are you implying that there is no precise notion of what a type formation rule, a term introduction rule, a term elimination rule and a corresponding computation rule are to be like?
So, maybe it’s not a precise definition, I am not sure I understand this yet, but Pfenning metions three rules that a set of introduction/elimination rules has to satify:
orthogonality
local soundness
local completeness .
Just a note, mostly to myself.
]]>Oh, dear, my bad again. My fingers’ that is. Sorry.
(By the way, why “sequent”? Is it a pun on “consequent”/”consequence”?)
Can we delete sequence calculus?
Just rename it to something like
sequence calculus > history
and leave it alone. Pages are “deleted” by having no pointers to them. Then move your material over to the genuine entry.
]]>Whoops, I accidentally followed your link to sequence calculus, started an entry, but now I see you’ve already made something at sequent calculus. Can we delete sequence calculus?
Anyway, the main thing I wanted to say there was that the raison d’être for sequent calculi is the subformula property, and there are calculi for many different logics and computation systems, and that sometimes one-sided calculi are useful.
]]>I hope “you” refers to Ulrik, because he’s just convinced me that I have no idea what sequent calculus is about.
]]>Could you remind me what the central difference is between sequent calculus and (what should I put here?) natural deduction?
And maybe, if you have a second, it would be nice to have a comment to this extent at sequence calculus.
]]>Gosh, sequent calculus is more bizarre than I ever dreamed. I think I will conclude from this that I don’t want to ever think about sequent calculus again.
]]>Urs, did you miss #78
Woops. Sorry, yes. I did miss that. My bad. But Thanks again!! This is exactly what I wanted.
]]>One more comment about the sequent calculus, and then I’ll be away for some hours:
Notice that the usual $\lambda$-terms are a poor fit for sequent calculus, and there are indeed several inequivalent ways to formulate typing rules for it (See Sørensen and Urzyczyn again (I found a free version here). Even better than the options there would be a focalized version to pick out which formulas to act on on the left, giving something like the $\lambda\mu$-calculus.
]]>Urs, did you miss #78 in which I linked to Frank Pfenning’s Logical Frameworks–A Brief Introduction?
(Meta-comment: is there a tag to put around 78 to make it a link to the anchor in the discussion page?)
]]>