tree-calculus icon indicating copy to clipboard operation
tree-calculus copied to clipboard

Some bugs in the PDF

Open olydis opened this issue 1 year ago • 2 comments

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:

  • 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"?
  • Section 5.6: Defines isStem2 to return a boolean in the sense of the "new" encoding (leaf = false, fork = truth) which is explained right before. However, isStem2 is then used in the definition of triage_comb as if it returned a K/KI boolean. I.e. I believe triage_comb = ... isStem2 z α β should be triage_comb = ... Δ (isStem2 z) α (K² β)
  • Section 5.7: Defines triage_comb but later refers to it as triage.

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.

olydis avatar Sep 10 '23 19:09 olydis

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: @.***>

barry-jay-personal avatar Sep 11 '23 23:09 barry-jay-personal

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.

spikeyarmaku avatar Oct 17 '23 09:10 spikeyarmaku