Test 2 Review A

[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18] [19] [20] [21]

Problem R2a.1.

Using the Church numerals, we can define the succ function in the lambda calculus to take a Church numeral representing some number n and return the Church numeral representing n + 1.

succ = λa.λs.λz.a s (s z)

Give a lambda calculus definition of the addition function +, which takes two Church numerals representing two numbers m and n and returns a Church numeral representing their sum, m + n.

λm.λn.m succ (n succ 0) or λm.λn.n succ m

Problem R2a.2.

Suppose we want to define a way to represent pairs (or 2-tuples) in the lambda calculus. We can do this by defining the following function pair, which takes two arguments and generates a representation of a pair of those two values.

pair = λx.λy.λf.f x y For example, to represent the value (2,3), we would call pair 2 3, which would give us λf.f 2 3.

Give a lambda expression for the function first that takes a pair represented as above and extracts the first item of the pair. Using your definition, I should be able to write first (pair 2 3) and get 2.

first = λp.p (λx.λy.x)

Problem R2a.3.

Consider the following Java program.

class Test { static int a = 1; static int f() { return a; } public static void main(String[] args) { int a = 2; System.out.println(f()); } }

a. If Java used dynamic variable scoping, what would it output?

b. If Java used static variable scoping, what would it output?

c. Does Java use static or dynamic scoping?

a. 2

b. 1

c. Java uses static scoping.

Problem R2a.4.

Consider the Python program below.

def a(): nonlocal x x = 3 def b(): x = 4 # defines a new 'x' variable hiding the global 'x' a() print(x) x = 2 # creates a global 'x' variable b() print(x)

a. If Python used statically scoped variables, what would this program print?

b. If it used dynamically scoped variables, what would it print?

c. Which does Python use?

a. 4 then 3

b. 3 then 2

c. Python uses static scoping.

Problem R2a.5.

Why would a language opt to use dynamic scoping (as Postscript and some old versions of Lisp do) rather than static scoping (as with nearly all other languages)?

Dynamic scoping is often easier to implement in an interpreted system, because it can be implemented with a single global dictionary that holds all variable-value mappings.

Problem R2a.6.

Recall from class that FORTRAN uses static variable allocation, while most other languages (including Java and Python) use stack-dynamic variable allocation.

a. Name and explain an advantage of static variable allocation over stack-dynamic variable allocation.

b. Name and explain an advantage of stack-dynamic variable allocation over static allocation.

a. Static allocation is marginally more efficient because the computer can use direct loads instead of indirect loads. Another answer: Static allocation allows for variables within functions that can remember values from previous calls to the function.

b. Stack-dynamic allocation is much more conducive to recursion, because each recursive call gets its own set of variables. Another answer: Stack-dynamic allocation is more space-efficient, as space is only allocated for the functions currently on the call stack.

Problem R2a.7.

Give an example of a Python program where a local variable could not be allocated on the stack and so would need to be on the heap.

def constantMultiply(c):

    def multiply(n):

        return c * n

    return multiply

The variable c is a variable local to the constantMultiply function, but its value persists beyond the end of the function call since the returned function multiply will need its value when it's called. Since its value must be kept beyond the end of the function call where it is created, it must be allocated on the heap.

Problem R2a.8.

Name and explain a reason why generics (such as generics in Java and templates in C++) are a useful feature for a programming language to include.

A generic allows the programmer to write subprograms in which a type can vary. For example, you could write a sort subprogram that works with an array of any type of data by using a generic. Without generics, in a statically typed language, you would need a separate sort subprogram for each type of array you might want to sort.

Problem R2a.9.

Explain why generics make more sense as a feature in statically typed languages than in dynamically typed languages.

The primary benefit of generics is to allow a programmer to write code that can accomodate a range of types. This is already possible in dynamically typed languages, since code can be ambiguous about type, and this is resolved at run-time.

Problem R2a.10.

Both C++ and Java allow a programmer to use a class name as a parameter to a generic class. Neglecting syntax and other usage rules, distinguish how the language have a different underlying implementation of such generics.

In C++, a generic (“template”) is used to generate a new class definition for each usage of it with a different type, and each of these definitions is compiled separately. In Java, there is only one instance of the generic compiled, and it is compiled to deal with Object as the generic parameter. The type information with the generic is used only for type-checking by the compiler.

Problem R2a.11.

What is the advantage of a tail-recursive function over other recursive functions?

The optimizer can remove tail recursion in a tail-recursive function, eliminating the overhead involved in function calls that would otherwise be incurred with other recursive calls and removing the possibility of stack overflow with the function.

The optimization works by simply taking the parameter values of the recursive call and placing them in their appropriate locations for the current call. Then, the function can simply jump back to the beginning, thus surrendering control to the result of the recursive call.

Problem R2a.12.

Convert the following Haskell function into an equivalent tail-recursive Haskell function.

pow2 0 = 1

pow2 n = 2 * pow2 (n - 1)

pow2 n = sub n 1

  where sub 0 ret = ret

        sub i ret = sub (i - 1) (ret * 2)

Problem R2a.13.

Describe the translation process that a compiler can use to eliminate recursive calls from a tail-recursive function.

To be a tail-recursive call, the return value of the recursive call must be the return value of the overall function. The compiler can generate code for this situation where the new parameters are calculated, then placed in the locations where the parameters were formally located, and then the computer jumps back to the function's beginning — rather than making a new function call. As a result, whatever the function now returns will end up being the overall return value.

Problem R2a.14.

Prove the following using our axiomatic scheme. Give a written justification of each mathematical fact.

{ sum = i² }
sum = sum + 2 * i + 1;
{ sum = (i+ 1)² }

1.	`sum` = `i`² ⇒ `sum` + 2 ⋅ `i` + 1 = (`i` + 1)²	Mathematical fact
2.	{ `sum` + 2 ⋅ `i` + 1 = (`i` + 1)² } `sum = sum + 2 * i + 1;` { `sum` = (`i` + 1)² }	Assignment
3.	{ `sum` = `i`² } `sum = sum + 2 * i + 1;` { `sum` = (`i` + 1)² }	Preconditions: 1, 2

The mathematical fact of step 1 follows from the equations (i + 1)² = i² + 2 ⋅ i + 1 = sum + 2 ⋅ i + 1.

Problem R2a.15.

Prove the following using our axiomatic scheme. The notation fib_i is used to represent the ith Fibonacci number.

{ a = fib_i ∧ b = fib_i − 1 }
c = a + b;
{ c = fib_i + 1 ∧ a = fib_i }

1.	`a` = `fib`_i ∧ `b` = `fib`_i − 1 ⇒ `a` + `b` = `fib`_i + 1 ∧ `a` = `fib`_i	Mathematical fact
2.	{ `a` + `b` = `fib`_i + 1 ∧ `a` = `fib`_i } `c = a + b;` { `c` = `fib`_i + 1 ∧ `a` = `fib`_i }	Assignment
3.	{ `a` = `fib`_i ∧ `b` = `fib`_i − 1 } `c = a + b;` { `c` = `fib`_i + 1 ∧ `a` = `fib`_i }	Preconditions: 1, 2

Problem R2a.16.

Provide a step-by-step partial correctness proof for the following. Justify each step with one of the three rules below, or “mathematical fact” if the conclusion is algebraically true and involves no assertions.

{ z = xⁱ }
z = z * x;
i = i + 1
{ z = xⁱ }

1.	`z` = `x`ⁱ ⇒ `z` ⋅ `x` = `x`^i + 1	Mathematical fact
2.	{ `z` ⋅ `x` = `x`^i + 1 } `z = z * x;` { `z` = `x`^i + 1 }	Assignment
3.	{ `z` = `x`ⁱ } `z = z * x;` { `z` = `x`^i + 1 }	Preconditions: 1, 2
4.	{ `z` = `x`^i + 1 } `i = i + 1;` { `z` = `x`ⁱ }	Assignment
5.	{ `z` = `x`ⁱ } `z = z * x;` `i = i + 1;` { `z` = `x`ⁱ }	Sequence: 3, 4

Problem R2a.17.

Prove the following using our axiomatic scheme.

{ i ⋅ k = n ∧ k mod 2 = 0 }
k = k / 2;
i = i * 2;
{ i ⋅ k = n; }

1.	`i` ⋅ `k` = `n` ∧ `k` mod 2 = 0 ⇒ (`i` ⋅ 2) ⋅ (`k` / 2) = `n`	Mathematical fact
2.	{ (`i` ⋅ 2) ⋅ (`k` / 2) = `n` } `k = k / 2;` { (`i` ⋅ 2) ⋅ `k` = `n` }	Assignment
3.	{ `i` ⋅ `k` = `n` ∧ `k` mod 2 = 0 } `k = k / 2;` { (`i` ⋅ 2) ⋅ `k` = `n` }	Preconditions: 1, 2
4.	{ (`i` ⋅ 2) ⋅ `k` = `n` } `i = i * 2;` { `i` ⋅ `k` = `n` }	Assignment
5.	{ `i` ⋅ `k` = `n` ∧ `k` mod 2 = 0 } `k = k / 2;` `i = i * 2;` { `i` ⋅ `k` = `n` }	Sequence: 3, 4

Problem R2a.18.

Prove the following using our axiomatic scheme

{ true }

if (n % 2 == 0) {

    n = n - 2;

} else {

    n = n - 1;

}

{ n mod 2 = 0 }

1.	`true` ∧ `n` mod 2 = 0 ⇒ (`n` − 2) mod 2 = 0	Mathematical fact
2.	{ (`n` − 2) mod 2 = 0 } `n = n - 2;` { `n` mod 2 = 0 }	Assignment
3.	{ `true` ∧ `n` mod 2 = 0 } `n = n - 2;` { `n` mod 2 = 0 }	Preconditions: 1, 2
4.	`true` ∧ ¬ (`n` mod 2 = 0) ⇒ (`n` − 1) mod 2 = 0	Mathematical fact
5.	{ (`n` − 1) mod 2 = 0 } `n = n - 1;` { `n` mod 2 = 0 }	Assignment
6.	{ `true` ∧ ¬ (`n` mod 2 = 0) } `n = n - 1;` { `n` mod 2 = 0 }	Preconditions: 4, 5
7.	{ `true` } `if (n % 2 == 0) { n = n - 2; } else { n = n - 1; }` { `n` mod 2 = 0 }	Condition: 3, 6

Problem R2a.19.

Distinguish proofs of total correctness against proofs of partial correctness.

A proof of total correctness includes arguments that the program terminates. A partial-correctness proof may omit this fact: It proves that if the program terminates, then it reaches its conclusion correctly.

Problem R2a.20.

What loop invariant allows you to prove the postcondition for the following?

{ n = 2^k ∧ k ≥ 0 }

i = 0;

j = 1;

while (j != n) {

    j = j * 2;

    i = i + 1;

}

{ n = 2ⁱ }

j = 2ⁱ

Problem R2a.21.

What loop invariant allows you to prove the postcondition for the following?

{ n ≥ 0 }

a = 0;

c = n;

while (c > a + 1) {

    b = (a + c) / 2;

    if (b * b <= n) {

        a = b;

    } else {

        c = b;

    }

}

{ a ≤ √n < a + 1 }

a ≤ √n < c