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).

Atrium > Mathematics, Physics & Philosophy: The Wiki History of the Universe

Bottom of Page

101 to 125 of 125

  1. <
  2. 1
  3. 2
  4. >
    • CommentRowNumber101.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2012

    Ah, never mind. I saw now the link to Logical frameworks. Good.

    I’ll create an nnLab stub logical framework in order to record this.

    • CommentRowNumber102.
    • CommentAuthorUlrik
    • CommentTimeSep 10th 2012

    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?)

    • CommentRowNumber103.
    • CommentAuthorUlrik
    • CommentTimeSep 10th 2012

    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.

    • CommentRowNumber104.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2012

    Urs, did you miss #78

    Woops. Sorry, yes. I did miss that. My bad. But Thanks again!! This is exactly what I wanted.

    • CommentRowNumber105.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2012

    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.

    • CommentRowNumber106.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2012

    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.

    • CommentRowNumber107.
    • CommentAuthorMike Shulman
    • CommentTimeSep 10th 2012

    I hope “you” refers to Ulrik, because he’s just convinced me that I have no idea what sequent calculus is about.

    • CommentRowNumber108.
    • CommentAuthorUlrik
    • CommentTimeSep 10th 2012

    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.

    • CommentRowNumber109.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2012
    • (edited Sep 10th 2012)

    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.

    • CommentRowNumber110.
    • CommentAuthorUrs
    • CommentTimeSep 11th 2012
    • (edited Sep 11th 2012)

    After the information Ulrik and Mile kept giving me finally penetrated my skull, I am now reading

    • Pfenning, Logical frameworks – a brief introduction (pdf)

    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:

    1. orthogonality

    2. local soundness

    3. local completeness .

    Just a note, mostly to myself.

    • CommentRowNumber111.
    • CommentAuthorUrs
    • CommentTimeSep 11th 2012
    • (edited Sep 11th 2012)

    Ulrik (or Mike or anyone),

    can you point me to a place in the literature on logical frameworks where inductive types are also discussed?

    • CommentRowNumber112.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    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.

    • CommentRowNumber113.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012

    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.)

    • CommentRowNumber114.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    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?

    • CommentRowNumber115.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012

    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.

    1. 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. ↩

    • CommentRowNumber116.
    • CommentAuthorUrs
    • CommentTimeSep 12th 2012
    • (edited Sep 12th 2012)

    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.

    • CommentRowNumber117.
    • CommentAuthorTim_Porter
    • CommentTimeSep 12th 2012

    By the way: FEIC is an Irish verb. (Ask Finn for details!)

    • CommentRowNumber118.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012

    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 33 is implicitly there in any definition of the system of natural numbers, even if you haven’t yet written down a definition of 33 itself.

    • CommentRowNumber119.
    • CommentAuthorTobyBartels
    • CommentTimeSep 12th 2012

    It looks like Mike invented ‘FIEC’ in #86.

    • CommentRowNumber120.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012

    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.

    • CommentRowNumber121.
    • CommentAuthorzskoda
    • CommentTimeOct 4th 2012
    • CommentRowNumber122.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 4th 2012

    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, SetsSets belongs to many different 2-categories, allowing it to play the role of dualizing object in very many ways.

    • CommentRowNumber123.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012

    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

    1. a natural-deduction “framework”

    2. with just the FIEC-rules for dependent product pre-specified

    3. 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.

    • CommentRowNumber124.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012
    • (edited Oct 4th 2012)

    I found the slides

    • Frade, Calculus of Inductive Constructions (pdf)

    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):

    Layers of foundations

    • CommentRowNumber125.
    • CommentAuthorUrs
    • CommentTimeOct 4th 2012

    but let’s rather branch the discussion of that list to its own thread.

101 to 125 of 125

  1. <
  2. 1
  3. 2
  4. >