Ch 1 Ch 2 Ch 3 Ch 4 Ch 5 Ch 6 Ch 7 Ch 8 Ch 9 Ch 10 Ch 11 Ch 12

- 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.
- The meaning of an inheritance lattice may be expressed as a first-order logic formula. An example is given in slide 9-logic.
- 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.
- See slide 9-subtypes.
- 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.
- 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. - 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.
- 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. - 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.
- See slides slide 9-c-subtypes, slide 9-c-intersection and slide 9-c-bounded.
- (a) {a : Int , f : Int → Int} , (b) {a : Int , f : Int → Int} , (c) {a : Int , f : Int → Int} .
- (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} .
- 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. - 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} . - The proof involves unrolling.
Let
{x : Int, y : Int}
and
T
_{2}= μα.{b : α→ α} . Now suppose that T_{1}\leqslant T_{2}then, by unrolling, we would have that T_{1}\leqslant T_{2}, and hence, by the function subtyping rule, that T_{2}\leqslant T_{1}and T_{2}\leqslant T_{1}. This would only hold if T_{1}= T_{2}, which is obviously not the case. - 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 τ.