Term algebra

I universell algebra och matematisk logik är en termalgebra en fritt genererad algebraisk struktur över en given signatur . Till exempel, i en signatur som består av en enda binär operation , är termen algebra över en uppsättning X av variabler exakt den fria magma som genereras av X . Andra synonymer för begreppet inkluderar absolut fri algebra och anarkisk algebra .

Ur ett kategoriteoretiskt perspektiv är en termalgebra det initiala objektet för kategorin av alla X -genererade algebror av samma signatur , och detta objekt, unikt upp till isomorfism , kallas en initial algebra ; den genererar genom homomorf projektion alla algebror i kategorin.

En liknande uppfattning är den om ett Herbrand-universum i logik , som vanligtvis används under detta namn i logikprogrammering , som är (absolut fritt) definierat med början från uppsättningen konstanter och funktionssymboler i en uppsättning satser . Det vill säga, Herbrands universum består av alla grundtermer : termer som inte har några variabler i sig.

En atomformel eller atom definieras vanligtvis som ett predikat som tillämpas på en tupel av termer; en jordatom är då ett predikat där endast jordtermer förekommer. Herbrandbasen är uppsättningen av alla markatomer som kan bildas från predikatsymboler i den ursprungliga uppsättningen av satser och termer i dess Herbrand-universum . Dessa två koncept är uppkallade efter Jacques Herbrand .

Termalgebror spelar också en roll i semantiken för abstrakta datatyper , där en abstrakt datatypdeklaration ger signaturen för en multisorterad algebraisk struktur och termen algebra är en konkret modell av den abstrakta deklarationen.

Universal algebra

En typ $\tau$ är en uppsättning funktionssymboler, där var och en har en tillhörande aritet (dvs. antal ingångar). För alla icke-negativa heltal $n$ , låt $\tau _{n}$ beteckna funktionssymbolerna i $\tau$ av arity $n$ . En konstant är en funktionssymbol för arity 0.

Låt $\tau$ vara en typ, och låt $X$ vara en icke-tom uppsättning symboler som representerar variabelsymbolerna. (För enkelhetens skull, antag att $X$ och $\tau$ är disjunkta.) Sedan går termuppsättningen T displaystyle $T(X)}$ av typen $\tau$ över $X$ är mängden av alla välformade strängar som kan konstrueras med hjälp av variabelsymbolerna för $X$ och konstanterna och operationerna för $\tau$ . Formellt $T(X)$ den minsta mängden så att:

• $X\cup \tau _{0}\subseteq T(X)$ — varje variabelsymbol från $X$ är en term i $T (X)$ , och så är varje konstant symbol från $\tau _{0}$ .
• För alla $n\geq 1$ och för alla funktionssymboler $f\in \tau _{n}$ och termer $t_{1},...,t_{n}\i T(X)$ , vi har strängen $f(t_{1},...,t_{n})\in T(X)$ — givet $n$ termer $t_{1},...,t_{n}$ , tillämpningen av en $n$ -är funktionssymbol $f$ på dem representerar återigen en term.

Termen algebra ${\mathcal {T}}(X)$ av typen $\tau$ över $X$ är, sammanfattningsvis, algebra av typen $\tau$ som mappar varje uttryck till dess strängrepresentation. Formellt definieras ${\displaystyle {\mathcal {T}}(X)} enligt följande:$

• Domänen för ${\mathcal {T}}(X)$ är $T(X)$ .
• För varje nullär funktion $f$ i $\tau _{0}$ , $f^{{\mathcal {T}}(X)}()$ definieras som strängen $f$ .
• För alla $n\geq 1$ och för varje n -är funktion $f$ i $\tau$ och element $t_{1},...,t_{n}$ i domänen, $f^{{\mathcal { T}}(X)}(t_{1},...,t_{n})$ definieras som strängen $f(t_{1}, ...,t_{n})$ .

En term algebra kallas absolut fri eftersom för alla algebra ${\mathcal {A}}$ av typen $\tau$ , och för alla funktioner $g:X\to {\mathcal {A}}$ , $g$ sträcker sig till en unik homomorfism $g^{\ast }:{\mathcal {T}}(X)\ till {\mathcal {A}}$ , som helt enkelt utvärderar varje term $t\in {\mathcal {T}}(X)$ till dess motsvarande värde ${ \displaystyle g^{\ast }(t)\in {\mathcal {A}}}$ . Formellt, för varje $t\in {\mathcal {T}}(X)$ :

• Om $t\in X$ , då $g^{\ast }(t)=g(t)$ .
• Om $t=f\in \tau _{0}$ , då $g^{\ast }(t)=f^{\ mathcal {A}}()$ .
• Om $t=f(t_{1},...,t_{n})$ där $f\in \tau _{n}$ och $n\geq 1$ , sedan $g ^{\ast }(t)=f^{\mathcal {A}}(g^{\ast}(t_{1}),...,g^{\ast }(t_{n}))$ .

Exempel

Som ett exempel kan typ inspirerad från heltalsaritmetik definieras av $\tau _{0}=\{0,1\}$ , $\tau _{1 }=\{\}$ , $\tau _{2}=\{+,*\}$ och $\tau _{i} =\{\}$ för varje $i>2$ .

Den mest kända algebra av typen $\tau$ har de naturliga talen som sin domän och tolkar $0$ , $1$ , $+$ och $*$ på vanligt sätt; vi hänvisar till det som ${\mathcal {A}}_{nat}$ .

För exempelvariabelmängden $X=\{x,y\}$ , ska vi undersöka termen algebra ${\mathcal {T}}(X )$ av typen $\tau$ över $X$ .

betraktas uppsättningen $T(X)$ av termer av typen $\tau$ över ${\displaystyle X} .$ Vi använder röd färg för att flagga dess medlemmar, som annars kan vara svåra att känna igen på grund av deras ovanliga syntaktiska form. Vi har tex

• ${\color {red}x}\in T(X)$ , eftersom $x\in X$ är en variabelsymbol;
• ${\color {red}1}\in T(X)$ , eftersom $1\in \tau _{0}$ är en konstant symbol; därav
• ${\color {red}+x1}\in T(X)$ , eftersom $+$ är en 2-är funktionssymbol; alltså i sin tur
• ${\color {red}*+x1x}\in T(X)$ eftersom $*$ är en 2-är funktionssymbol.

motsvarar varje sträng i ${\displaystyle T(X)} ett$ matematiskt uttryck byggt från de tillåtna symbolerna och skrivet med polsk prefixnotation ; till exempel, termen ${\color {red}*+x1x}$ motsvarar uttrycket $(x+1)*x$ i vanlig infixnotation . Inga parenteser behövs för att undvika oklarheter i polsk notation; t.ex. infixuttrycket $x+(1*x)$ motsvarar termen ${\color {red}+x*1x}$ .

För att ge några motexempel har vi t.ex

• ${\displaystyle {\color {red}z}\not \in T(X)} ,$ eftersom $z$ varken är en tillåten variabelsymbol eller en tillåten konstantsymbol;
• ${\displaystyle {\color {red}3}\inte \in T(X)} ,$ av samma anledning,
• ${\displaystyle {\color {red}+1}\inte \in T(X)} ,$ eftersom $+$ är en 2-är funktionssymbol, men används här med endast en argumentterm (dvs. ${\color {röd}1}$ ).

Nu när termmängden $T(X)$ är etablerad, betraktar vi termen algebra ${\mathcal {T}}(X)$ av typen $\ tau$ över $X$ . Denna algebra använder $T(X)$ som sin domän, där addition och multiplikation måste definieras. Adderingsfunktionen $+^{{\mathcal {T}}(X)}$ tar två termer $p$ och $q$ och returnerar termen ${ \displaystyle {\color {röd}+}pq}$ ; på liknande sätt mappar multiplikationsfunktionen $*^{{\mathcal {T}}(X)}$ givna termer $p$ och $q$ till termen ${\color {röd}*}pq$ . Till exempel, $*^{{\mathcal {T}}(X)}({\color {red}+x1},{\color {red}x })$ motsvarar termen ${\color {red}*+x1x}$ .

Som ett exempel på unik förlängbarhet av en homomorfism, betrakta $g:X\to {\mathcal {A}}_{nat}$ definierad av $g (x)=7$ och $g(y)=3$ . Informellt $g$ en tilldelning av värden till variabelsymboler, och när detta är gjort kan varje term från $T(X)$ utvärderas på ett unikt sätt i ${\mathcal {A}}_{nat}$ . Till exempel,

${\begin{array}{lll}&g^{*}({ \color {röd}+x1})\\=&g^{*}({\color {röd}x})+g^{*}({\color {röd}1})&{\text{ sedan } }g^{*}{\text{ är en homomorfism }}\\=&g({\color {röd}x})+g^{*}({\color {röd}1})&{\text{ eftersom }}g^{*}{\text{ sammanfaller på }}X{\text{ med }}g\\=&7+g^{*}({\color {röd}1})&{\text{ definition av }}g\\=&7+1&{\text{ eftersom }}g^{*}{\text{ är en homomorfism }}\\=&8&{\text{ enligt de välkända räknereglerna i }}{\mathcal {A}}_{nat}\\\end{array}}$

På liknande sätt får man $g^{*}({\color {röd}*+x1x})=...=8*g({\color {röd}x})=...=56$ .

Herbrand bas

Huvudartiklar: Herbrand tolkning och Herbrand struktur

Signaturen σ för ett språk är en trippel < O , F , P > bestående av alfabetet av konstanterna O , funktionssymbolerna F och predikaten P . Herbrandbasen för en signatur σ består av alla jordatomer av σ : av alla formler av formen R ( t ₁ , ..., t n ₎ , där t ₁ , ..., t _n är termer som inte innehåller några variabler ( dvs element i Herbrands universum) och R är en n -är relationssymbol ( dvs predikat ). I fallet med logik med likhet innehåller den även alla ekvationer av formen t ₁ = t ₂ , där t ₁ och t ₂ inte innehåller några variabler.

Beslutbarhet

Termalgebror kan visas som avgörbara med hjälp av kvantifierareliminering . Komplexiteten i beslutsproblemet ligger i INGENELEMENTÄRT eftersom binära konstruktorer är injektiva och därmed parfunktioner.

Se även

• Programmering med svarsuppsättning
• Klon (algebra)
• Diskursdomän / Universum (matematik)
• Rabins trädsats (den monadiska teorin om det oändliga fullständiga binära trädet kan avgöras)
• Initial algebra
• Abstrakt datatyp
• Termomskrivningssystem

Vidare läsning

• Joel Berman (2005). "Strukturen av fria algebror" . I strukturell teori om automater, semigrupper och universell algebra . Springer . s. 47–76. MR 2210125 .

externa länkar

• Weisstein, Eric W. "Herbrand Universe" . MathWorld .