1 HW1

1.1 Part 1

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.

1.2 Part 2

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.

1.3 Part 3

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

1.4 Part 4

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`.

1.5 Part 5

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
```

1.6 Part 6

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
```

Created: 2019-01-09 Wed 14:43

Validate