Nächste Seite:
Hausaufgaben
Aufwärts:
Abstrakte Reduktionssysteme (ARS)
Vorherige Seite:
Bezeichnungen (Eigenschaften v. Elementen)
Bezeichnungen (Eigenschaften v. Relationen)
ist
terminierend
(SN):
∀
x
∈
U
:
SN
(
x
)
ist
normalisierend
(WN):
∀
x
∈
U
:
WN
(
x
)
hat
eindeutige Normalformen
(UN): für alle Normalformen
y
1
,
y
2
gilt:
y
1
(←∪→)
*
y
2
y
1
=
y
2
hat
eindeutige NF für Reduktion
(UNR): für alle
x
, alle Normalformen
y
1
,
y
2
gilt:
y
1
←
*
x
→
*
y
2
y
1
=
y
2
DP:
∀
x
∈
U
:
DP
(
x
)
, äquiv.:
←
o
→ ⊆ →
o
←
lokal konfluent
(WCR):
∀
x
∈
U
:
WCR
(
x
)
äquivalente Spezifikation:
←
o
→ ⊆ →
*
o
←
*
konfluent
(CR): jedes
x
∈
U
ist konfluent
äquivalente Spezifikation:
←
*
o
→
*
⊆ →
*
o
←
*
Church-Rosser
(CR), wenn
(←∪→)
*
⊆ →
*
o
←
*
konvergent
, wenn
→
terminierend und konfluent ist
y1 = y2
y1 = y2