COMPSCI 3MI3 : Assignment 3 Fall 2021 Nicholas Moore Solutions submitted as a LATEXgenerated pdf file are eligible for 1 bonus point, so long as the source file is included with submission. List of Theorems in Topic 3 Theorem slide no. Determinacy of Single Step Evaluation 19 Every Value is in Normal Form 29 If t is in Normal Form, t is a Value 30 Uniqueness of Normal Forms 35 Termination of Evaluation 37 1. (10 points) Adding Addition Our UAE language is pretty bare bones by any objective standard. Let’s fill it out very slightly by adding an addition operator. Propose both syntax and small step semantics for an addition operator, which operates on numeric values. Please present your syntax in EBNF, and your semantics as a set of one or more inference rules. The theorems listed above above should still hold, if your proposed term is added to UAE. 2. (15 points) Determinacy of Single Step Evaluation If a language is determinate, then, for any term t and the evaluation relation→, the single-step evaluation of t is unique. Another way to say this is: t → t′ ∧ t → t′′ = t′ = t′′ (1) In topic 4, we demonstrated this result for the Boolean subset of UAE. Prove that this result still holds for UAE when we add our semantics for arithmetic expressions.
