Přepisující systémy - NALG011

• Anglický název: Term Rewriting Systems
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2018
• Semestr: zimní
• E-Kredity: 6
• Rozsah, examinace: zimní s.:2/0, --- [HT]; letní s.:2/0, Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: zrušen
• Jazyk výuky: čeština
• Způsob výuky: prezenční
• Kategorizace předmětu: Informatika > Teoretická informatika; Matematika > Algebra
• Korekvizity : NALG103

Anotace

čeština

Otázka zní: Nalézt efektivní způsob umožňující libovolný výraz daného jazyka přepsat do normální formy ekvivalentní s původním výrazem vzhledem k zadané soustavě identit. Odpovědí je přepisující systém. Základy teorie v rámci teorie grafů.

Poslední úprava: ()

angličtina

The question is: To find an efficient way enabling to rewrite an expression in a given language into a normal form, equivalent with the original expression with respect to a given list of identities. The answer is a term rewrite system.

Poslední úprava: T_KA (25.05.2001)

Literatura

N. Dershowitz, J.-P. Jouannaud: Rewrite systems. Chapter 6, 243--320 in J.~van Leeuwen, ed., Handbook of Theoretical Computer Science, B: Formal Methods and Semantics. North Holland, Amsterdam 1990

Poslední úprava: Zakouřil Pavel, RNDr., Ph.D. (05.08.2002)

Sylabus

čeština

A. Zimní semestr:.

1. Základy rovnicové logiky.

2. Konvergence v grafech.

3. Unifikace termů.

4. Kritické dvojice pro přepisující systém.

5. Knuth-Bendixův algoritmus.

B. Letní semestr:.

1. Teorie dobrých kvaziuspořádání.

2. Simplifikační kvaziuspořádání a jeho význam pro termínovanost.

3. Knuth-Bendixovo kvaziuspořádání.

4. Příklad: přepisující systém pro rovnicovou teorii grup.

5. Dershowitzovo kvaziuspořádání.

6. Perfektní baze rovnicových teorií.

Poslední úprava: ()

angličtina

A. Winter semester:

1. Foundations of equational logiic.

2. Convergence in graphs.

3. Unification of terms.

4. Critical pairs for term rewrite systems.

5. Knuth-Bendux algorithm.

B. Summer semester:

1. Theory of well quasiorders.

2. Simplification quasiordering and its i,portance for termination.

3. Knuth-Bendix quasiorders.

4. Example: Term rewrite system for the equational theory of groups.

5. Dershowitz quasiorders.

6. Perfect bases of equational theories.

Poslední úprava: T_KA (26.04.2004)