Re: help with basic derivations

jon.gallagher.04 wrote:


> The text I am using states that this evaluation rule means that when
> t1 = true, we can be sure the rule will always evaluate to t2. I
> believe it. I can't figure out how to prove it, or even how a
> derivation would get there. I try the following
>
> t1 <- T t2 <- T t3 <- T t1 = true
> ---------------------------------------------------
> if t1 then t2 else t3 t1 = true
> ------------------------------------------
> if true then t2 else t3 ---> t2
>
> From here how do I conclude t2?
>
> Thank you for any help you can give!


What you're describing looks like operational semantics for a simple
programming language. I'm currently working on a similar set of operational
semantic rules for another project.


I believe that you don't have to prove that "if true then t2 else t3"
evaluates to t2. I believe that this evaluation rule exists to define the
semantics of the if-then-else construct. It is not something for you to
prove. It is a basic building block you can use to prove more complicated
derivations.


--
Michiel Helvensteijn

Return to the comp.compilers page.
Search the comp.compilers archives again.