Timeline for How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 1, 2019 at 15:00 | history | edited | LSpice | CC BY-SA 4.0 |
Missing Markdown for a link
|
| Jan 31, 2019 at 0:42 | comment | added | Mike Shulman | Nowadays STLC refers to a general class of theories, as Andrej says in his answer (and if you read the rest of the Wikipedia page you'll see that), whereas Church's theory (nowadays STT or HOL) is built on top of a particular STLC but augments it with extra power such as propositions and connectives and deduction rules. But when Church wrote his original paper (I think), the general framework of STLC did not exist yet, so in defining STT he was implicitly also defining STLC as the foundation for it. Nowadays we disentangle the two, but we still credit Church with inventing both of them. | |
| Jan 31, 2019 at 0:41 | comment | added | Mike Shulman | I think that one source of confusion is that the same paper of Church "introduced" both STLC and STT, but nowadays they are used to mean different things. I think most of your sources for "Referring to Church's System as STLC" are actually intending to say that Church's theory was the first STLC, not that what we nowadays mean by "STLC" is identical to Church's system. | |
| Jan 30, 2019 at 19:27 | vote | accept | Mike Battaglia | ||
| Jan 30, 2019 at 19:21 | comment | added | Andrej Bauer | So isn't your question just a result of your expectation that people use "STLC" and "STT" consisently? That's not true at all, as @PeterLeFanuLumsdaine warned you about. | |
| Jan 30, 2019 at 18:41 | history | edited | Mike Battaglia | CC BY-SA 4.0 |
formatting
|
| Jan 30, 2019 at 18:24 | comment | added | Mike Battaglia | @PeterLeFanuLumsdaine: I just did a very very large edit of my post trying to clarify this. In short, my point was just that I've seen both the terms "STT" and "STLC" used interchangeably to describe the same thing, which is Church's system. I put together a bunch of sources that use either/both terms "Simple Type Theory" and "Simply Typed Lambda Calculus" to describe that system. I assumed the terms were interchangeably used to mean the same thing everywhere - I haven't seen many sources that clearly state the two terms refer to different systems and would be interested to see those. | |
| Jan 30, 2019 at 18:20 | history | edited | Mike Battaglia | CC BY-SA 4.0 |
huge clarification and resources comparing STT and STLC
|
| Jan 30, 2019 at 17:53 | answer | added | lambda.xy.x | timeline score: 5 | |
| Jan 30, 2019 at 11:49 | comment | added | Peter LeFanu Lumsdaine | so something like “system ABC is equivalent to system XYZ” may mean several reasonable but different things to different people, and it’s very easy to read a paper that summarises its results as “ABC is equivalent to XYZ”, remember the summary not the precise results, and end up with the belief that ABC is equivalent to XYZ in some stronger (or just different) form from what the paper actually showed. | |
| Jan 30, 2019 at 11:46 | comment | added | Peter LeFanu Lumsdaine | @MikeBattaglia: Andrej’s answer lays out a lot of the relevant situation quite well, but for resolving the apparent contradiction you outline, I recommend just (1) expand the beliefs you’ve stated briefly (like “STLC is equivalent to STT”) into fully precise and unambiguous statements of what you believe to hold; (2) try to make precise your argument for how they’re contradictory. The trouble in logic is that terminology is not very well standardised, especially in comparing different kinds of logical systems, [cont’d] | |
| Jan 30, 2019 at 7:57 | answer | added | Andrej Bauer | timeline score: 27 | |
| Jan 30, 2019 at 3:59 | history | edited | Mike Battaglia | CC BY-SA 4.0 |
clarification
|
| Jan 30, 2019 at 3:48 | comment | added | Mike Battaglia | @MikeShulman it's in Church's original type theory paper, but a good description of the relation between Church's type theory higher-order logic is at Stanford's Encyclopedia of Philosophy: plato.stanford.edu/entries/type-theory-church | |
| Jan 30, 2019 at 3:43 | comment | added | Mike Battaglia | @user40276: You wrote this comment as I was editing my post for clarification. The point is that the simply typed lambda calculus is typically considered to be equivalent in expressive power to propositional logic (i.e. it is not strong enough to be Turing complete). I don't understand how this is possible, given that it is also stronger than first-order logic. | |
| Jan 30, 2019 at 3:43 | comment | added | Mike Shulman | Can you cite a source for the equivalence of STLC with STT (= HOL)? In what sense is this equivalence meant? | |
| Jan 30, 2019 at 3:41 | history | edited | Mike Battaglia | CC BY-SA 4.0 |
clarification
|
| Jan 30, 2019 at 3:39 | comment | added | user40276 | I cannot grasp exactly your concern. Normalisation for reasonable type systems implies decidability of type checking, but neither imply completeness. How would you be able to find a term of the Gödel sentence with the normalisation property? By using untyped terms (i.e., realisability), you certainly can. However it's impossible when one respects the typing rules. | |
| Jan 30, 2019 at 2:55 | history | asked | Mike Battaglia | CC BY-SA 4.0 |