help with basic derivations

"jon.gallagher.04" <jon.gallagher.04@gmail.com>
Mon, 26 Jan 2009 09:25:50 -0800 (PST)

          From comp.compilers

Related articles
help with basic derivations jon.gallagher.04@gmail.com (jon.gallagher.04) (2009-01-26)
Re: help with basic derivations m.helvensteijn@gmail.com (Michiel Helvensteijn) (2009-01-28)
Re: help with basic derivations jon.gallagher.04@gmail.com (jon.gallagher.04) (2009-01-30)
Re: help with basic derivations m.helvensteijn@gmail.com (2009-02-03)
| List of all articles for this month |

From: "jon.gallagher.04" <jon.gallagher.04@gmail.com>
Newsgroups: comp.compilers
Date: Mon, 26 Jan 2009 09:25:50 -0800 (PST)
Organization: Compilers Central
Keywords: types, question
Posted-Date: 27 Jan 2009 15:43:15 EST

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!



Post a followup to this message

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