Korrektheit Sequentieller Systeme

Alle volgenden Sysmbole müssen eindeutig zuordbar sein $\Leftrightarrow$ alle Mengen sind disjunkt. Bei $\subset$ ist die gleichheit nicht ausgeschlossen

Sorten

$S=\left(s_{1},\ldots,s_{n}\right)$ wie Liste von Datentypen

Signatur

$\Sigma=\left(\Sigma_{ws}\right)_{ws\in S^{*}S}$ Angabe über Fuktionssymbole mit dazugehörigen Stelligkeiten und Sorten.
0-stellig $=$ Konstante

Variablensymbole

$\mathcal{V}=\left(\mathcal{V}_{s}\right)_{s\in S}$

• $\mathcal{V}\left(\phi\right)$ Menge aller Variablen Symbole in $\phi$
• $\mathcal{V}_{f}\left(\phi\right)\subset\mathcal{V}\left(\phi\right)$ Menge aller freien Variablen Symbole in $\phi$, also die nicht abquantifizierten

Terme

$\mathcal{T}\left(\Sigma,\mathcal{V}\right)\subset\left(\mathcal{V}\cup\Sigma\right)^{*}$ Menge der syntaktisch korrekten Terme aus den angegebenen Funktionen und Variablen

Grundterme

$\mathcal{T}\left(\Sigma\right)$ Terme ohne Variablen

sensible

Signatur hat von jeder Sorte mindestens ein Konstantensymbol

$\Sigma$-Algebra

ist paar $A=\left(\mathcal{A},\alpha\right)$ mit

Trägermengen

$\mathcal{A}=\left(\mathcal{A}_{s}\right)_{s\in S}$

Deutungsfunktionen

$\alpha=\left(\alpha_{f}\right)_{f\in\Sigma}$ die Signatur von $f$ respektiert

Deutung

$A:\mathcal{T}\left(\Sigma\right)\rightarrow_{S}\mathcal{A}$ bei gegebener $\Sigma$-Algebra $A$

Formeln

$\mathcal{F}\left(\Sigma,\mathcal{V}\right)\subset\left(\mathcal{V}\cup\Sigma\cup\left\{ \equiv,\neg,\wedge,\forall\right\} \right)^{*}$

• Sprache wird auch um andere gewohnte boolsche Operatoren erweitert
• $\mathcal{F}_{g}$ Menge der geschlossenen Formeln, enthalten keine freien Variablen

Atomare Formeln

$\mathcal{AT}\left(\Sigma,\mathcal{V}\right)\ni t_{1}\equiv t_{2}$ mit $t_{1},t_{2}\in\mathcal{T}\left(\Sigma,\mathcal{V}\right)$

pränexe Normalform

ist eine Formel $\phi$ wenn alle Quantoren $\left(\forall,\exists\right)$ ganz links stehen.

universelle Formeln

wenn pränex und alle Quantoren $\forall$
$\mathcal{F}_{\forall}\left(\Sigma,\mathcal{V}\right)$ ist Menge aller solcher Formeln über geg. Signatur

Gleichung

siehe Atomate Formel $\mathcal{E}\left(\Sigma,\mathcal{V}\right)=\mathcal{AT}\left(\Sigma,\mathcal{V}\right)$

universelle Gleichung

universelle Formel, die hinter den Quantoren nur nich genau ein $=$ steht
$\mathcal{E}_{\forall}\left(\Sigma,\mathcal{V}\right)$ ist die Menge aller solcher universelller Geichungen

Allabschluss

für ein $e\in\mathcal{E}\left(\Sigma,\mathcal{V}\right)$ ist $\forall e$ die Gleichung, in der alle freien Variablen abquantifiziert wurden. Analog für Formelmengen.

$\Sigma$-Interpretation

ist ein Paar $I=\left(A,\mathfrak{a}\right)$ mit der $\Sigma$-Algebra $A$ und $\mathfrak{a}:\mathcal{V}\rightarrow_{S}\mathcal{A}$.

Deutung

von Formel: $\alpha$ auf Funktionen und $\mathfrak{a}$ auf Variablen rekursiv anwenden. Atomare Formeln liefern bool. Dieses mit Boolschen Funktionen verknüpfen.
$I\models_{Alg\left(\Sigma\right)}\phi$ $\Leftrightarrow$ die $\Sigma$-Interpretation $I$ erfüllt eine Formel $\phi\in\mathcal{F}\left(\Sigma,\mathcal{V}\right)$ gdw. die Auswertung true liefert.

erfüllbar

ist $\phi$ gdw. es einer $\Sigma$-Interpreation $I$ gibt die Formel $\phi$ erfüllt

allgemeingültig

ist $\phi$ gdw. jede $\Sigma$-Interpreation $I$ die Formel $\phi$ erfüllt

folgt

$\Phi\models_{\mathcal{F}\left(\Sigma,\mathcal{V}\right)}\phi$ $\Leftrightarrow$ eine Formel $\phi$ folgt aus einer Formelmenge $\Phi$, gdw. alle Interpretationen die $\Phi$ wahr machen, auch $\phi$ wahr machen.

Folgerungen

$\Phi^{\models\mathcal{F}\left(\Sigma,\mathcal{V}\right)}$ ist die Menge aller Folgerungen aus $\Phi$

allgemeingültig

wenn $\emptyset\models_{\mathcal{F}\left(\Sigma,\mathcal{V}\right)}\phi$

äquivalent

$\phi_{1}\approx\phi_{2}$ gdw. $\phi_{1}\leftrightarrow\phi_{2}$ allgeimeingültig

Theorie

$Th\left(A\right):=\left\{ \phi\in\mathcal{F}_{g}\left(\Sigma,\mathcal{V}\right)\vert A\models\phi\right\}$ zu gegebener $\Sigma$-Algebra $A$

• ist angeschlossen und vollständig $\phi$ oder $\neg\phi$sind (nicht)enthalten in $Th\left(A\right)$
• $Th\left(A\right)\subset Th\left(B\right)\Rightarrow Th\left(A\right)=Th\left(B\right)$

Substitution

$\sigma:\mathcal{V}\rightarrow_{S}\mathcal{T}\left(\Sigma,\mathcal{V}\right)$

• rekursiv erweitern für gesamte Terme

Grundsubstitution

$\sigma\left(x\right)\in\mathcal{T}\left(\Sigma,\mathcal{V}\right)\cap\left\{ x\right\}$ für alle $x\in\mathcal{V}$

Substitutionlemma

$\mathfrak{a}\left(\sigma\left(t\right)\right)=\mathfrak{a}\left[x_{1}/\mathfra... ...t(t_{1}\right),\ldots,x_{n}/\mathfrak{a}\left(t_{n}\right)\right]\left(t\right)$

• $A\models\forall l\equiv r\Rightarrow A\models\sigma\left(l\right)\equiv\sigma\left(r\right)$ für bel. Substitution $\sigma$

Klasse der $\Sigma$-Algebren

$\textrm{Alg}_{\Sigma}$

• Für $\Phi\subset\mathcal{F}_{g}\left(\Sigma,\mathcal{V}\right)$ ist $\textrm{Mod}_{\Sigma}\left(\Phi\right)\subset\textrm{Alg}_{\Sigma}$ die Klasse aller $\Sigma$-Algebren $A$ mit $A\models\Phi$

$\Sigma$-Homomorphismus

Für $A,B$ $\Sigma$-Algebren ist $h:\mathcal{A}\rightarrow_{S}\mathcal{B}$ ein Homomorphismus wenn

$$h_{s}\left(\alpha_{f}\left(a_{1},\ldots,a_{n}\right)\right)=\beta_{f}\left(h_{s_{1}}\left(a_{1}\right),\ldots,h_{s_{n}}\left(a_{n}\right)\right)$$

• $id^{A}:A\rightarrow A$ ist Homomorphismus
• Verkettung von Homomorphismen ist wieder Homomorphismus
• $h\left(A\left(t\right)\right)=B\left(t\right)$ für alle $t\in\mathcal{T}\left(\Sigma\right)$

Äquivalenzrelation

ist $\sim\in M\times M$ wenn

reflexiv

$m\sim m$

symmetrisch

$m\sim n\Leftrightarrow n\sim m$

transitiv

$m\sim n\wedge n\sim k\Rightarrow m\sim k$

• Für Mengen $M,N$ und $f:M\rightarrow N$ ist $\sim_{F}$ definiert durch $m_{1}\sim_{F}m_{2}\Leftrightarrow F\left(m_{1}\right)=F\left(m_{2}\right)$ eine Äquivalenzrelation
• Äquivalenzklassen sind disjunkte Zerlegung der Gesamtmenge

Äquivalenzklasse

$\left[m\right]_{\sim}=\left\{ n\in M\vert n\sim m\right\} \subset2^{M}$

Quotientenmenge

$M/_{\sim}=\left\{ \left[m\right]_{\sim}\in2^{M}\vert m\in M\right\}$

$\Sigma$-Isomorphismus

ist eine bijektiver Homomorphismus

• $A\simeq_{\Sigma}B$ sind zwei $\Sigma$-Algebren, wenn ein isomorphismus zwischen ihnen exisitert
• $\simeq_{\Sigma}$ ist Äquivalenzrelation
• Isomorphe Algebren haben gleiche Theorie

Abstrakter Datentyp

für eine Signatur $\Sigma$ ist eine Klasse $\textrm{C}\subset\textrm{Alg}_{\Sigma}$ von $\Sigma$-Algebren, die unter Isomorphie abgeschlossen ist, d.h. es gilt für alle $A,B\in\textrm{Alg}_{\Sigma}$

• $A\in\textrm{C}\Rightarrow\left(A\simeq_{\Sigma}B\Rightarrow B\in\textrm{C}\right)$

  monomorph

  <#1162#>heißt $C$ falls $A\in\textrm{C}\Rightarrow\left(B\in\textrm{C}\Rightarrow A\simeq_{\Sigma}B\right)$

  polymorph

  andernfalls

initial

ist eine $\Sigma$-Algebra $A\in\textrm{Alg}_{\Sigma}$ gdw. gilt: Für jede $\Sigma$-Algebra $B$ existiert genau ein $\Sigma$-Homomorphismus von $A$ nach $B$.

• gilt $A\simeq_{\Sigma}B$ ist auch $B$ initial

Termalgebren

Sei $\Sigma$ eine Signatur bzgl. einer Sortenmenge $S$. Dann ist die Termalgebra $T_{\Sigma}=\left(\mathcal{T}\left(\Sigma\right),\tau\right)$ definiert durch

$$\tau_{f}\left(t_{1},\ldots,t_{n}\right):=ft_{1}\ldots t_{n}$$

• Diese Termalgebra ist inital in der Klasse aller $\Sigma$-Algebren

Kongruenzrelation

ist $\approx\subset\left(\mathcal{A}_{s}\times\mathcal{A}_{s}\right)_{s\in S}$ wenn:

• $\approx_{s}$ ist Äquivalenzrelation
• Kongruenzeigenschaft
  $a_{1}\approx_{s_{1}}a_{1}'\wedge\ldots\wedge a_{n}\approx_{s_{n}}a_{n}'\Righta... ...a_{1},\ldots,a_{n}\right)\approx_{s}\alpha_{f}\left(a_{1}',\ldots,a_{n}'\right)$

  Kongruenzklasse

  $\left[a\right]_{\approx_{s}}$ analog Äquivalenzklasse

  Quotientenmenge

  $\mathcal{A}_{s}/_{\approx_{s}}$ analog $\ldots$

Quotientenalgebra

ist eine $\Sigma$-Algebra zu gegebenen $A$ und $\approx$: $A/_{\approx}:=\left(\mathcal{A}/_{\approx},\tilde{\tilde{\alpha}}\right)$ mit

$$\tilde{\tilde{\alpha}}_{f}\left(\left[a_{1}\right]_{\approx_{s_{1... ...}}\right):=\left[\alpha_{f}\left(a_{1},\ldots,a_{n}\right)\right]_{\approx_{s}}$$

Quotiententermalgebra

Für eine $\Sigma$-Algebra $A$ sei $\approx_{A}\subset\mathcal{T}\left(\Sigma\right)\times\mathcal{T}\left(\Sigma\right)$ für alle $t_{1},t_{2}\in\mathcal{T}\left(\Sigma\right)$ definiert durch

$$t_{1}\approx_{A}t_{2}\Leftrightarrow A\left(t_{1}\right)=A\left(t_{2}\right)$$

die Quotiententermalgebra von $A$ ist dann definiert als $T_{\Sigma}/_{\approx_{A}}=\left(\mathcal{T}\left(\Sigma\right)/_{\approx_{A}},{{\approx_{A}\atop \tau}}\right)$

• Für Variablenbelegung $\mathfrak{t}$ und Term $t$ gilt $\mathfrak{t}\left(t\right)=\left[t\right]_{\approx_{A}}$

kanonische Termalgebra

heißt $A\left(\mathcal{A},\alpha\right)$ gdw.: $\mathcal{A}\subset\mathcal{T}\left(\Sigma\right)$ und $\forall t\in A:A\left(t\right)=t$

Teilsignatur

ist eine Signatur, bei der einige Funktionssymbole weggleassen wurden

Erzeugte $\Sigma$-Algebra

Seien $\Sigma^{c}$ und $\Sigma$ $S$-Signaturen mit $\Sigma^{c}\subset\Sigma$ und sei $A=\left(\mathcal{A},\alpha\right)$ eine $\Sigma$-Algebra. Dann ist $A$ durch $\Sigma^{c}$ erzeugt gdw. gilt: $\forall s\in S,a\in\mathcal{A}_{s}:\exists q\in\mathcal{T}\left(\Sigma_{s}^{c}\right):a=A\left(q\right)$

• bei erzeugter Algebra sind alle Trägermengen abzählbar
• $A$ initial $\Rightarrow$ $A$ erzeugt
• $A$ erzeugt $\Rightarrow$ $A\simeq_{\Sigma}T_{\Sigma}/_{\approx_{A}}$
• Sei $h:A\rightarrow B$ Homomorphismus ist eindeutig, falls $A$ erzeugt
• erzeugte Algebren mit gleicher Theorie sind isomorph

frei

erzeugt wenn zusätzlich gilt $\forall s\in S,q_{1},q_{2}\in\mathcal{T}\left(\Sigma_{s}^{c}\right):A\left(q_{1}\right)=A\left(q_{2}\right)\Rightarrow q_{1}=q_{2}$
$\textrm{Gen}_{\Sigma}\subset\textrm{Alg}_{\Sigma}$ bezeichnet die Klasse aller erzeugten $\Sigma$-Algebren

• (frei) erzeugtheit vererbt sich durch Isomorphie und Quotiententermalgebra bildung
• alle Konstruktoren werden als injektive Funktionen gedeutet
• Es existiert eine isomorphe kanonische Termalgebra $T_{A}$ zu $A$

Redukt

ist Reduzierte Algebra zu kleinerer Signatur

• $A$ durch $\Sigma^{c}\subset\Sigma$ erzeugt und sei $A^{c}$ das $\Sigma^{c}$ Redukt von $A$
  $A$ freu erzeugt durch $\Sigma^{c}\Leftrightarrow A^{c}\simeq_{\Sigma^{c}}T_{\Sigma^{c}}$

Expansion

ist vollständige Algebra zu großer Signatur

Kongruenz aus Relation

Sei $A$ eine $\Sigma$-Algebra, und $R=\subset\left(\mathcal{A}_{s}\times\mathcal{A}_{s}\right)$. Es existiert eine kleinste Kongruenzrelation $\approx_{R}$ die $R$ noch enthält

Kongruenz aus Gleichung

Für $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$ ist

$$R_{E}: = \left\{ \left(\theta\left(l\right),\theta\left(r\right)\right)\in\mathcal{T}\left(\Sigma\right)\times\mathcal{T}\left(\Sigma\right)\vert\right.$$

$$\left.l\equiv r\in E\wedge\theta\textrm{ ist Substitution}\right\}$$

und $\approx_{E}:=\approx_{R_{E}}$

• Für alle $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$gilt $T_{\Sigma}/_{\approx_{E}}\models\forall E$
• Sei $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right).$Dann ist $T_{\Sigma}/_{\approx_{E}}$ initial in $\textrm{Mod}_{\Sigma}\left(\forall E\right)$

Vorgehen

Gegeben sei $S$, $\Sigma^{c}\subset\Sigma$ und $E\subset\mathcal{E}\left(\Sigma,\mathcal{V}\right)$, so dass $T_{\Sigma/_{\approx_{E}}}$ eine durch $\Sigma^{c}$ freu erzeugte Quotiententermalgebra ist.

• Wir erweitern $S$ zu $S'$, $\Sigma^{c}$ zu $\Sigma^{c'}$, $\Sigma^{d}$ zu $\Sigma^{d'}$und $E$ zu $E'\subset\mathcal{E}'\left(\Sigma',\mathcal{V}\right)$
• Wir benötigen Gleichungen nur, wenn wir $\Sigma^{d}$ um ein neues Funktionssymbol $f$ zu $\Sigma^{d'}$ erweitern.
• <#1257#>Solch eine Gleichungsmenge $E'\backslash E$ muß garantieren, daß $T_{\Sigma'}/_{\approx_{E'}}$ durch $\Sigma^{c}$ frei erzeugt ist, d.h. für alle $q_{i}\in\mathcal{T}\left(\Sigma^{c}\right)$ein $q\in\mathcal{T}\left(\Sigma^{c}\right)$mit
  $$T_{\Sigma'}/_{\approx_{E'}}\left(fq_{1}\ldots q_{n}\right)\in\left[q\right]_{\approx_{E'}}$$
  existiert und für alle $q\in\mathcal{T}\left(\Sigma^{c}\right)$
  $$\mathcal{T}\left(\Sigma^{c}\right)\cap\left[q\right]_{\approx_{E'}}=\left\{ q\right\}$$
  gilt. Wir nennen solche Gleichungsmengen $E'\backslash E$ zulässig.
• ${{E\atop \tau}}_{f}\left(q_{1},\ldots,q_{n}\right):=q$ gdw. ${{\approx_{E}\atop \tau}}_{f}\left(\left[q_{1}\right]_{\approx_{E}},\ldots,\left[q_{n}\right]_{\approx_{E}}\right)=\left[q\right]_{\approx_{E}}$ definiert eine frei erzeugte kanonische Termalgebra $T_{\Sigma,E}=\left(\mathcal{T}\left(\Sigma^{c}\right),{{E\atop \tau}}\right)$ für die gilt $T_{\Sigma,E}\simeq_{\Sigma}T_{\Sigma}/_{\approx_{E}}$

structure

struct <= $cons_{1}\left(sel_{1,1}:sct_{1,1},\ldots,sel_{1,n_{1}}:sct_{1,n_{1}}\right),\ldots$

• $sct_{i,h}\in\left(S\backslash\left\{ bool\right\} \right)\cup\left\{ struct\right\}$ für alle $i\in\left\{ 1,\ldots,k\right\}$ und alle $h\in\left\{ 1,\ldots,n_{i}\right\}$. ( $sct=struct$)
• $n_{i}\ge0$ für alle $\left\{ 1,\ldots,k\right\}$
• Anzahl der Konstruktoren: $k\ge1$

Axiome

$EQ_{struct}$

• Gleichheit von Konstanten $eq_{struct}\left(cons_{i},cons_{i}\right)\equiv true$
• Gleichheit von längeren Konstruktoren (geschachtelt, allquantifiziert) $eq_{struct}\left(cons_{i}\left(\ldots\right),cons_{i}\left(\ldots\right)\right)\equiv eq\left(eq\left(\ldots\right)\right)$
• Nichgleichheit bei führenden Konstruktoren $eq_{struct}\left(cons_{i}\left(\ldots\right),cons_{j}\left(\ldots\right)\right)\equiv false$
• Falsch angewendete Selektoren liefern Beispielterm (Konstante)
• Selektoren $\forall x_{1}:struct_{i,1}\ldots.sel_{i,h}\left(cons_{i}\left(\ldots\right)\right)\equiv x_{h}$
• $if_{struct}\left(true,x,y\right)\equiv x$
  $if_{struct}\left(false,x,y\right)\equiv y$

function

$proc\left(x_{1}:struct_{1},\ldots,x_{k}:struct_{k}\right):struct<=R_{proc}$

• $x_{i}$ Parameter vom Typ $struct_{i}$
• name $Proc$ und Rückgabe vom Typ $struct$
• $R_{proc}$ ist Rumpf und muss sich zu $struct$ auswerten lassen

konstruktive Spec.

$S$ ist eine Folge $\left\langle D_{0},\ldots,D_{n}\right\rangle$ von Datenstruktur- und Prozedurdefinitionen.

• $S\left(0\right)=\left\{ bool\right\}$, $\Sigma\left(0\right)_{bool}^{c}=\left\{ true,false\right\}$, $\Sigma\left(0\right)_{bool,bool,bool,bool}^{c}=\left\{ if_{bool}\right\}$
• $S,\Sigma^{c},\Sigma^{d},E,\mathcal{V}$ sind Funktionen von $i$ $\rightarrow$ nummer der konstruktionsiteration
• $\left\langle D_{0},\ldots,D_{n}\right\rangle \oplus D=\left\langle D_{0},\ldots,D_{n},D\right\rangle$

zulässige Spec.

Eine Konstruktive Spezifikation $S=\left\langle D_{0},\ldots,D_{n}\right\rangle$ ist zulässig, gdw. die $\Sigma\left(n\right)$-Algebra $T_{\Sigma\left(n\right)}/_{\approx_{E_{n}}}$ frei erzeugt durch $\Sigma\left(n\right)^{c}$ ist

• Datenstrukturdefinitionen sind automatisch zulässig in Verifun

prozedur Relation

für gegebenes $proc$ ist

$$>_{proc}\subset\left(\mathcal{T}\left(\Sigma^{c}\right)_{struct_{1}}\times\ldots\times\mathcal{T}\left(\Sigma^{c}\right)_{struct_{n}}\right)^{2}$$

$\left(q_{1},\ldots,q_{n}\right)>_{proc}\left(q_{1}',\ldots,q_{n}'\right)$ gdw. beim Aufruf von $proc\left(q_{1},\ldots,q_{n}\right)$ wird $proc\left(q_{1}',\ldots,q_{n}'\right)$ rekursiv aufgerufen

• Eine Prozedur terminiert und damit ist ihre Definition zulässig, gdw. $>_{proc}$ fundiert ist.

Fundierte Relation

Eine Relation $\succ\subset M\times M$ heißt fundiert gdw. es gibt keine unendliche Folgen $m_{0},m_{1},\ldots$ mit $m_{i}\succ m_{i+1}$ für alle $i\in\mathbb{N}$