2 Bugs in definitions of Z{f} and swap {f} in the PDF

[RonaldMonson]

The expositional style in this book is very Knuth-like - just enough information to reach understanding ... but no more. Hence, assuming that reported typos attract a A$3.00 bounty (up from Knuth's $2.56 due to inflation, Australian dollar conversion and the smaller margin of error required for subversive texts), here are two:

---

1.

pg 46 the definition of Z{f} has a missing closing "}" to complete wait's definition, i.e.

Z{f} = wait{self_apply, d{wait { self_apply} (K f)}

should read

Z{f} = wait{self_apply, d{wait { self_apply} (K f)} }

2.

pg 47 the definition of swap has the wrong (left) precedence by not having d { K f} apply to the term defined by "all" the remaining symbols that therefore need to be ()-wrapped i.e.

swap{f} = d{K f} d { d{K} (K delta) }( K delta)

should read

swap{f} = d{K f} (d { d{K} (K delta) }( K delta))

---

(Both however, are correctly implemented in Coq in Extensional_Programs.v )

[barry-jay-personal]

Thanks Ronald,I agree about the style. After some years, I realised that I was (unfortunately?) a poet. Prose should reveal all on one reading while poetry reveals more on rereading. The book could have been three times longer but then who would read it? Thanks for the feedback. I’m working on typed tree calculus now.Yours,BarryEnjoying life, working hardOn 10 Dec 2023, at 4:42 pm, RonaldMonson @.***> wrote: The expositional style in this book is very Knuth-like - just enough information to reach understanding ... but no more. Hence, assuming that reported typos attract a A$3.00 bounty (up from Knuth's $2.56 due to inflation, Australian dollar conversion and the smaller margin of error required for subversive texts), here are two:

pg 46 the definition of Z{f} has a missing closing "}" to complete wait's definition, i.e. Z{f} = wait{self_apply, d{wait { self_apply} (K f)} should read Z{f} = wait{self_apply, d{wait { self_apply} (K f)} }

pg 47 the definition of swap has the wrong (left) precedence by not having d { K f} apply to the term defined by "all" the remaining symbols that therefore need to be ()-wrapped i.e. swap{f} = d{K f} d { d{K} (K delta) }( K delta) should read swap{f} = d{K f} (d { d{K} (K delta) }( K delta))

(Both however, are correctly implemented in Coq in Extensional_Programs.v )

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

[RonaldMonson]

Hi Barry Yes, I agree that the text bears further fruit on re-readings-- perhaps also partly due to the new nature of the subject matter. Indeed perhaps even more brevity is possible from omitting all the connections to other models of computation and footnoting failed/less optimal attempts (as interesting as these are). I came toTree Calculus in need of "intentionality" as part of trying to establish greater rigor for my Wolfram Language code beyond improvements to its unit-testing framework. Systematically seeking such correctness at this bottom, compilation level seems insanely ambitious but tree calculus at least, at times, seems to make it appear somewhat less insane!

Regards Ron

On Mon, 11 Dec 2023 at 03:53, barry-jay-personal @.***> wrote:

Thanks Ronald,I agree about the style. After some years, I realised that I was (unfortunately?) a poet. Prose should reveal all on one reading while poetry reveals more on rereading. The book could have been three times longer but then who would read it? Thanks for the feedback. I’m working on typed tree calculus now.Yours,BarryEnjoying life, working hardOn 10 Dec 2023, at 4:42 pm, RonaldMonson @.***> wrote: The expositional style in this book is very Knuth-like - just enough information to reach understanding ... but no more. Hence, assuming that reported typos attract a A$3.00 bounty (up from Knuth's $2.56 due to inflation, Australian dollar conversion and the smaller margin of error required for subversive texts), here are two:

pg 46 the definition of Z{f} has a missing closing "}" to complete wait's definition, i.e. Z{f} = wait{self_apply, d{wait { self_apply} (K f)} should read Z{f} = wait{self_apply, d{wait { self_apply} (K f)} }

pg 47 the definition of swap has the wrong (left) precedence by not having d { K f} apply to the term defined by "all" the remaining symbols that therefore need to be ()-wrapped i.e. swap{f} = d{K f} d { d{K} (K delta) }( K delta) should read swap{f} = d{K f} (d { d{K} (K delta) }( K delta))

(Both however, are correctly implemented in Coq in Extensional_Programs.v )

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

— Reply to this email directly, view it on GitHub https://github.com/barry-jay-personal/tree-calculus/issues/7#issuecomment-1849064951, or unsubscribe https://github.com/notifications/unsubscribe-auth/AHEULXTBDDD5B3JVBLHMVXLYIYHM3AVCNFSM6AAAAABAOKD5QGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNBZGA3DIOJVGE . You are receiving this because you authored the thread.Message ID: @.***>

[barry-jay-personal]

Hi Ron,I share your insane ambitions 😉 it should be possible to represent the types, the stack, the heap and all the caches as trees, in a broad spectrum, declarative language. I imagine it would be easy to build an interpreter for tree calculus in Mathematica; might this help with your goals? What sort of intensionality are you in need of?Yours,BarryEnjoying life, working hardOn 12 Dec 2023, at 9:45 am, RonaldMonson @.***> wrote: Hi Barry

          Yes, I agree that the text bears further fruit on

re-readings-- perhaps also partly due to the new nature of the subject

matter. Indeed perhaps even more brevity is possible from omitting all the

connections to other models of computation and footnoting failed/less

optimal attempts (as interesting as these are). I came toTree Calculus in

need of "intentionality" as part of trying to establish greater rigor for

my Wolfram Language code beyond improvements to its unit-testing framework.

Systematically seeking such correctness at this bottom, compilation level

seems insanely ambitious but tree calculus at least, at times, seems to

make it appear somewhat less insane!

Regards

Ron

On Mon, 11 Dec 2023 at 03:53, barry-jay-personal @.***>

wrote:

Thanks Ronald,I agree about the style. After some years, I realised that I

was (unfortunately?) a poet. Prose should reveal all on one reading while

poetry reveals more on rereading. The book could have been three times

longer but then who would read it? Thanks for the feedback. I’m working on

typed tree calculus now.Yours,BarryEnjoying life, working hardOn 10 Dec

2023, at 4:42 pm, RonaldMonson @.***> wrote:

The expositional style in this book is very Knuth-like - just enough

information to reach understanding ... but no more. Hence, assuming that

reported typos attract a A$3.00 bounty (up from Knuth's $2.56 due to

inflation, Australian dollar conversion and the smaller margin of error

required for subversive texts), here are two:

pg 46 the definition of Z{f} has a missing closing "}" to complete wait's

definition, i.e.

Z{f} = wait{self_apply, d{wait { self_apply} (K f)}

should read

Z{f} = wait{self_apply, d{wait { self_apply} (K f)} }

pg 47 the definition of swap has the wrong (left) precedence by not having

d { K f} apply to the term defined by "all" the remaining symbols that

therefore need to be ()-wrapped i.e.

swap{f} = d{K f} d { d{K} (K delta) }( K delta)

should read

swap{f} = d{K f} (d { d{K} (K delta) }( K delta))

(Both however, are correctly implemented in Coq in Extensional_Programs.v

)

—Reply to this email directly, view it on GitHub, or unsubscribe.You are

receiving this because you are subscribed to this thread.Message ID:

@.***>

—

Reply to this email directly, view it on GitHub

https://github.com/barry-jay-personal/tree-calculus/issues/7#issuecomment-1849064951,

or unsubscribe

https://github.com/notifications/unsubscribe-auth/AHEULXTBDDD5B3JVBLHMVXLYIYHM3AVCNFSM6AAAAABAOKD5QGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNBZGA3DIOJVGE

.

You are receiving this because you authored the thread.Message ID:

@.***>

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

[RonaldMonson]

Hi Barry

<Hi Ron,I share your insane ambitions

Great! life is too short :)

<It should be possible to represent the types, the stack, the heap and all the caches as trees, in a broad spectrum, declarative language. I imagine it would be easy to build an interpreter for tree calculus in Mathematica; might this help with your goals? What sort of intensionality are you in need of

Indeed possible (as per all universal/complete languages) but as I take it here, "feasible". Yes have an inkling of its feasibility (with potentially profound consequences!) but having taken a few tentative steps, it seems there are some technical obstacles related to Y2 and encoding that seem to require more than just "engineering" to overcome? Probably not appropriate to outlay here in a bug report but could send privately if you have some time?

---

To a potential typo (or my misunderstanding) on pg 86-87 we have:

"The root-first evaluation of Chapter 6.7 has a useful property [to say the least] that is not shared by the other evaluation strategies of Chapter 6: if a combination M has a normal form N then root-and-branch evaluation will find it."

Is this consistent given that root-and-branch evaluation is another evaluation strategy of Chapter 6? (or is this somehow being qualified on the input?)

Regards Ron

[barry-jay-personal]

You can email me directly at @. life, working hardOn 13 Dec 2023, at 7:18 pm, RonaldMonson @.> wrote: Hi Barry

<Hi Ron,I share your insane ambitions

Great! life is too short :)

<It should be possible to represent the types, the stack, the heap and all the caches as trees, in a broad spectrum, declarative language. I imagine it would be easy to build an interpreter for tree calculus in Mathematica; might this help with your goals? What sort of intensionality are you in need of

Indeed possible (as per all universal/complete languages) but as I take it here, "feasible". Yes have an inkling of its feasibility (with potentially profound consequences!) but having taken a few tentative steps, it seems there are some technical obstacles related to Y2 and encoding that seem to require more than just "engineering" to overcome? Probably not appropriate to outlay here in a bug report but could send privately if you have some time?

---

To a potential typo (or my misunderstanding) on pg 86-87 we have:

"The root-first evaluation of Chapter 6.7 has a useful property [to say the least] that is not shared by the other evaluation strategies of Chapter 6: if a combination M has a normal form N then root-and-branch evaluation will find it."

Is this consistent given that root-and-branch evaluation is another evaluation strategy of Chapter 6? (or is this somehow being qualified on the input?)

Regards Ron

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