1 00:00:04,000 --> 00:00:07,930 In the next couple of videos, we're going to be looking at the details of the Kuhl 2 00:00:07,930 --> 00:00:11,611 operational semantics going over the semantics of each individual kind of 3 00:00:11,611 --> 00:00:15,691 expression. We'll start with easy ones and work our way up to the more complicated 4 00:00:15,691 --> 00:00:23,495 ones. So the easiest rules are the rules for the constants in Kuhl. So the value 5 00:00:23,495 --> 00:00:29,269 true, the expression true I should say, evaluates to a Boolean with the value true 6 00:00:29,269 --> 00:00:35,186 And it doesn't modify the store so the store is unchanged because it doesn't do 7 00:00:35,186 --> 00:00:42,196 any updates obviously And there's a corresponding rule for false And integers 8 00:00:42,196 --> 00:00:48,377 are very, very similar so if a integer expression, integer literal i will 9 00:00:48,377 --> 00:00:54,816 evaluate to, and integer object with the value i and again the store is not 10 00:00:54,816 --> 00:01:02,124 modified by such evaluation. And finally, strings if a, if s is a string literal of 11 00:01:02,124 --> 00:01:08,999 length n, then it will be evaluated by the string object of which the properties n 12 00:01:08,999 --> 00:01:17,513 and the string constant s. The evaluation of identifiers is very straightforward, 13 00:01:17,513 --> 00:01:23,593 given that we have both in environment in the store. So to evaluate an identifier 14 00:01:23,593 --> 00:01:29,823 and this would be a variable lane y x or y or for What do we do? Well first we look 15 00:01:29,823 --> 00:01:35,228 up in the environment where that identifier is stored so now we give us 16 00:01:35,228 --> 00:01:40,627 back a memory location l. So by in this case And then we look up in the store what 17 00:01:40,627 --> 00:01:45,407 the value is at that memory locations, So, we use the same memory location here as an 18 00:01:45,407 --> 00:01:49,693 argument to the store to get back the value that, that, that variable currently 19 00:01:49,693 --> 00:01:53,925 has And notice I just have a reference, this is a read of memories so this is 20 00:01:53,925 --> 00:01:58,596 loading, I think it was loading the value of the variable. This does not affect the 21 00:01:58,596 --> 00:02:03,102 store so the store is the same before and after. This is just looking at the value 22 00:02:03,102 --> 00:02:09,986 of the variable not updating the variable. The expression self just evaluates to the 23 00:02:09,986 --> 00:02:14,940 self object. So, this is a place where we just make use of the fact that the self 24 00:02:14,940 --> 00:02:20,204 object is part of the environment so let's just copy them over here as the result of 25 00:02:20,204 --> 00:02:25,220 expression and that was again that the store is unaffected by evaluation of self. 26 00:02:26,480 --> 00:02:31,720 Now let's see of a more slightly more complicated evaluation is evaluated, in 27 00:02:31,720 --> 00:02:36,896 particular the assignment expression. So an assignment consists of two parts, an 28 00:02:36,896 --> 00:02:42,333 identifier that is being updated and an expression that is going to give us the 29 00:02:42,333 --> 00:02:47,771 new value. So for example, just to remind you we might have something like x gets 30 00:02:47,771 --> 00:02:53,340 one + one so one + one here would be the expression e and x would be the identifier 31 00:02:53,340 --> 00:02:58,395 All right? And so in order to evaluate the assignment, the first thing we have to do 32 00:02:58,395 --> 00:03:03,509 is we have to know what value we're going to be writing into the identifier. So what 33 00:03:03,509 --> 00:03:08,036 is the, what is the update we're going to perform? So the first thing to do is to 34 00:03:08,036 --> 00:03:12,856 evaluate e, okay? And notice here that e is evaluated in the same environment so it 35 00:03:12,856 --> 00:03:17,559 has the same three components here, and here, all right? So it just says the first 36 00:03:17,559 --> 00:03:22,455 thing we do is we run e. Okay. That will give us back a new value. We're going to 37 00:03:22,455 --> 00:03:27,904 get back on value b excuse and possibly an updated score so you can arbitrate a piece 38 00:03:27,904 --> 00:03:32,530 of code. You could yourself have assignment statements in it so the story 39 00:03:32,530 --> 00:03:37,346 that we get out might be different. Alright, so e produces the value of e and 40 00:03:37,346 --> 00:03:42,857 an update store s1 And now it's actually due to assignment, what do we do? Well we 41 00:03:42,857 --> 00:03:48,067 have to know what memory location was supposed to update so we look up the 42 00:03:48,067 --> 00:03:53,834 memory location for id and that would give us some location else of id. And then we 43 00:03:53,834 --> 00:03:59,600 modify the store with the new, we modify the store at that point with the new value 44 00:03:59,600 --> 00:04:04,811 so we replace the location l, i, d or we update the value of l, i, d to be the 45 00:04:04,811 --> 00:04:10,368 value of e, the value b and we do that in store s1 which gives us a new store s2. 46 00:04:10,368 --> 00:04:15,674 And I've noticed. That s2 is the store that results from the evaluation of e, 47 00:04:15,674 --> 00:04:21,616 okay? So after we do the assignment, the assignment returns the value b which is of 48 00:04:21,616 --> 00:04:27,037 course the value of a, of running e. And, it returns the updated store s2. Next, 49 00:04:27,037 --> 00:04:34,080 let's talk about the operational rule for addition. So, to evaluate e1+e2, what we 50 00:04:34,080 --> 00:04:40,246 are going to do? So, first we evaluate e1 And notice that is done in the same 51 00:04:40,246 --> 00:04:45,678 context as the context of the entire e xpression, okay? So the components the 52 00:04:45,678 --> 00:04:51,806 context here for evaluating one are exactly the same as the components for the 53 00:04:51,806 --> 00:04:57,098 overall expression e1 + e2. So when we evaluate e1 it's going to give us a value 54 00:04:57,098 --> 00:05:02,460 of e1 and it's also going to give us an updated store s1 And then we're going to 55 00:05:02,460 --> 00:05:08,570 evaluate e2 and notice here And I think context is different. The soft objects in 56 00:05:08,570 --> 00:05:14,704 the environment are the same; same but now we're running e2 in the new store s1. And 57 00:05:14,704 --> 00:05:20,262 what does its saying is that if e2 has, has assignments or variable references in 58 00:05:20,262 --> 00:05:25,356 it those assignments and variable references have to be done on the store 59 00:05:25,356 --> 00:05:30,781 that resulted from running e1, okay? So, it's very important that we get that any 60 00:05:30,781 --> 00:05:35,809 side effects would happen in running e1 are visible or that are seen by the 61 00:05:35,809 --> 00:05:40,639 expression e2. So we run e2 in this environment, we're going to get the value 62 00:05:40,639 --> 00:05:45,914 of e2 and the updated store s2 And then the result of the entire expression is 63 00:05:45,914 --> 00:05:51,137 going to be b1 + b2 and the results it store will be the store s2. And notice 64 00:05:51,137 --> 00:05:57,065 here how the stores tell you the order in which you have to evaluate the 65 00:05:57,065 --> 00:06:03,538 expressions. So because e1 is evaluated in the same store as the overall expression 66 00:06:03,538 --> 00:06:10,401 that tells you that e1 has to be evaluated first. And then because e2 is evaluated in 67 00:06:10,401 --> 00:06:16,484 the store that's produced by e1, that tells you that e1, e2 excuse me, has to be 68 00:06:16,484 --> 00:06:22,847 evaluated after you've evaluated e1 and then the fact that. S2 is the result of 69 00:06:22,847 --> 00:06:28,293 the whole thing. It tells you [inaudible] is also the last thing that you evaluate 70 00:06:28,293 --> 00:06:34,358 during the execution of this particular expression. Okay, let's take a look at the 71 00:06:34,358 --> 00:06:40,260 statement block and just a variety here on the change my colors. How are we going to 72 00:06:40,260 --> 00:06:45,051 evaluate the, a statement block of statements e1 through en, okay, so, while 73 00:06:45,051 --> 00:06:50,219 this is semantics, this is that we should run, I mean order beginning of e1 and the 74 00:06:50,219 --> 00:06:55,136 results of the entire execution will be the, let's say the value of the entire 75 00:06:55,136 --> 00:06:59,927 block with the value of the last expression. And this, this rule just says 76 00:06:59,927 --> 00:07:05,032 that. So, first, we evaluate e1 and also it's done on the same store as the overall 77 00:07:05,032 --> 00:07:10,390 expressio n as it tells you it has to come first and that produces a new store s1 and 78 00:07:10,390 --> 00:07:16,389 the value b1. Okay And then e2 is evaluated in the store s1 and it produces 79 00:07:16,389 --> 00:07:23,406 the store s2 and so on And then expression en is evaluated in the store sn - one and 80 00:07:23,406 --> 00:07:29,246 it produces a value of bn and an updated store s (N). Okay? And then the result of 81 00:07:29,246 --> 00:07:34,175 the whole thing is the value of vn and also the updated store s (N) and this 82 00:07:34,175 --> 00:07:39,042 tells you, this would really tell you the order which had to evaluate the sub 83 00:07:39,042 --> 00:07:44,220 expressions. The dependencies here on the store of course you do evaluate e1 and 84 00:07:44,220 --> 00:07:49,336 then e2 and then e3 and so on so you have to do them to net order to get the side 85 00:07:49,336 --> 00:07:53,607 effects to get. You know the side effects in the correct order for all of these 86 00:07:53,607 --> 00:07:57,640 expressions And furthermore, it also tells you the only value that you're going to 87 00:07:57,640 --> 00:08:01,624 keep is the value vn. Notice that none of the other values that are produced here 88 00:08:01,624 --> 00:08:07,319 are used for anything. They don't appear anywhere else in the rules. Let's think 89 00:08:07,319 --> 00:08:13,531 what we've learned so far and do a small example. So we want to know what happens 90 00:08:13,531 --> 00:08:19,040 when we evaluate the block. X gets assigns seven + five, that's the first statement 91 00:08:19,040 --> 00:08:23,518 and the second and the last statement in the block, is just the expression four. 92 00:08:23,518 --> 00:08:28,165 And the first thing we have to do is to say what the context did and which we are 93 00:08:28,165 --> 00:08:32,530 going to evaluate this and the context consists of three parts. There'll be a 94 00:08:32,530 --> 00:08:37,064 self object and in this case it doesn't really matter what's in the self object 95 00:08:37,234 --> 00:08:41,768 because self is not referred to in the program and so it won't play any role in 96 00:08:41,768 --> 00:08:46,246 the evaluation. But we, we still need it so there still be, there'll be some self 97 00:08:46,246 --> 00:08:51,028 object out there just won't get used and Now, in the new environment which tells us 98 00:08:51,028 --> 00:08:55,887 the locations where all the free variables in the programs. So, we'll just need a 99 00:08:55,887 --> 00:09:00,908 place for x is going to be stored and so s will be stored in some location l And then 100 00:09:00,908 --> 00:09:07,409 we know our memory content is, where our store is and let's just say that at l we 101 00:09:07,409 --> 00:09:13,374 have initially the value zero, okay? So now we can use our rules to run this 102 00:09:13,374 --> 00:09:19,340 program or to evaluate thi s program. I'm going to make this line here much longer 103 00:09:19,340 --> 00:09:25,876 And recall that, that evaluation of block consist of the evaluation of the, all the 104 00:09:25,876 --> 00:09:32,337 statements within the block. Okay, so the first one is going to be s gets seven+5 105 00:09:32,337 --> 00:09:38,489 and that will be evaluated in the same environment as the overall expression. So, 106 00:09:38,489 --> 00:09:44,865 we have up here. So the same context excuse me and I should say I often slip 107 00:09:44,865 --> 00:09:50,820 and I realize and say environment for the entire left hand side of one of these 108 00:09:50,820 --> 00:09:55,935 judgments. I'll try to be consistent. And just use environment for the, for the 109 00:09:55,935 --> 00:10:00,686 second components of the context often in the literature people call the entire 110 00:10:00,686 --> 00:10:05,022 thing on the left hand side of the environment that's why they make this 111 00:10:05,022 --> 00:10:09,714 mistake but you know for this instead of notes I'm trying to be consistent the 112 00:10:09,714 --> 00:10:14,465 entire, all the components on left hand side together are called the context and 113 00:10:14,465 --> 00:10:18,920 the environment is just the second component. The mapping from variables to 114 00:10:18,920 --> 00:10:25,302 their locations Anyway coming back to the example, The first statement in the block 115 00:10:25,302 --> 00:10:32,316 is s gets seven+5 alright. And then we're going to have the second statement as 116 00:10:32,316 --> 00:10:38,652 well. And we know that the self object and the environment won't change but we don't 117 00:10:38,652 --> 00:10:44,446 know what the store will be. The store might be different so I'll leave the store 118 00:10:44,653 --> 00:10:50,378 empty for now and we'll figure that out later and we're going to be evaluating the 119 00:10:50,378 --> 00:10:55,482 expression four. Okay, so this is the structure of the evaluation now in 120 00:10:55,482 --> 00:11:01,344 progress. We should look at, at this first statement trying to make some forward 121 00:11:01,344 --> 00:11:06,734 progress on that one. So, to evaluate the assignment, what do we have to do? Well, 122 00:11:06,734 --> 00:11:12,474 the very first thing we have to do is we have to evaluate the right hand side so 123 00:11:12,474 --> 00:11:18,214 we're going to have the context for that is going to be the same And the context 124 00:11:18,214 --> 00:11:23,600 we've been looking at all on because it's the first thing that's actually going to 125 00:11:23,600 --> 00:11:29,064 happen is to evaluate Seven + five, okay? And now, I'm leaving a little space down 126 00:11:29,064 --> 00:11:34,545 here for the rest of the assignment role which we're not going to fill in just yet. 127 00:11:34,545 --> 00:11:40,300 Now to evaluate the plus expression we have to evaluate the first express ion and 128 00:11:40,300 --> 00:11:46,006 the second expression, okay? And so, how do we do that? Well, we know, finally, I 129 00:11:46,006 --> 00:11:52,272 think how to do that because we're finally down and we're going to have a single 130 00:11:52,272 --> 00:12:01,850 integer there and that. We already have a rule for it, okay and so [inaudible] the 131 00:12:01,850 --> 00:12:08,678 literal evaluates to institute your object, okay And inside that object is 132 00:12:08,678 --> 00:12:16,227 just about the value, okay. And the store is unmodified All right? And then 133 00:12:16,227 --> 00:12:31,346 similarly for the other argument here, Okay. So the five will also evaluate to an 134 00:12:31,346 --> 00:12:37,295 integer object with the value of five and the store will be unmodified okay so 135 00:12:37,295 --> 00:12:43,169 that's the two sum expressions of this edition and so now we can fill in the 136 00:12:43,169 --> 00:12:49,344 results here so to take the contents of the two integers we'll add them. That will 137 00:12:49,344 --> 00:12:55,518 also be integer object so we're going to have the integer object twelve. And the 138 00:12:55,518 --> 00:13:00,364 store has not been changed, okay? So the, the store that we get out of here happens 139 00:13:00,364 --> 00:13:04,971 to be the same as the store that went in just because this expression had no 140 00:13:04,971 --> 00:13:10,065 assignments in it, okay? And now we're ready to do the assignment. Okay. So how 141 00:13:10,065 --> 00:13:16,814 do we do that? Well, we have to form a new store. Alright, so we're going to have a 142 00:13:16,814 --> 00:13:24,795 new store which will the L gets zero with the value of l. Number which way, my 143 00:13:24,795 --> 00:13:31,391 notation went here, I think it's the number comes first and we're going to put 144 00:13:31,391 --> 00:13:38,691 twelve in the location l and of course, that's store was just equal to the store 145 00:13:38,691 --> 00:13:45,903 where l has the value twelve, okay And so now, what happens down here and we do the 146 00:13:45,903 --> 00:13:52,486 assignment and we get out The new value. Okay so, the value of the right hand side 147 00:13:52,486 --> 00:13:58,339 is twelve and we have a new store where the location l has twelve, all right? So 148 00:13:58,339 --> 00:14:04,192 now we're going to evaluate the second statement in the block and that will be 149 00:14:04,192 --> 00:14:10,267 done in the store where l has the location twelve and of course this is just an 150 00:14:10,267 --> 00:14:16,181 integer And so that will evaluate to the integer constant of four, the integer 151 00:14:16,181 --> 00:14:21,806 value excuse me, 4or integer object containing, the integer object with the 152 00:14:21,806 --> 00:14:27,356 value four and our store. And it's just going to fit not quite, all right? And 153 00:14:27,356 --> 00:14:33,057 that's then the result of the entire evaluation . So, this block will produce 154 00:14:33,057 --> 00:14:39,367 the value four, an integer object with the value four and an updated store where 155 00:14:39,367 --> 00:14:46,456 location l has the value twelve. So, the next expression I would like to take a 156 00:14:46,456 --> 00:14:52,225 look at is the if, then, else expression and to evaluate if, then, else what do we 157 00:14:52,225 --> 00:14:57,180 do? Actually there should be if, then, else. See of course, so evaluating if, 158 00:14:57,180 --> 00:15:02,256 then, else as well. First we have to evaluate the, the predicate and it's done 159 00:15:02,256 --> 00:15:07,732 in the same store, the same context as the overall expression and if the result is 160 00:15:07,732 --> 00:15:12,598 true If the, if the Boolean predicate returns the value true. Then we want to 161 00:15:12,598 --> 00:15:17,623 evaluate just the true branch and not the false branch so that's why you only see 162 00:15:17,623 --> 00:15:22,404 here, evaluation of e2 and e3 isn't mentioned anywhere and just know here that 163 00:15:22,404 --> 00:15:27,614 the predicate may have side effects and so e2 is evaluated in whatever store that e1 164 00:15:27,614 --> 00:15:32,150 produces And then the results of the entire expression is the value of e2. 165 00:15:32,150 --> 00:15:38,134 Okay, that's v and also just the final store is produced by running the then 166 00:15:38,134 --> 00:15:44,497 branch. And there is a symmetric rule for what happens if the predicate evaluates 167 00:15:44,497 --> 00:15:49,859 the false. In that case, you would evaluate e3 and not e2. Next we'll take a 168 00:15:49,859 --> 00:15:54,895 look with what happens with while loops and cool. So there are two cases. First if 169 00:15:54,895 --> 00:15:59,807 the predicate of the while loop evaluates the false, okay. Well, in this case the 170 00:15:59,807 --> 00:16:04,905 loop body is not going to execute, alright so the first thing we do is we evaluate 171 00:16:04,905 --> 00:16:10,066 the predicate and that's done in the same context as the evaluation of the overall 172 00:16:10,066 --> 00:16:15,164 expression and if the predicate is false then we exit the loop and so the results 173 00:16:15,164 --> 00:16:19,765 of the loop is void. The value void and just whatever store resulting from 174 00:16:19,765 --> 00:16:25,031 evaluating the predicate. The other possibility is that the predicate 175 00:16:25,031 --> 00:16:30,421 evaluates the true. So here we evaluate the predicate again in the same context as 176 00:16:30,421 --> 00:16:35,745 the overall loop. And if the predicate evaluates the true then we're going to run 177 00:16:35,745 --> 00:16:40,569 the loop audio once. Okay. So we'll evaluate the loop audio and also that's 178 00:16:40,569 --> 00:16:45,768 done in this, in whatever store results from evaluating the predicate. Evaluating 179 00:16:45,768 --> 00:16:51,032 the loop audio is g onna give us a value of v and a new store s2 and then what we 180 00:16:51,032 --> 00:16:56,361 need to do is we need to go back around and execute the loop again and how can we 181 00:16:56,361 --> 00:17:01,560 do that? Well, we're really just running the whole loop in the new context. So, the 182 00:17:01,560 --> 00:17:06,958 next thing we do is we evaluate the entire loop. Right in the new store So, after I 183 00:17:06,958 --> 00:17:12,254 execute the loop by, loop body one time, then we go around and just evaluate the 184 00:17:12,254 --> 00:17:17,616 loop again And when this may run for zero or more iterations, alright. And when I 185 00:17:17,616 --> 00:17:23,112 finally terminate, if it terminates, it will produce it will produce a new store 186 00:17:23,112 --> 00:17:28,877 s3 evaluated while because always produced the value of a void. And then what we'll 187 00:17:28,877 --> 00:17:33,971 produce for the entire loops, for the entire expression is the value void and 188 00:17:33,971 --> 00:17:40,373 the update and store s3. The next interesting expression to take a look at 189 00:17:40,373 --> 00:17:45,577 is the let expression. So recall how, what this looks like so let and cool has a 190 00:17:45,577 --> 00:17:51,045 variable thing declared and it's type and an initializer which is optional so this 191 00:17:51,045 --> 00:17:56,512 is the value that the identifier will be initialized to and then the expression in 192 00:17:56,512 --> 00:18:01,581 which that new variable is available. And so how do we evaluate this? Well first, 193 00:18:01,581 --> 00:18:06,155 we're going to evaluate the initial value of the, of the new variables. So we 194 00:18:06,155 --> 00:18:11,106 evaluate e1 and as usual that's done in the initial store it produces possibly 195 00:18:11,106 --> 00:18:16,118 modified store. And now the question is, what are going to, what's going to be the 196 00:18:16,118 --> 00:18:21,194 context here for the evaluation of e2 for the body of the latter? And so it seems 197 00:18:21,194 --> 00:18:26,144 clear that it's going to involve s1 because it has all the updates from e2 but 198 00:18:26,144 --> 00:18:31,220 it also has to have this new identifier in it. And so how are we going to do that? 199 00:18:31,800 --> 00:18:36,292 So, what we want is to have a new environment e but with new binding of ID 200 00:18:36,292 --> 00:18:40,609 to refresh location. So, we're introducing a new variable. Remember that the 201 00:18:40,609 --> 00:18:45,159 environment has tracked all the free variables so this is one situation where 202 00:18:45,159 --> 00:18:50,177 you should going to extend the environment e with the new binding, alright. And that 203 00:18:50,177 --> 00:18:54,436 location, the location for the new variable has to be a fresh location. We 204 00:18:54,436 --> 00:18:58,870 don't want to conflict with any other memory locations we are already using. 205 00:18:58,870 --> 00:19:03,960 Okay And so, we're going to allocate a new memory location for the variable And then 206 00:19:03,960 --> 00:19:09,231 the store, the new store will also will be like as one as we said we have to include 207 00:19:09,231 --> 00:19:13,897 all the, the values for s1 But also, we can have these new location for the 208 00:19:13,897 --> 00:19:20,328 variable and that's going to have the initial value of the variable e1. To 209 00:19:20,328 --> 00:19:25,607 express that we need a new location, we're going to introduce a new operation on the 210 00:19:25,607 --> 00:19:30,635 store which gives us a new fresh location. So new lo applied to a store it's just 211 00:19:30,635 --> 00:19:35,851 going to give us some location that isn't being used by the store. So, the store has 212 00:19:35,851 --> 00:19:40,690 a domain where it's a mapping from locations to values and we'll just pick 213 00:19:40,690 --> 00:19:46,032 some new location that isn't in the current list of locations within the store 214 00:19:46,032 --> 00:19:51,311 and that will be the one returned or that will be one, that will be the one returned 215 00:19:51,311 --> 00:19:56,485 by new lo. Okay, so new lo if you can think of As modeling the memory allocation 216 00:19:56,485 --> 00:20:01,897 function in the runtime system. So, then, here we can write out the rule. So, this 217 00:20:01,897 --> 00:20:07,052 is the most complicated rule we seen so far. So, I'll just take a moment to walk 218 00:20:07,052 --> 00:20:12,110 through it All right? So, the first thing we do is we evaluate e1, the initializer 219 00:20:12,110 --> 00:20:17,079 for the new variable, okay? So just like before, this is done in the same context 220 00:20:17,079 --> 00:20:21,734 as the overall expression and this is going to give us a value for e1 and an 221 00:20:21,734 --> 00:20:26,389 updated store, all right? Then in the updated store, using the updated store 222 00:20:26,389 --> 00:20:31,627 here we find an unused location, l new. Okay And then we're going to create a 223 00:20:31,627 --> 00:20:37,548 store where that new location has, has the value of e1. So we're going to store the 224 00:20:37,548 --> 00:20:43,243 value of e1 at that new location. We're going to update the store s1 to reflect 225 00:20:43,243 --> 00:20:48,714 that and further more we're going to extend our environment with the new 226 00:20:48,714 --> 00:20:54,860 identifier which will be stored at this new location and this is the context then. 227 00:20:54,860 --> 00:21:00,187 Okay, with this updated environment in store in which we evaluate the body of the 228 00:21:00,187 --> 00:21:05,580 lab which will produce the value b2 and possible update in store s2 and those are 229 00:21:05,580 --> 00:21:08,080 the results of the overall expression.