CS 421 – Spring 2007Lecture Notes Set 32:Transition Semantics Continued and CPSElsa L. Gunter1Transcribed by: Pooja MathurCorresponding to Slides: 20a-trans-sem (slides 12-end) 26-CPS (slides 1-3)Made available: April 16, 2007Revision 1.01 Change Log1.0 Initial Release.2 Last notes on Transition Semantics2.1 Commands (slides 12-13)So last time, we finished talking about some of the commands. We ended with skip, assignment, and sequence. Now,we will talk about the if then else case. Here there are two overall cases. First if the expression is for the if statementis already a boolean value, then the next step would simlpy be to evaluate the case the if statement points to. If theexpression needs to be evaluated, that’s what you do first.Then there is the while command. To do this, you expand the while into an if then else expression. What you doto translate it is take the boolean expression that starts the while loop and then that becomes the if statement. Then asingle iteration of the command that you perform during the while loop becomes the then case along with another callto the while loop. The else case, the case that is called when the if statement is no longer true just has a skip in it. Toclarify, you do one of three things, you either, have to evaluate the boolean expression (if it hasn’t been evaluated yet),run one iteration of the while loop and call it again, or complete the while loop with the else case and move on.2.2 Example (slides 14-21)So, we want to evaluate (if x > 5 then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}) → ?? (Recall this is the same example thatwe showed how to solve with natural semantics.So what do we do first? What is the first step? Well, it is to evaluate the boolean expression. So that is what wedo. We need to evaluate (x > 5, {x → 7}) → ? Ok, from here, what would be our next step? We need to evaluate thex, so that is what we do: (x, {x → 7}) → 7. So at this point your tree should look like:Now that you have the 7, you can iterate that down the tree and now you have you next step of evaluating theboolean expression. So you have (7 > 5, {x → 7}) on the right side of the arrow on the second level. Next you caniterate that expression down, so now your new problem to solve is: (if 7 > 5 then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}).Now... that was just the first step of evaluating the original command and you should have a tree that looks like:1c 2007, Share and Enjoy1So what should the second step be? Well, we have to continue evaluating the boolean expression. So the bottomof the tree has: (if 7 > 5 then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}) → ?? And then what do we do, we evaluate 7 >5 and that returns true, so we send that down and get: (if true then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}). After thesecond step, our tree looks like:For the third step, we figure out which case our boolean is telling us to take:In the fourth step, we need to start evaluating the expression of the assignment, so we go and evaluate the 2 + 3.We get 5 back and then we know that the next thing we want to evaluate is (y:= 5 , {x → 7}). Our tree for this step is:Our final step is to make the finalized assignment. So we put y → 5 in memeory. This gives us the tree:If you look at all the bottom levels, you can watch the evaluation happen step by step. That is, you have:(if x > 5 then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}) →(if 7 > 5 then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}) →(if true then y:= 2 + 3 else y:= 3 + 4 fi, {x → 7}) →(y:= 2 + 3 , {x → 7}) →(y:= 5 , {x → 7}) →{y → 5, x → 7}2.3 Overall idea of evaluation (slides 22,29-31)So the idea behind transition semantics is that you have a string of proof trees. That is every transition from one stepto the next has a proof tree associated with it. The tree can be really small or really big, but it’s there. In comparison,in natural semantics, you create one huge proof tree above your initial expression.Basically, if you look at the tree we built for natural semantics the other day and then the trees for the evaluate thisway, you have a perfect example. The natural semantics tree ends up being on big one with many levels. Here the”proof tree” has steps. So, the tree in step one points to the tree for step two, which points to the tree for step four...allthe way to six, where we cannot evaluate any farther.Where transition semantics shows the relations between specific steps in evaluations, natural semantics show therelationship between steps and your final value.So why do we have both? Well, with natural semantics, it is much more intuitive to expression recursive programswhile transition semantics make it easy to show iterative programs. While natural semantics are more concise, wehave to still worry about our program never terminating.22.4 Adding Local Declarations (slides 23-25)Let’s now add in LetIn, functions, and function applications.So, for LetIn, the rule is going to look like: (let I = V in E, m). That is to say, let some identifier I be equal to somevalue V in the some expression E (and that goes with the memory m). So, here, since we already have the value, wecan just stick it in the expression. That is to say, anywhere we see the identifier I in the expression E, we are going toreplace with the value V. However, if the value has not been evaluated yet, we have to start evaluating it. So that is, ifthe whole thing has the structure, let some identifier I be equal to some expression E in some other expression E’, thefirst thing we have to do is evaluate the expression E. So that is what we do, and we get an E” back and then we cansay that the identifier I is equal to E” in the other expression E’.For functions, we can have (fun I → E) V with some memory m. What this is saying is that there is a functionthat takes an argument I and puts that arguement into the expression E. In that expression, I gets the value V appliedto it. So that’s what we get, we say that in the expression E, for any place that has the argument I, we will replaceit with V. That, however, is the case that the value we are passing in is already a value. But what if we are passingin an expression. In this case we have to evaluate the expression first, and then move on with the replacement andeverything in the next step.Note, …
View Full Document
Unlocking...