TypinferenzTypinferenz(mit Bitvectoren)(mit Bitvectoren)
Prolog Aufbaukurs SS 2000
Heinrich-Heine-Universität Düsseldorf
Christof Rumpf
Gast: Wolfram Bernhardt
05.06.2000 Typinferenz 2
Typensignatur zu ‚Shieber 1‘Typensignatur zu ‚Shieber 1‘top >> category, featval.
category >> verbal, np :: HEAD:head.
featval >> head, agr, gen, pers, num, vform.
head >> vhead, nhead.
verbal >> v, vp, s :: HEAD:vhead.
np :: HEAD:nhead.
nhead :: AGREEMENT:agr.
agr :: GENDER:gen, PERSON:pers, NUMBER:num.
gen >> masc, fem, neut.
pers >> first, second, third.
num >> sing, plur.
vhead :: FORM:vform, SUBJECT:np.
vform >> finite, base.Kilbury 1997,
QType-Syntax
05.06.2000 Typinferenz 3
TyphierarchieTyphierarchie
category
verbal np
v vp s
head
vhead nhead
gen
masc fem neut
pers
first second third
num
sing plur
vform
finite base
featval
top
agr
05.06.2000 Typinferenz 4
Typhierarchie (mit Bitvectoren)Typhierarchie (mit Bitvectoren)
category(1111)
verbal(111) np(1000)
v(1) vp(10) s(100)
head(11000000000)
vhead(1000000000) nhead(10000000000)
gen(1110000)
masc(10000) fem(100000) neut(1000000) pers(1110000000000000)
first(10000000000000) second(100000000000000) third(1000000000000000)
num(110000000)
sing(10000000) plur(100000000) vform(1100000000000)
finite(100000000000) base(1000000000000)
featval(1111111111110000)
top(1111111111111111)
agr(10000000000000000)
05.06.2000 Typinferenz 5
SubtypenSubtypen
Ein Subtyp ist ein Typ, bei dem dieselben Bits gesetzt sind wie beim seinem Supertyp, dessen totaler Wert jedoch kleinergleich dem des Supertypen ist. Dies kann mit einem Subsumptionscheck (siehe spätere Folie) geprüft werden.
subtype(ST,T):- bitset_subsumes(T,ST).
05.06.2000 Typinferenz 6
Echte SubtypenEchte Subtypen
% true_subtype(?SubType,?Type)
% SubType is a true subtype of Type.
true_subtype(T1,T2):-
subtype(T1,T2),
T1 \= T2.
05.06.2000 Typinferenz 7
Minimale (Sub-)TypenMinimale (Sub-)Typen
minimal_subtype(MiniType,Type):-
subtype(MiniType,Type),
minimal(MiniType).
minimal(T):- T >> [] :: _.
Bei minimalen Subtypen ist genau ein Bit gesetzt; sein Zahlenwert beträgt also eine Potenz von 2. Falls keine Operation zum Zählen gesetzer Bits vorliegt, ist die Überprüfung auf diesem Wege kompliziert, so daß wie gehabt auf die Typensignatur zurückgegriffen werden sollte:
Eine allgemeine Möglichkeit ist festzustellen, ob ein Typ true_subtyps hat. Wenn nicht, ist er ein minimaler Typen:
minimal(T):- \+ true_subtype(_,T).
05.06.2000 Typinferenz 8
Extension eines TypsExtension eines TypsDie Extension eines Typen ist direkt aus seinem Bitvector abzulesen. Jedes gesetzte Bit entspricht einem minimalen Typen.
Z.B. Category (1111) np (1000) v (0001) vp (0010) s (0100)
Durch Operationen wie z.B. Komplementberechnung können Bitvektoren entstehen, die keine Entsprechung in der Typsignatur haben. Dennoch kann mit ihnen gearbeitet werden, da sie auf jeden Fall eine eindeutige Extension haben:
_Noname (100010001001) np (000000001000)v (000000000001)sing (000010000000)nhead (100000000000)
05.06.2000 Typinferenz 9
GLB über ExtensionGLB über Extension
• extension/2 liegt als berechnete Faktenmenge vor.
• Das zweite Argument von extension/2 ist alphabetisch sortiert.
• Jeder Typ hat entweder keinen oder mindestens zwei unmittelbare Subtypen.
% glb(?T1,?T2,?T3)
glb(T1,T2,T3):-extension(T1,E1),extension(T2,E2),intersection(E1,E2,E4),sort(E4,E3),extension(T3,E3).
Nebenstehende Definition hat folgende Voraussetzungen:
05.06.2000 Typinferenz 10
GLB - Berechnung / Typ-UnifikationGLB - Berechnung / Typ-UnifikationEin Hauptvorteil der Repräsentation durch Bitvectoren ist eine einfache Berechnung der größten unteren Schranke zweier Typen (greatest lower bound) durch die schnell Bitoperation AND.
Um die größte untere Schranke zweier Typen zu berechnen, werden ihre Bitvectoren mit logischem UND verknüpft:
Beispiele:
category (1111) /\ np(1000) = np(1000)
featval(1111111111110000) /\ second(1000000000000000) = second(1000000000000000)
Aufgrund dieser Repräsentation und Berechnung ist glb/3 immer deterministisch.
glb(T1,T2,T3):-
T3 is T1 /\ T2.
05.06.2000 Typinferenz 11
Untere SchrankenUntere Schranken
Da die größte untere Schranke zweier Typen leicht zu berechnen ist und alle anderen unteren Schranken Subtypen dieser sind, können sie so berechnet werden:
lb(T1,T2,T3):-
glb(T1,T2,GLB),
subtype(T3,GLB).
05.06.2000 Typinferenz 12
Typen-Generalisierung / LUBTypen-Generalisierung / LUB
Die Generalisierung von Typen läßt sich entgegen der Intuition nicht über die Vereinigung (logisches ODER) realisieren.
verbal(111)
v(1) vp(10) s(100)
v(1) \/ v(10) = ?(011) !!! statt verbal(111)
Hier muß auf die bekannte Methode zurückgegriffen werden.
05.06.2000 Typinferenz 13
LUB über Extension - LUB über Extension - nicht vollständignicht vollständig
• extension/2 liegt als berechnete Faktenmenge vor.
• Das zweite Argument von extension/2 ist alphabetisch sortiert.
• Jeder Typ hat entweder keinen oder mindestens zwei unmittelbare Supertypen.
% lub(?T1,?T2,?T3)
lub(T1,T2,T3):-
extension(T1,E1),
extension(T2,E2),
union(E1,E2,E4),
sort(E4,E3),
extension(T3,E3).
Nebenstehende Definition hat folgende Voraussetzungen:
05.06.2000 Typinferenz 14
Komplementberechnung Komplementberechnung ohne Bitvektorenohne Bitvektoren
% complement(?Type,-Complement)% The Complement of Type relative to all other Types.
complement(Type,Complement):-type(Type),complement(Type,top,Complement).
% complement(?Type,+ContextType,-Complement)% The Complement of Type relative to ContextType. % ContextType is the LUB for the complement types.
complement(Type,CT,Complement):-setof1(ST,subtype(ST,CT),Types),complement_in_context(Type,Types,Complement0),lubs(Complement0,Complement),Complement \= [], !.
05.06.2000 Typinferenz 15
Komplement im KontextKomplement im Kontextohne Bitvektorenohne Bitvektoren
% complement_in_context(?Type,+Context,-Complement)
% The Complement of Type relative to Context. Context is a
% list of candidate types for the complement. Every type in
% Context that has no lower bound with Type is in Complement.
complement_in_context(_,[],[]):- !.
complement_in_context(Type,[T|Ts],Complement):-
lb(Type,T,_), !,
complement_in_context(Type,Ts,Complement).
complement_in_context(Type,[T|Ts],[T|Complement]):-
complement_in_context(Type,Ts,Complement).
05.06.2000 Typinferenz 16
Komplement mit Bitvectoren IKomplement mit Bitvectoren I
Die Komplementberechnung über Bitvektoren bietet zwei Vorteile:
- einfach und schnell
- Ergebnis ist ein weiterer Bitvektor anstatt einer Menge
complement(BVType,Complement):-type(Type),bitvector_for_type(top,BVTOP),complement_in_context(BVType,BVTOP,Complement).
Die Berechnung des Komplements in einem Kontext erfolgt über ein logisches NOT und ein AND:
complement_in_context(T, CT, COMP) :-COMP is ( (\(T)) /\ CT).
05.06.2000 Typinferenz 17
Auf diese Weise können Bitvektoren entstehen, die keine Entsprechung im Typenverband haben
Komplement mit Bitvectoren IIKomplement mit Bitvectoren II
category(1111)
verbal(111) np(1000)
v(1) vp(10) s(100)
complement_in_context(T, CT, COMP) :-COMP is ( (\(T)) /\ CT).
Berechnet werden soll das Komplement von v(1) in Kontext von category(1111):
COMP is ( (\(1)) /\ 1111) ==>
COMP is ( (...110) /\ 1111) ==>
COMP is 1110
05.06.2000 Typinferenz 18
Auf diese Weise können Bitvektoren entstehen, die keine Entsprechung im Typenverband haben
Komplement mit Bitvectoren IIKomplement mit Bitvectoren II
category(1111)
verbal(111) np(1000)
v(1) vp(10) s(100)
complement_in_context(T, CT, COMP) :-COMP is ( (\(T)) /\ CT).
Berechnet werden soll das Komplement von v(1) in Kontext von category(1111):
COMP is ( (\(1)) /\ 1111) ==>
COMP is ( (...110) /\ 1111) ==>
COMP is 1110
05.06.2000 Typinferenz 19
Problem: Identische BitvektorenProblem: Identische BitvektorenIn bestimmten Fällen kann es dazu kommen, daß im Typenverband mehreren Typen derselbe Bitvektor zugewiesen wird.
Unäre Vererbung:
a(111)
b(111)
BCPO-Verletzung
a(11) d(11)
c(1) b(10)
Diese Typen sind dann nicht mehr voneinander zu unterscheiden (z.B. bei Subtyp-Berechnung).
05.06.2000 Typinferenz 20
LiteraturLiteratur• Hassan Ait-Kaci & Robert Boyer & Patrick
Lincoln & Roger Nasr (1989): Efficient Implementation of Lattice Operations, ACM Transactions on Programming Languages and Systems, pg. 115-146
• Christof Rumpf & Christian Fischbach & Wolfram Bernhardt (2000): QType Manual (to appear)
• Wolfram Bernhardt (2000): ???, master thesis (to appear)
05.06.2000 Typinferenz 21
Aufgaben zu Bitvektoren:
Aufgabe 1: Schreibe das Prädikat build_bitvectors/0, das aus einem gegebenen Typenverband (z.B. shieber1) die Faktenmenge bitvector_to_type/2 erzeugt.
Aufgabe 2: • a) Schreibe das Prädikat vector2set(+Bv, -Tl), das einem beliebigen Bitvektor die Liste der überdeckten Typen zuordnet. • b) Versuche vector2set/2 deklarativ zu machen: vector2set(?Bv, ?Tl)
Hilfe: Möglicherweise benötigst Du die Operationen shift-left/2 und shift-right/2, um Bitketten zu verschieben: ‘>>‘ verschiebt nach rechts (Division durch 2), ‘<<‘ verschiebt nach links (Multiplikation mit 2).1 << 4 = 16 (1 viermal nach links geschoben)
Aufgabe 3:Überlege, wie Problem mit identischen Bitvectoren vermieden und bekämpft werden können.