Timeline for Do you know important theorems that remain unknown?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 22, 2021 at 9:58 | history | edited | Damiano Mazza | CC BY-SA 4.0 |
added 36 characters in body
|
| Nov 22, 2021 at 9:44 | history | edited | Damiano Mazza | CC BY-SA 4.0 |
Added a reference to Tito Nguyen's Ph.D. thesis.
|
| Dec 9, 2020 at 9:28 | comment | added | Damiano Mazza | Also, you say that the reference I give discusses "what does $o\to o\to o$ in the STLC encode". This is a misunderstanding: that type is basically irrelevant in Hillebrand and Kanellakis's work, any type with a partition of its normal forms into two non-empty sets "True" and "False" would do. The real question is: what languages may be decided by terms taking a Church string and outputting True/False according to some fixed convention? The string encoding being the same (called "Church") makes it interesting to compare the answer in the pure $\lambda$-calculus, System F, STLC, etc. | |
| Dec 9, 2020 at 7:22 | comment | added | Damiano Mazza | About $o\to o\to o$, I don't know who calls that "Church encoding", I most certainly didn't. Now I see that the sentence I wrote may be parsed ambiguously: it should be "These are the standard types of (Church binary strings) and (booleans)", i.e., "Church" only goes with "binary strings". Still, I wouldn't see any problem in calling $\lambda x.\lambda y.x$ and $\lambda x.\lambda y.y$ the "Church Booleans". Regardless of whether it is historically accurate, I stand by my point above: there is no standard minimum expressiveness for this name to be legitimate! | |
| Dec 9, 2020 at 7:15 | comment | added | Damiano Mazza | I've been reading $\lambda$-calculus-related research papers for almost 20 years now. The map $n\mapsto\lambda f.\lambda x.f(\ldots fx\ldots)$ with $n$ occurrences of $f$ is universally known as "the Church encoding" of natural numbers (because it was first used by Church, it would seem). Related encodings (like binary strings) are often called "Church" too. In any case, I have never seen anybody setting an "expressiveness bar" under which it would be illegitimate to call such encodings "Church". | |
| Dec 8, 2020 at 20:39 | comment | added | Blaisorblade | IMHO that's also why these results is not well-known — they sunk a research area out of interest for most people, except maybe for research like dl.acm.org/doi/10.1145/346048.346051 (which, no offense, seems for now a niche even within SIGPLAN or at POPL). | |
| Dec 8, 2020 at 20:36 | comment | added | Blaisorblade |
"What does o -> o -> o in pure STLC encode?" is a perfectly sensible question, which your reference discusses. They call that "Church encoding", and I didn't know anybody did that. But today, perhaps thanks to that work, we avoid considering that setting or calling that a Church encoding, at least not without strong warnings. I just checked TAPL, and it describes Church encodings for untyped LC and for System F (chapter 23).
|
|
| Dec 7, 2020 at 21:22 | comment | added | Damiano Mazza | @Blaisorblade I'm not sure I understand your comments. Why would the Church-encoding "not really work in STLC"? I have the impression that you think the Church encoding or the type $o\to o\to o$ don't work because they don't give you the expressiveness you'd like. But this is not about what you like: the question "what is the class $\mathsf{ST}\lambda$" is natural, well posed and has a very nice answer, whether you like it or not. In fact, what's interesting is precisely that these types do not give you everything one would normally expect from a general-purpose programming language. | |
| Dec 6, 2020 at 14:35 | comment | added | Blaisorblade |
As a consequence, standard presentations of STLC add datatypes such as naturals as primitives with their operations. Even booleans better be primitive if you want if at all types in general — as soon as you have more than 1 base type, o -> o -> o breaks down.
|
|
| Dec 6, 2020 at 14:29 | comment | added | Blaisorblade | > These are the standard types of Church binary strings and booleans I think that deserves a big caveat: Church-encoding is well-known to not really work in STLC because you must fix the result type, and it only works properly in either untyped lambda calculus, or in System F (where it’s best called Böhm-Berarducci encoding). Indeed, Church encoding supports naturals, which of course can’t be modeled (correctly) in the category of finite sets. | |
| Apr 3, 2018 at 11:27 | history | edited | Damiano Mazza | CC BY-SA 3.0 |
edited body
|
| S Apr 3, 2018 at 10:56 | history | answered | Damiano Mazza | CC BY-SA 3.0 | |
| S Apr 3, 2018 at 10:56 | history | made wiki | Post Made Community Wiki by Damiano Mazza |