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
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 4, 2019 at 10:08 | history | edited | lambda.xy.x | CC BY-SA 4.0 |
typo
|
| Feb 1, 2019 at 14:37 | history | edited | lambda.xy.x | CC BY-SA 4.0 |
typos
|
| Jan 31, 2019 at 16:27 | comment | added | lambda.xy.x | I updated the text that it becomes clearer - Church did not make a difference between the lambda calculus as a term language and his Hilbert system. Since LC by itself is already pretty useful, the two were disentangled at some point. | |
| Jan 31, 2019 at 16:25 | history | edited | lambda.xy.x | CC BY-SA 4.0 |
Expanded on LC vs STT
|
| Jan 30, 2019 at 18:39 | comment | added | Mike Battaglia | For example, in your comment to Andrej above, you say "STLC" doesn't have product types, citing Church's paper. But if Church's paper is an example of "STLC," then Church's paper also has universal quantification $\Pi$ as a primitive symbol, for example, but in this answer you say that "STLC" doesn't have quantification. Church's paper also had a set of axioms that could be used for inference (including extensionality and so on), but the quantification constant is defined before any of those and is a primitive symbol of his theory, whether it's "STT" or "STLC" or something else. | |
| Jan 30, 2019 at 18:37 | comment | added | Mike Battaglia | Hello lambda.xy.x - since you wrote this, I have since edited my original post to further clarify what I am trying to ask. Basically, though, I am very confused on how STLC and STT differ - all resources I can find using either of those terms cite Church's paper as having introduced "STLC" or "STT" or whatever. | |
| Jan 30, 2019 at 17:55 | review | First posts | |||
| Jan 30, 2019 at 18:28 | |||||
| Jan 30, 2019 at 17:53 | history | answered | lambda.xy.x | CC BY-SA 4.0 |