1996 MTC Qual Questions

John Mitchell Wednesday, May 22

1. (a) Given objects A and B in a category C, state the conditions for object D to be a

product of A and B.

(b) Show that in Set, the set A × B = { {a, {a, b}} | a ∈ A, b ∈ B } is a product of A and B.

(c) Define n-ary product in a category.

(d) In Set, is A_{1} × … × A_{n} = { {a_{1}, {a_{1}, a_{2}}, …, {a_{1}, …, a_{n}}} | a_{i} ∈ A_{i} } a product of sets A_{1}, …, A_{n}? Prove your claim.

2. Suppose we have a set P of processes, a set A of actions and a relation →⊆ P × A × P which we will call evaluation. We write P →^{a}Q for → (P, a, Q). A relation ∼⊆ P × P on processes is called a bisimulation if, whenever P ∼ Q, the following two conditions are satisfied:

if P →^{a}P′ then there is some Q′ with Q→^{a}Q′ and P′ ∼ Q′
if Q→^{a}Q′ then there is some P′ with P →^{a}P′ and P′ ∼ Q′

Processes P and Q are bisimilar if there is some bisimulation ∼ with P ∼ Q.

Given two processes, presented as finite graphs, how hard is it to decide whether the processes are bisimilar? What standard problem in automata theory is this equivalent to? Explain why these two problems are equivalent.

3. We could develop a typed functional calculus of objects using a simple class construct of the form

class ⟨class-name⟩ { : ⟨superclass⟩ } constructor ⟨name⟩ : ⟨type⟩ → ⟨class-name⟩ = ⟨expression⟩; private {⟨name⟩ : ⟨type⟩ = ⟨expression ⟩}^{∗} public {⟨name⟩ : ⟨type⟩ = ⟨expression⟩}^{∗}

end;

where {…} is used to indicate optional syntax and {…}^{∗} the option to write zero or more occurrences of the enclosed declarations.

Explain what kind of typing rules you would expect to give for this construct. More specifically, explain:

(a) The form of an appropriate typing judgement,

(b) The number of typing hypotheses and the intuitive interpretation of each hypothesis,

(c) The appropriate form of judgement for each hypothesis

(d) A suitable typing rule for the entire declaration or some approximation of a correct rule.

Give an example class and subclass and explain why they would be (or should be) considered type-correct, according to your rule. Please state clearly any assumptions you make about the language concepts you are formalizing.