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).
Solution: Safety (violated by the finite steps where I come home and there is no beer in the fridge.)
Solution: Liveness (violated only after infinite time, where I come home and never drop on to the couch or drink a beer)
Solution: Liveness (for an unbounded definition of “later”)
Solution: Liveness
Solution: Safety
Solution: Safety
Solution: Liveness
1
Solution: As the state space has at least two states, we can assume there exists a state a ∈ Σ and a different state b ∈ Σ.
Then, we can construct two liveness properties, M and N:
M={paω |p∈Σ⋆}
N={pbω |p∈Σ⋆}
Here Σ⋆ refers to the set of finite sequences of states. Stated in English, the property M says that “the program will eventually loop forever (or terminate) in state a”, and the property N says that “the program will eventually loop forever (or terminate) in state b”. Before ending up in that final state, the program is free to do any finite sequence of actions.
These two properties are liveness properties as we cannot refute them merely by observing a finite prefix of the behaviour. Also, they are disjoint, that is, M ∩ N = ∅, because there is no behaviour that can both terminate in state a and in state b, as they are different states.
Recall that the union of a liveness property and any other property is also a liveness property. This means that for some arbitrary property P , the properties P ∪ M and P ∪ N are both liveness properties. Therefore, to show that any property P is the
intersection of two liveness
We do this with set theory
properties, it suffices to show that: (P ∪M)∩(P ∪N)=P
below:
((P ∪M)∩P)∪((P ∪M)∩N)
P ∪((P ∪M)∩N)
P ∪((P ∩N)∪(M ∩N)) P ∪((P ∩N)∪∅) P∪(P∩N)
P
(P ∪M)∩(P ∪N)
= = = = = =
distrib. of ∩ over ∪ ∩ absorption distrib. of ∩ over ∪
disjointness of M,N ∪identity ∪ absorption
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)) Page 2
(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).
(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.
Solution:
e1 :τ1 →τ2 e2 :τ1 e1 e2 : τ2
K:τ1 →τ2 →τ1
S:(τ1 →τ2 →τ3)→(τ1 →τ2)→τ1 →τ3
Solution: We must show that, assuming e : τ and e → e′, that e′ : τ. We will proceed by rule induction on e → e′.
Basecase. Whene=(App(App(AppSx)y)z)ande′ =(App(Appxz)(Appyz)), from the rule for S.
We know from the fact that e : τ that there exists types τ1 and τ2 such that:
• x:τ1 →τ2 →τ • y:τ1 →τ2
• z : τ1
Then we can show that e′ : τ:
x:τ1 →τ2 →τ z:τ1 (Appxz):τ2 →τ
y:τ1 →τ2 z:τ1 (Appyz):τ2
(App (App x z) (App y z)) : τ Basecase.Whene=(App(AppKx)y)ande′ =x,fromtheruleforK. Weknow
from e : τ that there exists a type τ1 such that: • x:τ
• y : τ1
Seeing as e′ = x, we know that e′ : τ already.
Inductive case. When e = (App e1 e2), and e1 → e′1, and e′ = (App e′1 e2). We get
that the induction hypothesis (from e1 → e′1) that, for any type τ, if e1 : τ then e ′1 : τ .
We know from e : τ that there exists a type τ1 such that:
Page 3
• e1 : τ1 → τ
• e2 : τ1
Seeing as e1 has type τ1 → τ, we know from our inductive hypothesis that e′1 : τ1 → τ. Therefore (App e1 e2) : τ from the application typing rule.
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.
Solution: Solutions may vary, but Int + 1 is the simplest.
Solution: rect.1+t
Solution: rect.(Int×t×t)+Int
Solution: Yes, (Roll (InR (Roll (InL 3)))) is an example finite value.
Solution: No, the only way to express a value of this type is something like (Recfun f.x. (Roll (Pair 4 x)))
Which in a call-by-value (strict) semantics would be non-terminating, but acceptable in a non-strict (lazy) semantics.
Solution: Yes, the only finite values are (InR True) and (InR False). All other values are infinite.
Page 4
Solution: The representation of unary natural numbers seen in question 2 suffices here:
The mapping is defined as: g(x) =
rect.1+t
(Roll (InL ())) if x = 0 (Roll(InRg(x−1))) ifx>0
(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.
Solution: One of the simplest is (rect.1+t)×Bool, i.e. a natural number combined with a sign bit. The mapping works as follows, where False represents negative numbers and True represents positive. Note that we offset the negative numbers by one so that there are not two zero values:
x < 0, (pair g(−x − 1), False) x ≥ 0, (pair g(x), True)
f(x) =
Solution: Seeing as a rational number is just a pair of integers to represent the numerator and denominator respectively, we can use our integer type from before (Z = (rec t. 1 + t) × Bool) and just use the type Z × Z.
Technically there are more pairs of integers than there are rational numbers. We can simplify this by judging two values of this type to be equal even if they are not structurally identical. A pair (p1, q1) and a pair (p2, q2) are equal iff p1q2 = p2q1.
Solution: A real number consists of an integer whole component and a possibly infinite sequence of fractional decimal digits.
For the integer component, it suffices to use our existing Z type.
Then, we just need an infinite sequence of digits, which we can define for binary digits with:
rec t. (Bool × t)
Therefore, a computable real number is just Z × (rec t. (Bool × t)).
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
Solution: The type required is A → A + B. InL
Page 5
Solution: The type required is A × B → A. fst
(c) [⋆⋆] P ∨ P ⇔ P
Hint: Recall that A ⇔ B is shorthand for A ⇒ B ∧ B ⇒ A.
(d) [⋆⋆] (A∧B⇒C)⇔(A⇒B⇒C)
Solution: Thetyperequiredis(A+A→A)×(A→A+A). ((λs. case s of InL x. x; InR x. x), InL)
Solution: The type required is a product of:
x1 :(A×B→C)→(A→B→C)
And:
x1 = λabc. λa. λb. abc (a,b)
x2 :(A→B→C)→(A×B→C)
x2 = λabc. λab. abc (fst ab) (snd ab) So the final answer is (x1, x2).
(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
Solution: ThetyperequiredisP+(Q×R)→(P+Q)×(P+R).
λpOrQR. case pOrQR of
InL p. (InL p, InL p);
InR qr. (InR (fst qr),InR (snd qr))
Solution: The type required is P → (P → 0) → 0, which we can implement with: λp. λnotP. notP p
Solution: This theorem does not hold constructively, so there is no term in standard typed lambda calculus.
Solution: Therequiredtypeis(((P →0)→0)→0)→P →0.
Recall our solution for part (d) was of type P → (P → 0) → 0. Call this function d. Then we can implement this type with:
Page 6
(i) [⋆⋆⋆] (P ∨¬P) ⇒ ¬(¬P) ⇒ P
λnnnp. λp. nnnp (d p)
Solution: The required type is (P + (P → 0)) → ((P → 0) → 0) → P
λpOrNotP. λnotNotP. case pOrNotP of InL p. p;
InR notP. absurd (notNotP notP)
Page 7