Slajdy2007

e vyloučených
• Shanonovská informace: informace je míra snížení
entropie (neurčitosti)
• čím více možných světů vyloučíme, tím více snížíme
neurčitost
P114_6 11
Carnapovská informace
• Nechť P je množina propozic a R1 ⊆ Tim je časový
interval, q je nějaká propozice:
Wrd(P,R1) = {w∈Wrd | [[qw]t]=Pravda ∧ q ∈P ∧ t
∈R1}
Wrd(P,R1) se nazývá přípustný logický prostor
množiny propozic P vzhledem k časovému
intervalu R1.
• Čím je Wrd(P,R1) menší, tím více informace je v
Carnapově smyslu podáno.
• Wrd(P,R1) = Wrd ... P nedává žádnou informaci
P114_6 12
Carnapovská informace - pokračování
• Je-li R1 = Tim, hovoříme o přípustném logickém
prostoru vzhledem k množině propozic P a
značíme Wrd(P).
• Jestliže Wrd(P) ≠ Wrd, pak Wrd(P) je vlastní
podmnožina Wrd, a říkáme, že množina propozic
P dává (poskytuje) informaci.
• Jestliže Wrd(P,R1) ≠ Wrd, pak Wrd(P,R1) je
vlastní podmnožina Wrd, a říkáme, že množina
propozic P dává (poskytuje) informaci v časovém
intervalu R1.
P114_6 13
logické vyplývání
• rozdíl Implikace (⇒) vs. Logické vyplývání (⊃)
• implikace (pravdivostní funkce) (BoolBoolBool)-objekt
nezávislý na stavu světa
• Propozice B logicky vyplývá z propozice A, značíme
A ⊃ B, tehdy, když pro ∀ w ∈ Wrd, ∀ t ∈ Tim platí
[[Aw]t] = Pravda ⇒ [[Bw]t] = Pravda
• jestliže [[Aw]t] = Nepravda nebo je nedefinováno, pak o
pravdivostní hodnotě propozice B nelze nic říci.
P114_6 14
uspořádání podle množství podávané
informace
(1) Nechť P, Q jsou množiny propozic takové, že pro každé
q ∈ Q platí,
buď q ∈ P nebo
∃p ∈ P tak, že p ⊃ q.
Potom pro přípustné logické prostory množin propozic
P a Q platí Wrd(P,R1) ⊆ Wrd(Q,R1) pro libovolné
R1 ⊆ Tim. (Důkaz plyne z definice logického vyplývání).
(2) Říkáme, že množina propozic Q dává nejvýše tolik
informace, jako množina propozic P, nebo že Q dává
méně nebo stejně informace jako P.
(3) Značíme Q ∠i P. Relace ∠i je částečné quasi-uspořádání
na množině množin propozic. (Proveďte důkaz !)


P114_6 15
Funkce Cn - důsledek
• P je množina propozic
(((Wrd, Tim) → Bool) → Bool) - objekt
označme ((Wrd, Tim) → Bool) = Pr, pak P/(Pr → Bool)
• Cn / (Pr → Bool) → (Pr → Bool)
definovaná
Cn = λp [∪ λq(q ∠i p)]
kde p, q :: (Pr → Bool).
• Cn se nazývá funkce „důsledek“ a dává na každé
množině propozic P množinu všech možných
jejich logických důsledků
P114_6 16
Tvrzení o Cn
• Tvrzení 1:
Operace (funkce) Cn je idempotentní:
[Cn[Cn P]] = [Cn P]
• Proveďte důkaz!
• Tvrzení 2:
Q ∠i P právě když [Cn Q] ⊆ [Cn P]
• Proveďte důkaz!
• Důsledek:
Množinu tříd propozic
{[Cn P] | P je libovolná množina propozic}
lze částečně uspořádat.
• Proveďte důkaz!
P114_6 17
... více o Cn
• Pi třída propozic, i = 1,..,n
• Pi ⊆ [Cn Pi]
• „obrácená trojúhelníková nerovnost“:
∪i=1n [Cn Pi] ⊆ [Cn (∪i=1n Pi)]
Proveďte důkaz!
• ... abychom věděli co to znamená, když říkáme „... to je
přece logické, když ...“
P114_6 18
Informační schopnost IS
• CO se má udělat = specifikace provedení
– jaké informace bude IS poskytovat = vymezení třídy
dotazů nad daným IS zodpověditelných
• jak zadat třídu dotazů, které mají být daným IS
zodpověditelné
• vytvořit seznam všech takových dotazů? NE!
• určit „bázi“ prostoru dotazů, které mají být
zodpověditelné
• Najít konstrukce, které generují propozice
dávající právě požadované odpovědi
P114_6 19
konstrukce generující množiny
propozic
x3∋x27
()∋∗
x15x16x17x21+x18(∃x16x7x3x16x13 ,x14x7−.x14+x18x15x17x18x7−x14
/%x17x60x8
,x14x7−.x14x16x91%x13x8x17x72
,x14x7−.x144x16x13x18x7x17x21x14
/%x17x60x8
,x14x9x18∃x8x14x16x91%x13x8x17x72
,x144x21x13x16x17x7x24x6x16x14
.5x245x16x23x8x177
P114_6 20
• W::Wrd, t::Tim, z::ZAM, x::PLAT
∀ λwλtλzλx([[[PlatZam(w)]t]z]=x)
(x je ale jediné - nutno použít singularizátor)
∀ λwλtλzιx([[[PlatZam(w)]t]z]=x) (k)
• Konstrukce (k) generuje všechny možné
propozice tvaru :
„Zaměstnanec Novák má plat 15 000,-Kč“
„Zaměstnanec Mach má plat 17 500,-Kč“
....
„Existuje zaměstnanec s platem nad 16 000,-Kč.“
P114_6 21
? jaké propozice generuje atribut:
x1x2x1 x3x4x2x3x5
x2x1x4
x6x7x8x9x10x13x14x15x16x17x10 x15x18x15x19x20x19x14x15x16x17x21
x2x15x22x1x18x15x3x22x18x23x24
x25x26x27
x14x14x28x28
x25x26x27
P114_6 22
? jaké propozice generuje atribut:
x27x30x2x39∗:x5
x3x4x2x3x5
x1x2x1 x2x1x4
x27x17x18x3x22x18x1x18x15x2x15x22;x164
x15x16x17x21+x18
x15x9%+%
x15x18x15x16x17x21
x15x16x17x10x13
x15x16x17x21x13%
x25x26x27
x14x14x28x28
x25x26<
;∋9
x20x14x15x16x17x21x13
;∋9x14=x14>x1∋∗?x27x26x14!x2x1x5x30∋≅
x7x23x20x28x14x17Αx7x240x18x20x10x14.x18.x244x17x10x14x7−.
P114_6 23
Bázové propozice generované atributem
• A je atribut,
A / ((Wrd, Tim) → (T → S)) nebo
A / ((Wrd, Tim) → (T → (S → Bool)))
T, S jsou entity nebo deskripce, resp. jejich n-tice
-- viz přednáška 3
• Množina bázových propozic generovaná atributem A ve
stavu světa W /(Wrd, Tim) je definována takto:
BP(A)W = λp (∃x (∃y ([[A W] x] = y ∧
∧ p = (λw [[A w] x] = y)))),
kde p::Pr, w::(Wrd, Tim), x::T, y::S nebo y::(S → Bool)
P114_6 24
Informační kapacita atributu
• Informační kapacitou atributu A ve stavu světa W
nazýváme množinu všech propozic generovaných
atributem A ve W, tj. množinu P(A)W všech logických
důsledků bázových propozic generovaných atributem A ve
W:
P(A)W = [Cn BP(A)W]
• Informační kapacita množiny atributů {A1,...,An}
ve W je dána množinou všech logických důsledků
propozic generovaných atributy Ai:
P(A1,...,An)W = [Cn ∪i=1n P(Ai)W]
P114_6 25
Důsledky
• Informační kapacity (množin) atributů lze
částečně uspořádat. -- proveďte důkaz!
• ... jsme schopni porovnávat informační
schopnosti databází a IS
P114_6 26
... zpět k propozicím generovaným PlatZam:
• Zaměstnanec Novák má plat 15 000,-Kč./ ((BoolTim)Wrd)
(propozice)
• Zaměstnanec / (((BoolUniv)Tim)Wrd)
(vlastnost individuí)
• Novák / Univ
(jméno individua jako nálepka)
• má plat / (((TimUniv)Tim)Wrd)
(fce z individuí do reálných čísel v závislosti na možném světě a x1 x1
čase)
• Propozice říká
– 1) že Novák je zaměstnanec a
– 2) že má plat a
– 3) že ten plat je 15 000,-
• ... stavět konstrukce přímo nad epistémickou bází je
pragmaticky neúnosné !
P114_6 27
„Zaostření“ pozornosti
• proces modelování (zájmové části) světa se podobá
zaostřování při fotografování: před našim objektivem je
vše, my ale snímkem zobrazíme jasně pouze to, na co jsme
zaostřili
• To znamená:
– nad EB vybereme určité typy a na ty zaostříme
pozornost
– modely pak obsahují pouze konstrukce těchto
„zaostřených“ typů
• Zaostřené typy jsou: funkce tzv. jednoduchých
typů (viz přednáška 3) a funkce definující tzv. sorty
(viz dále)
P114_6 28
příklady sort
Sorta ZAMESTNANEC:

je třída (extenze) individuí, kterou v určitém časovém intervalu
R a v aktuálním světě wa generuje konstrukce
λwλt([[Být_zaměstnancem(w)]t]), kde
Být_zaměstnancem :: (((BoolUniv)Tim)Wrd)

Sorta PLAT:

je třída (extenze) čísel konstruovaná konstrukcí
λr([Plat(r)]=Pravda), kde Plat :: (BoolTim)


P114_6 29
definice deskriptivní sorty
x1x2x3x4x5x6x7x8x6x9x10x11x14x3x15x5x8x15x16x14>.x18.x244x17x18%x144x18x9x7x18%≅x14Βx8x14x6x16Χx15x19x14x16∃1x18x9x24x7x13x240x6−
x20−∆74∃x24x7x8∃x17x19x14x13x17x18Χx24x17x16x28
• Εx8x14x7x18x14x7x8x15−x14x9x8x6%x94x24x20x177x14x13x17x18Χx24x17x16x28
• Εx8x14x7x18x14x13x17x18Χx24x17x16x14x9x8.x9x8x23x8x17x7x18x20x16x7x8∃x17x19x14x17x16x14.x18∆7x7x16∆x24x28
Εx8x14x20Χx15−x14x15x19x17x16x14x17ΦΒx16x6x18%x14x15x8/x24x17x2407x26x14x6x7x8x9x19x14%x13x18ΧΓ%Βx8x14x9x18x23+x18x15x17x18%x7x26x14x23x15x16
x15x16x17x10x145x8x7Φx23x14x23x17x16x62x14x9x84.x28x14x15x16x17x21x14∆74∃x18x14.x16x757x14x15x18x14x7x21x7x18x144x18x9x7−x14∆x24x14x17x24x6x18∃x24x20x28
∗x18x7x18x14x9x18x23+x18x15x18x20x19x177x14Βx8x14x17x8x23x19x20x244∃x21x14x17x16x144x7x16x20%x144x20Φx7x16x14>x17x16x14Ηx9x15x14x16x14∗x24x13≅x28
∗7x13x14Β4x13x8x14x13x8x23x24x14x18x22Βx8x6x7−x14x17x16Ιx8+x18x14x23x6x18%x13x19x177x14x23x165x16x15x24∃x24x14x24x14.x9x20x6−x14Βx16x23−x6x16x26
x6x7x8x9x10x13x144x8x14x20−Βx16x155%Βx8x13x8x14Αx14x23x8Βx13x21x17x16x14x17x19x23x20−x14x6x18x17x6x9x21x7x1770+x14x18x22Βx8x6x72x14Βx16x6x18
ϑx17x19∃x8.x6−Κx28
P114_6 30
definice entitní sorty
Nechť R ⊆ Tim je rozumné časové okolí (bylo-je-bude)
přítomnosti. Nechť r∈R je časový okamžik a wa je aktuální
svět.
Nechť T1, …, Tm jsou ne nutně různé typy nad EB.
Nechť Pi / (((BoolTi)Tim)Wrd) jsou konkrétní vlastnosti
přisouditelné Ti-objektům.
Označme C(Pi,r,wa) třídu Ti-objektů generovanou vlastností Pi
v daném časovém okamžiku r a aktuálním světě wa.
Potom:
r∈R C(Pi,r,wa) je entitní sorta definovaná vlastností Pi.
i=1..m r∈R C(Pi,r,wa) je entitní sorta definovaná disjunkcí
vlastností Pi, i=1,...,m.
i=1..m r∈R C(Pi,r,wa) je entitní sorta definovaná konjunkcí
vlastností Pi, i=1,...,m.
P114_6 31
sortalizace
• výběr vhodných entitních a deskriptivních sort pro
popis zájmového výseku reality
• definice entitních sort
• popis hodnot deskriptivních sort
• sortalizace je to co jiní autoři nazývají klasifikací,
tj. výběr základních tříd, nad nimiž budeme
operovat : jak při modelování, tak při práci s
databázovým systémem
• Uvědomme si, že entitní sorty jsou extenze!
• …stejně jako prvky každé báze
P114_6 32
Jednoduché typy, HIT-atributy
• HIT-atributy (funkční závislosti) jsou objekty tzv.
jednoduchých typů
(a) ((((S1,..., Sm)(T1,..., Tn))Tim)Wrd)
(b) ((((Bool(S1,..., Sm))(T1,...,Tn))Tim)Wrd)
pokud platí, že alespoň jedna ze sort Si nebo Ti je
entitní sorta.
• číslo m+n se nazývá složitost HIT-atributu
• HIT-atributy konstruujeme nad tzv. bází sort BS.
Sorty viz definice entitních a deskriptivních sort.
BS je určena tak, že pragmaticky odpovídá
našemu konkrétnímu zájmu.
P114_6 33
vztah sort k modelování
• entitní a deskriptivní sorty jsou objekty zájmu, o kterých
hovoří uživatelé IS, a ze kterých bereme hodnoty funkcí a
jejich argumentů při popisu výseku reálného světa
• jejich podmnožiny jsou definiční obory a obory hodnot
funkcí uložených formou tabulek v databázích
• v modelech nás zajímají konstrukce těch typů (tj. funkcí
nad EB), které „v rozumném časovém okolí přítomnosti“ a
v aktuálním světě poskytují tyto sorty (pro případ entitních
sort), resp. poskytují tyto sorty nezávisle na stavu světa
(pro případ deskriptivních sort)
P114_6 34
Příklady k procvičení
P114_6 35
Porovnejte informační kapacitu:
které bázové propozice generují?
které propozice generují?
x3x4x2x3x5
x1x2x1
x15x18x15x19x20x16Β707
x15x16x17x21
x1x18x15x3x22x18x23x24
x3x4x2x3x5
x1x2x1
x15x18x15x19x20x16Β707
x15x16x17x21
x1x18x15x3x22x18x23x24
P114_6 36
které bázové propozice generuje?
které propozice generuje?
x1x2x1 x3x4x2x3x5
x2x1x4
x6x7x8x9x10x13x14x15x16x17x10 x15x18x15x19x20x19x14x15x16x17x21
x2x15x22x1x18x15x3x22x18x23x24
x25x26x27
x14x14x28x28
x25x26x27
P114_6 37
které bázové propozice generuje?
které propozice generuje?
x27x30x2x39∗:x5
x3x4x2x3x5
x1x2x1 x2x1x4
x27x17x18x3x22x18x1x18x15x2x15x22
x15x16x17x21+x18
x15x9%+%
x15x18x15x16x17x21
x15x16x17x10x13
x15x16x17x21x13%
x25x26x27
x14x14x28x28
x25x26<
P114_6 38
které bázové propozice generuje?
které propozice generuje?
x27x30x2x39∗:x5
x3x4x2x3x5
x1x2x1 x2x1x4
x27x17x18x3x22x18x1x18x15x2x15x22;x164
x15x16x17x21+x18
x15x9%+%
x15x18x15x16x17x21
x15x16x17x10x13
x15x16x17x21x13%
x25x26x27
x14x14x28x28
x25x26<
;∋9
x20x14x15x16x17x21x13
x14x30x16.x24Ιx7x8x14x15x8/x24x17x240x8x14x20x14x16x7x9x24x22%x7%x14
x14%x20x8x15x8x17x100+x144x18x9x7x14Λ
P114_7 1
P114
Pojmy metody HIT
sortalizace, základní a jednoduché
typy
7
P114_7 2
Témata
• zaostření pozornosti a báze základních typů
• definice bázových typů
• HIT-atributy
• sémantika HIT-atributů
• integritní omezení
• poměr HIT-atributu
• podstata modelování
P114_7 3
„Zaostření“ pozornosti
• proces modelování (zájmové části) světa se podobá
zaostřování při fotografování: před našim objektivem je
vše, my ale snímkem zobrazíme jasně pouze to, na co jsme
zaostřili
• To znamená:
– nad EB vybereme určité typy a na ty zaostříme
pozornost
– modely pak obsahují pouze konstrukce těchto
„zaostřených“ typů
• Zaostřené typy jsou: funkce tzv. jednoduchých
typů (viz přednáška 3) a funkce definující tzv. sorty
(viz dále)
P114_7 4
vztah sort k modelování
• entitní a deskriptivní sorty jsou objekty zájmu, o kterých
hovoří uživatelé IS, a ze kterých bereme hodnoty funkcí a
jejich argumentů při popisu výseku reálného světa
• jejich podmnožiny jsou definiční obory a obory hodnot
funkcí uložených formou tabulek v databázích
• v modelech nás zajímají konstrukce těch objektů (tj.
funkcí nad EB), které „v rozumném časovém okolí
přítomnosti“ a v aktuálním světě poskytují tyto sorty (pro
případ entitních sort), resp. poskytují tyto sorty nezávisle
na stavu světa (pro případ deskriptivních sort)
P114_7 5
... zopakování
• EB = {Bool, Univ, Tim, Wrd}
• Typ nad EB:
– Bool, Univ, Tim, Wrd
– jsou-li T1, ..., Tn typy nad EB, pak (T1, ..., Tn) je typ nad EB
– jeli ještě T typ nad EB, pak ((T1, ..., Tn) → T) je typ nad EB
• Nad EB máme celou hierarchii typů
• jejich prvky jsou vesměs funkce
• tyto prvky umíme identifikovat pomocí konstrukcí
– atomických (přesněji atomických + „trivializace“)
– aplikace
– n-tice, projekce
– abstrakce
• pro obecné manipulace máme modifikovaný typovaný
lambda-kalkul
P114_7 6
Princip zaostření pozornosti (1)
• Nad EB definujeme tzv. uzlové typy, kterými
jsou entitní nebo deskriptivní sorty
• POZOR!!! Ve slovním spojení uzlové typy má
nyní slovo typ jiný význam než v definici typů nad
bází B resp. nad epistémickou bází.
• Přidáme bázový typ Bool a n-ticové typy, čímž
získáme množinu základních typů
• Provádíme přesun od epistémické báze k „bázi
základních typů“, která je tvořena něčím jiným než
původními typy a dokonce ani nemá vlastnost báze
v původním smyslu !!!
P114_7 7
Princip zaostření pozornosti (2)
• Nad základními typy konstruujeme HIT-
atributy, jako prvky tzv. jednoduchých typů
• TEDY: v hierarchii typů nad EB provedeme
zaostřením pozornosti jakousi redukci, a
jednotlivé prvky (objekty) konstruujeme jenom
nad základními typy;
konstrukcí prvků základních typů se nezabýváme
! Nahrazujeme ji definicemi !
• Podrobněji viz DM2
P114_7 8
modifikovaná hierarchie typů pro
DM
• E-typy, D-typy
• uzlové typy
• n-ticové typy
• základní typy
• prvky H-typů
E-typy
typ Bool
prvky H-typů
základní typy
konstruovány
nad
uzlové typy
n-ticové typy
D-typy
se dělí na
se dělí na
P114_7 9
sortalizace
• Určení základních typů pro danou
zájmovou oblast, kterou chceme modelovat,
se nazývá sortalizace.
• Název souvisí s bází sort BS - viz minulá přednáška.
Sortalizace je to, co jiní autoři nazývají klasifikací, či
výběrem základních tříd a pod.
• Sortalizaci provádíme procesem „zaostření
pozornosti“
P114_7 10
Entitní typy (E-typy)
• E-typem nazýváme každou entitní sortu (extenzi)
definovanou „v rozumném časovém okolí
přítomnosti“ a v aktuálním světě pomocí vlastností
nad EB, tj. pomocí intenzí
• Samotný E-typ je extenze !
• typicky, ale ne vždy, bývá E-typ podmnožinou Univ (viz
dále)
• E-typy jsou nedisjunktní a typově-teoreticky polymorfní
• ZBOZI, DODAVATEL, ODBERATEL,
ZAMESTNANEC, ...
P114_7 11
E-typy (pokračování)
• Při praktickém použití jsou E-typy často třídy individuí, které
vnímáme závisle na stavu světa (na wt)
• Ale mohou to být třídy libovolně složitých typů T nad EB (např.
DODÁVKA, VÝPUJČKA, ALGORITMUS, DRUH VÝROBKU, ...)
• Abychom se dorozuměli (veškeré modelování děláme pro
zlepšení komunikace !), musíme každý E-typ definovat
• Pro definici E-typu používáme vždy takového pojmového
systému, který pokládáme za srozumitelný těm, kterým
definici předkládáme (o tom je třeba učinit dohodu na tzv.
formovacím semináři)
• Praktický problém je ve vnímání množiny Univ: říkáme sice, že Univ
je nám dána a priori, ale jak se postupně „učíme“ rozumět určitému
prostředí, tak se naše vnímání množiny Univ obohacuje o nové prvky,
které jsme v předchozím stádiu učení ještě nevnímali.
P114_7 12
definice E-typů
• Prvkem typu (#jmeno E-typu) je každý (takový objekt),
pro který platí ...
• Příklady (pragmaticky zjednodušené):
– Objektem typu (#Artikl) je každý produkt nebo služba nebo právo,
který může být předmětem nákupu či prodeje a to včetně
produktů, služeb nebo práv dosud neexistujících, ale potenciálně
vytvořitelných pro účely rozvojových aktivit obchodní
společnosti.
– Objektem typu (#Dokument) je každý záznam nebo zpráva,
jehož/jejíž zaznamenání má pro organizaci smysl.
– Objektem typu (#Business Partner) je každé takové individuum,
které je, bylo nebo může být účastno obchodních aktivit naší
společnosti a které je zajímavé z pohledu rozvojových aktivit naší
společnosti.
P114_7 13
Deskriptivní typy (D-typy)
• D-typem je každá analytická funkce, která
poskytuje deskriptivní sortu
• obvykle charakteristická funkce (T → Bool), kde
T = Tim nebo T = Univ, při čemž do Univ zahrnujeme
všechny možné řetězce znaků reprezentovatelné na počítači
• D-typy jsou vždy extenze
• DATUM, PLAT, RODNE CISLO, TEL-CISLO,
JMENO, ...
• každý D-typ použitý v modelu musí být definován
P114_7 14
definice D-typu
• Prvkem typu (jmeno D-typu) je každý řetězec znaků
(každé číslo), který splňuje podmínky ...
• Příklady:
– Prvkem typu (Datum) je každý řetězec číslic 8 znaků dlouhý, který
má tvar RRRRMMDD, kde RRRR je číslo roku, MM je číslo
dvouciferné měsíce a DD je dvouciferné číslo dne v měsíci.
– Prvkem typu (Jmeno) je každý maximálně 45 znaků dlouhý
řetězec písmen a znaků „-“, „.“, „ “, který začíná písmenem, a ve
kterém v každé dvojici sousedních znaků je alespoň jedno
písmeno.
– Prvkem typu (Mnozstvi) je každé přirozené číslo nebo nula.
– ...
P114_7 15
n-ticové typy
• n-ticový typ je každý typ tvaru (D1, ..., Dm), kde
každé Di je D-typ (pragmaticky zúžená definice)
• D-typy v n-ticovém typu nemusí být nutně různé
• n-ticové typy jsou extenze
• POZN.: někteří autoři připouštějí i n-ticové typy, ve kterých se jako
komponenty vyskytují i E-typy. To je pro modelování zbytečné (vždy
lze obejít vhodnou konstrukcí prvku H-typu) a v praxi spíše
nevýhodné. Avšak pro formulace a důkazy obecných tvrzení je
potřebné n-ticový typ brát v tomto širším smyslu.
• n-ticový typ má svoje jméno (jako každý jiný základní typ)
• OBDOBI(OD, DO), ADRESA(PSC, MESTO, ULICE,
CISLO_DOMU)
P114_7 16
definice n-ticového typu
• T = (D1, D2, ..., Dm),
kde
D1, D2, ..., Dm
již byly definovány jako D-typy
• Adresa = (PSC, Mesto, Ulice, Cislo_domu),
(Mesto znamená jméno města, Ulice znamená jméno ulice)
P114_7 17
H-typy
• T1,...,Tn nechť jsou uzlové (ne nutně různé) typy, z
nichž alespoň jeden je E-typem.
• S nechť je libovolný základní typ
• H-typem je každý typ formy
(Wrd → (Tim → ((T1, ..., Tn) → S)))
nebo
(Wrd → (Tim → ((T1, ..., Tn) → (S → Bool))))
- ve druhém případě S nesmí být Bool
P114_7 18
HIT-atributy (v TIL s jtt)
• Objekt A nechť je nějakého H-typu
tj.
A/ (Wrd → (Tim → ((T1, ..., Tn) → S)))
resp.
A/ (Wrd → (Tim → ((T1, ..., Tn) → (S → Bool))))
• potom objekt A nazýváme HIT-atribut
• Každý HIT-atribut je intenze
• HIT-atribut A je konstruován konstrukcí
λwt λx1...xn ιy ([Awt(x1,,..., xn)] = y) v prvém případě
a
λwt λx1...xn λy [[Awt(x1, ..., xn)] y] ve druhém případě
P114_7 19
HIT-