P114_5 1 P114 Konstrukce užití l - kalkulu 5 P114_5 2 Témata •TIL s jednoduchou teorií typů •atomické konstrukce •konstrukce aplikace •konstrukce abstrakce •konstrukce n-tice a projekce •ekvivalence konstrukcí •uzavřené a otevřené konstrukce P114_5 3 Elementární konstrukt přiřazení Přiřazení - zobrazení - funkce: je to předpis = procedura, který říká jaký výsledek (výstup) je přiřazen k danému vstupu P114_5 4 funkce (filozoficky) •bazální pojem: pojem funkce •skoro vše, o čem přemýšlíme jsou funkce (až na P,N, časové okamžiky, individua) •způsob, jak přemýšlíme: něco něčemu přiřazujeme, tj. základním konstruktem přemýšlení je funkce •jsme zvyklí jednotliviny, v něčem si podobné, „sypat“ do samostatných kontejnerů a přemýšlet a vyjadřovat se pomocí těchto kontejnerů = typů P114_5 5 funkce jako procedura •procesní pohled •(parciální) funkce je „výpočetní“ resp. „vyhodnocovací“ pravidlo/procedura, které poskytne buď nic nebo výsledek z množiny M, jestliže jí na vstupu zadáme hodnoty parametrů z M1x...xMn •deklar x1,..., xn::M1,..., Mn deklar y::M (tělo proc) •xi ... formální parametry, y ... výsledek P114_5 6 jak zadat konkrétní funkci ? •Máme dánu bázi B. Objekty nad B jsou –prvky množin tvořících B (bázových množin) –všechny funkce definované nad B •Vezměme funkci f /(BA) a prvek a z A. Nechť f(a) = b, b je prvkem B. b je hodnotou f na a. •Funkci f - objekt typu (BA) - a objekt a typu A lze použít jako způsob určení jiného objektu - objektu b/B. •Jak sestrojit (zadat) konkrétní funkci? Sestrojit typ (množinu všech funkcí) umíme ... •Jak obecně zadávat objekty, abychom s nimi mohli pracovat? P114_5 7 klíčový „pojem“: konstrukce •návod k určitým intelektuálním krokům, pomocí kterých porozumíme významu jazykových výrazů, tj. –porozumíme tomu, co ony reprezentují –identifikujeme přesně to, co ony (někdy ne zcela jednoznačně) označují •srovnej s KTO v přednášce č. 4 P114_5 8 konstrukce v TIL s jtt (1) •Termínem T-konstrukce rozumíme specifický způsob určení (zadání) nějakého T-objektu. •Je-li objekt zadán nějakou konstrukcí, řekneme, že konstrukce konstruuje tento objekt. •Konstrukce souvisí s „procedurou identifikace“ něčeho v rámci všeho ostatního •POZOR: konstrukce objektu je zcela něco jiného než objekt sám. •Nechť f(a) = b. Z objektu b nelze žádným způsobem poznat, že byl zadán právě konstrukcí f(a). P114_5 9 konstrukce v TIL s jtt (2) •TIL s jtt = TIL s jednoduchou teorií typů (původní varianta TIL, která byla v 80-tých létech použita jako základ metody HIT datového modelování) •v TIL s jtt sama konstrukce není objektem zájmu, ale pouze prostředek k identifikaci objektů nad EB •v tomto (jednodušším) pojetí v konstrukcích přímo vystupují objekty •později (DM2) ukážeme korekci tohoto přístupu použitím TIL s rtt (= TIL s rozvětvenou teorií typů) zavedením zásadního triku - tzv. triviální konstrukce nebo-li běžněji konstrukce trivializace •odkaz na TIL s jtt budeme v dalším vynechávat P114_5 10 konstrukce (3) •Nechť f(a) = b. Říkáme, že objekty f a a se vyskytují v konstrukci objektu b. Konstrukce jsou složeniny objektů. •V konstrukci se některé objekty mohou vyskytnout víckrát. •V konstrukcích vystupují přímo objekty, nikoli neinterpretované symboly, kterým by objekty byly přiřazovány nějakou interpretací. V tom spočívá transparentní pojetí. •Jedním z cílů je reprezentace informací v počítačích: proto se pohybujeme v dualismu transparentní - formální. P114_5 11 konstrukce, valuace (4) •Nevlastní konstrukce: neexistuje objekt, který by byl konstruován touto konstrukcí. •Nechť f je nedefinovaná na a. Potom konstrukce f(a) nezadává žádný objekt, a říkáme, že tato konstrukce je nevlastní. •Představa konstrukce jako procedury na počítači: dosazením konkrétních argumentů za formální parametry (valuací) procedura –buď něco „spočítá“ = konstruuje nějaký objekt –nebo abortuje = je při tomto dosazení nevlastní P114_5 12 proměnné, valuace (5) •Nechť pro každý typ T nad B máme přiřazenu spočetnou množinu VT tak, že VT je disjunktní s každým typem nad B (speciálně tedy VT je disjunktní s množinou T), a pro každé dva různé typy T1, T2 platí VT1 je disjunktní s VT2. Prvky množiny VT nazýváme T-proměnnými. Proměnná je T-proměnná pro nějaký typ T. •Totální funkce v z množiny všech proměnných do množiny všech objektů se nazývá valuace, jestliže pro jakoukoli T-proměnnou x platí, že vx je T-objekt. •valuace znamená dosazení hodnot za všechny proměnné při zachování „typové kázně“ P114_5 13 konstrukce atomické (6) •Nechť X je nějaký T-objekt. Tento objekt je zadán sám sebou. Říkáme, že X je T-konstrukce a nazýváme ji T-atom. Nechť v je libovolná valuace. T-konstrukce X v-konstruuje objekt X. •Nechť X je nějaká T-proměnná. Jako taková může konstruovat libovolný T-objekt. Opět řekneme, že X je T-konstrukce a nazveme ji T-atom. Nechť v je libovolná valuace. T-konstrukce X v-konstruuje objekt vX. •T-atom nemůže nikdy být nevlastní. P114_5 14 konstrukce „n-tice“ (tuple construction) •Ai, i = 1,..., n, jsou (ne nutně různé) Ti-konstrukce •Pak (A1, ..., An) je konstrukce konstruující objekty typu (T1, ..., Tn) •Nechť v je libovolná valuace: –konstrukce (A1, ..., An) je v-nevlastní, jestliže některé Ai je v-nevlastní –jsou-li všechny Ai v-vlastní, nechť Ai jsou jimi v-konstruované objekty: potom (A1, ..., An) v-konstruuje objekt (A1,... , An) P114_5 15 konstrukce projekce •Nechť B je n-ticová konstrukce konstruující objekty typu (T1, ..., Tn), kde Ti již nejsou n-ticové typy. •Potom B(i), i = 1, ..., n, jsou Ti-konstrukce (projekce na i-tou složku) •Nechť v je libovolná valuace: –je-li B v-nevlastní, pak každé B(i) je v-nevlastní –v opačném případě B v-konstruuje objekt B/(T1,...,Tn) a B(i) v-konstruuje objekt B(i) /Ti -- tzv. i-tou složku objektu B. P114_5 16 konstrukce aplikace (7) •Nechť T, T1, ... , Tn jsou jakékoli typy nad B. Nechť A je (TT1...Tn)-konstrukce, B1 je T1-konstrukce, ..., Bn je Tn-konstrukce. –A je konstrukce, která zadává objekty, jež jsou funkce (T¬(T1,...,Tn)) –Bi jsou konstrukce, jež zadávají objekty typu Ti, o kterých dále nic nevíme •[AB1...Bn] je T-konstrukce zvaná aplikace A na B1, ..., Bn. –zadání funkce lze aplikovat na zadání jiných objektů –objekt (funkci) nemohu aplikovat na jiné objekty !!! (srov. s čím pracujeme např. v integrálním počtu) P114_5 17 konstrukce aplikace (8) •Nechť v je libovolná valuace. Nechť A v-konstruuje (objekt) funkci A/(TT1...Tn) a nechť pro každé i, Bi v-konstruuje objekt Bi/Ti. Mohou nastat dva případy: –funkce A je na n-tici (B1, ... , Bn) nedefinována: potom řekneme, že konstrukce [AB1...Bn] je v-nevlastní –funkce A na n-tici (B1, ... , Bn) je definována: potom řekneme, že konstrukce [AB1...Bn] v-konstruuje T-objekt, který je hodnotou funkce A na n-tici (B1, ... , Bn) P114_5 18 konstrukce aplikace (9) •V ostatních případech, když buď –neexistuje objekt v-konstruovaný A nebo –pro nějaké i neexistuje objekt v-konstruovaný Bi –( a stačí alespoň něco z toho) •nelze konstrukci [AB1...Bn] přiřadit žádný v-konstruovaný objekt a říkáme, že je tato konstrukce v-nevlastní •PŘÍKLADY –z matematiky –ze života P114_5 19 konstrukce aplikace (9a) --příklady •sčítání v oboru reálných čísel :: ((Tim, Tim) ® Tim) [+ 5 2] konstruuje Tim-objekt 7 [+ 5 x] v-konstruuje Tim-objekt 5+x •dělení v oboru reálných čísel :: ((Tim, Tim) ® Tim) [: 6 2] konstruuje Tim-objekt 3 [: 6 0] je v-nevlastní pro všechna v, nekonstruuje nic [+ 5 [: 6 0]] je rovněž v-nevlastní pro všechna v •relace > v oboru reálných čísel :: ((Tim, Tim) ® Bool) [> 6 2] konstruuje Bool-objekt Pravda [> 2 6] konstruuje Bool-objekt Nepravda [> 6 [: 6 0]] je v-nevlastní pro všechna v [> x 2] v-konstruuje Bool-objekt Pravda pro ty valuace v, které přiřadí x číslo větší než 2 a Nepravda pro všechny ostatní valuace v P114_5 20 konstrukce aplikace (9b) --příklady •ZAM’ / (Wrd ® (Tim ® (Univ ® Bool))) [[[ZAM’ w] t] Novák] konstruuje v daném světě w a čase t Pravda, jestliže individuum s „nálepkou“ Novák je zaměstnancem, a konstruuje Nepravda, jestliže není; [[ZAM’ w] t] konstruuje v daném světě w a čase t množinu individuí, která mají tu čest právě v tomto w a t býti zaměstnanci •PlatZam / (Wrd ® (Tim ® (ZAM ® PLAT))) [[PlatZam w] t] konstruuje tabulku (dvousloupcovou) platů zaměstnanců, která platí v daném světě w a čase t; [[[PlatZam w] t] Novák] konstruuje tu hodnotu z množiny PLAT, která je přiřazena předchozí tabulkou Novákovi; [[[[PlatZam w] t] Novák] 8000] konstruuje P nebo N podle toho, zda Novák má či nemá plat 8000. P114_5 21 konstrukce aplikace (9c) --příklady •RektorMU / (Wrd ® (Tim ® Univ)) [[RektorMU w] t] konstruuje Univ-objekt označený nálepkou, která je jménem rektora MU v daném w a daném čase t; v čase t=1912 a v aktuálním světě je v-nevlastní v čase t= 2001 konstruovala v aktuálním světě Jiřího Zlatušku •RektorZDSBotanicka / (Wrd ® (Tim ® Univ)) [[RektorZDSBotanicka w] t] je v-nevlastní pro všechny v (v žádném možném světě není žádné individuum rektorem ZDŠ - to je naše domluva na významu slova rektor a na významu slova ZDŠ) •RektorZDS / (Wrd ® (Tim ® (Univ ® Bool)) [[RektorZDS w] t] v-konstruuje {} pro všechny valuace v P114_5 22 konstrukce abstrakce (10) •Nechť T, T1, ... , Tn jsou jakékoli typy nad B. Nechť A je T-konstrukce. Nechť x1, ... , xn jsou navzájem různé proměnné, xi je Ti-proměnná, značíme xi :: Ti. •Definujeme, že „l x1...xn (A)“ je (TT1 ... Tn)-konstrukce, zvaná (lambda-) abstrakce A vzhledem k proměnným x1, ... , xn. •Všimněme si, že to připomíná zápis: procedure X1 ... Xn (tělo procedury), který z „holého“ algoritmu nějakého výpočtu vyrábí (opakovatelně použitelnou a jako celek použitelnou) funkci •lambda-abstrakce vyrábí (objekty) funkce z n-tic (T1,..,Tn) do T. P114_5 23 konstrukce abstrakce (11) •Jaké objekty lambda-abstrakce konstruuje? •Příprava na odpověď: •Nechť v je libovolná valuace. Označme v(x1:=X1, ... , xn:=Xn), kde Xi jsou Ti-objekty, valuaci která se od v liší pouze tím, že proměnným xi (i=1,...,n) přiřazuje objekty po řadě Xi/Ti. Všem ostatním proměnným přiřazuje to co valuace v. •Nechme Xi probíhat všechny objekty z Ti, tj. postupně je „dosazujeme“ do v(x1:=X1, ..., xn:=Xn) P114_5 24 konstrukce abstrakce (11a) •Definujme funkci F / (TT1...Tn) takto: •F(X1,..., Xn) je nedefinováno, jestliže A je v(x1:=X1,...,xn:=Xn)-nevlastní •F(X1,..., Xn) je T-objekt v(x1:=X1,...,xn:=Xn)-konstruovaný A, jestliže A není v(x1:=X1,...,xn:=Xn)-nevlastní. •Potom říkáme, že l x1...xn (A) v-konstruuje F • P114_5 25 konstrukce abstrakce (12) •lamda-abstrakce nemůže být nikdy nevlastní, může maximálně dávat všude nedefinovanou funkci •to že l x1...xn (A) je (TT1...Tn)-konstrukce se zapisuje l x1...xn (A) :: (TT1...Tn) •říkáme, že je to x1,...,xn - uzávěr otevřené konstrukce A •volná proměnná: lze jí valuací v udělit libovolnou hodnotu •uzavřená konstrukce: neobsahuje volné proměnné •nechť A obsahuje nejvýše proměnné x1, ..., xn. Potom l x1...xn (A) je uzavřená konstrukce P114_5 26 konstrukce abstrakce - příklady •otevřená konstrukce: x+5 k ní uzavřená konstrukce: lx (x+5) •v je valuace, která x přiřadí 3 a y přiřadí 4: ly [> x y] v-konstruuje (Bool Tim)-objekt -- třídu čísel menších než 3 lx [> x y] v-konstruuje třídu čísel větších než 4 lxy [> x y] konstruuje (nezávisle na v) relaci „>“ (Bool Tim Tim)-objekt lx ly [> x y] konstruuje funkci, která každému číslu m (dosazenému za x) přiřadí třídu čísel menších než m ly lx [> x y] konstruuje funkci, která každému číslu m (dosazenému za y) přiřadí třídu čísel větších než m • P114_5 27 konstrukce abstrakce - příklady •Nechť x::ZAM, y::PLAT, w::Wrd, t::Tim PlatZam::(((PLAT ZAM)Tim)Wrd) •lw lt lx ly[[[[ PlatZam w]t]x]y] konstruuje co? •poněvadž datové funkce nad EB jsou (vzhledem k w, t) totální, lze uplatnit Shönfinkelovu redukci, a ekvivalentně psát: lwt lx ly[[[ PlatZam (w, t)]x]y] •tato konstrukce ale konstruuje funkce typu ((((Bool PLAT) ZAM)(Tim,Wrd)) •jak vyjádřit, že množina ly[[[ PlatZam (w, t)]x]y] je pro dané (w,t) a dané x vždy jednoprvková ? •funkce „singularizátor“ -- viz dále P114_5 28 podkonstrukce •Nechť A je konstrukce. •(1) A je podkonstrukce A •(2) Je-li A tvaru [BB1...Bn], pak B, B1, ..., Bn jsou podkonstrukce A. •(3) Je-li A tvaru l x1...xn B, pak B je podkonstrukce A. •(4) Jeli A tvaru (B1, ..., Bn), pak B1, ..., Bn jsou podkonstrukce A. •(5) Je-li C podkonstrukce B a B je podkonstrukce A, pak C je podkonstrukce A. •Nic jiného, než je řečeno v (1) až (5) není podkonstrukce P114_5 29 vázané výskyty a volné proměnné •Mějme konstrukci l x1...xn (A) (1) •všechny výskyty proměnných x1, ..., xn v (1) jsou vázané výskyty těchto proměnných v konstrukci (1) •Nechť C je podkonstrukcí B. Výskyty proměnných, které jsou vázanými výskyty v C, jsou vázanými výskyty v B. To platí pro všechna taková B, že C je podkonstrukcí B. •Výskyty proměnných, které nejsou vázanými výskyty v dané konstrukci, nazýváme volnými výskyty . •Proměnné, které mají alespoň jeden volný výskyt v A, nazýváme volné proměnné konstrukce A. P114_5 30 ekvivalence konstrukcí •konstrukce C1 je ekvivalentní s konstrukcí C2, jestliže pro libovolnou valuaci v a libovolný objekt A platí C1 v-konstruuje A právě tehdy, když C2 v-konstruuje A . •Srov. princip extenzionality •ekvivalentní transformace konstrukcí /MaPaZla - str.78/ pravidlo alfa-redukce: Jestliže konstrukce C obsahuje vázané i volné výskyty proměnné x, pak všechny vázané výskyty x můžeme přejmenovat na libovolné jméno y takové, které se nevyskytuje v konstrukci C. Výsledkem je konstrukce ekvivalentní s C. •transparentní formulace pravidla beta-redukce z lambda kalkulu: P114_5 31 pravidlo beta-redukce: •konstrukce A::T nechť obsahuje volné proměnné x1::T1,... , xn::Tn •l x1...xn(A) :: (TT1...Tn) •definujeme operaci A(x1, ..., xn := B1, ..., Bn) : –ta v konstrukci A nahradí každý výskyt proměnné xi konstrukcí Bi::Ti –a je přípustná pouze tehdy, když nahrazení nevede k tomu, že některá z volných proměnných konstrukce Bi se po nahrazení stane vázanou proměnnou v Bi P114_5 32 pravidlo beta-redukce - pokračování •Potom pro každou valuaci v: konstrukce A(x1, ..., xn := B1, ..., Bn) a konstrukce [(l x1...xn (A))B1...Bn] v-konstruují týž T-objekt nebo jsou obě v-nevlastní • P114_5 33 otevřené a uzavřené konstrukce •Nechť A je konstrukce, která obsahuje volné proměnné. Potom A se nazývá otevřená konstrukce. •Nechť A je konstrukce, která neobsahuje žádnou volnou proměnnou. Potom A se nazývá uzavřená konstrukce. •To co konstruují otevřené konstrukce, je vždy závislé na valuaci. Uzavřené konstrukce konstruují objekty nezávisle na valuaci. •Uzavřené konstrukce jsou vhodné pro modelování těch objektů, které chceme vnímat jako celé funkce, tj. kde pracujeme s funkcí jako takovou, nikoli s jejími jednotlivými hodnotami v závislosti na konkrétních argumentech •Otevřené konstrukce jsou vhodné pro modelování toho, co je přirozené vnímat jako závislé na konkrétní valuaci: databázový stroj (obecně stroj = „engine“) který umožňuje manipulovat s daty P114_5 34 PŘÍKLADY –logických operátorů –matematických funkcí –konstrukce množin –funkcí ze života –jak je to s nevlastností ekvivalentních konstrukcí ? • P114_5 35 kvantifikátory, singularizátor •X::T, B je Bool- konstrukce •LT::((T ® Bool) ® Bool) je tzv. obecný kvantifikátor: [LT lx B] = Pravda, když lx B konstruuje právě T, jinak, tj. když lx B konstruuje T´ Ì T, je [LT lx B] = Nepravda •VT::((T ® Bool) ® Bool) je tzv. existenční kvantifikátor: [VT lx B] = Pravda, když lx B konstruuje neprázdnou podmnožinu T, jinak Nepravda •IT::((T ® Bool) ® T) je tzv. singularizátor: [IT lx B] = t, když lx B konstruuje jednoprvkovou podmnožinu {t}Í T, jinak je nedefinován •místo [LT lx B] píšeme "x (B) místo [VT lx B] píšeme $x (B) místo [IT lx B] píšeme ix (B) P114_5 36 reálný svět •Mějme atribut (viz přednáška č. 3) OdbDodZbozi = odběratelé (#ODB) kterým daný dodavatel (#DOD) dodává dané zboží (#ZBOZI) :: (...((DOD, ZBOZI) ® (ODB ® Bool))) •Jak vypadá jeho konstrukce: x::DOD, z::ZBOZI, y::ODB, w,t jako obvykle: lwt (lxz (ly ([[OdbDodZboziwt (x,z)] y]))) P114_5 37 jak je to s nevlastností ekvivalentních konstrukcí ? •Nechť C1 je ekvivalentní s C2. Nechť v je libovolná valuace. •C1 je v-nevlastní právě tehdy, když C2 je v-nevlastní. •Proveďte důkaz. P114_5 38 otázky •co je to matematika ? •je matematika více o objektech nebo o konstrukcích •co nám více pomůže při domlouvání? objekty nebo konstrukce? •jsou v reálném světě objekty? jsou v něm konstrukce? •jak je to s objekty a konstrukcemi v ideálních světech: jeden IdSvet versus dva a více IdSvetu, vytváření společné kultury •kultura lidí vs. kultura lidí + matematických strojů