Timeline for How to state the adequacy of an encoding of lambda calculus in itself?
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 19, 2017 at 18:25 | comment | added | Andrej Bauer | Of course not, the relevant bit is just one paragraph in the beginning, explaining what it takes to have an acceptable coding of syntax. | |
| Mar 18, 2017 at 14:21 | answer | added | Andrew Polonsky | timeline score: 5 | |
| Mar 13, 2017 at 14:16 | comment | added | Andrea Asperti | @Andrej Bauer I can't believe you need all that stuff. Not to solve my issue. | |
| Mar 13, 2017 at 13:51 | comment | added | Andrej Bauer | What @DamianoMazza said. I tried to explain some of this in math.andrej.com/2016/01/04/… | |
| Mar 13, 2017 at 10:07 | answer | added | Andrea Asperti | timeline score: 4 | |
| Oct 4, 2015 at 10:10 | history | tweeted | twitter.com/StackCSTheory/status/650613959612059648 | ||
| Sep 30, 2015 at 20:18 | comment | added | Damiano Mazza | I think you actually listed the key operations: telling the kind of term (variable, abstraction, application) and, where appropriate, taking subterms. The only delicate point is representing the binding of lambdas, but you can do that using de Bruijn notation. Any other reasonable operation (for instance, counting the depth) follows from these, because you are able to completely deconstruct a term. Would you agree? | |
| Sep 29, 2015 at 19:26 | comment | added | cody | Pick a given concrete "adequate encoding" (say, the one given by Kleene). Say that an encoding $\iota$ is adequate if there is a $\lambda$-term taking a $\iota$-encoded term $\iota(M)$ to the Kleene encoding. This is a bit silly, but would this work for your purposes? | |
| Sep 29, 2015 at 11:55 | review | First posts | |||
| Sep 29, 2015 at 19:24 | |||||
| Sep 29, 2015 at 11:54 | history | asked | Brennan.Tobias | CC BY-SA 3.0 |