help with basic derivations

I am very new to studying types, and I am struggling with derivation
rules. I would appreciate any help that can be offered, and greatly
so!


I am using a convention that a <- A means a is an element of the set
A.


a ---> a' is used to mean that a evaluates to a' in a single step.


I have the following as given:


true <- T false <- T


t1 <- T t2 <- T t3 <- T
----------------------------------------
if t1 then t2 else t3




And an evaluation rule


if true then t2 else t3 ---> t2


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!

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