Model the syntax and evaluation semantics of a simple language. Include:

• a syntactic category (a "judgment") of unary natural numbers, defined properly, i.e., it should not be defined in terms of expressions
• a syntactic category of booleans
• a syntactic category of expressions with:
  • booleans and natural numbers
  • functions and application
  • booleans and if

  • dictionaries: n-ary tuples of key/value pairs with key-based projection.

    The keys should be symbolic, such as a, b, c, …, and values should either numbers or booleans. The syntax should allow a user to specify any number of key/value pairs when creating a dictionary, and project any key from an arbitrary expression. The projection operation should work regardless of nesting; i.e., the user does not need to know about the nested structure of the dictionary, they only need to know the key. You can express this either via nesting or via ellipses. For example, to express list of number of arbitrary length, I could allow nesting:

e ::= (e, e)
(1, (2, (3, 0)))

or use ellipses to specify arbitrary length:

e ::= (e, ..., e)
(1, 2, 3, 4)

As long as the projection operation works the same for both:

list-ref 1 (1, 2, 3, 4)     = 2
list-ref 1 (1, (2, (3, 0))) = 2

• nat-fold: a fold (recursion) operator over natural numbers.

  nat-fold takes three sub-expressions: e₁, e₂, and e₃. e₁ is expected to be an expression that produces a natural number, while e₂ is expected to be an arbitrary expression, and e₃ is expected to be an expression that produces a function that takes two arguments. When e₁ is 0, the result of nat-fold should be e₂. When e₁ is a non-zero natural number, the result should be e₃ applied to the sub-expression of e₁ and a recursive application of nat-fold to the sub-expression of e₁ and the same e₂ and e₃. nat-fold should implement induction on natural numbers.

First, formally define the syntax using a BNF grammar. Explain the grammar in English. Explain which expressions are introduction forms and which are elimination forms, and argue that the BNF grammar is inductively well-defined. Recall that a well-defined judgment has:

• at least one base case, with no additional self-references
• some measure that is smaller in the self-referenence than in the conclusion of the judgment

Your model should use unary natural numbers, but feel free to writing in decimal notation.

Define the reduction relation, conversion relation, and evaluation function for this language. You do not have to define capture-avoiding substitution. Describe (in English) the reduction rule(s) for nat-fold, and which rules are conguence rules.

Explain whether all syntactic expressions are well-defined, in the sense that they produce valid values.

Create a dictionary mapping the symbol a to 5, b to 120, and c to false. Prove that projecting b from the dictionary evalutes to 120.

Implement (not model) is the is-zero? function. is-zero? takes one argument, and evaluates to true when given 0 and false when given add1 n. Prove the following with a derivation tree showing each of step of conversion or reduction:

eval (is-zero? 0) = true

Prove the following equationally, not with formal derivation trees. Instead, write the series of reductions or conversions, explaining which rules are required. You may skip steps when there are multiple applications of the same rule or uninteresting rules like transitivity, but be sure to list which rule you elide.

eval (is-zero? 1) = false
eval (is-zero? 2) = false

Implement (not model) the addition function +, and demonstrate the following with a derivation tree.

eval (+ 0 0) = 0

Prove the following equationally. It may also help to prove and reuse subsidiary lemmas.

eval (+ 0 1) = 1
eval (+ 1 1) = 2
eval (+ 1 2) = 3
eval (+ 2 2) = 4