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
15 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Oct 16, 2022 at 20:24 | history | suggested | Dan Zheng | CC BY-SA 4.0 |
Fix multiple typos
|
| Oct 16, 2022 at 20:06 | review | Suggested edits | |||
| S Oct 16, 2022 at 20:24 | |||||
| Jan 30, 2019 at 20:00 | comment | added | Mike Battaglia | @AndrejBauer well, when I first wrote the question, I didn't realize STLC and STT were often used to mean two very different things in different contexts. I'll accept your answer since you put a lot of effort into it, although I should perhaps ask a new question about terminology. | |
| Jan 30, 2019 at 19:27 | vote | accept | Mike Battaglia | ||
| Jan 30, 2019 at 19:17 | comment | added | Andrej Bauer | What I tried to convey in my answer is a possible source of confusion. I believe my use of terminology is broadly standard. But please keep in mind that STLC and STT are not exactly defined. Even things like "first-order logic" and "set theory" are not precisely defined, and there are many versions of everything. Fortunately, mathematics is robust with respect to foundations. | |
| Jan 30, 2019 at 19:14 | comment | added | Andrej Bauer | I recommend taking heed of Peter Lumsdaine's advice: the terminology is not standard, and there are many variants of everything. Products or no products? Is equality up to $\beta$ or up to $\beta\eta$-equivalence? Do we assume any basic types, and how many? And so on, and so on. The only safe way is to always make precise references to precisely given formal systems, and not to assume anything. | |
| Jan 30, 2019 at 19:12 | comment | added | Andrej Bauer | The product types are inessential as far as expressive power is concerned. | |
| Jan 30, 2019 at 18:33 | comment | added | Mike Battaglia | Also, as lambda.xy.x mentioned, I don't think Church's original paper has product types, although I am not sure if they could somehow be derived indirectly. | |
| Jan 30, 2019 at 18:32 | comment | added | Mike Battaglia | Andrej - as per request, I just edited my original post to try to clarify. I am somewhat confused about the distinction between STLC and STT, since in the sources I had read, those terms have both been used to describe Church's paper (and papers describing related/equivalent systems simplifying it). In Church's system there is a basic propositional type and a basic type of individuals (which seems to be more general than the naturals). Is the term "STLC" used in some settings to exclude things like Church's system? I would appreciate some reading material if you have some. | |
| Jan 30, 2019 at 17:28 | comment | added | lambda.xy.x | To my knowledge, System T has product types but simply typed lambda calculus does not (at least according to Church: "A Formulation of the Simple Theory of Types" and Benzmüller, Miller: "Automation of Higher-Order Logic", which are my standard sources regarding STT). | |
| Jan 30, 2019 at 9:17 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 17 characters in body
|
| Jan 30, 2019 at 8:25 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 82 characters in body
|
| Jan 30, 2019 at 8:10 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 298 characters in body
|
| Jan 30, 2019 at 8:04 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 298 characters in body
|
| Jan 30, 2019 at 7:57 | history | answered | Andrej Bauer | CC BY-SA 4.0 |