7 Homework 1 – Practice Modeling a Language
In this assignment, I ask you to model a non-trivial language. The assignment is meant to be challenging, but it will not be marked harshly. The assignment is meant to teach you, not assess what you’ve learned. Don’t be scared, but try your best.
You may use Redex if you like, and can find additional help on Redex at https://www.williamjbowman.com/doc/experimenting-with-redex/. This will introduce many features I haven’t explained in class. Restrict yourself only to defining judgments, and do not use metafunctions or reduction relations from Redex. You may use other features, such as pattern matching and testing features.
The assignment is due Jan. 24th at 11:59pm. Send it to me by email, either as a plaintext document, a PDF, or a Redex implementation with comments.
7.1 Part 1: Define a collection of expressions
Model the syntax and evaluation function for a simple language.
A syntactic category ("judgment", but you can use BNF grammars) of inductively defined natural numbers.
While you should model natural numbers inductively, you may use decimal notation in examples. If you need to use decimal numbers in Redex, you can use the following metafunction to convert between representations.Examples:> (require redex/reduction-semantics) > (define-language L) > (define-metafunction L to-nat : number -> any [(to-nat 0) the-representation-of-zero] [(to-nat number_1) (the-representation-of-add1 (to-nat ,(sub1 (term number_1))))]) > (term (to-nat 0)) 'the-representation-of-zero
> (term (to-nat 5)) '(the-representation-of-add1
(the-representation-of-add1
(the-representation-of-add1
(the-representation-of-add1
(the-representation-of-add1 the-representation-of-zero)))))
A metafunction is a short-hand for a judgment with a clear interpretation as a recursive function for which we only care about the output. The evaluation function and substitution are examples of metafunctions. You can use a Redex metafunction in any place that Redex expects some Redex term.A syntactic category of boolean expressions.
- A syntactic category of expressions with:
Natural numbers. Note that these should be separately defined from the syntactic category of natural numbers. For example, the expression (s true).
Booleans and If
Functions and application
Dictionaries: n-ary tuples of key/value pairs with key-based projections.
Keys should be symbols, such as a or b, and values should be either natural numbers or booleans.
Dictionaries should not have fixed sizes. The syntax should enable the user to add new key/value pairs to an existing dictionary, similar to how a user can add a new element to a linked list.
The projection operation should work regardless of the size or length of the dictionary.
nat-fold: a fold (recursion) operator over natural numbers.
nat-fold should act similar to the functional programming foldr construct on lists. nat-fold takes three sub-expressions: e1, e2, and e3. e1 is expected to be an expression that produces a natural number. e2 is expected to be an arbitrary expression. e3 is expected to be an expression that produces a function that takes two arguments.
For the reduction rules: When e1 is zero, the result of nat-fold should be e2. When e1 is (s e), the result should be e3 applied to e and a recursive application of nat-fold to e as the first argument, e2 as the second argument, and e3 as the third argument.
nat-fold should implement recursion on natural numbers and allow you to write loops over natural numbers.
You should define this language either in Redex or on paper. (I strongly recommend Redex.)
First, formally define the syntax using a BNF grammar. Explain the grammar briefly in English. Explain which expressions are introduction forms and which are elimination forms. Argue that the grammar is inductively well-defined. Recall that a well-defined judgment has some measure that is smaller in the self-referenencing premises than in the conclusion of the judgment.
7.2 Part 2: Define operations on expressions
Define the reduction relation, conversion relation, and evaluation function for this language. You do not have to define capture-avoiding substitution.
7.3 Part 3: Properties
Explain whether all syntactic expressions are well-defined, in the sense that they produce valid observations in the evaluation function.
7.4 Part 4: Prove some stuff
7.4.1 About dictionaries
Create a dictionary mapping the symbol a to the value 5, b to the value 120, and c to the value false.
Prove that projecting b from this dictionary evaluates to 120.
7.4.2 About numbers
Implement a function in your langauge called is-zero?. This will require writing an expression in your model, not adding new expressions to your model.
The is-zero? function takes one argument and evaluates to true when given 0, and false when given (s e).
You might find the Redex function define-term helpful.
Note that below I use decimal numbers, which you may need to translate into your formal model.
Prove that eval (is-zero? 0) = true by constructing derivation trees showing each step of conversion or reduction. If you use Redex, translate the derivation into on-paper notation.
Prove the following equationally, not with formal derivation trees. Instead of writing formal derivations, 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 the addition function +. Note that you were not allowed to add + to your model.
Prove that eval (+ 0 0) = 0 by giving derivation trees.
Prove the following equationally. It may help to prove and reuse some lemmas.
eval (+ 0 1) = 1
eval (+ 1 1) = 2
eval (+ 1 2) = 3
eval (+ 2 2) = 4