Timeline for Application of lambda function in Simply Typed Lambda Calculus
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 22, 2018 at 13:24 | vote | accept | Nyfiken Gul | ||
| May 22, 2018 at 13:14 | comment | added | Rodolphe Lepigre | You are welcome, I added my comments as an answer. | |
| May 22, 2018 at 13:13 | answer | added | Rodolphe Lepigre | timeline score: 3 | |
| May 22, 2018 at 12:52 | comment | added | Nyfiken Gul | @RodolpheLepigre Right, I understand. Thank you so much for the explanation, if you want me to accept you, you could post your second comment as an answer if you want. | |
| May 22, 2018 at 12:39 | comment | added | Rodolphe Lepigre | Yes, the term $u\;r$ should definitely reduce to a function, but it does not really matter for the first reduction steps that you want to take. Remember that you only want to evaluate your term to $(u\;r)\;(\lambda x.x)$, which corresponds to the application of $u$ to the argument $r$ and $\lambda x.x$ (which are given one after the other, and not the two at once). | |
| May 22, 2018 at 12:33 | comment | added | Nyfiken Gul | @RodolpheLepigre Oh, of course.. I think it makes sense now. So what my professor says is that (u r) must be a function? Because otherwise this would crash, right? | |
| May 22, 2018 at 12:12 | comment | added | Rodolphe Lepigre | In the first one, $(\lambda x.(x\;(\lambda x.x)))$ corresponds to a function, taking as input a function (argument $x$), which is applied to the identity function $\lambda x.x$ (or ($\alpha$-)equivalently $\lambda y.y$). The second one has a very different nature because it denote the application of the identity function to the identity function, which reduces to the identity function. | |
| May 22, 2018 at 11:32 | answer | added | chi | timeline score: 4 | |
| May 22, 2018 at 11:27 | comment | added | Nyfiken Gul | @RodolpheLepigre Please enlighten me with what the difference is between the two readings. As I read them, the second lambda function is passed as indata to the first one in both cases, and then that 'concatenated' function is called with u and r as indata. Is that wrong? | |
| May 22, 2018 at 11:24 | comment | added | Nyfiken Gul | @YuvalFilmus Yeah, but I replaced the 'x' in the first lambda with the whole second lambda function. Is that wrong? | |
| May 22, 2018 at 10:40 | comment | added | Rodolphe Lepigre | Actually, I think that you did not parse the term correctly. It should be read as $(\lambda x.(x\; (\lambda x.x)))\;(u\;r)$, not as $((\lambda x.x)\;(\lambda x.x))\;(u\;r)$. | |
| May 22, 2018 at 10:35 | comment | added | Yuval Filmus | In your second line, an instance of $x$ went missing. It should be $(\lambda x.\, x(\lambda z.\, z)) \; (u\; r)$. | |
| May 22, 2018 at 9:33 | history | asked | Nyfiken Gul | CC BY-SA 4.0 |