Tuple,Set
Név
(....)-Tuple {....}-Set
Szintaxis
Expression ::= (Expression,...,Expression) |{Expression,...,Expression}
Egy Tuple-nek legalább két kifejezést kell tartalmaznia és a halmaz nem állhat egyetlen séma referenciából.
Típus szabályok
Ha egy kifejezés (E1,...,En) alakú és és tíusai T1,..,Tn sorban akkor a kifejezés maga T1 × T2 × ... × Tn típusú.
Ha egy kifejezés {E1,...,En} alakú akkor minden részhalmazának a típusa T és a kifejezés típusa ℘(t)
Leírás
Az (x1,x2,..,xn) egy n-tuple-t reprezentál aminek a komponensei x1,...,xn.
Az {x1,...,xn} hamlaz tagjai csak az x1,...,xn objektumok.Néhány elem ismétlődhet is.
Ebben az esetben az ismétlődések figyelmen kívül maradnak és az elemek felsorolásának
a sorrendje sem számít.
Törvények
1. (x1,...,xn) = (y1,...,yn) ⇔ ha x1 = y1 ∧ ... ∧ xn = yn
2. y ∈ {x1,...,xn} ⇔ ha y = x1 ∨ ... ∨ y = xn
Hatványhalmaz, direkt szorzat
Név
℘ - Hatványhalmaz × - direkt szorzat
Szintaxis
Expression ::= ℘ Expression | Expression × ... × Expression
Típus szabályok
A ℘(E) kifejezésben az E argumentumnak egy ℘(t) halmaz típusnak kell lennie.Így a kifejezés típusa ℘(℘(t)).Például ha E egy egész számokat tartalmazó halmaz ℘(ℤ) típussal akkor a ℘(E)-nek ℘(℘(ℤ)) a típusa.Egy E1 × ... × En kifejezésben minden egyes argumentumnak ℘(Ti) típusúnak kell lennie.Így a típusa ℘(T1 x ... x Tn).
Leírás
Ha S egy halmaz akkor ℘(S) az S összes részhalmazának a halmaza.Ha S1,...,Sn halmazok akkor S1 × ... × Sn az összes (x1,...,xn) alakú n-tuple halmaza ahol xi ∈ Si minden i ∈ {1,...,n}.
Törvények
S1 x ... x S2 = {x1 : S1; ... ; xn : Sn • (x1,...,xn) }
Lambda és Mu kifejezések
Név
λ - Lambda kifejezés μ - Mu kifejezés
Szintaxis
Expression :: = (λ Schema-Text • Expression)
:: = (μ Schema-Text [ • Expression])
Hatókör szabályok
A (λ S • E) és a (μ S • E) kifejezésekben az s séma szöveg lokális változókat vezet be amik az
E kifejezére is kiterjednek.
Típus szabályok
Egy Mu-kifejezésben ha a kifejezés részt kihagyjuk a default érték egy karakterisztikus tuple.
A (λ S • E) kifejezésben legyen T az E típusa és a T' az Sdeklarációjában szereplő karakterisztikus
tuple típusa.Ekkor a teljes kifejezés ℘(T' x T ) típusú.
A (μ S • E) kifejezésben ha az alkifejezés típusa t akkor a kifejezés típusa is t.
Leírás
A (λ S • E) kifejezés egy függvényt jelöl ami egy alakzatot vár argumentumként amit S
határoz meg.Ez egyenlő { S • (C,E)} halmazzal ahol C a karakterisztikus tuple-je az S-nek
A (μ S • E) kifejezés csak akkor definiált ha van egy egyedi mód az S által bevezetett
változók értékadására ami az S tulajdonságát kielégíti.Ha ez így van akkor az értéke E.
Érdemes ezeket a kifejezéseket mindig zárójelbe tenni, hogy elkerüljük a kétértelműséget.
Halmaz rövidítések
Név
{ | • } -halmaz rövidítés
Szintaxis
Expression ::= {Schema-Text [• Expression]}
Kezdőértékek
Az { S • E } kifejezésben az S séma szöveg lokális változókat vezet be. A hatókörük az E kifejezésre
is kiterjed.
Típus szabályok
Az { S • E } kifejezésben ha az E alkifejezés típusa T akkor a kifejezésé ℘(T);
Leírás
A { S • E } halmaz tagjai azok az E kifejezés által felvett értékek akkor amikor az S által bevezetett változók
felveszik az összes lehetséges értéket ami kielégíti S tulajdonságot
Törvények
y ∈ { S • E } ⇔ (∃ S • y = E) ahol y nem az S változója
Lokális definíció
Név
let - lokális definíció
Szintaxis
Expression ::= (let Let-Def; ... ; Let-Def • Expression)
Let-Def ::= Ident == Expression
Hatókör szabályok
A (let x1 == E1 ; ... ; xn == En • E ) let-kifejezésben az x1,...,xn változók lokálisak és
hatókörük az E kifejezésre is kiterjed de az E1,...En kifejezésekre nem amik a lokális definíció jobb oldalai.
Típus szabályok
A (let x1 == E1 ; ... ; xn == En • E ) let-kifejezésben minden egyes lokális változó xi ugyanazzal típussal
rendekezik mint a hozzátartozó Ei kifejezés.A teljes kifejezés típusa E.
Leírás
A let-kifejezés értéke a törzse által felvett érték akkor amikor a lokális változók felveszik a jobboldali
kifejezésük által adott értéket.A (let x1 == E1 ; ... ; xn == En • E ) kifejezés definiált ha minden jobboldal
E1,..,En definiált és E is definiált a kötésben ahol x1,...,xn felveszi E1,...,En értékeit.A kifejezés értéke E
ebben a kötésben.
Törvények
(let x1 == E1 ; ... ; xn == En • E ) = (&mu x1 : t1; ... ;xn : tn | x1 = E1; ... ; xn = En • E).
Alkalmazás
Név
Alkalmazás - függvények alkalmazása
Szintaxis
Expression ::= Expression Expression
Típus szabályok
Az E1 E2 kifejezésben az E1 alkifejezésnek ℘(T1 × T2) típusúnak E2-nek pedig T1 típusúnak kell lennie.
Az egész kifejezés típusa T2.
Leírás
Az f x kifejezés az f függvény x argumentummal való alkalmazását jelöli.Az alkalmazás balasszociatív.
Törvények
(∃!y : Y • (x,y) ∈ f) ⇒
(x,f(x) ∈ f ∧ f(x) = (μ y : Y | (x,y) ∈ f)
Szelekció
Név
. - szelekció
Szintaxis
Expression ::= Expression Expression.Ident
Típus szabályok
Az E.y kifejezésben az E alkifejezésnek ⊳ x1 : t1, ... , xn : tn ⊲ sémájúnak kell lennie
és az y azonosítónak az egyik xi kompónenssel azonos nevűnek kell lennie,
Leírás
Ez szolgál egy kompónens kiválasztására.
Törvények
a ∈ S ⇒ a.y = (λ S • y)(a)