Programming Language Foundations

Booleans and Conditional Computation

Learning Objectives

  • You can define a simple language using formation rules and represent it as an AST in Rust.
  • You understand how evaluation rules for if-then-else work.
  • You know what syntax sugar is and how desugaring (lowering) works.
  • You can implement desugaring transformations from a sugared AST to a core language.

Overview

In this chapter we will focus on another language, which instead of operating on integers, operates on booleans. We start by defining its grammar with formation rules, followed by a Rust enum representing its abstract syntax. After that, we naturally define how its terms evaluate to values. Finally, we will learn about lowering surface language to a lower, less human-readable language with fewer operations.

In the next chapter, we will merge the prefix arithmetic language and this boolean language.

Boolean Language ℬ

Our boolean language, denoted ℬ, has two literals true and false. In addition, we will initially only have one boolean operation: if-then-else (the boolean recursor). For example, the following is a term in the language:

if true then false else true

The if-then-else operation might be familiar to some as the ternary conditional operator (? :) available in some programming languages.

Grammar of The Boolean Language

Together, true, false and if-then-else are expressed with the following formation rules:

true∈ℬfalse∈ℬ𝑡1∈ℬ𝑡2∈ℬ𝑡3∈ℬite𝑓if𝑡1then𝑡2else𝑡3∈ℬ

The first two are “axioms” so we treat them as base rules and don’t bother drawing a line on top.

As an example, the term if true then false else true has the following formation tree:

true∈ℬfalse∈ℬtrue∈ℬite𝑓if true then false else true∈ℬ

AST in Rust

The type of abstract syntax tree for the boolean language can be written as the following enum in Rust

enum AST {
    True,
    False,
    Ite {
        cond: Box<AST>,
        if_true: Box<AST>,
        if_false: Box<AST>,
    }
}

Evaluation Rules

We will use 𝟚 for the set/type of booleans, i.e. the two-element set {0,1} where 0 denotes false and 1 true.

The evaluation relation has the following shape: 𝑡⇓𝑏, where 𝑡∈ℬ and 𝑏∈{0,1}. The base rules are straight-forward:

false⇓0true⇓1

Let’s try to think about what the evaluation rules of if-then-else look like.

?if𝑡1then𝑡2else𝑡3⇓?

First, what are the possible values of an if-then-else expression? Clearly there are two options:

  • The value of 𝑡2 if 𝑡1 evaluates to true.
  • The value of 𝑡3 if 𝑡1 evaluates to false.

In addition, even though it’s mathematically irrelevant, we want to avoid unnecessarily evaluating the other branch.

Next, what are the premises in each option?

  • If 𝑡1 evaluates to true, we need for 𝑡2 to evaluate to some value, e.g. 𝑡2⇓𝑏2.
  • If 𝑡1 evaluates to false, we need for 𝑡3 to evaluate to some value, e.g. 𝑡3⇓𝑏3.

These two options can be defined nicely with two evaluation rules.

𝑡1⇓1𝑡2⇓𝑏2IfTrueif𝑡1then𝑡2else𝑡3⇓𝑏2𝑡1⇓0𝑡3⇓𝑏3IfFalseif𝑡1then𝑡2else𝑡3⇓𝑏3
Loading Exercise...
Loading Exercise...
Loading Exercise...
Loading Exercise...
Loading Exercise...

Syntax Sugar

Syntax sugar is the term used for syntax which gets converted to a lower, less human readable syntax. For example lists in 𝕊𝕋𝕃ℂ++ can be written as [1, 2, 3:Int] which is not converted to an AST node List(1, 2, 3) but rather to a nested Cons(1, Cons(2, Cons(3, Nil(Integer)))) structure.

The process of lowering (or desugaring) syntax sugar can take place between a high-level AST and a lower level AST. One of the primary reasons behind lowering syntax sugar comes the fact that evaluation is likely simpler to implement at the lower level.

Let’s add some more syntax and operators to ℬ:

𝑡∈ℬnot𝑓!𝑡∈ℬ𝑡1∈ℬ𝑡2∈ℬand𝑓𝑡1and𝑡2∈ℬ𝑡1∈ℬ𝑡2∈ℬor𝑓𝑡1or𝑡2∈ℬ𝑡1∈ℬ𝑡2∈ℬxor𝑓𝑡1xor𝑡2∈ℬ

We represent the binary operators in infix style (as opposed to prefix) as we don’t need to write a parser for them and it makes them more natural to read.

We would like to avoid having to define any extra semantics for these operators by desugaring the sugared syntax to the “core language” consisting only of true, false and if-then-else terms. After parsing an expression in ℬ, we can lower it to an AST using a translation function.

This is a nice way programming languages can add convenient features which don’t fundamentally alter the behavior of the language.

First, let’s define the SugaredAST in Rust:

enum AST {
    True,
    False,
    Ite {
        cond: Box<AST>,
        if_true: Box<AST>,
        if_false: Box<AST>,
    },
    Not(Box<AST>),
    And(Box<AST>, Box<AST>),
    Or(Box<AST>, Box<AST>),
    Xor(Box<AST>, Box<AST>),
}

Let’s denote the translate function with double square bracket notation

⟦−⟧:SugaredAST→AST

We want the unsugared fragment (True, False and Ite) of the sugared language to effectively “remain unchaged” during the desugaring.

⟦SugaredAST::True⟧=AST::True⟦SugaredAST::False⟧=AST::False⟦if𝑡1then𝑡2else𝑡3⟧=if⟦𝑡1⟧then⟦𝑡2⟧else⟦𝑡3⟧

Next, let’s start with how to desugar ! b. The definition of negation of a boolean 𝑏∈{0,1} is:

¬𝑏={01if𝑏=1otherwise

This definition has the mathematical structure of an if-then-else expression. Therefore it’s straight-forward to encode it in AST with an if-then-else:

⟦! t⟧=if⟦𝑡⟧then false else true

Pulling Back Across The Sugar

Using this operation, we can simply pull back the evaluation function to get

evalSugaredAST:SugaredAST→𝟚evalSugaredAST(𝑡)=evalAST⟦𝑡⟧

Now all of the following terms evaluate to the values we expect.

ExampleThe following statements are true:evalSugaredAST(false)=0evalSugaredAST(if false then true else not false)=1evalSugaredAST(false or (false and true))=0evalSugaredAST(false xor true)=1

In the next exercise, your task is to desugar And, Or, Xor into just True, False and Ite.

Loading Exercise...
Loading Exercise...
← Evaluation and Big-Step Semantics
Conditional Arithmetic →