Operational Semantics to Denotational Semantics I made a interpretive mistake on Wednesday. To prove completeness, on Wednesday, I tried to derive the inference rules of operational semantics, and that wasn't right. What I should have done (which would have been easier and accurate) is show that the inference rules of operational semantics actually give the right answer. Operational Semantics: ->true ->sigma' ____________________________________ ->sigma'. ->false ->sigma' ____________________________________ ->sigma'. Denotational Semantics: C[[if b then c1 else c2]] (sigma) = B[[b]] (C[[c1]](sigma),C[[c2]](sigma)) Correctness (soundness): If ->true, then B[[b]] = true from structural induction. So, C[[if b then c1 else c2]] (sigma) = C[[c1]](sigma) = something which we will call sigma' which, by structural induction means that ->sigma' From our operational semantics, ->sigma'. Therefore C[[if b then c1 else c2]](sigma) also equals sigma'. If ->false, then B[[b]] = false from structural induction. So, C[[if b then c1 else c2]] (sigma) = C[[c2]](sigma) = something which we will call sigma' which, by structural induction means that ->sigma' From our operational semantics, ->sigma'. Therefore C[[if b then c1 else c2]](sigma) also equals sigma'. Completeness: If we assume C[[if b then c1 else c2]] (sigma) = B[[b]] (C[[c1]](sigma),C[[c2]](sigma)) Once again, if B[[b]] is true, we know that ->true C[[if b then c1 else c2]](sigma) = C[[c1]](sigma) If C[[c1]](sigma) = sigma' (by definition) then ->sigma' by structural induction, so we can get that ->sigma'. From these two rules, operational semantics derives ->sigma', which matches the equation from denonational semantics, the derivation gives the right answer. Once again, if B[[b]] is false, we know that ->false C[[if b then c1 else c2]](sigma) = C[[c2]](sigma) If C[[c2]](sigma) = sigma' (by definition) then ->sigma' by structural induction, so we can get that ->sigma'. From these two rules, operational semantics derives ->sigma', which matches the equation from denonational semantics, the derivation gives the right answer. The while loop is trickier. The other proofs were more straightforward because we were building commands from smaller commands. Sequence is two smaller commands pasted together. if is also two smaller commands pasted together. Operational semantics: ->false ___________________________ ->sigma ->true ->sigma'' ->sigma' _____________________________________________________________________ ->sigma'. Denotational semantics: C[[while b do c]](sigma) = B[[b]] (C[[while b do c]](C[[c](sigma)),sigma) Structural induction assumes that the two semantics are true for the "smaller statements" I'm building from and from that I demonstrate that it's true for the larger statement. (Seq, if). However, for while, I'm not building a while loop from a smaller statement. I'm building a while loop from the same statement. We can do recursion on the number of the times the loop runs. We know that the loop does not run an infinite number of times because we are assuming no infinite loops because operational semantics doesn't work for them. Let's prove true the loop that runs 0 times. If the loop runs 0 times, then b is false. We have the operational semantics: ->false ___________________________ ->sigma now, our denotational semantics C[[while b do c,sigma]] = sigma since the loop doesn't run, which matches our equation C[[while b do c]](sigma) = B[[b]] (C[[while b do c]](C[[c](sigma)),sigma). Conversely, if the equation is true, C[[while b do c]] (sigma) will give us sigma since B[[b]] is false. Since B[[b]] is false, we know that ->false and since our derived statement ->sigma, this tells us that our operational semantics are correct in this case. So, now let's say that the loop runs n times. We can assume that our operational and denotational semantics match for loops that run fewer than n times. ->true ->sigma'' ->sigma' _____________________________________________________________________ ->sigma'. We see that the loop in the assumptions runs one fewer time than the loop in the conclusion. The loop on top starts at the state that follows the first iteration of the command. So, for that loop in the top, we can assume that the semantics match. So, assuming operational semantics work, C[[while b do c]] (sigma) = ... We know that C[[c]](sigma) = sigma'' and we know that C[[while b do c]](sigma'') = sigma' from induction/structural induction. So, C[[while b do c]](sigma) = sigma' (from operational semantics) and the equation C[[while b do c]](C[[sigma]]) = sigma' as well from the computation above, so, again the equation holds: C[[while b do c]](sigma) = B[[b]] (C[[while b do c]](C[[c](sigma)),sigma) since we know that B[[b]] is true because we're running a loop that runs at least once. Conversely, suppose the denotational semantics is correct. We know that B[[b]] is true since the loop is more than once. We know that ->true from structural induction. C[[c]](sigma) has to equal something, call it sigma''. From structural induction, we know that ->sigma''. C[[while b do c]](C[[c](sigma)): The while loop is running one time fewer than the one on the left, since both start from sigma, but this one here has already once. So, from induction, if we define sigma' to be C[[while b do c]](sigma''), we can conclude that ->sigma'. So, from these under assumptions under operational semantics we derive ->sigma'. And that is also the answer of the denotional semantics equation. C[[while b do c]](sigma) = B[[b]] (C[[while b do c]](C[[c](sigma)),sigma) We know that b is true since the loop is running at least once. So, the expression on the right C[[while b do c]](C[[c](sigma)) = C[[while b do c]](sigma'') = sigma'. So, the operational semantics yielded the correct answer. ********** The first programming language that Dr. Poe ever learned. (1978). The first language I ever learned was APL. APL: A Programming Language Invented by Kenneth Iverson, and he got the Turing award for it. APL: language-neutral. There are no keywords in APL. Everything is symbolic. You need a special character set for APL. APL does not use ASCII. APL heavily promoted and developed by IBM, APL's character set is more closely related to EBCDIC, but it isn't EBCDIC, either. In the old teletype days, some characters could only be created by overstrike. You would type a symbol, backspace, and then type another symbol. A simple example is the exclamation point, which did not exist on the APL keyboards of that time. You would type an apostrophe, back space, and type a period. Once terminals/monitors were used for APL, then you could get the special keyboard that would allow you to type in characters without backspacing. (Although, when APL2 came out, you still had backspace until the terminals were able to accommodate this.) You type from left to right (like everything else). The program is parsed from right to left. There is no order of operations in APL. You just move from right to left. 5x3+3 = 30 in APL. 3+3x5 = 18 in APL. You can use parentheses. (5x3)+3 = 18. Iota generates an array from 1 to the specified argument. iota 10 gives you the array 1 2 3 4 5 6 7 8 9 10 The / means compress. From the array on the right, compress the array as directed on the left.?