Overview

• We consider EXP and its operational semantics

• EXP supports Boolean constants, negation and conjuction

• We extend EXP with Boolean disjunction

• We discuss some alternative specifications and its consequences

EXP: A simple expression language

The syntax of EXP is as follows.

 B ::= true | false

 E ::= B | !E | E && E

The operational semantics of EXP is defined as follows.

          E => true
(Not-1)  -------------
          !E => false

          E => false
(Not-2)  -------------
          !E => true

           E1 => false
(And-1)   -----------------
           E1 && E2 => false

           E1 => true
           E2 => false
(And-2)   -----------------
           E1 && E2 => false

           E1 => true
           E2 => true
(And-3)   -----------------
           E1 && E2 => true

Fact: The above rules are deterministic and evaluation never gets stuck.

Deterministic means that for any expression E, if E => true, then E => false is impossible (and vice versa).

Never stuck means that for any expression E, we either find E => true or E => false.

The deterministic results follows by inspection of the preconditions of rules. For example, for Boolean conjunction we find that the preconditions of rules (And-1), (And-2) and (And-3) are mutually exclusive.

The never stuck results follows again by inspection of the above rules. For example, if we would omit rule (And-3), then evaluation of true && true would get stuck.

Extension with Boolean disjunction

We consider the following language extended with Boolean disjunction.

 B ::= true | false

 E ::= B | !E | E && E | E || E

Here are additional rules to cover evaluation of Boolean disjunction.

          E1 => true
(Or-1)  -----------------
          E1 || E2 => true


          E1 => false
          E2 => true
(Or-2)  -----------------
          E1 || E2 => true


          E1 => false
          E2 => false
(Or-3)  -----------------
          E1 || E2 => false

The above rules are commonly employed by programming languages such as Go, Java and many others.

The important point to note is that the above rules evaluae Boolean expressions in a specific order: From right to left. This makes compilation of the above rules are straightforward.

For example, the Go compiler will translate

        var b bool
    b = f() || g()

into

        var b bool
    if f() {
        b = true
    } else {
        b = g()
    }

Alternative specification of ||

Consider the following alternative set of rules to cover Boolean disjunction.

         E1 => true
(Or-1)  -----------------
          E1 || E2 => true


          E2 => true
(Or-2')  -----------------
          E1 || E2 => true


          E1 => false
          E2 => false
(Or-3)  -----------------
          E1 || E2 => false

The first and the last (third) remain the same. But in the second rule, we only check if the right operand evaluates to true.

For our simple language, evaluation yields the same result, regardless if we replace (Or-2) by (Or-2’). However, there’s a difference in case we consider an extended language.

Consider the following Go program code.

func f() bool {
    b := true
    for b {
    }

    return false
}

func g() bool {
    return true
}

func exp() {
    var b bool
    b = f() || g()
    fmt.Println(b)

}

If we use (Or-2) instead of (Or-2’), evaluation of f() || g() will not terminate because the evaluation rules demand that we evaluate expressions from left to right. The left-most expression f() never terminates. Hence, f() || g() will not evaluate to any result.

On the other hand, if we use (Or-2’) instead of (Or-2), evaluation of f() || g() terminates with the result true.

So, why not use (Or-2’) instead of (Or-2)? Compilation of programs becomes much harder.

We would need to concurrently executed f() and g(). If either of them evaluates to true the result will be true. Below is some concrete Go code that follows the specification of rules (Or-1), (Or-2’) and (Or-3).

func exp2() {
    var b bool
    trueSig := make(chan int)
    falseSig_f := make(chan int)
    falseSig_g := make(chan int)

    go func() {
        x := f()
        if x {
            trueSig <- 1
        } else {
            falseSig_f <- 1
        }
    }()

    go func() {
        y := g()
        if y {
            trueSig <- 1
        } else {
            falseSig_g <- 1
        }
    }()

    select {
    case <-trueSig:
        b = true
    case <-falseSig_f:
        select {
        case <-trueSig:
            b = true
        case <-falseSig_g:
            b = false
        }
    case <-falseSig_g:
        select {
        case <-trueSig:
            b = true
        case <-falseSig_f:
            b = false
        }
    }

    fmt.Println(b)
}

Here’s some complete runnable code to play around with exp and exp2