Timeline for Lambda calculus - church encoding and lists
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 15, 2021 at 20:18 | comment | added | gaming4 mining | I've posted the questiom here: link, however I'm not sure if I shouldn't edit this question instead, because the contents of it depends on given solution to this one. | |
| Aug 15, 2021 at 13:19 | comment | added | Taroccoesbrocco | @gaming4mining - I guess you can prove that $F_n'[\mathsf{times}/c, \underline{1}/m] \to_\beta^* n!$ by straightforward induction on $n \in \mathbb{N}$. If you have trouble with this proof, please ask a question in a new post, to keep the site tidy. | |
| Aug 15, 2021 at 12:35 | comment | added | gaming4 mining | How would the induction proof look like? I can't seem to be getting the correct result. | |
| Aug 15, 2021 at 12:23 | comment | added | Taroccoesbrocco | @gaming4mining - Yes, absolutely. This is essentially the way the function $\mathsf{foldr}$ works in Haskell. | |
| Aug 15, 2021 at 12:09 | comment | added | gaming4 mining | Thank you for the answer, I was thinking would it be possible to proof that by induction somewhat like: $F'_n[times/c,1/n] →_\beta^* n! $ thus $F_n times 1 →_\beta^* n!$ where ! is factorial and $times \ a \ b$ reduces to $a * b$? | |
| Aug 14, 2021 at 23:47 | vote | accept | gaming4 mining | ||
| Aug 14, 2021 at 16:31 | history | answered | Taroccoesbrocco | CC BY-SA 4.0 |