Explain the significance of the following general theorem for temporal abstraction. Instantiate r and f for the

Fantastic news! We've Found the answer you've been seeking!

Question:

Explain the significance of the following general theorem for temporal abstraction.
Instantiate r and f for the case of a positive edge-triggered D-type flipflop, and
describe what the general theorem states for these instantiations.
` ∀f r.
(∃t. f t) ∧
(∀t. f t ⇒ (∃n. Next f (t,t+n) ∧ r(t,t+n))) ⇒
(∀u. r(TimeOf f u,TimeOf f (u + 1)))
[10 marks]
12 Types
Give rules for deriving ML typing assertions of the form
x1 : σ1, . . . , xn : σn ` M : σ
You may assume that the types σ1, . . . , σn, σ are built up from type variables and a
type of booleans using function-, product-, and list-type constructors, and that
the expressions M involve only identifiers, true, false, abstraction, application,
projections, pairing, nil, cons, and let-declarations. [5 marks]
What does it mean for one ML type to be more general than another? What is
meant by the principal type of a closed ML expression? [3 marks]
Give an account of an algorithm for deciding typability and producing principal
types for the above fragment of ML. (Facts about unification may be quoted without
proof.) [12 marks]
5 [TURN OVER
CST.95.7.6
13 Designing Interactive Applications
At the reception desk of a highly secure organisation, all visitors and staff are
required to register before entry to the building. The organisation's management is
concerned to reduce registration delays without increasing levels of staffing at the
desk.
(a) Write a one-sentence statement of a problem in interactive system design,
aimed at addressing this situation. [3 marks]
(b) The figure above shows the screen layout of a possible system for visitor
and staff registration, using multiple terminals, each equipped with display,
keyboard, keypad and mouse. Name three methods you might use in assessing
the usability of this design, and the reasons why each method might be useful.
[5 marks]
(c) Describe, for the benefit of a new member of the design team, how to go about
applying one of the three methods you have named in part (b). [8 marks]
(d) What interaction style, other than the direct-manipulation style illustrated in
the figure, would be appropriate for this application,
6
CST.95.7.7
14 Additional Topics
Discuss briefly the way in which a formal definition can assist the design and
implementation of a programming language. [7 marks]
Explain the notion of a delivery judgement in Natural Semantics. Explain the
ingredients of the judgement form
E `v exp ⇒ R
which represents the evaluation of an expression in Standard ML. Describe the
rules which allow one to infer a judgement
E `v exp atexp ⇒ v
representing the application of a function to a value

State the hierarchy theorems for time and space. [4 marks]
A linear time reduction from a language L1 to L2 is a reduction that can be
computed by a deterministic Turing machine in time O(n).
A class of languages C is closed under linear time reductions if whenever L2 ∈ C
and L1 is linear-time reducible to L2, then L1 ∈ C.
For each of the following complexity classes (a) to (d), say
• whether it is closed under linear time reductions
• whether it contains problems that are complete under linear time reductions