Instructors' Guide

1. In knowledge representation, inheritance is primarily applied to describe taxonomic structures in a declarative way. Employing exceptions in inheritance networks leads to non-monotony. Non-monotonic inheritance networks may give rise to inconsistencies. See slide 9-knowledge.
2. The meaning of an inheritance lattice may be expressed as a first-order logic formula. An example is given in slide 9-logic.
3. A type denotes a set of individuals. The subtyping relation is essentially the set inclusion relation, with some additional constraints. However, the subtype relation is best defined by means of subtype refinement rules.
4. See slide 9-subtypes.
5. The contravariant nature of the function subtype refinement rule may be explained by relying on the business service metaphor: refining a service means better work for less money. Or, put differently, refining a function means imposing less constraints on the client, yet delivering a result that is more tightly defined. See slide 9-functions.
6. The notion of objects as records is introduced simply to justify the interpretation of objects as records or tuples of values and functions. Again employing a business metaphor, regarding an object as a collection of services, improving such a collection means offering more, and possibly better, services. See slide 9-objects.
7. Typed formalisms provide protection against errors. Yet, untyped formalisms are generally more flexible. In the practice of computer science and mathematics, untyped formalisms are surprisingly popular.
8. A first distinction may be made between universal polymorphism and ad hoc polymorphism, which accounts for overloading and coercion. Universal polymorphism may be subdivided into parametric polymorphism, which covers template classes, and inclusion polymorphism, which results from derivation by inheritance. See slide 9-flavors.
9. Inheritance allows for the incremental development of object descriptions. A child class may be regarded as modifying the parent base class, as it may include additional attributes and methods and may refine inherited attributes or methods.
10. See slides slide 9-c-subtypes, slide 9-c-intersection and slide 9-c-bounded.
11. (a) {a : Int , f : Int → Int} , (b) {a : Int , f : Int → Int} , (c) {a : Int , f : Int → Int} .
12. (a) No, since {a : Int , f : Int → Int} . (b) No, since {a : Int , f : Int → Int} , because {a : Int , f : Int → Int} . (c) Yes, since {a : Bool, f : Bool → Int} \leqslant {a : Bool} .
13. To give an example, if you have a record x of type \E α. {val : α. op : α→ Int} then you do not need to know the precise nature of the (hidden) type \E α. {val : α. op : α→ Int} to be able to type the expression x.op( x.val ) as Int. See slide 9-ADT.
14. A possible realization is given by the record x.op( x.val ) , for E = if  even(x)  then  true  else  false . The corresponding package is given by the expression E = if  even(x)  then  true  else  false . Another realization is given by the record type {a : R, f : R → Bool} where R stands for {x : Int, y : Int} .
15. The proof involves unrolling. Let {x : Int, y : Int} and T₂ = μα.{b : α→ α} . Now suppose that T₁ \leqslant T₂ then, by unrolling, we would have that T₁ \leqslant T₂ , and hence, by the function subtyping rule, that T₂ \leqslant T₁ and T₂ \leqslant T₁ . This would only hold if T₁ = T₂ , which is obviously not the case.
16. Let σ = μα.{c : α, b : τ→ α} and assume that σ = μα.{c : α, b : τ→ α} , then by unrolling we have that {c : σ, b : τ→ σ} \leqslant {b : τ→ τ} which clearly holds since {c : σ, b : τ→ σ} \leqslant {b : τ→ τ} . And, by applying the refinement rule for recursive types (given in slide 9-recursion), we indeed have that σ\leqslant τ.