# 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" 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?