Mon, 26 Jan 2009 09:25:50 -0800 (PST)

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) |

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.