2 Lab Playing with PCF-value

Exercises

Feel free to copy any code you need from the lecture notes.

Exercise 1. Design a variant of PCF, including the evaluator, that passes its arguments by value. This task requires:

• the use of beta-z instead of beta-y

• a reflection on the relations for basic arithmetic

• an appropriate definition of evaluation context (focus on the leftmost-outermost redex)

Do you have to modify the definition of the set of values? Do you have to modify the eval function?

Exercise 2. Add strings to the PCF language (or your PCF-value language from the preceding exercise if you are comfortable with the solution). Check in Redex’s documentation for the string pattern. Use the syntax (e ++ e) to represent the concatenation operation on strings.

Hint

> (string-append "hello" " " "world")

"hello world"

Exercise 3. In PCF (as defined), a program may end up adding a function to a number or let a function flow into the test position of an if. In the existing model, the “execution” of such programs gets stuck. Take a look at this program

(λx.(if x (+ x 1) (+ (λy.y) 2)))

Suppose the program is applied to 1. What kind of reduction sequence do you get in the existing PCF model? What is the result of eval?

Eliminate all stuck states from the PCF model (or your PCF-value language from the preceding exercise if you are comfortable with your solution). That is, add a reduction relation that recognizes bad situations, say, (1 + (1 + (λy.x))), and transitions to an error state.

This task requires:

• the addition of an error message to the language; and

• the addition of reduction relations from stuck states to error messages.

Are you convinced that you have covered all possible stuck states?