Sistema di riduzione

Nella logica matematica e nell'informatica teorica , il termine sistema di riduzione , o sistema di riduzione astratto , o in breve ARS , sta per una generalizzazione dei sistemi di riscrittura dei termini . Nella sua forma più semplice, un ARS è un insieme di oggetti insieme a una relazione binaria , comunemente indicata come. Nonostante la sua semplicità, un ARS è sufficiente per descrivere importanti proprietà dei sistemi di riscrittura dei termini, come: B. forme normali , terminazione e vari concetti di confluenza . ${\ displaystyle \ rightarrow}$

Storicamente, ci sono state diverse astrazioni differenti della riscrittura dei termini, ognuna con le sue specifiche. La formalizzazione più usata oggi, che viene qui seguita, si basa sul lavoro di Gérard Huet (1980).

definizione

Un ARS è costituito da un insieme A , gli oggetti, insieme a una relazione binaria su A , solitamente indicata con. Questa relazione è chiamata relazione di riduzione o semplicemente riduzione .${\ displaystyle \ rightarrow}$

In quanto oggetto matematico, un ARS è lo stesso di un sistema di transizione non contrassegnato . Tuttavia, il focus e la terminologia differiscono in queste due aree: in un sistema di transizione si è interessati a interpretare i segni come azioni, mentre in un ARS il focus è su come gli oggetti vengono trasformati (ridotti) in altri.

esempio

L'insieme di oggetti è T = { a , b , c } e la relazione binaria → è definita come segue: → ; questo di solito è scritto come ${\ displaystyle = \ {(a, b), (b, a), (a, c), (b, c) \}}$

Se si legge questo come regole con cui gli elementi possono essere trasformati in altri, allora si vede che sia una e b possono essere trasformati (ridotti) in c . Apparentemente questa è una proprietà importante del sistema. In un certo senso, c è un oggetto "più semplice" nel sistema, poiché nessuna delle regole può essere applicata a c per trasformare ulteriormente questo elemento.

Termini di base

L'esempio sopra porta ad alcuni termini importanti nel contesto di un ARS.

• ${\ displaystyle {\ stackrel {*} {\ rightarrow}}}$è la shell transitiva di , dove = è l' identità ; d. H. è il più piccolo quasi-ordine ( relazione riflessiva e transitiva ) che contiene. È anche il guscio riflessivo e transitivo di .${\ displaystyle \ rightarrow \ cup =}$${\ displaystyle {\ stackrel {*} {\ rightarrow}}}$${\ displaystyle \ rightarrow}$${\ displaystyle \ rightarrow}$

• ${\ displaystyle \ leftrightarrow}$è , d. H. l'unione della relazione con la sua relazione inversa ; è anche chiamato inviluppo simmetrico di .${\ displaystyle \ rightarrow \ cup \ rightarrow ^ {- 1}}$${\ displaystyle \ rightarrow}$${\ displaystyle \ leftrightarrow}$${\ displaystyle \ rightarrow}$
• ${\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$è lo scafo transitivo di , i.e. H. è la più piccola relazione di equivalenza che contiene. È anche noto come inviluppo simmetrico transitivo riflessivo di .${\ displaystyle \ leftrightarrow \ cup =}$${\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$${\ displaystyle \ rightarrow}$${\ displaystyle \ rightarrow}$

Forme normali e parola problema

Un oggetto x in A si dice riducibile se c'è un oggetto y in A diverso da x con ; altrimenti si chiama irriducibile o forma normale . Un oggetto y è chiamato la forma normale di x se contiene e y è irriducibile. Se x ha una forma normale univoca , allora è indicata con. ${\ displaystyle x \ rightarrow y}$${\ displaystyle x {\ stackrel {*} {\ rightarrow}} y}$${\ displaystyle x \ downarrow}$

Nell'esempio sopra, c è una forma normale di a e b . Poiché un e b sono riducibili è c anche l'unica forma normale di questi elementi . Se ogni oggetto ha almeno una forma normale, l'ARS viene chiamato normalizzazione . ${\ Displaystyle c = a \ downarrow = b \ downarrow}$

Uno dei problemi importanti che possono essere formulati nel contesto di un ARS è la parola problema : dati x e y , questi due oggetti sono equivalenti sotto la relazione ? Questo è un quadro molto generale per la parola problema; così è z. B. la parola problema per i gruppi è un caso speciale del problema parola ARS. Il problema della parola è più facile da affrontare quando ci sono forme normali uniche: in questo caso, due oggetti con la stessa forma normale sono equivalenti sotto . La parola problema per un ARS è generalmente non decidibile . ${\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$${\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$

Per l'indagine sulla questione dell'esistenza di forme normali, i termini proprietà Church-Rosser e confluenza sono di fondamentale importanza.

gonfiarsi

• Franz Baader, Tobias Nipkow: Term Rewriting e tutto il resto. Cambridge University Press, 1998. Adatto ai principianti.
• Nachum Dershowitz e Jean-Pierre Jouannaud Rewrite Systems , Capitolo 6 in Jan van Leeuwen (a cura di), Manuale di informatica teorica. Volume B: Modelli formali e semantica. Elsevier / MIT Press, 1990, ISBN 0-444-88074-7 , pagg. 243-320.
• Ronald V. Book , Friedrich Otto: String rewriting systems. Springer, Berlino 1993. Capitolo 1: Sistemi di riduzione astratta. ISBN 0-387-97965-4 .
• Marc Bezem, JW Klop, Roel de Vrijer: sistemi di riscrittura dei termini. Cambridge University Press, 2003, ISBN 0-521-39115-6 , Capitolo 1. (Questa è un'ampia monografia).
• John Harrison: Manuale di logica pratica e ragionamento automatizzato. Cambridge University Press, 2009, ISBN 978-0-521-89957-4 , Capitolo 4: Uguaglianza.
• Gérard Huet: Riduzioni confluenti: proprietà astratte e applicazioni ai sistemi di riscrittura dei termini. In: Journal of the ACM (JACM), Vol.27, No.4, ottobre 1980, pp. 797-821.

Prove individuali

1. ↑ Ronald V. Book, Friedrich Otto: String rewriting systems. P. 9.
2. ↑ Ronald V. Book, Friedrich Otto: String rewriting systems. P. 10.
3. ↑ Marc Bezem, JW Klop, Roel de Vrijer: Sistemi di riscrittura dei termini. Pp. 7-8.
4. ^ Franz Baader, Tobias Nipkow: Term Rewriting and All That. Pp. 8-9.
5. ^ Franz Baader, Tobias Nipkow: Term Rewriting and All That. P. 11 f.