COMP3161/9164
Concepts of Programming Languages
FINAL EXAM
Copyright By PowCoder代写 加微信 powcoder
Term 3, 2022
Total Number of Parts: 4
Total Number of marks: 100
All parts are of equal value.
Answer all questions.
Excessively verbose answers may lose marks
Failure to make the declaration or making a false declaration results in a 100% mark penalty.
Ensure you are the person listed on the declaration.
All questions must be attempted individually without assistance from anyone else.
You must save your exam paper using the button below before time runs out.
Late submissions will not be accepted.
You may save multiple times before the deadline. Only your final submission will be considered.
Declaration
Part A (25 marks)
Consider the following inductive definition of a toy language , where programs can perform arithmetic computations, and
send/receive numbers over the network. We assume a language of arithmetic expressions, the details of which are
unimportant here. Arithmetic expressions are open, in the sense that they may contain variables; for example, we would
expect to hold.
Here is its small-step semantics. We assume a standard big-step semantics for arithmetic expressions, which means that
we treat arithmetic expressions as if their evaluation takes a single step.
The final states of the small-step semantics are the expressions the form where .
1. (3 marks) Show the step-by-step evaluation of
2. (4 marks) The small-step semantics above is not confluent.
1. Give an example program that shows why confluence fails. Motivate your answer.
x + 1 Arith
x String e Arith p L
𝚕𝚎𝚝 x := e 𝚒𝚗 p L
e Arith p L
𝚜𝚎𝚗𝚍(e). p L
x String p L
𝚛𝚎𝚌𝚎𝚒𝚟𝚎(x). p L
𝚛𝚎𝚝𝚞𝚛𝚗 e L
𝚕𝚎𝚝 x := e 𝚒𝚗 p ↦ p[x := v]
𝚜𝚎𝚗𝚍(e). p ↦ p
𝚛𝚎𝚌𝚎𝚒𝚟𝚎(x). p ↦ p[x := v]
e ⇓ v e ≠ v
𝚛𝚎𝚝𝚞𝚛𝚗 e ↦ 𝚛𝚎𝚝𝚞𝚛𝚗 v
𝚛𝚎𝚝𝚞𝚛𝚗 v v ∈ ℤ
𝚕𝚎𝚝 x := 2 + 2 𝚒𝚗 𝚜𝚎𝚗𝚍(x). 𝚛𝚎𝚝𝚞𝚛𝚗(x + x)
2. Give an intuition for why this language should not be confluent.
3. (4 marks) Rules (1) and (3) of the above semantics uses substitution, but we never defined substitution. Give a
recursive definition of substitution. The in binds into but not into , and the in
binds into . It suffices to define substitution of a single name for a natural number. You can assume that a suitable
definition of substitution for arithmetic expressions already exists.
4. (2 Marks) Do we need the side-condition in rule (4)? What happens if we drop it?
5. (6 marks) The semantics above is a substitution semantics. Give an equivalent small-step environment semantics for
this language. To write an inference rule with premises, you can write the rule as A, B ⊢ C. You may assume
the existence of a big-step environment semantics for arithmetic expressions, without giving its definition. .
6. (3 Marks) Does the above semantics have any stuck states? And does your answer depend on the semantics of
in any way? Motivate.
7. (3 Marks) The final states of the above semantics gives the return value of an execution. We may also be interested in
which messages were sent out during execution. How would you modify the above semantics so that the final state
contains that information? You do not need to actually construct such a semantics — explaining your idea suffices.
Part B (25 marks)
1. (3 marks) Give an example where the choice between call-by-value and call-by-name matters for something
beyond performance.
2. (6 marks) Provide the most general type for each of the following MinHS programs, if it exists. If it does not
exist, briefly explain why not.
x 𝚕𝚎𝚝 x := e 𝚒𝚗 p p e x 𝚛𝚎𝚌𝚎𝚒𝚟𝚎(x). e
(𝖨𝗇𝖫 𝚃𝚛𝚞𝚎, 𝙵𝚊𝚕𝚜𝚎)
3. (7 marks) Use the Curry-Howard isomorphism to provide a MinHS or Haskell program (if it exists) that
constitutes a proof for each of the following logical propositions. If no such program exists, briefly explain why
4. (5 marks) Using , , , and , write a type that encodes the following rose tree datatype:
Recall that is Haskell notation for the type of lists with element type . Your type should have a similar
structure to the original type. (Hence answering is not accepted, even though is technically
isomorphic to ).
5. (4 marks) Write a MinHS expression that has the following type:
Be explicit about any packing and unpacking of existential types.
Part C (25 marks)
1. (2 marks) Is every unityped language type safe? Explain your reasoning.
2. (4 marks) Alice maintains a programming language. Her users got sick of explicitly converting ints to floats all
day, so she added subtyping with the ordering . But her users, ever a quarrelsome bunch, are now
sick of converting floats to ints, so they insist that Alice also admits . If Alice agreed to this request,
how would it break the type system?
3. (10 marks) Consider the type class , a cousin of defined as follows:
𝗋𝖾𝖼𝖿𝗎𝗇 f x = x f
𝗋𝖾𝖼𝖿𝗎𝗇 f x = 𝖼𝖺𝗌𝖾 x 𝗈𝖿 (𝖨𝗇𝖫 y) → x; (𝖨𝗇𝖱 z) → x
(A ∧ A) → (A ∨ B)
(A → B) → A → B
((A → 𝙵𝚊𝚕𝚜𝚎) → 𝙵𝚊𝚕𝚜𝚎) → A
𝗋𝖾𝖼 𝙸𝚗𝚝 × + 1
datatype 𝚃𝚛𝚎𝚎 =
𝙽𝚘𝚍𝚎 [𝚃𝚛𝚎𝚎]
𝚃𝚛𝚎𝚎 𝙸𝚗𝚝 𝙸𝚗𝚝
∃S. S × (S → 𝖨𝗇𝗍) × ((S × S) → S)
𝖨𝗇𝗍 ≤ 𝖥𝗅𝗈𝖺𝗍
𝖥𝗅𝗈𝖺𝗍 ≤ 𝖨𝗇𝗍
𝖢𝗈𝗆𝗈𝗇𝖺𝖽 𝖬𝗈𝗇𝖺𝖽
An example instance of this type class is infinite lists (aka s), defined as follows:
1. What is a type class dictionary? What would the dictionary for this type class look like?
2. There is no instance of for the type constructor, if we require that all methods are total.
Why not? Hint: how would you define ?
If we remove the constructor and only keep , we can define an instance. Show how.
4. (6 marks) Give an example of a covariant, contravariant and invariant type constructor.
5. (3 marks) Assume that is a subtype of . What, if any, is the subtype relationship between and
? If there is a subtyping relationship, provide either a subtyping derivation for it or a conversion
function in terms of this assumed coercion function:
Part D (25 marks)
1. (6 marks) For each of the following properties, determine whether it is a safety or liveness property, or some
combination of the two. Explain your answer.
1. I will have tea, but not before breakfast.
2. The program will call the function.
class 𝖢𝗈𝗆𝗈𝗇𝖺𝖽 m where
extract :: m a → a
extend :: (m a → b) → m a → m b
datatype 𝖲𝗍𝗋𝖾𝖺𝗆 a = 𝖲𝖢𝗈𝗇𝗌 a (𝖲𝗍𝗋𝖾𝖺𝗆 a)
instance 𝖢𝗈𝗆𝗈𝗇𝖺𝖽 𝖲𝗍𝗋𝖾𝖺𝗆 where
extract (𝖲𝖢𝗈𝗇𝗌 x xs) = x
extend f (𝖲𝖢𝗈𝗇𝗌 x xs) = 𝖲𝖢𝗈𝗇𝗌 (f (𝖲𝖢𝗈𝗇𝗌 x xs)) (extend f xs)
𝖢𝗈𝗆𝗈𝗇𝖺𝖽 𝖬𝖺𝗒𝖻𝖾
data 𝖬𝖺𝗒𝖻𝖾 a = 𝖭𝗈𝗍𝗁𝗂𝗇𝗀 | 𝖩𝗎𝗌𝗍 a
𝖭𝗈𝗍𝗁𝗂𝗇𝗀 𝖩𝗎𝗌𝗍
𝙰 𝙱 𝙰 → 𝙰 → 𝙰
coerce : 𝙰 → 𝙱
3. I won’t drink vodka before dinner.
2. (6 marks) In the following program, the shared variables and are initially 0. is a local variable of process .
1. Assume each instruction is executed atomically. What are the possible final values of ?
2. In reality, the program above may yield a final state where . Why?
3. What is the limited critical reference restriction, and how does it apply to the above discrepancy?
3. (6 marks) In addition to and , most lock implementations will have a function. The invocation
will attempt to claim the lock ; if successful, return . If we failed to claim the lock, return .
Needless to say, an attempt to claim the lock will not succeed if another process currently holds the lock.
Assume multiple process are running the above code concurrently, using the same shared lock . Is this a solution to
the critical section problem? Motivate your answer, and explain any further assumptions about the behaviour of
that your answer depends on.
4. (7 marks) In the lecture, we discussed the Software Transactional Memory (STM) approach to critical sections.
1. In contrast to locks, STM is said to be an optimistic concurrency control model. Why?
2. Does STM satisfy the starvation-freedom liveness property? Why or why not?
3. How can the type system be used to ensure that STM transactions are only performed inside an atomic block?
END OF EXAM
(don’t forget to save!)
x := y + z;
take release tryLock
tryLock(l) l 𝚝𝚛𝚞𝚎 𝚏𝚊𝚕𝚜𝚎
while(𝚝𝚛𝚞𝚎) {
(non-critical section)
while(!tryLock(l));
(critical section)
release(l);
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com