Instructors' Guide
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
T2 = μα.{b : α→ α} .
Now suppose that
T1 \leqslant T2 then,
by unrolling, we would have
that
T1 \leqslant T2 ,
and hence, by the function subtyping rule,
that
T2 \leqslant T1 and
T2 \leqslant T1 .
This would only hold if
T1 = T2 ,
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 τ.
slide: Answers