CMSPC 461: Programming Language Concepts Assignment 7

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

Assignment 7

CMSPC 461: Programming Language Concepts

Fall 2022

Question 1 (7+7=14pts)

Consider the simply typed λ-calculus and its typing rules defined in Note 4 (with type inference).

a)  (7pt) What constraints are generated for the term (λx. (λy . (x + y))) if we use the type system defined in Note 4? Justify your answer by writing down the proof tree for this term.

b)  (7pt) Suppose that during type inference, a compiler generates the following constraints to be solved: α → β = bool → α;β = α

Solve those constraints by the unification algorithm in Note 4. You need to write down the steps during constraint solving.

Question 2 (4+4=8pts)

Prove that the following two Hoare triples are valid.  (Hint:  in predicate logic P1  ⇒ P2  is equivalent to ¬P1 ^ P2).

a)  (4pt)

{x = 2}

y := x +  3;

y := y * 4;

y := y -  5;

{y > 11}

b)  (4pt)

{y < 7}

if (y>5) x := y-3;

else if (y>3) x := y- 1;

else x :=  9-y;

{x > 1}

Question 3 (4+4+6=14pts)

Below is a Hoare triple that includes pseudo code which computes the product c of two integers a and b.

{b ≥ 0}

c :=  0;

n := b;

while (n>0)   {

c := c + a;

n := n -  1;

}

{c = a × b}

a)  (4pt) Complete the following Hoare triple by writing down the strongest postcondition for the first two statements in this program fragment. {b ≥ 0}

c :=  0;

n := b;

{

}

b)  (4pt) Write down a loop invariant for proving the correctness of this program.  That is, write down an invariant that is 1) true before the first execution of the loop, 2) true before execution of every successive repetition of the loop, and 3) strong enough to prove the correctness of the code (i.e., c=a×b is true after the loop).

c)  (6pt) Briefly explain why the invariant you developed satisfies all three conditions stated in the previous problem. You might need to use your answer of 2 a) for this question.

Question 4 (5*4=20pts)

The type of a generic typed variable is unknown until a value is assigned. Let the type of a generic type be denoted as α, if multiple generically typed variables exists that need not share a type their types can be denoted as α,β respectively.

Note:If these variables are unbounded the expression could be untypeable

For example the type of λy .(λx.y) would be α → β → α . As λy and y must share a type but x is not under the same constraint.

For each of the following lambda expressions e, if the expression is typeable provide a proof tree of their types otherwise describe why the expression is not typeable. Make sure to include restraints:

a)  x

b)  (λx.x)

c) λy .(λx.x)

d)  (λx.(λy .x + y))

e) λx.(λy .x + y) (y)


2022-12-09