Wed, 28 Jan 2009 00:28:55 +0100

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: | Michiel Helvensteijn <m.helvensteijn@gmail.com> |

Newsgroups: | comp.compilers |

Date: | Wed, 28 Jan 2009 00:28:55 +0100 |

Organization: | Compilers Central |

Keywords: | types |

Posted-Date: | 27 Jan 2009 19:09:32 EST |

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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.