LARA

Homework 07

Due Wednesday, 24 November, 10:10am. Please hand it in to Hossein before the beginning of the exercise session.

Problem 1

If the following programs type-check according to the rules given in the course, give the corresponding type derivation tree, otherwise give a partial tree that shows where it doesn’t work.

a) Assume the types Pos and Neg are defined as described in the lecture. 

  def func1( f: Pos => Int): Int = f(5)
  def func2( f: Int): Neg = -5
  val z: Pos = func1(func2)

b) Note that Lists are immutable collections in Scala. 

  class A
  class B extends A
  class C extends B
  def func1( a: (List[B],List[C]) => List[A]): B
  def func2( a: List[A], b: List[A]): List[C]
  val a: Array[A]
  a(0) = func1(func2)

Problem 2

Recall the TOOTOOL language as defined in the lecture notes. This language supports the following types:

  • Int
  • Pos <: Int
  • Neg <: Int

We slightly change the syntax of the TOOTOOL language so that it allows just multiplication and exponentiation. The new language has the following BNF syntax.

S::=VarDeclaration* Assignment*
VarDeclaration::=var Identifier: Type
Assignment::=Identifier = Expression
Expression::=Factor ((* | ^) Factor)?
Factor ::=IntegerLiteral | Variable

The goal of this exercise is to find a sound type system so that the program never evaluates an expression which has exponentiation by a negative number.
The state of a program at each moment consists of a mapping from its variables to an Int, Pos, or Neg number. Initially all the Int variables have the value 0, the Pos variables have the value 1 and the Neg variables have the value -1.
Given an initial state, we can define the computation of a program. A computation is a series of consecutive configurations of the program. A configuration contains the commands to be executed and the current state. Given a set of assignment commands and an initial state, a computation proceeds following a set of inference rules.

As an example, consider the following piece of code. 

  var x: Int
  var y: Pos
  x = 2
  y = 3
  x = x ^ y

The initial state as mentioned above is $ \Sigma= \{x \rightarrow 0, y \rightarrow 1\}$. The computation of the program is as the following.
$(x = 2;y = 3;x = x ^ y , \{x \rightarrow 0, y \rightarrow 1\}) \longrightarrow $
$(y = 3;x = x ^ y , \{x \rightarrow 2, y \rightarrow 1\}) \longrightarrow$
$(x = x ^ y , \{x \rightarrow 2, y \rightarrow 3\} \longrightarrow $
$( , \{x \rightarrow 8, y \rightarrow 3\})$

The inference rules are defined using the evaluation function $f_\Sigma$ that evaluates an expression in a give state $\Sigma$.

  • $f_{\Sigma}(Variable) = \Sigma(Variable)$
  • $f_{\Sigma}(IntegerLiteral) = IntegerLiteral$
  • $f_{\Sigma}(Factor_1 \hat\ Factor_2) = f_{\Sigma}(Factor_1) \hat\ f_{\Sigma}(Factor_2)$
  • $f_{\Sigma}(Factor_1 * Factor_2) = f_{\Sigma}(Factor_1) * f_{\Sigma}(Factor_2)$

We have the following inference rule in this version of the TOOTOOL program.

  • $( variable = expression;s_1;\cdots;s_n , \Sigma) \longrightarrow (s_1;\cdots;s_n , \Sigma \oplus \{variable\mapsto f_{\Sigma}(expression)\})$

Assume that we have the configuration $c = (p,\Sigma)$ at some point of computation. We say $c$ is very good if the following two criteria holds.

  • The program $p$ is type checked according to the type checking rules.
  • Each variable in $\Sigma$ belongs to the domain determined by its type (if z:Pos, then z is strictly positive).

a) Give the type checking rules that express the properties of multiplication and exponentiation in this setting.
b) Show that if a configuration is very good, after one step of computation according to the inference rule it remains very good in the next configuration.
If your type system of part a does not obey this behavior, you should change it.
c) Use induction to prove that the program never attempts to compute $x^y$ with a negative value $y$.