Homework 7

This homework is important, it may carry more points than others. For this homework only, you can do it in groups of 2 and hand in only one solution per group, but write down the name of others that you worked with.

We consider a small language that contains the x^y operator. Our goal is to design a system where x^y is never evaluated for negative y.

We have the following types:

Int
Pos <: Int (Pos is a subtype of Int)
Ref[Int], Ref[Pos]

In scala, Ref[T] would look like this:

class Ref[T](var content : T) {...}

References are explained in Subtyping with Assignment and Generics

Expressions are built (non-recursively) from:

integer constants
variables
binary operators $+$ , $*$ , ^
variable.content expressions

More precisely, the grammar of expressions e is:

e ::= cvar | cvar + cvar | cvar * cvar | cvar ^ cvar | cvar.content
cvar ::= var | constant

Assignment statements are the only statements. They have an expression on their right hand side and their left hand side is given by the following grammar:

lhs ::= var | var.content

A program is simply a sequence of variable declarations, followed by a sequence of assignments. Example:

x : Ref[Int]
y : Ref[Pos]
z : Int

x.content = 3
x = y
y.content = x.content

The typing rules for $+$ and ^ are:

$\begin{equation*} \frac{p:Pos, q:Pos} {p+q : Pos} \end{equation*}$

$\begin{equation*} \frac{p:Int, q:Int} {p+q : Int} \end{equation*}$

$\begin{equation*} \frac{p:Pos, q:Pos} {p \hat\ q : Pos} \end{equation*}$

$\begin{equation*} \frac{p:Int, q:Pos} {p \hat\ q : Int} \end{equation*}$

Note that e.g. a derivation

$\begin{equation*} \frac{x:Int, y:Pos} {x+y : Int} \end{equation*}$

follows from the above rules and the subtyping rule Pos <: Int, because we have a general rule

$\begin{equation*} \frac{p : T, T <: T'} {p : T'} \end{equation*}$

Part a)-multiplication

Give type checking rules that express properties of multiplication * , referring only to types Int and Pos. Your rules should be as precise as possible, but they should refer only to types of sub-expressions, not to their values.

Part b)-subtyping

The initial type environment is built according to declarations. For each

var x : T

we have $x \mapsto T$ in the environment.

To type-check a program, we use the rule

$\begin{equation*} \frac{\Gamma \vdash s_1 : \mbox{ok} \qquad \Gamma \vdash s_2;s_3...s_n : \mbox{ok}} {\Gamma \vdash s_1;s_2...s_n : \mbox{ok}} \end{equation*}$

Give the remaining

type checking rules (when is an assignment well-typed?), and
subtyping rules (in addition to Pos <: Int) for statements and their expressions, including rules for Ref[Int] and Ref[Pos].

Task c)-environment

Because we have assignment, we'll use an evaluation environment in the semantics of evaluation. Our environment will contain two kinds of things: mappings for variables and mapping for cells. A variable is mapped to an Int, Pos, or cell. A cell is mapped to an Int or Pos. Cells are like addresses in a memory.

We need to create an initial evaluation environment $\Sigma$ according to the initial declarations. Our convention is to initialize variables of type Int to 0 and Pos to 1. References are initialized to fresh cells.

Example:

x : Ref[Int]
y : Ref[Pos]
z : Pos

$\Sigma = \{x\mapsto cell_1, y\mapsto cell_2, cell_1\mapsto 0, cell_2\mapsto 1, z \mapsto 1\}$

Let us now give operational semantics for our language:

We define $f_{\Sigma}$ to be the function that evaluates an expression in evaluation environment $\Sigma$ :

$f_{\Sigma}(var) = \Sigma(var)$
$f_{\Sigma}(var.content) = \Sigma(\Sigma(var))$
$f_{\Sigma}(constant) = constant$
$f_{\Sigma}(cvar_1 + cvar_2) = f_{\Sigma}(cvar_1) + f_{\Sigma}(cvar_2)$
$f_{\Sigma}(cvar_1 \hat\ cvar_2) = f_{\Sigma}(cvar_1) \hat\ f_{\Sigma}(cvar_2)$
$f_{\Sigma}(cvar_1 * cvar_2) = f_{\Sigma}(cvar_1) * f_{\Sigma}(cvar_2)$

We have two evaluation rules:

$(\Sigma, var = expr; s_1...s_n) \longrightarrow (\Sigma \oplus \{x\mapsto f_{\Sigma}(expr)\}, s_1...s_n)$
$(\Sigma, var.content = expr; s_1...s_n) \longrightarrow (\Sigma \oplus \{f_{\Sigma}(x)\mapsto f_{\Sigma}(expr)\}, s_1...s_n)$

We will define the notion that program state type checks, by saying that both the program and the state type check in $\Sigma$ :

$\begin{equation*} \frac{\Gamma \vdash \Sigma, \Gamma \vdash p} {\Gamma \vdash (\Sigma,p) : \mbox{ok}} \end{equation*}$

Here $\Gamma \vdash p$ is what you defined in b)-subtyping. Now, define $\Gamma \vdash \Sigma$ , which, intuitively, will check that the values of variables and reference cells make sense according to types. (In principle, any definition here is acceptable as long as your proof in d)-good and e)-induction work. You may need to revisit this part if d) or e) do not work.)

Task d)-good

Show that if $\Gamma \vdash (\Sigma,p) : \mbox{ok}$ and the program $p$ starts with the statement

x = y ^ z

then $\Sigma(z)$ is a positive integer. (This is desirable so that the evaluation of ^ does not crash.)

Task e)-induction

Show that if the program and evaluation environment type check and we execute one assignment statement, the program and the environment again type check in the new environment i.e.

if: $\Gamma \vdash (\Sigma ,p) : \mbox{ok}$ and $(\Sigma ,p) \longrightarrow (\Sigma ',p')$

then: $\Gamma \vdash (\Sigma ',p') : \mbox{ok}$ .

Task f)-safety

Explain why c),d),e) taken together imply that, no matter what the program is, if it type checks, then its execution from the initial state will never attempt to evaluate x^y for a negative value of y.

Note that this property would continue to hold if we added loops and jumps to our language.

Task g)-java

Suppose we change the rules so that

Ref[Pos] <: Ref[Int]

Show that f)-safety does not hold any more, that is, give an example of a well-typed program whose execution crashes due to ^ being applied to a negative number.

Task h)-broken

If you take the same definition of $\Gamma \vdash \Sigma : \mbox{ok}$ as in d), prove or disprove that the claim in e) holds in the presence of the new subtyping rule Ref[Pos] <: Ref[Int]. If you prove the claim, the proof should follow the structure as in e), if you disprove the claim, you should give an example $\Sigma$ and $p$ for which e) does not hold.