Unverified Commit ccf0b870 authored by Philip K.'s avatar Philip K. 🌝

termersetzung: wrote up initial draft

parent 7291164e
\section{Polynomordnungen \hfill 9 Punkte}
\section{Polynomordnungen und TES \hfill 9 Punkte}
Wir definieren ein Termersetzungssystem mit der Signatur $\Sigma$
bestehend aus einem unärem Operator $\ast(x)$ (geschrieben als
$x^{\ast}$) und einem binärem, infix Operator $x \vdash y$:
\begin{align}
(x \vdash y^\ast) \;&\rightarrow_{0}\; (x \vdash y)
\tag{1.1}\label{tes11}
\\
(x \vdash y) \vdash z \;&\rightarrow_{0}\; z \vdash (y \vdash x^\ast)
\tag{1.2}\label{tes12}
\\
x \vdash (y^\ast)^\ast \;&\rightarrow_{0}\; (x \vdash y^\ast) \vdash y
\tag{1.3}\label{tes13}
\end{align}
\begin{enumerate}
\item \points{3}
\item \points{3}
\item \points{3}
\item Zeigen \points{3} Sie, dass das TES nicht stark normalisierend
ist.
\item Gehen \points{3} sie im Folgenden davon aus, dass Regel (1.2)
entfernt wird. Zeigen Sie mithilfe von geeigneten Polynomordnungen,
dass das TES jetzt stark normalisierend ist.
\item Es \points{3} gibt nur ein einziges kritisches Paar. Bestimmen Sie
dieses und prüfen Sie, ob das TES konfluent ist.
\end{enumerate}
%%% Local Variables:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment