COMP3161/COMP9164
Properties and Datatypes Exercises
Liam O’Connor November 1, 2019
1. Safety and Liveness Properties
(a) [⋆] For each of the following properties, identify if it is a safety or a liveness property.
i. When I come home, there must be beer in the fridge.
ii. When I come home, I’ll drop onto the couch and drink a beer.
iii. I’ll be home later.
iv. When process p has executed line 5, then process q must execute line 17 again.
v. When process p has executed line 5, then process q cannot execute line 17 again. vi. Process q cannot execute line 17 again unless process p has executed line 5.
vii. Process p has to execute line 5 before q can execute line 17 again.
(b) [⋆⋆⋆⋆] By considering a property as a set of behaviours (infinite sequences of states), show that if the state space Σ has at least two states, then any property can be expressed as the intersection of two liveness properties.
Hint: It may be helpful to know that the union of a liveness property and any other prop- erty is also a liveness property (this result follows from the fact that liveness properties are dense sets).
2. Type Safety: Consider this very simple language with function application and two built-in functions:
e ::= (App e1 e2) |S
|K
The dynamic semantics evaluate the left hand side of applications as much as possible:
e 1 → e ′1
e 1 e 2 → e ′1 e 2
The K function takes two arguments and returns the first one. (App (App K x) y) → x
The S function takes three arguments, applies the first argument to the third, and applies the result of that to the second argument applied to the third. More clearly:
(App (App (App S x) y) z) → (App (App x z) (App y z))
(a) [⋆⋆] Define a set of typing rules for this language, where the set of types is described by:
τ ::= τ1→τ2 |ι
Note that → is right-associative, so τ1 → τ2 → τ3 means τ1 → (τ2 → τ3). 1
(b) [⋆⋆⋆] In order to prove that your typing rules are type-safe, we must prove progress and preservation. For progress, we will define the set of final states as all states that have no successor:
F ={s|s′.s→s′}
This trivially satisfies progress, as progress states that all well-typed states either have a successor state or are final states.
Preservation, however, requires a nontrivial proof. Prove preservation for your typing rules with respect to the dynamic semantics of this language.
3. Haskell Types: Determine a MinHS type that is isomorphic to the following Haskell type declarations:
(a) [⋆] data MaybeInt = Just Int | Nothing (b) [⋆] data Nat = Zero | Suc Nat
(c) [⋆] data IntTree = Tree Int IntTree IntTree | Leaf Int
4. Inhabitation: Do the following MinHS types contain any (finite) values? If not, explain why.
If so, give an example value. (a) [⋆] rect.Int+t
(b) [⋆] rect.Int×t
(c) [⋆] (rect.Int×t)+Bool
5. Encodings: For each of the following sets, give a MinHS type that corresponds to it. Justify why your MinHS type is equivalent to the set, for example by providing a bijective function that, given a element of that set, gives the corresponding MinHS value of the corresponding type.
(a) [⋆] The natural number set N.
(b) [⋆⋆] The set of integers Z.
(c) [⋆⋆] The set of rational numbers Q.
(d) [⋆⋆⋆] The set of (computable) real numbers RTM. It may be useful to assume a lazy
semantics.
6. Curry-Howard: Give a term in typed λ-calculus that is a proof of the following propositions. If there is no such term, explain why.
(a) [⋆] A⇒A∨B
(b) [⋆] A∧B⇒A
(c) [⋆⋆] P ∨ P ⇔ P
Hint: Recall that A ⇔ B is shorthand for A ⇒ B ∧ B ⇒ A.
(d) [⋆⋆] (A∧B⇒C)⇔(A⇒B⇒C)
(e) [⋆⋆] P ∨(Q∧R)⇒(P ∨Q)∧(P ∨R)
(f) [⋆⋆] P ⇒ ¬(¬P)
Hint: Recall that ¬A is shorthand for A ⇒ ⊥.
(g) [⋆⋆⋆] ¬(¬P)⇒P
(h) [⋆⋆⋆] ¬(¬(¬P )) ⇒ ¬P
(i) [⋆⋆⋆] (P ∨¬P) ⇒ ¬(¬P) ⇒ P
Page 2