Lab 10: Operational Semantics Worksheet

Boolean Expressions

Considering the following grammar for (closed) Boolean expressions in Python. Operators are given in order of increasing precedence along with their associativity in the following table:

<expr> ::= <expr> and <expr>
         | <expr> or <expr>
	 | not <expr>
	 | True
	 | False

Operator

Associativity

or

left

and

left

not

N/A

Write down small-step and big-step semantics for Boolean expressions. Make sure that operands of an operator are evaluated from left to right), and that you handle short-circuiting, e.g., the right operand of a conjunction should not be evaluated if the left operand evaluates to False. (Challenge. Implement an evaluator for Boolean expressions in OCaml)

Substitution

Perform the following substitutions. In the case of capture-avoidance, you are free to choose whatever variable names you want which maintian \alpha-equivalence.

  1. [(\lambda x . x)/ y](\lambda x. \lambda x . y)
  2. [(\lambda x . x) / y](\lambda y. \lambda x. x)
  3. [(\lambda x . x) / f](\lambda y. \lambda x. f(yx))
  4. [(\lambda x . y) / z](\lambda x. \lambda y. z)
  5. [(\lambda z . x) / y][(\lambda x . y) / z](\lambda y. \lambda x. zy)