barry-jay-personal / tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus
MIT License
51 stars 4 forks source link

Some bugs in the PDF #6

Open olydis opened 1 year ago

olydis commented 1 year ago

Hi, what a great book! I love thinking about PLs with maximum "effectivity / spec size" ratio as a hobby and this made quite the dent[^1] in where I suspected the theoretical limit of that ratio to be for years. So thanks for that, and thanks for jumping in at the end of the "Combinators: A 100-Year Celebration" video, which is what led me here.

Some minor things I noticed while reading:

Happy to contribute fixes directly, but AFAICT the repo only contains PDFs rather than LaTeX sources or similar.

[^1]: Apart from being more powerful, I noticed that hacking up a high-perf evaluator for tree calculus also turned out simpler than what I managed to do for SKI/Iota-based systems. Iota being a one-point basis combinator feels like a bit of a lie anyways: Either one introduces auxiliary bases S and K and rewrites IOTA x = x S K and S and K as usual. Or one rewrites (say) IOTA (IOTA (IOTA IOTA)) x y = x and IOTA (IOTA (IOTA (IOTA IOTA))) x y z = x z (y z) and accepts Iota to not be "behaving like" \x -> x (\a -> \b -> \c -> a c (b c)) (\a -> \b -> a) for all inputs.

barry-jay-personal commented 1 year ago

Hi Johannes,Glad you like the book, and thanks for finding the typos; I aim to handle them in the next edition.  For me, IOTA is merely an encoding of S and K that yields another semantics for the natural trees but it cannot treat them as queryable data structures. As for performance, mydream is that tree calculus account for the intermediate language, the assembler, the cache hierarchy, the pointer arithmetic, all the way down.I spent a little time thinking about adding a heap to an interpreter, but decided the bigger issue is types. I now have a simply-typed  variant of tree calculus that supports the mu-recursive functions as typed normal forms. This could be done in SK-calculus (exercise for you?) but not (I believe) in lambda-calculus. Next step is to type triage. I have a version using parametric polymorphism that I don’t like; so am aiming for a simply-typed solution.You can write me direct at @.,BarrySent from my iPhoneOn 11 Sep 2023, at 5:25 am, Johannes Bader @.> wrote: Hi, what a great book! I love thinking about PLs with maximum "effectivity / spec size" ratio as a hobby and this made quite the dent1 in where I suspected the theoretical limit of that ratio to be for years. So thanks for that, and thanks for jumping in at the end of the "Combinators: A 100-Year Celebration" video, which is what led me here. Some minor things I noticed while reading:

Abstract: "... waits for a second argument for evaluation begins." sounds off, maybe "before evaluation begins" or "for evaluation to begin"? Section 5.4: untag is defined via fst and snd but those are spelled out (first and second) when defined in section 3.6. Section 5.5: "which not be addressed until" missing "will"?

Happy to contribute fixes directly, but AFAICT the repo only contains PDFs rather than LaTeX sources or similar. Footnotes

Apart from being more powerful, I noticed that hacking up a high-perf evaluator for tree calculus also turned out simpler than what I managed for SKI/Iota-based systems. Iota being a one-point basis combinator feels like a bit of a lie anyways: Either one introduces auxiliary bases S and K and rewrites IOTA x = x S K and S and K as usual. Or one rewrites (say) IOTA (IOTA (IOTA IOTA)) x y = x and IOTA (IOTA (IOTA (IOTA IOTA))) x y z = x z (y z) and accepts Iota to not be "behaving like" \x -> x (\a -> \b -> \c -> a c (b c)) (\a -> \b -> a) for all inputs. ↩

—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: @.***>

spikeyarmaku commented 11 months ago

I think I have also found a problem in the PDF: in secton 5.4 (Tagging), theorem 13 (page 57), the equation for Y2_t: tag seems to be missing its first parameter.