koncepcio: bacsi e par exp (specifikacio elemzese) | | i = eb | | V V imp bod ib Tulajdonsagok felirasa + tulajdonsagok bizonyitasa. Definicio: termek szarmaztatasa. Adva SZIGMA = (S, OP) szignatura es a hozzatartozo E szemantikai egyenletek halmaza, rogzitett X = X_e mellett, minden e =(L,R) \in E eseten. Az egyenlet ket helyettesitesi szabalyt definial: L -> R; R -> L; Ha a t1 -> t2 szabaly alkalmazhato egy t \in T_{OP}(X) termre, es t1 a t-nek egy resztermje, akkor t1 helyettesitese t2-vel a t termben egy ujabb t' termet eredmenyez. Jeloles: t'=t(t1/t2). Ekkor azt mondjuk, hogy t' term kozvetlen szarmaztatasa t termnek E axiomai altal a t1->t2 szabaly felhasznalasaval. -=- A kozvetlen szarmaztatasok egy t0 -> t1 -> ... -> tn sorozata eseten t=t0 es t'=tn jeloles mellett az e'=(t,t') egyenlet E-bol szarmaztatott egyenletnek nevezzuk az adott SZIGMA szignaturahoz tartozo rogzitett X mellett. A szarmaztatott egyenlet helyes, ha t kiertekelese megegyezik t' kiertekelesevel. -=- bool is a type specification = sorts: bool oprs: T:->bool F:->bool ~:bool -> bool ^:bool bool -> bool [infix] eqns: b \in bool; ~T=F ~(~b)=b b^T=b b^F=F end bool; Tetel: ~F=T; Bizonyitas: b->T ~T->F (~(~b)=b) -> (~(~T)=T) -> (~F=T) -=- or: bool bool -> bool; b1, b2 \in bool; b1 or b2 = ~(~b1 ^ ~b2); Tetel: b1 or T = T; Bizonyitas: b2->T ~T->F (b1 or b2) = ~(~b1 ^ ~b2)) -> (b1 or T = ~(~b1 ^ ~T)) -> ~b1 ^ F -> F (~F -> T) -> (b1 or T = ~(~b1 ^ F)) -> (b1 or T = ~(F)) -> (b1 or T = T). -=- PAR -> EXP SZIGMA = (S, OP); SZIGMA-algebra = (S_A, OP_A); SPEC_A = (S_A, OP_A, E_A); d_a=(A, F, E_a); d_a=({A_0, A_1, ..., A_n}, {f_0 -> A_0, ..., f_m:A_i ... A_i -> A_k}, {..., \alpha(a) => f_s(f_c(a))=h(a), ...}; a \in A:(a_i, ..., a_k) \in (A_i x ... x A_i); Jelolesek: F = F_c \union F_s; f_c \in F_c; f_s \in F_s; -=- Egyenloseg axioma: a_1 = a_2 \tirplaegyenlo ([a_1 = f_0 \and a_2 = f_0] \xor [(\forall f_s \in F_s)(f_s(a_1)=f_s(a_2))]); A helyettesitesi szabaly: a_1 = a_2 -> ([a_1 = f_0 \and a_2 = f_0] \xor [(\forall f_s\in F_s)(f_s(a_1)=f_s(a_2))]); Peldaul: n_1 = n_2 -> ([n_1 = zerus \and n_2 = zerus] \or [ prec(n_1) = prec(n_2)]); -=- Pelda. Axioma: prec(succ(n))=n; Tetel: n!=zerus => succ(prec(n))=n; Bizonyitas: n!=zerus => succ(prec(n))=n -> prec(succ(prec(n))) = prec(n) -> prec(n)=prec(n) -> T. -=- Strukturalis indukcio: Adott SZIGMA = (S, OP); a szgnaturahoz tartozo X valtozokkal. Legyen p predikatum, amely t\in T_{OP}(x) termekre van ertelmezve. Ha 1. (\forall t \in K es \forall t \in X)(p(t)\triplaegyenlo T); 2. (\forall N(t1, ..., tn)'in T_{OP}(X))(p(N(t_1, ..., t_n) \triplaegyenlo T); akkor (\forall t \in T_{OP}(X))(p(t)\triplaegyenlo T). -=- Strukturalis indukcio atfogalmazasa: Adott SZIGMA = (S, OP); a szignaturahoz tartozo X valtozokkal. Legyen p(t): H_1(t) = H_2(t) predikatum, amely a t \in T_{OP}(X) termekre van ertelmezve. Ha 1. Alapeset: (\forall t \in K es \forall t \in X)(H_1(t)=H_2(t) \triplaegyenlo T); 2. Indukcios lepes: (\forall N(t_1, ..., t_n)\in T_{OP}(X))(H_1(N(t_1, ..., t_n)) = H_2(N(t_1, ..., t_n)) \triplaegyenlo T); akkor (\forall t\in T_{OP}(X))(H_1(t)=H_2(t) \triplaegyenlo T). -=- Adott SZIGMA=(S, OP); t \in T_{OP}(X); Legyen t_1 = H_1(f_s(t)); t_2=H_2(t); Tekintsuk a f_s(f_c(t))=H_{sc}(t); axiomat. Tetel: H_1(f_s(t)) = H_2(t); Bizonyitas: Alapeset: Bizonyitsuk be f_0 konstans szimbolumra, hogy t=f_0 eseten: H_1(f_s(f_0)) = H_2(f_0); Strukturalis indukcios lepes: Mutassuk ki, hogy minden t = f_c(t') \in T_{OP}(X) konstrukcios muveletre, hogy ha H_1(f_s(t')) = H_2(t')=T, akkor H_1(f_s(f_c(t'))) = H_2(f_c(t')) \triplaegyenlo T; azaz H_1(H_{sc}(t)) = H_2(f_c(t')) \triplaegyenlo T; A strukturalis indukcio ket helyettesitesi szabalya: 1. alapeset: H_1(f_s(t)) = H_2(t) -> H_1(f_s(f_0)) = H_2(f_0); 2. indukcios lepes: H_1(f_s(f_c(t'))) = H_2(f_c(t')) -> H_1(H_{sc}(t)) = H_2(f_c(t')); -=- e kettos par ---------------------> exp absztrakt specifikacio specifikacio | | i| = | eb | | V V imp ---------------------> bod konkret specifikacio ib -=- Reprezentacios fuggveny. Adva egy adattipus absztrakt es konkret specifikacioja: d_a=(A,F,E_a); d_c=(C, G, E_c); A={A_0, ..., A_n}; C={C_0, ..., C_m}; F={f_0:->A_0, ..., f_i:A_i...A_k->A_l, ...}; G={g_0 -> C0, ..., g_i:C_i...C_k->C_l, ...}; Az absztrakt es konkret objektumok egymashoz valo viszonya: \fi: C->A \fi=(\fi_0, ..., \fi_n), ahol \fi_0:C_0->A_0; ...; \fi_n:C_n -> A_n; -=- Definicio. Adva d_a absztrakt es d_c konkret tipusspecifikaciok, amelyeknek szignaturajuk azonos. Adva tovabba \fi: C->A, morfizmus. A C objektumhalmazt az A egy _reprezentaciojanak_ nevezzuk, ha (\forall a \in A)((\exists c \in C)(a=\fi(c)); -=- Tetel. Adva d_a absztrakt es d_c konkret tipusspecifikaciok azonos szignaturaval. \fi: C->A morfizmus. F_c \subset F a konstrukcios muveletek halmaza. Felteves: \forall f_c \in F_c konstrukcios muveletre fennall: a\in A \and f_c(a)\in A \and c\in C \and g_c(c)\in C \and a=\fi(c). Ha (\forall c \in C \and \forall f_c\in F_c)(f_c(\fi(c))=\fi(g_c(c))), akkor C objektumhalmaz az A egy reprezentacioja. Bizonyitas. Strukturalis indukcioval: a.) alapeset: a=f_0. f_0\in A_0, g_0\in C_0, feltevesunk szerint f_0=\fi(g_0). Tehat a=f_0 eseten letezik olyan c\in C_0, hogy a=\fi(c). b.) indukcio: a'=f_c(a), ahol feltesszuk, hogy a=\fi(c) es c\in C_0. Tehat a'=f_c(\fi(c)) es muvelettartasra vonatkozo feltevesunk alapjan: a'=\fi(g_c(c)), es c'=g_c(c) valasztas mellett a'=\fi(c') es c'\in C_0. -=- A reprezentacios fuggveny implicit definicioja: f_0=\fi(g_0); (\forall f_c\in F_c)(f_c(\fi(c))=\fi(g_c(C)); -=- A reprezentacios fuggveny rekurziv (explicit) definicioja: Tegyuk fel, hogy c=g_c(g_s(c)). Ennek alapjan a reprezentacios fuggveny rekurziv definicioja: \fi(c)=if c = g_0 then f_0 else f_c(\fi(g_s(c))). A reprezentacios fuggveny definicioja nem egyertelmu!