C03pl

7/26/2019 C03pl

1/65

Curs 3

2015-2016 Programare Logica1/41

7/26/2019 C03pl

2/65

Cuprins

1 Izomorfisme de algebre multisortate

2 Tipuri Abstracte de Date

3 Termeni. Algebra de termeni.

4 Algebre initiale

2/41

7/26/2019 C03pl

3/65

Amintiri

Definitie

Osignatura multisortataeste o pereche (S, ), unde

S= este o multime desorturi.

este o multime desimboluri de operatiide forma

:s1s2. . . sn s.

3/41

7/26/2019 C03pl

4/65

Amintiri

Definitie

Osignatura multisortataeste o pereche (S, ), unde

S= este o multime desorturi.

este o multime desimboluri de operatiide forma

:s1s2. . . sn s.

Definitie

Oalgebra multisortata de tip (S, )este o structura A= (AS, A)unde

AS={As}sSeste o multime S-sortata (multimea suport).

A={A} este o familie de operatii astfel ncatdaca :s1 . . . sn s n , atunci A :As1 . . . Asn As(operatie).daca : s n , atunci A As (constanta).

3/41

7/26/2019 C03pl

5/65

Amintiri

Fie doua (S, )-algebreA

= (AS, A

) siB

= (BS, B

).

Definitie

Unmorfism de (S, )-algebre h: A Beste o functieS-sortatah= {hs}sS :{As}sS {Bs}sScare verificaconditia decompatibilitate:

pt. or. :sdin avem hs(A) =B.

pt. or. :s1. . . sn sdin si or. a1 As1 , . . . , an Asn avem

hs(A(a1, . . . , an)) =B(hs1(a1), . . . , hsn(an)).

As1 A

sn

A

As

hs1 . . . hsn hs

Bs1 BsnB Bs

4/41

7/26/2019 C03pl

6/65

Izomorfisme de algebre multisortate

5/41

7/26/2019 C03pl

7/65

Definitie si proprietati

Definitie

Un -morfism h:A Bse numeste izomorfismdaca exista un-morfism g :B A astfel ncat h; g= 1A si g; h= 1B.

Daca -morfismul g de mai sus exista, atunci este unic:

fie un -morfism f : B A astfel ncat h; f = 1A si f; h= 1Bavem g=g; 1A =g; (h; f) = (g; h); f = 1B; f =f

Deoarece geste unic, de obicei se noteaza h1

h; h

1

= 1A

si h

1

; h= 1B

(1A)1 = 1A

6/41

7/26/2019 C03pl

8/65

Proprietati

PropozitieFie h:A Bun -morfism. Atunci

h este izomorfism este functie S-sortata bijectiva.

Demonstratie

()Presupunem ca h este izomorfism.

Atunci exista -morfismul h1 :B A a.. h; h1 = 1A sih1; h= 1B.

Deducem ca hs; h1s = 1As si h1s ; hs= 1Bs, or. sS.Deci hseste inversabila, si deci bijectiva, pt. or. sS.

In concluzie, h este functie S-sortata bijectiva.

7/41

7/26/2019 C03pl

9/65

Demonstratie (cont.)

()Presupunem ca h este functieS-sortata bijectiva.

Pt. or. sS exista h1s :BsAs a.. hs; h1s = 1As si

h1s ; hs= 1Bs.

Definim -morfismul h1 ={h1s }sS.

Evident avem

(h; h1)s=hs; h1s = 1As = (1A)s

(h1; h)s=h1s ; hs= 1Bs = (1B)s

Deci h; h1 = 1A si h1; h= 1B.

8/41

7/26/2019 C03pl

10/65


Trebuie sa aratam ca functia S-sortata h1 :BA este -morfism.

Fie :s1. . . sn s n si (b1, . . . , bn) Bs1 . . . Bsn .

Cum h este -morfism, pt. h1s1 (b1) As1 , . . . , h1sn

(bn) Asn avem

hs(A(h1s1 (b1), . . . , h

1sn (bn))) = B(hs1(h

1s1 (b1)), . . . , hsn(h

1sn (bn)))

= B(b1, . . . , bn).

Aplicam h1s n ambele parti si obtinem:

A(h

1

s1 (b1), . . . ,

h

1

sn (bn

)) =h

1

s (B(b1, . . . ,

bn

)),

Deci h1 :B A este izomorfism.

9/41

7/26/2019 C03pl

11/65

Proprietati

Propozitie

Compunerea a doua izomorfisme f :A B si g :B Ceste unizomorfism. Mai mult,

(f; g)1 =g1; f1.

Demonstratie

Exercitiu!

10/41

7/26/2019 C03pl

12/65

-algebre izomorfe

Definitie

Doua -algebre A si Bsuntizomorfedaca exista un izomorfismf :A B.

Daca A si B sunt izomorfe, notam A B.Daca A B, atunci AsBs, or. sS.

A A (1A este izomorfism)

A B B A

A B si B C A C

Relatia de izomorfism este o relatie de echivalenta(reflexiva, simetrica si tranzitiva).

11/41

7/26/2019 C03pl

13/65

Exemple

ExempluNAT = (S={nat}, ={0 : nat, succ :natnat})

NAT-algebraA: Anat := N, A0 := 0, Asucc(x) :=x+ 1

NAT-algebraB: Bnat :={0, 1}, B0:= 0, Bsucc(x) := 1 x

NAT-algebraC: Cnat :={2n | n N}, C0 := 1, Csucc(2

n) := 2n+1

A B

nu exista niciun NAT-morfism g :B A

A C:h={hnat}: {Anat} {Cnat}, hnat(n) := 2

n

h este izomorfism

12/41

7/26/2019 C03pl

14/65

Observatie

Algebrele izomorfe sunt identice (modulo redenumire).

13/41

7/26/2019 C03pl

15/65

Tipuri Abstracte de Date

14/41

7/26/2019 C03pl

16/65

ADT - Abstract Data Type

Untip abstract de dateeste o multime dedate(valori) si operatiiasociate lor, a caror descriere (specificare) este independenta deimplementare.

15/41

7/26/2019 C03pl

17/65



Oalgebraeste formata dintr-omultime de elemente si omultime deoperatii.

15/41

7/26/2019 C03pl

18/65




Algebrele pot modela tipuri de date.

15/41

7/26/2019 C03pl

19/65




Algebrele pot modela tipuri de date.

Doua algebreizomorfeau acelasi comportament, deci trebuie sa fie

modele ale aceluiasi tip de date. Aceasta asigura independenta deimplementare.

15/41

7/26/2019 C03pl

20/65


Osignatura(S, ) esteinterfata sintacticaa unui tip abstract dedate.

16/41

7/26/2019 C03pl

21/65



O(S, )-algebraA= (AS, A) este oposibila implementare.

16/41

7/26/2019 C03pl

22/65




Daca A B, atunci A si B implementeaza acelasi tip de date.

16/41

7/26/2019 C03pl

23/65




Daca A B, atunci A si B implementeaza acelasi tip de date.

Definitie

Untip abstract de dateeste oclasa C de (S, )-algebre cu proprietateaca oricare doua (S, )-algebre din C sunt izomorfe:

A, B C A B.

[A] :={B(S, )-algebra| A B}este tip abstract de date.

16/41

7/26/2019 C03pl

24/65

Termeni. Algebra de termeni.

17/41

7/26/2019 C03pl

25/65

Termeni fara variabile

Fie (S, ) o signatura multisortata.

Definitie

Multimea S-sortata atermenilor fara variabile,

T,

este cea mai mica multime de siruri finite peste alfabetul

L=

w,sw,s {(, )} {, }

care verifica:

1 Daca :s n , atunci (T)s,

2 Daca :s1. . . sns n si ti(T)si, or. 1 in, atunci(t1, . . . , tn) (T)s.

18/41

E l

7/26/2019 C03pl

26/65

Exemple

Exemplu

NATBOOL= (S, )

S={bool, nat}

={T : bool, F : bool, 0 :nat, s :natnat,:nat natbool}

TNATBOOL:

(TNATBOOL)nat={0, s(0), s(s(0)), . . .}

(TNATBOOL)bool={T, F, (0, 0), (0, s(0)), . . .}

Cateva siruri carenu sunt termeni: (T, F), s(0), Ts(0), . . .

19/41

E l

7/26/2019 C03pl

27/65

Exemple

Exemplu

NATEXP= (S, )

S={nat}

={0 :nat, s :natnat,+ :nat natnat, : nat natnat}

TNATEXP:

(TNATEXP)nat={0, s(0), s(s(0)), . . . ,+(0, 0), (0, +(s(0), 0)), . . .}

Cateva siruri carenu sunt termeni: +(0), 0(s)s(0), (s(0)), . . .

20/41

M l i d i bil

7/26/2019 C03pl

28/65

Multime de variabile


Definitie

Omultime de variabileeste o multime S-sortata X ={Xs}sS astfelncat

Xs Xs =, or. s, s S, s=s,

Xs {}:s1...sns =,

Xs {}:s =.

Simbolurile de variabile sunt distincte ntre ele si sunt distincte desimbolurile de operatii/constante din .

21/41

T i ( ii)

7/26/2019 C03pl

29/65

Termeni (expresii)

Fie (S, ) o signatura multisortata si Xo multime de variabile.

Definitie

Multimea S-sortata atermenilor cu variabile din X,

T(X),

este cea mai mica multime de siruri finite peste alfabetul

L=

sSXs

w,sw,s {(, )} {, }care verifica:

1 XT(X),

2 Daca :s n , atunci T(X)s,

3 Daca :s1. . . sns n si tiT(X)si, or. 1 in, atunci(t1, . . . , tn) T(X)s.

tT(X) se numestetermen(expresie).

Notam cu Var(t)multimea variabilelor care apar n termenul t.

T=T()

22/41

E l

7/26/2019 C03pl

30/65

Exemple

ExempluNATEXP= (S, )

S={nat}

={0 :nat, s :natnat,

+ :nat natnat,

: nat natnat}X:

Xnat={x, y}

TNATEXP(X):

TNATEXP(X)nat={0, x, y, s(0), s(x), s(y), s(s(0)), s(s(x)), . . . ,

+(0, 0), +(0, x), (0, +(s(0), 0)), . . .}

Cateva siruri carenu sunt termeni: +(x), 0x, 0(s)s(0), (s(0)), . . .

23/41

E emple

7/26/2019 C03pl

31/65

Exemple

Exemplu

STIVA= (S, )

S={elem, stiva}

={0 : elem, empty : stiva, push:elem stiva stiva,pop:stiva stiva, top:stiva elem}

X:Xelem ={x, y} si Xstiva =

TSTIVA(X):

TSTIVA(X)elem ={0, x, y, top(pop(empty)),top(push(x, empty)), . . .}

TSTIVA(X)stiva ={empty, push(y, empty), pop(empty),push(top(empty), empty), . . .}

Cateva siruri carenu sunt termeni: pop(0), (pop)top(empty), empty(y)

24/41

Inductia pe termeni

7/26/2019 C03pl

32/65

Inductia pe termeni


Fie P oproprietateastfel ncat:

pasul initial:

P(x) =true, or. xX,P() =true, or. :s.

pasul de inductie:

pt. or. :s1. . . sn s si or. t1T(X)s1 , . . . , tn T(X)sn ,daca P(t1) = . . .= P(tn) =true, atunci P((t1, . . . , tn)) =true.

Atunci P(t) =true, oricare tT(X).

25/41

Termeni ca arbori

7/26/2019 C03pl

33/65

Termeni ca arbori

Un termen tT(X) poate fi reprezentat ca unarbore arb(t)astfel:

daca t= (simbol de constanta), atunci arb(t) := ,

daca tX (variabila), atunci arb(t) :=t,

daca t= (t1, . . . , tn), atunci arb(t) :=

arb(t1) arb(tn). . .

26/41

Exemple

7/26/2019 C03pl

34/65

Exemple

Exemplu

NATEXP= (S, )

S={nat}


arb((0, +(s(0), 0))) =

0 +

s 0

0

27/41

Algebra termenilor

7/26/2019 C03pl

35/65

Algebra termenilor


Definitie

Multimea S-sortata a termenilor T(X) este o (S, )-algebra, numitaalgebra termenilor cu variabile din X si notata tot T(X), cu operatiiledefinite astfel:

pt. or. :sdin , operatia corespunzatoare esteT := T(X)s

pt. or. :s1. . . sn sdin , operatia corespunzatoare este

T :T(X)s1...sn T(X)sT(t1, . . . , tn) := (t1, . . . , tn)

or. t1 T(X)s1 , . . . , tn T(X)sn .

T algebra termenilor fara variabile (X =)

28/41

Exemple

7/26/2019 C03pl

36/65

Exemple

Exemplu

NATEXP= (S, )

S={nat}


TNATEXP:(TNATEXP)nat={0, s(0), s(s(0)), . . . ,

+(0, 0), (0, +(s(0), 0)), . . .}

Algebra termenilor:

Multimea suport: TNATEXPOperatii:

T0 := 0, Ts(t) :=s(t),T+(t1, t2) := +(t1, t2),T(t1, t2) := (t1, t2).

29/41

Observatii

7/26/2019 C03pl

37/65

Observatii

Semantica unui modul n Maude (care contine doar declatii de sorturi,

operatii si variabile) este o algebra de termeni.

30/41

7/26/2019 C03pl

38/65

Algebre initiale

31/41

Algebra initiala

7/26/2019 C03pl

39/65

Algebra initiala

Fie

(S, ) o signatura multisortata,

Ko clasa de (S, )-algebre.

Definitie

O (S, )-algebra I Kesteinitiala n Kdaca pentru orice B K

exista un unic (S, )-morfism f :I B.

32/41

Proprietati

7/26/2019 C03pl

40/65

Proprietati

Propozitie

DacaIeste initiala n K si A Kastfel ncat A I, atunciA esteinitiala n K.

33/41

Proprietati

7/26/2019 C03pl

41/65

p

Propozitie

DacaIeste initiala n K si A Kastfel ncat A I, atunciA esteinitiala n K.

Demonstratie

CumA Kastfel ncat A I, fie A :A Iun izomorfism.Fie B K. CumIeste initiala, exista un unic morfism fB :I B.

Demonstram ca exista un unic morfism h:A B:

Existenta. Consideram h:= A; fB :A B. Deoarece compunerea

morfismelor este morfism, obtinem ca h este morfism.

Unicitatea. Presupunem ca exista un alt morfism g :A B.Atunci 1

A ; g :I Beste morfism, deci 1

A ; g=fB. Rezulta ca

g= A; fB =h.

33/41

Proprietati

7/26/2019 C03pl

42/65

p

PropozitieDacaA1 si A2 sunt initiale n K, atunciA1 A2.

34/41

Proprietati

7/26/2019 C03pl

43/65

p

PropozitieDacaA1 si A2 sunt initiale n K, atunciA1 A2.

Demonstratie

CumA1 si A2 sunt initiale n K, existaun unic morfism f :A1 A2 si

un unic morfism g :A2 A1.

Avem f; g :A1 A1, 1A1 :A1 A1 si A1 initiala, deci f; g= 1A1 .

Similar obtinem g; f = 1A2 .

In concluzie A1 A2.

34/41

(S, )-algebra initiala

7/26/2019 C03pl

44/65

( , ) g


Consideram Kclasatuturor (S, )-algebrelor.

Ieste (S, )-algebra initiala daca pentru orice (S, )-algebraBexista un unic morfism f :I B.

Teorema

Pentru orice(S, )-algebraB, exista un unic morfism f :T B.

f(t) este interpretarea termenului tT n B.

35/41

7/26/2019 C03pl

45/65

Demonstratie

Fie Bo (S, )-algebra.Demonstram ca exista un unic morfism f :T B.

36/41

7/26/2019 C03pl

46/65

Demonstratie


Existenta. Definim f :T Bprin inductie pe termeni:

(P(t) = f(t) este definit)

36/41

7/26/2019 C03pl

47/65

Demonstratie




pasul initial: daca :s, atunci fs() :=B.

36/41

7/26/2019 C03pl

48/65

Demonstratie




pasul initial: daca :s, atunci fs() :=B.pasul de inductie: daca :s1. . . sns sit1 (T)s1 . . . , tn (T)sn astfel ncat fs1(t1), . . . , fsn(tn) definite,atunci fs((t1, . . . , tn)) :=B(fs1(t1), . . . , fsn(tn)).

36/41

7/26/2019 C03pl

49/65

Demonstratie





Din principiului inductiei pe termeni, f(t) este definita pt. or. tT.

36/41

7/26/2019 C03pl

50/65

Demonstratie






Demonstram ca f este morfism.

36/41

7/26/2019 C03pl

51/65

Demonstratie







daca :s, atunci fs(T) =fs() =B;

36/41

7/26/2019 C03pl

52/65

Demonstratie







daca :s, atunci fs(T) =fs() =B;

daca :s1. . . sn s si t1 (T)s1 , . . . , tn(T)sn , atuncifs(T(t1, . . . , tn)) =fs((t1, . . . , tn)) =B(fs1(t1), . . . , fsn(tn)).

36/41

7/26/2019 C03pl

53/65


Unicitatea. Fie g :T Bun morfism.Demonstram ca g=f prin inductie pe termeni:

(P(t) = gs(t) =fs(t))

37/41

7/26/2019 C03pl

54/65



(P(t) = gs(t) =fs(t))

pasul initial: daca :s, atunci gs() =gs(T) =B =fs().

37/41

7/26/2019 C03pl

55/65



(P(t) = gs(t) =fs(t))


pasul de inductie: daca :s1. . . sns sit1 (T)s1 , . . . , tn(T)sn a. .gs1(t1) =fs1(t1), . . . , gsn(tn) =fsn(tn), atunci

37/41

7/26/2019 C03pl

56/65



(P(t) = gs(t) =fs(t))



gs((t1, . . . , tn)) =gs(T(t1, . . . , tn)) =B(gs1(t1), . . . , gsn(tn)) =B(fs1(t1), . . . , fsn(tn)) =fs((t1, . . . , tn)).

37/41

7/26/2019 C03pl

57/65



(P(t) = gs(t) =fs(t))



gs((t1, . . . , tn)) =gs(T(t1, . . . , tn)) =B(gs1(t1), . . . , gsn(tn)) =B(fs1(t1), . . . , fsn(tn)) =fs((t1, . . . , tn)).

Conform principiului inductiei pe termeni, gs(t) =fs(t), oricare tT, s,deci g=f.

37/41

Consecinta

7/26/2019 C03pl

58/65

Corolar

T este(S, )-algebra initiala.

38/41

Exemplu

7/26/2019 C03pl

59/65

Exemplu

(S, ) signatura multisortata

39/41

Exemplu

7/26/2019 C03pl

60/65

Exemplu


(S, )-algebraD= (DS, D)

Ds := N, or. s S,

daca : s, atunci D := 0daca :s1 . . . sn s, k1, . . . , kn N, atunciD(k1, . . . , kn) := 1 + max(k1, . . . , kn).

39/41

Exemplu

7/26/2019 C03pl

61/65

Exemplu



Ds := N, or. s S,


f :T D unicul morfism

39/41

Exemplu

7/26/2019 C03pl

62/65

Exemplu



Ds := N, or. s S,



Ce reprezinta valoarea f(t) pentru un termen t?

39/41

Exemplu

7/26/2019 C03pl

63/65

Exemplu



Ds := N, or. s S,



Ce reprezinta valoarea f(t) pentru un termen t?

f(t) este adancimea arborelui arb(t).

39/41

Observatii

7/26/2019 C03pl

64/65

Untip abstract de dateeste oclasaC

de (S,

)-algebre cuproprietatea ca oricare doua (S, )-algebre din C sunt izomorfe(A, B C A B.)

Consideram clasa de (S, )-algebre

I(S,) ={I | I (S, )-algebra initiala}

I(S,) este untip abstract de date.

T I(S,).

Un modul n Maude (care contine doar declatii de sorturi si

operatii) defineste un astfel de tip abstract de date si construiesteefectiv algebra T.

40/41

7/26/2019 C03pl

65/65

Pe saptamana viitoare!

41/41

C03pl

Documents

Transcript of C03pl