p.86 of the hardcopy

[alexhkurz]

I am referring to the rule for function calls. I propose the following (thanks to my students):

===

1. in f(a1 , ... an) the "n" should an "m"

2. the gamma in "gamma.x1" on the left just above the horizontal line should be a gammaₘ

3. the gamma′ should be a gamma′.delta (the delta is needed to make work the below)

4. the gammaₘ on the right below the horizontal bar should be a gamma′

===

Wrt to item 2), the book says that it does not matter whether one would put gamma or gammaₘ . But if we take the following C program

int x = 10; int f (int y) { return ++x; }

then calling f(++x) modifies the global variable x to 12. This is not compatible with running { return ++x; } in context gamma (which has x:=10) but requires that { return ++x; } is run in context gammaₘ (which has x:=11).

[andreasabel]

Thanks for the report!

Yes, as soon as you have global variables, or nested environments like in Pascal, you need the changes 2.-4.

In my lectures, I separated the function signature sigma from the variable environment gamma. The rule then becomes:

sigma;gamma_{i-1}        |- a_i ==> <v_i,gamma_i>  for i=1..m
sigma;(x_i=v_i)_{i=1..m} |- ss  ==> <v,_>
------------------------------------------------------------- sigma(f) = x_{1..m}.ss
sigma;gamma_0 |- f(a_1,...,a_m) ==> <v,gamma_m>

So, the body ss of function f is run in a fresh environment only containing the bindings for its parameters. The function signature sigma stays fixed throughout interpretation.

[alexhkurz]

On Apr 23, 2021, at 03:10, Andreas Abel ***@***.***> wrote: Thanks for the report! Yes, as soon as you have global variables, or nested environments like in Pascal, you need the changes 2.-4. In my lectures, I separated the function signature sigma from the variable environment gamma. The rule then becomes: sigma;gamma_{i-1} |- a_i ==> <v_i,gamma_i> for i=1..m sigma;(x_i=v_i)_{i=1..m} |- ss ==> <v,_> ------------------------------------------------------------- sigma(f) = x_{1..m}.ss sigma;gamma_0 |- f(a_1,...,a_m) ==> <v,gamma_m> So, the body ss of function f is run in a fresh environment only containing the bindings for its parameters. The function signature sigma stays fixed throughout interpretation.

Thanks ... but doesnt my example show that the body ss needs to be run in gammaₘ and to return an environment gamma′ that takes into account updates to gammaₘ? Here are the details: In my example, gamma₀ has x:=10. gammaₘ has x:=11 (because the function call does a preincrement on x) after the function call we have a new environment which has x:=12 (because ss increments x) I don't see that your rule is doing this. With your rule the result of the function is the same as in my case, but the value of x after the function call in the environment is x:=11 in your case and x:=12 in my case. I verified that when I run the program in C++, the environment does have x:=12 after the function call.

…

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[andreasabel]

Sorry, maybe I was not clear enough.

• You are absolutely right if global variables (like int x = 10; outside of the function) are part of the game.
• However, the fragment of C that the book deals with does not include global variables. Thus, my refinement is valid. (++x is an ill-scoped expression ruled out by the type-checker.)

[alexhkurz]

ok, thanks for the clarification ... so I will treat this as an exercise in the future: how to extend the rule so that it can account for global variables ... anyway, it still looks to me that the "... a _ n" instead of "... a _ m" remains a misprint that you could take up in the list of errata

…

On Apr 23, 2021, at 08:29, Andreas Abel ***@***.***> wrote: Sorry, maybe I was not clear enough. • You are absolutely right if global variables (like int x = 10; outside of the function) are part of the game. • However, the fragment of C that the book deals with does not include global variables. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[andreasabel]

anyway, it still looks to me that the "... a _ n" instead of "... a _ m" remains a misprint that you could take up in the list of errata

Yes, it's there: andreasabel@1d87dad