Re: help with basic derivations

Michiel Helvensteijn <>
Wed, 28 Jan 2009 00:28:55 +0100

          From comp.compilers

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

From: Michiel Helvensteijn <>
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

Michiel Helvensteijn

Post a followup to this message

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