tag:blogger.com,1999:blog-827419514217130218.post6421868563013322419..comments2015-10-26T03:12:33.234-04:00Comments on Request for Logic: Totally nameless representationRobhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-827419514217130218.post-56775638467853440372010-11-19T12:02:25.886-05:002010-11-19T12:02:25.886-05:00I'm not sure about what exactly has been imple...I'm not sure about what exactly has been implemented in Agda. I believe Andreas Abel has done most of the work himself (though I could be wrong), so there is a high chance that the system is similar to that of his PhD thesis (which describes Fomega actually but the ideas are similar, you can also see the work on MiniAgda).<br /><br />The language of sizes only contains the symbols $ (for successor) and # (for infinity) with 0 and max depending on the version. This means that you can not explicitly write a size that is larger than omega. However, and this is the important part, you can express structural decrease (and other kinds of decrease) on inductive types as the -difference- of sizes is always far less than omega (usually less than 3). You can have a look at http://perso.ens-lyon.fr/colin.riba/papers/tutorial-tbt.pdf for some more explanations.<br /><br />Thanks for the update!thecodhttp://www.blogger.com/profile/10717993079747767784noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-8636263745104493572010-11-17T11:02:12.908-05:002010-11-17T11:02:12.908-05:00Do sized types in Agda scale past omega? More gene...Do sized types in Agda scale past omega? More generally: was your comment about sized types generally, or their current state of implementation in Agda (which I am unclear about).<br /><br />As for what I would call simultaneous substitutions: that works too; I've added the example to the bottom of <a href="http://bitbucket.org/robsimmons/agda-lib/src/tip/Demo/STLC.agda" rel="nofollow">the code example for this post</a>. It uses some library functions; "LIST.All P xs" just says "P holds for every x in xs", which translates to "there is a term in the new context for every type in the old context." Indeed, the result is slicker than either of the approaches I originally presented.<br /><br />Our experience with the metric technique I demonstrated here is primarily cut elimination arguments, not substitution - substitution was just used as an example. However, if substitution is what you're actually hoping to get at, then I think the presheaf approach/simultaneous substitution definition looks pretty good. Thanks thecod!Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-69452195335488330412010-11-17T10:02:58.509-05:002010-11-17T10:02:58.509-05:00Fun post! As far as sized types go, it just so hap...Fun post! As far as sized types go, it just so happens that they are strictly -more- powerful than structural induction: the latter only allows recursive calls on subterms, whereas size based termination allows recursive calls on -all- smaller terms (as far as the type system can tell that they are smaller). Just to clear things up, the notion of size is actually the abstraction of an ordinal, to allow recursive calls on inductive terms of higher type.<br /><br />Your first presentation of substitution is essentially the algebraic presentation commonly referred to as the "presheaf approach" which is itself related to the "monadic approach". In these cases, weakening is the action of the term functor on context renamings (exactly your wk function), and substitution is actually -more- general: all variables are substituted in one go. I wonder if that more general defnition allows for an even simpler definition of tm-subst, which would suggest that this is the natural presentation of substitution in this context...thecodhttp://www.blogger.com/profile/10717993079747767784noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-40406932764844017882010-11-15T22:49:54.459-05:002010-11-15T22:49:54.459-05:00I just mean intrinsically typed; your data type wo...I just mean intrinsically typed; your data type would have to have a "bvar : ∀{A} → A ∈ Γ → Term Γ A" as well as a "fvar : ∀{A} → A → Name → Term Γ A". I can imagine writing "open" and "close" functions for such a type; I don't know how you'd get the right induction principles out of that, though.Robhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-30029371325227230402010-11-15T22:31:28.482-05:002010-11-15T22:31:28.482-05:00Nice post!
I'm curious what you mean about ...Nice post! <br /><br />I'm curious what you mean about being able to do an intrinsically typed locally nameless: do you mean just intrinsicially typed, or also intrinsicially scoped? The problem with intrinsicially scoped locally nameless is that you need proofs that the names are in the context---at which point you're back to de Bruijn indices! You really need some proof irrelevance for it not to degenerate to de Bruijn.<br /><br />Regarding "Dan's said on a couple of occasions that he thinks there are less painful ways of doing this sort of thing, existing Agda techniques that avoid the annoying duplication of data types." I think what I had in mind is defining <br />Metric : (Γ : Ctx)(A : Tp) → Term Γ A → Set<br />recursively: for each constructor, you have recursive Metrics whereever you need recursive calls. Then you prove that Metric e is the same as Metric (exchage e), etc. I've used this once, but I'm not sure what the tradeoffs are in your setting.<br /><br />Also, the right citations for this representation are Bellegarde and Hook, 94; Altenkirch and Reus, 99; Bird and Patterson, 99---see the biblio of basically any paper I've written in the past 3 years for the deets.Dan Licatahttp://www.blogger.com/profile/05419342217317164459noreply@blogger.com