#$|$

We will define the syntax and semantics for SAEL, the Simple

Arithmetic Expression Language. SAEL is our object language. The

metalanguage we $($well$,$ you$)$ will use to define SAEL is ACL$2$s$.$ The

meta$-$metalanguage we $($well$,$ us $--$ Ferdinand & Olin, in this

assignment$)$ use to discuss all of this is Mathematical English.

Here's a "Fundies $1"$ style data definition.

A simple arithmetic expression, saexpr, is one of the following:

$-$ a rational number $($we use the builtin ACL$2$s type rational$)$

$-$ a variable $($we use the builtin ACL$2$s type var$)$

$-$ a unary expression, which is a list of the form

$(-)$ ; Negation

$(/)$ ; Reciprocal

where is an arithmetic expression

$-$ a binary expression, which is a list of the form

$()$

where is one of $+,-,*,/$ or $^$

and both $\text{'}$s are simple arithmetic expressions.

$|$#

; It really isn't important to know the exact definition of varp,

; although you can query ACL$2$s with $"$:pe varp". Just notice that none

; of the operators are vars, but symbols such as x$,$ y$,$ z$,$ etc are

; vars.

$($check$=($varp $\text{'}-)$ nil$)$

$($check$=($varp $\text{'}+)$ nil$)$

$($check$=($varp $\text{'}*)$ nil$)$

$($check$=($varp $\text{'}/)$ nil$)$

$($check$=($varp $\text{'}^)$ nil$)$

$($check $($varp $\text{'}$x$))$

;; Q$1$

;; Use defdata to define the unary operators. Fill in the XXXs

;; below. If you have questions, ask on Piazza.

$($defdata uoper $($enum XXX$))$

;; Q$2$

;; Use defdata to define boper the binary operators

$($defdata boper $($enum XXX$))$

$($check $($boperp $\text{'}*))$

$($check $($boperp $\text{'}^))$

$($check$=($boperp $\text{'}!)$ nil$)$

;; Q$3$

;; Use defdata to define saexpr. We will want names for all the

;; subtypes, so use the following template. Note that data definitions

;; can be mutually recursive.

$($defdata

$($saexpr $($or rational ; or is the same as oneof

var

usaexpr ; unary sael expression

bsaexpr$))$ ; binary sael expression

$($usaexpr XXX$)$

$($bsaexpr XXX$))$

;; We now have a formal definition of the SAEL language! That is$,$ we

;; have a recognizer saexprp, which is defined in our metalanguage,

;; ACL$2$s$,$ and which recognizes expressions in the object language,

;; SAEL. We formalized the syntax of SAEL expressions! Notice that

;; defdata made this very easy to do$.$

;; In short, a SAEL expression can now be represented as a

;; piece of ACL$2$ data, so we can operate on one with ACL$2$ code.

$($check $($saexprp $\text{'}(($x $+$ y$)-(/$ z$))))$

$($check$=($saexprp $\text{'}($x $+$ y $+$ z$))$ nil$)$

;; We are now going to define the semantics of SAEL expressions.

;; First, some helper definitions.

;; An assignment is an alist from vars to rationals.

;; An alist is just a list of conses.

;; In the RAP notes, the term "valuation" is also used instead of assignment.

$($defdata assignment $($alistof var rational$))$

$($check $($assignmentp $\text{'}(($x $.1)($y $.1/2))))$

;; This is nil because $(1),(1/2)$ are not rationals.

$($check$=($assignmentp $\text{'}(($x $1)($y $1/2)))$ nil$)$

;; Now, on to the semantics.

;; How do we assign semantics to SAEL expressions such as

;; $($x $+$ y$)?$

;; We will define saeval $($below$),$ a function that given an saexpr and

;; an assignment evaluates the expression, using the assignment to

;; specify the values of var's.

;; If a var appears in the saexpr but is not in the assignment, then

;; the value of the var should be $1.$

;; Q$4$

;; Use the following helper function to lookup the value of v in a$.$

;; $($Remember return $1$ if v isn't in a$.)$

$($definec lookup $($v :var a :assignment$)$ :rational

XXX$)$