tag:blogger.com,1999:blog-5382571416341492754.post91549706941522211..comments2024-11-05T04:45:17.688-05:00Comments on Blogface.org: Simply Typed Lambda Calculus vs. UntypedNelshttp://www.blogger.com/profile/07085287093689227850noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-5382571416341492754.post-34769595080288056252023-05-23T16:19:56.142-04:002023-05-23T16:19:56.142-04:00Grateful for sharingg thisGrateful for sharingg thisHamlet Againhttps://medium.com/@HamletAgainnoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-67021433161865475672009-09-17T15:01:21.000-04:002009-09-17T15:01:21.000-04:00Aah, yes. You can encode the untyped lambda calcul...Aah, yes. You can encode the untyped lambda calculus into a lambda calculus with one recursive type "μx.x→x", but not the simply typed lambda calculus, per jcreed. I was just confused by the setup.simrobnoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-40404211029991326472009-09-17T14:19:16.000-04:002009-09-17T14:19:16.000-04:00Yes, that makes sense! Thanks.Yes, that makes sense! Thanks.nolacoasternoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-82351196205213423172009-09-17T14:18:53.000-04:002009-09-17T14:18:53.000-04:00I can give more details after we get to that lectu...I can give more details after we get to that lecture in 814 (which I am sitting in on, four years later). :-)nolacoasternoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-10803478163989674312009-09-17T14:17:55.000-04:002009-09-17T14:17:55.000-04:00This is just me paraphrasing a comment made by Bob...This is just me paraphrasing a comment made by Bob four years ago in 814 that a typed language is strictly more expressive than an untyped language because you can encode an untyped language in a typed one where every single value has the same type.<br /><br />As jcreed points out above, if you want to encode the untyped lambda calculus with a typed language, that language cannot be the simply typed lambda calculus, because it's not Turing complete.nolacoasternoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-12949077662542763542009-09-17T14:13:39.000-04:002009-09-17T14:13:39.000-04:00The encoding of the untyped lambda calculus into t...<i>The encoding of the untyped lambda calculus into the lambda calculus.</i><br /><br />I actually don't know what this means, and the way I interpret it it shouldn't be possible...simrobnoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-26699971196480827872009-09-17T13:47:02.000-04:002009-09-17T13:47:02.000-04:00Note that that typed lambda calculus that has D = ...Note that that typed lambda calculus that has D = D → D is decidedly <i>not</i> the simply-typed lambda calculus anymore, and of course it can't be, since it's turing complete and the STLC is not.jcreednoreply@blogger.comtag:blogger.com,1999:blog-5382571416341492754.post-61007731533553068442009-09-17T13:45:26.000-04:002009-09-17T13:45:26.000-04:00Yes, the un(i)typed lambda calculus is turing-comp...Yes, the un(i)typed lambda calculus is turing-complete.<br /><br />If you want a typed model of the untyped lambda calculus, the everything type, call it D, has to be isomorphic ("has to be effectively the same type as") to D → D. The everything type <i>is</i> a function type, and its functions expect an <i>everything</i> and return an <i>everything</i>.<br /><br />To actually describe what this set of things is carefully, you sometimes resort to tricky domain-theory tricks invented by Dana Scott.jcreednoreply@blogger.com