Programare Logica

download Programare Logica

of 164

  • date post

    15-Dec-2014
  • Category

    Documents

  • view

    79
  • download

    3

Embed Size (px)

description

progrmare logica

Transcript of Programare Logica

Cuprins1 ALGEBRE MULTISORTATE 51.1 CONCEPTUL DE ALGEBRA MULTISORTATA . . . . . . . . . . . . . . . . . . . . . . . 51.1.1 Mult imi si funct ii multisortate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.1.2 Signaturi multisortate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61.1.3 Algebre multisortate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.1.4 Morsme de algebre multisortate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.1.5 Izomorsme de algebre multisortate . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.2 ALGEBRE LIBERE - APLICATII . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.2.1 Expresii . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111.2.2 Unicitatea abstract ie de un izomorsm a algebrelor libere . . . . . . . . . . . . . . . 131.2.3 Tipuri abstracte de date - introducere . . . . . . . . . . . . . . . . . . . . . . . . . . 141.3 SUBALGEBRE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161.3.1 Operator de nchidere. Familie Moore . . . . . . . . . . . . . . . . . . . . . . . . . . 171.3.2 P arti stabile, Subalgebre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181.3.3 Morsme si p art i stabile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201.4 EXISTENTA ALGEBRELOR LIBERE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211.4.1 Algebre libere si algebre Peano . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211.4.2 Algebre Peano . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231.4.3 Algebra arborilor de derivare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 241.4.4 Existent a algebrelor init iale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261.4.5 Existent a algebrelor libere . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261.5 SEMANTICA ALGEBREI INITIALE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271.5.1 Semantica unui sir de cifre ca num ar natural . . . . . . . . . . . . . . . . . . . . . . 271.5.2 Un calculator de buzunar . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 281.5.3 Arbori de derivare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301.5.4 Scrierea polonez a invers a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 331.5.5 Compilare . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 341.6 CONGRUENT E si ALGEBRE CAT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 351.6.1 Congruent e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 361.6.2 Algebre cat . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 381.7 ALGEBRE PROIECTIVE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391.7.1 Proiectivitatea algebrelor libere . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391.7.2 Alte proprietat i . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391.8 SPRE ABSTRACTIZAREA TIPURILOR DE DATE . . . . . . . . . . . . . . . . . . . . . 401.8.1 Ecuat ii . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401.8.2 Ecuat ii condit ionate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 411.8.3 Necesitatea utiliz arii cuanticatorilor n ecuat ii . . . . . . . . . . . . . . . . . . . . . 421.8.4 In primul r and semantica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421.8.5 Punctul de vedere local . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431.8.6 Congruent a semantica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4312 CUPRINS1.8.7 Problema programarii prin rescriere . . . . . . . . . . . . . . . . . . . . . . . . . . . 451.9 TIPURI ABSTRACTE de DATE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 451.9.1 Tipul abstract al numerelor naturale - continuare . . . . . . . . . . . . . . . . . . . . 452 RESCRIERI 492.1 TEORII DEDUCTIVE `A la MOISIL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492.2 LOGICA ECUAT IONALA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 502.2.1 Reguli de deduct ie, corectitudine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 502.2.2 Completitudine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 512.3 RESCRIERE LOCALA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 522.3.1 Preliminarii . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 522.3.2 Inchiderea la contexte . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 532.3.3 Inchiderea la preordini compatibile cu operat iile . . . . . . . . . . . . . . . . . . . . 542.3.4 rescriere . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 552.3.5 Corectitudinea rescrierii . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 572.4 Relat ia de ntalnire, Forme normale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 572.4.1 Conuent a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 572.4.2 Completitudinea ntalnirii prin recriere . . . . . . . . . . . . . . . . . . . . . . . . . . 582.4.3 Forme normale . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 582.4.4 Relat ii canonice . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 602.5 RESCRIERE IN SUBTERMENI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 612.5.1 Completitudinea