Termalgebra - Term algebra
I universell algebra og matematisk logikk er et begrep algebra en fritt generert algebraisk struktur over en gitt signatur . For eksempel i en signatur som består av en enkelt binær operasjon , begrepet algebra over et sett X er variabler nøyaktig den frie magma generert av X . Andre synonymer for begrepet inkluderer absolutt gratis algebra og anarkisk algebra .
Fra et kategoriteori- perspektiv er et begrep algebra det første objektet for kategorien av alle X- genererte algebraer med samme signatur , og dette objektet, unikt opp til isomorfisme , kalles en initial algebra ; det genererer ved homomorf projeksjon alle algebraer i kategorien.
En lignende forestilling er den om et Herbrand-univers i logikk , vanligvis brukt under dette navnet i logisk programmering , som er (absolutt fritt) definert med utgangspunkt i settet med konstanter og funksjonsymboler i et sett med ledd . Det vil si at Herbrand-universet består av alle grunntermer : termer som ikke har noen variabler.
En atomformel eller et atom er vanligvis definert som et predikat som brukes på en termeruttall; et jordatom er da et predikat der bare grunntermer vises. Den Herbrand basen er settet med alle jord atomer som kan dannes fra underliggende symboler i det opprinnelige sett av setninger og uttrykk i sin Herbrand universet. Disse to konseptene er oppkalt etter Jacques Herbrand .
Begrepsalgebraer spiller også en rolle i semantikken til abstrakte datatyper , hvor en abstrakt datatypedeklarasjon gir signaturen til en flersortert algebraisk struktur og begrepet algebra er en konkret modell av den abstrakte erklæringen.
Avgjørbarhet
Begrepet algebras kan vises avgjørende ved hjelp av kvantifiseringseliminering . Kompleksiteten i beslutningsproblemet er i NONELEMENTARY .
Herbrand-base
Den signatur σ fra et språk er en trippel < O , F , P > består av alfabetet konstanter O , funksjonssymbolene F , og predikater P . Den Herbrand bunnen av en signatur σ består av alle grunn atomer av σ : av alle formler av formen R ( t 1 , ..., t n ), hvor t 1 , ..., t n er ord inneholder ingen variabler (dvs. elementer av Herbrand-universet) og R er et n -ary forholdssymbol ( dvs. predikat ). Når det gjelder logikk med likhet, inneholder den også alle ligninger av formen t 1 = t 2 , der t 1 og t 2 ikke inneholder noen variabler.
Se også
- Svar-sett programmering
- Klon (algebra)
- Diskursområde / univers (matematikk)
- Rabins tresetning (monadeteorien om det uendelige komplette binære treet kan avgjøres)
- Innledende algebra
- Abstrakt datatype
Referanser
Videre lesning
- Joel Berman (2005). "Strukturen til frie algebraer" . I Structural Theory of Automata, Semigroups og Universal Algebra . Springer . s. 47-76. MR 2210125 .