Programming Languages Assignment 4

Due: Wednesday April 6th

  1. 10 points

    For each of the following F♭ programs, show a proof tree that uses the operational semantics rules to demonstrate how it is evaluated. Make sure that your proof uses the F♭ operational semantics rules correctly; don't skip any steps.

    1. True And (False Or True) And True
    2. 3 + (If 3 = 3 Then 1 + 2 Else 2)
    3. Function x -> x + 1
    4. (Function a -> a) (Function b -> b + b) 5

  2. 15 points

    Write F♭ functions to encode a binary tree structure. You must provide the following definitions:

    1. tempty: Represents the empty tree.
    2. tbuild v l r: Creates a tree with the provided data value and the specified left and right children.
    3. tleft tree: Retrieves the left child from a tree node.
    4. tright tree: Retrieves the right child from a tree node.
    5. tdata tree: Retrieves the data value from a tree node.
    6. tisempty tree: Evaluates to True if the tree is the empty tree or False if it is not.

    Passing these definitions to the following F♭ program should cause it to iterate over a tree and sum all nodes it contains. (Below, Y is assumed to be the Y-combinator.) 

    (Y (Function this -> Function tree ->
    If tisempty tree Then 0 Else
    (tdata tree) + (this (tleft tree)) + (this (tright tree))
)))

    For instance, we would expect 55 if the following tree were provided to it: 

    tbuild 10
    (tbuild 20
        (tbuild 2 tempty tempty)
        (tbuild 4 tempty tempty))
    (tbuild 7
        (tbuild 12 tempty tempty)
        tempty)

    To make life easier, you may use the definitions of pr, left, and right which appear in §2.3.4 of the book. (You are not required to submit this answer in a source file, but you may want to test your answer in the F♭ toploop.)

  3. 25 points

    Write operational semantics rules for the language F♭r: F♭ with rings. These rules must do the actual work; they cannot be simple encodings. The rings in F♭r are a new kind of value; thus, the types of values in F♭r are functions, integers, booleans, and rings. A ring is like a circular list; a cell in a ring has a forward link and a backward link. All rings must contain at least one element. The syntax of F♭ is extended as follows, using the non-terminal e' to represent the expression non-terminals from F♭.

    • e ::= e' | Left e | Right e | RingAdd e1 e2 | RingDrop e | RingGet e | Ring e1 @ ... @ en

    The Ring value links a series of expressions together, with the last expression being linked to the first. The Left and Right operations cycle the ring. RingAdd adds a new value at the current position in the ring while RingDrop drops the current value in a ring (resulting in the cell to its right). RingGet retrieves the value in the current cell.

    The following examples should help you understand the behavior of these syntactic constructs.

    • Ring 5 @ 3 represents a ring containing two elements: 5 and 3
    • Ring 2 @ 1 @ True represents a three-element ring. Note that there is no type system to enforce that rings must have homogenously-typed contents.
    • Ring 1 + 2 @ 3 + 4 ⇒ Ring 3 @ 7. Observe that rings are eagerly evaluated; we do not wait for a RingGet to evaluate a ring element.
    • Left (Ring 1 @ 2 @ 3) ⇒ Ring 2 @ 3 @ 1
    • Left Left Left (Ring 1 @ 2 @ 3) ⇒ Ring 1 @ 2 @ 3
    • Right (Ring 1 @ 2 @ 3) ⇒ Ring 3 @ 1 @ 2
    • Left (Ring 0) ⇒ Ring 0
    • RingAdd (Ring 1 @ 2) False ⇒ Ring False @ 1 @ 2
    • RingDrop (Ring 1 @ 2 @ 3) ⇒ Ring 2 @ 3
    • RingDrop (Ring 1) diverges (because rings must always have at least one element)
    • RingGet (Ring 2 @ 4) ⇒ 2

    Remember to consider peculiar cases when writing your rules. Since F♭r does not have exceptions, you should diverge when appropriate.

  4. 10 points

    Now write the rules for F♭Sr: F♭ with rings and state. (This is actually relatively straightforward. For examples of stateful operational semantics rules, see Section 4.1 of the book.) Note that we're not specifically trying to create mutable rings; we're simply adding the rings to a stateful language. (If we wanted a mutable ring, we could create a ring of cells.)

  5. 30 points
    1. 15 points

      For each of the following pairs of expressions, indicate whether or not the stated operational equivalence holds in F♭. If it does not, show some context that evaluates differently dependent upon which of the two expressions you use. (Remember: it only takes one of the infinitely many contexts to make the two expressions operationally inequivalent, so think hard about any context you could put the code in.)

      1. True And x ≅ x
      2. Function x -> x ≅ Function y -> y
      3. Function x -> x x ≅ Function x -> x x x
      4. Function f -> Function x -> (f x) + (f x) ≅ Function f -> Function x -> (Function y -> y + y) (f x)
      5. Function f -> Function x -> (Function y -> x) (f x) ≅ Function f -> Function x -> x
    2. 15 points

      Repeat the above exercise but for F♭SR.

  6. 10 points

    F♭ programs are quite prone to type errors, such as trying to apply an integer as a function or adding an integer to a boolean, which cause divergence. While Chapter 6 of the book discusses basic type systems and how they can prevent this sort of problem, one simple (if sloppy) approach is to add a construct for checking the type of a value at runtime. We can imagine the F♭C language: F♭ extended with runtime type checking. This language contains three new keywords: IsFunction, IsInt, and IsBool. We could then imagine defining an integer list as simply as:

    empty def=False
    cons x y def=pr x y
    head lst def=left lst
    tail lst def=right lst
    isempty lst def=IsBool lst

    (The definition of length remains the same as in the book.) This would obviously be inappropriate for lists of booleans (since we are using a boolean as a sentinel value), but it would work well for integers and functions. Consider the following definitions of the operational semantics for F♭C:

    e ⇒ True
    IsBool e ⇒ True
    e ⇒ False
    IsBool e ⇒ True

    e ⇒ v     v ∈ ℤ
    IsInt e ⇒ True
    e ⇒ Function x -> e
    IsFunction e ⇒ True

    1. 5 points

      What is wrong with the rules as they are defined here?

    2. 5 points

      Provide a correct set of operational semantics rules for F♭C.

Submission Method

Submit your homework via Blackboard. If you hand-wrote your homework, you will need to scan it. There is a scan-to-email copier in NEB224 if you don't have access to a scanner.

If you wish to use LaTeX for your homework, you may be interested in the mathpartir package which provides (among other things) support for typesetting proof trees and logical rules. (Debian and Ubuntu users merely need to install the mathpartir package; other users may need to download the .sty file and use it directly.)