Sistemi di riscrittura

Presentazione
Riscrittura come computazione
Calcolo di un espressione:
Parte del corso
• Passo da un espressione all’altra.
dedicato alla presentazione dei sistemi di riscrittura di termini (term
rewriting system).
• Insieme finito di regole.
teoria alla base
• Non determinismo - confluenze.
• Riscrittura locale.
• programmazione funzionale,
• Terminazione risultato.
• logica,
Macchine di Turing.
• funzionale-logica,
Sistemi di riscrittura di Post.
• sistemi concorrenti.
Lambda calcolo.
Testo di riferimento Terese-Light.
Programmazione funzionale.
P. Di Gianantonio (Udine)
Rewriting Systems
1 / 111
P. Di Gianantonio (Udine)
Abstract reduction system
Rewriting Systems
2 / 111
ARS, notazione e definizioni
Trascuro la natura degli oggetti riscritti.
Guardo il grafo delle riduzioni.
a →α b:
Definizione
• a riduce a b in un passo di α-riduzione (computazione).,
[Abstract reduction system]
• b e` l’α ridotto in un passo di a,
• a e` l’α espansione in un passo di b.
A := (A , →)
Definizione
• sequenza di riduzione (finita o infinita)
• A insieme
• → relazione binaria su A
rappresenta il passo di riduzione.
a0 → a1 → . . . → an →
• a0 riduce a an , an e` il ridotto di a0 ,
In alcuni ambiti (concorrenza), si definisce un insieme di relazioni di
riduzione.
A := (A , {→α | α ∈ I})
Altro nome per questo concetto: label transition system (LTS)
P. Di Gianantonio (Udine)
Rewriting Systems
3 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
4 / 111
Proprieta` degli ARS: confluenza
ARS, relazioni derivate
Posso fare convergere ad un unico risultato riduzioni diverse.
Un ARS puo` essere visto come grafo orientato, eventualmente etichettato.
→+ chiusura transitiva di →
a →∗ b sse a riduce in n passi a b, con n > 0
→∗
Definizione
come grafo: esiste un cammino non vuoto da a a b
Un elemento a e` debolmente confluente, debolmente Church Rosser
(WCR)
∀b , c. b ← a → c implica che ∃d. b →∗ d ∗← c.
chiusura riflessiva e transitiva di →
per ogni a, a →∗ a.
∀b , c. b ∗← a →∗ c implica che ∃d. b →∗ d ∗← c.
Un elemento a e` confluente, Church Rosser (CR)
a = b chiusura simmetrica, riflessiva e transitiva di →
implicitamente: a → b allora considera a e b uguali,
come grafo: a e b appartengono alla stessa componente
connessa.
Un ARS si dice (debolmente) Church Rosser se lo sono tutti i suoi
elementi.
CR ci assicura che possiamo far confluire qualsiasi coppia di riduzioni.
WCR e` piu` semplice da verificare.
Notazione: L’Identita` sintattica si rappresenta con ≡
WCR e` una proprieta` strettamente piu` debole di CR. Controesempio: . . .
P. Di Gianantonio (Udine)
Rewriting Systems
5 / 111
P. Di Gianantonio (Udine)
Confluenza: esempi
Rewriting Systems
6 / 111
Varie nozioni di confluenza
Esiste una pletora di altre nozioni di confluenza, stessa definizione con la
stessa struttura, cambio le relazioni coinvolte
Risoluzione espressioni aritmetiche.
Linguaggi funzionali puri.
• Diamond property: ∀b , c. b ← a → c implica ∃d. b → d ← c,
Controesempi, la confluenza non e` garantita nei:
Definizioni per pattern matching.
Linguaggi logici.
Linguaggi per la concorrenza (CCS).
• →α weakly commutes with →β : ∀b , c. b ←α a →β c implica ∃d.
b →∗β d ←∗α c,
• ...
Le piu` significative restano CR e WCR.
P. Di Gianantonio (Udine)
Rewriting Systems
7 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
8 / 111
Proprieta` degli ARS: terminazione
Proprieta` degli ARS: confluenza su forme
normali
Caratterizzo le proprieta` di terminazione del mio sistema di riscrittura.
Definizione
Definizione
• a e` in forma normale (normal form) se b .a → b.
• a e` in debolmente normalizzante (weakly normalizing) (WN) se ∃b in
forma normale . a →∗ b.
• un ARS ha la “normal form property” (NF) se
∀a , b . b normal form ∧ a = b ⇒ a →∗ b
• a e` in fortemente normalizzante (strong normalizing) (SN) se, a
partire da a, ogni riduzioni termina.
• un ARS ha la “unique normal form property” (UN) se
∀a , b . a , b, forme normali ∧ a = b ⇒ a ≡ b
• un ARS e WN (SN) se lo e` ogni suo termine.
P. Di Gianantonio (Udine)
Rewriting Systems
9 / 111
P. Di Gianantonio (Udine)
Relazioni logiche tra le varie proprieta`
10 / 111
Term rewriting system (TRS)
ARS nozione astratta.
TRS particolari sistemi di riduzione (riscrittura) dove
Theorem
• gli oggetti sono termini del primo ordine (di un algebra)
• regole di riduzione:
• definite in forma parametrica, mediante variabili e pattern matching;
• applicabili ovunque (in ogni contesto).
• SN ∧ WCR ⇒ CR
• WN ∧ UN ⇒ CR
• CR ⇒ NF
• NF ⇒ UN
→ viene chiamata riscrittura.
Esercizi.
P. Di Gianantonio (Udine)
Rewriting Systems
Riduzioni su strutture algebriche.
Esempio: la semplificazione di espressioni algebriche.
Rewriting Systems
11 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
12 / 111
Termini definiti mediante una sintassi
Definizione alternativa
Signature Σ: elenco delle costanti, e delle funzioni con relativa arita` (arity).
Costanti viste come funzioni con zero argomenti.
A questa sintassi si aggiunge spesso un insieme di variabili V .
L’insieme dei termini e` generato dalla grammatica
Definizione
L’insieme termini su Σ, V ( T (Σ, V ) ) e` generato dalle seguenti regole
• ∀x ∈ V
T := x1 | x2 | . . .
c1 () | c2 () | . . .
u1 (T ) | u2 (T ) | . . .
f1 (T , T ) | f2 (T , T ) | . . .
g1 (T , T , T ) | g2 (T , T , T ) | . . .
x ∈ T (Σ, V )
• ∀f ∈ Σ, arity (f ) = n,
f (t1 , . . . tn ) ∈ T (Σ, V )
t1 , . . . tn ∈ T (Σ, V )
Secondo questa definizione una costante c va scritta come c (), cosa da
evitare.
Non si prevede la notazione infissa.
Esercizio: definire la sintassi delle espressioni dell’algebra booleana, delle
espressioni analitiche.
P. Di Gianantonio (Udine)
Rewriting Systems
13 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
Conteggi
Contesti
Regole di riscritture applicate anche a sottotermini di un termine,
ossia a termini inseriti in contesto (context).
`
Il contesto cio` che resta di un termine dopo aver eliminato un suo (o piu)
sottotermini.
Formalmente:
Definizione
• Termini ground: senza variabili, appartenenti a T (Σ, ∅)
• Termini lineari: ogni variabile occorre (e` presente) al piu` una volta.
• Var (t ) denota l’insieme delle variabili che occorrono in t.
t ground ⇔ Var (t ) = ∅.
• Lunghezza di un termine t (numero di simboli che vi appaiono) |t |
• |x | = 1
• |f (t1 , . . . , tn )| = 1 + |t1 | + . . . + |tn |
Profondita` di un termine t (massimo numero di applicazioni
consecutive)
• depth (x ) = 1
• depth (f (t1 , . . . , tn )) = 1 + max(depth (t1 ), . . . , depth (tn ))
P. Di Gianantonio (Udine)
Rewriting Systems
14 / 111
Definizione
Un contesto su Σ e` un termine generato dalla grammatica Σ ∪ {[ ]}.
Il simbolo [ ], detto buco (hole), rappresenta un sottotermine mancante.
Siamo interessati ai “one hole context”.
Notazione C [ ],
esempi: f (c0 , [ ], g (c1 , c2 )), (3 + 8) × ([ ] + 5)
Operazione base: sostituire il buco di un contesto C [ ] con un termine t;
C [t ].
15 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
16 / 111
Term tree
Posizioni
I termini sono alberi ordinati scritti in forma lineare.
Per analizzare i termini o per ragionare sui termini e` conveniente pensarli
come alberi ordinati.
In un term tree ogni sottotermine e` individuato dal percorso “radice sottotermine”.
Percorso (posizione) descritto da un sequenza di numeri, che indicano di
volta in volta in quale sottoalbero spostarsi.
Notazione
• n1 , . . . , ni sequenze;
• variabili e costanti sono foglie.
• ogni simbolo di funzione rappresenta un nodo e i sottotermini sono i
sottoalberi.
• n1 , . . . , ni · m1 , . . . , mj concatenazione di sequenze;
• t | n0 ,...,ni sottotermine t individuato dalla posizione;
• t [ ] n0 ,...,ni contesto individuato dalla posizione
t meno il sottotermine t | n0 ,...,ni
Esempi:
P. Di Gianantonio (Udine)
Rewriting Systems
17 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
18 / 111
Sostituzioni
Domini
L’operazione di sostituire, in un termine con variabili, alcune variabili con
dei termini.
Definizione
Dominio di σ e` l’insieme delle variabili modificate da σ
Dom(σ) = {x ∈ V | σ(x )
Definizione
• Una sostituzione e` una funzione σ : V → T (Σ, V ).
x}
Codominio, le variabili nell’immagine del dominio
• Estesa ai termini per induzione sulla sintassi:
σ(f (t1 , . . . , tn )) = f (σ(t1 ), . . . , σ(tn )).
Var (σ(x ))
Cod (σ) =
x ∈Dom(σ)
σ(t ) viene scritto come t σ o come t σ .
Definizione diversa da quella standard di dominio di una funzione.
P. Di Gianantonio (Udine)
Rewriting Systems
19 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
20 / 111
Sostituzioni a dominio finito
Composizione di sostituzioni
Tratteremo sostituzioni con domini finito,
rappresentazione finita:
{x1 /s1 , . . . , xn /sn }
Viste come funzioni su termini, le sostituzioni possono essere composte:
(σ ◦ τ)(t ) = σ(τ(t ))
Definiamo la sostituzione solo dove fa qualcosa di interessante, sulle altre
`
variabili si comporta come l’identita.
Nella nostra notazione
Notazioni alternative {x1 → s1 , . . . , xn → sn } oppure {s1 /x1 , . . . , sn /xn }
Restrizione di un sostituzione
σ|v =
Sulle variabili:
σ(x )
x
se x ∈ V
altrimenti
t τσ = (t τ )σ
τσ(x ) = (τ(x ))σ
Composizione associativa (quasi per definizione).
Commutativa?
Unioni di sostituzione con domini disgiunto:
σ1 ∪ σ2
P. Di Gianantonio (Udine)
Rewriting Systems
21 / 111
Composizione di sostituzioni
P. Di Gianantonio (Udine)
Rewriting Systems
22 / 111
Composizione di sostituzioni a domini
finito
Viste come funzioni su termini, le sostituzioni possono essere composte:
Date due sostituzioni a domini finito:
(σ ◦ τ)(t ) = σ(τ(t ))
Nella nostra notazione
Sulle variabili:
σ = {x1 /s1 , . . . , xm /sm }
τ = {y1 /t1 , . . . , yn /tn }
t τσ = (t τ )σ
dal calcolo di στ sulle variabili si ricava στ e` dato dall’insieme
τσ(x ) = (τ(x ))σ
τ
{x1 /s1τ , . . . , xm /sm
, y1 /t1 , . . . , yn /tn }
Composizione associativa (quasi per definizione).
Commutativa? Trovare controesempio.
P. Di Gianantonio (Udine)
Rewriting Systems
a cui sono rimossi i binding yi /ti con yi ∈ {x1 , . . . , xm } = Dom(σ) e
(per compattezza) i binding xi /xi , per cui quegli xi tali che xi = xiστ .
22 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
23 / 111
` tra
Ordine di sussunzione (generalita)
termini
Renaming (ridenominazione)
Definizione
Se s ≡ t σ :
Sostituzioni che sostituiscono variabili con variabili,
e variabili distinte con variabili distinte.
• s e un istanza di t
σ e` un renaming per t se σ|Var (t ) e` un renaming.
• t e` istanziato (is matched) sull’istanza s dalla sostituzione σ.
• t sussume s, t e` piu` generale di s.
• s
t
La relazione
e` un quasi ordine (relazione riflessiva e transitiva). Dim?
Se s
s, t e` una variante di s, s
s
t et
t sse esiste un renaming σ tale che s ≡ t σ
s ≺ t definito come s
P. Di Gianantonio (Udine)
Rewriting Systems
24 / 111
t
P. Di Gianantonio (Udine)
t ma s
t, (s istanza propria di t).
Rewriting Systems
25 / 111
Proprieta` del quasi-ordine di sussunzione
Matching
Risolve il problema: dati s e t costruire, se esiste, una sostituzione σ tale
che s ≡ t σ .
Conviene generalizzare il problema al matching di sequenze di termini con
una singola sostituzione
{t1 /s1 , . . . , tn /sn }
• due termini s e t hanno sempre un sup r,
s r, t r e ∀q.(s q) ∧ (t q) ⇒ r q,
Definizione
• due termini s e t non hanno necessariamente un’istanziazione
comune, ma se questa esiste allora esiste anche la piu` generale delle
istanze comuni (mgci – most general comon instance).
[Algoritmo di Matching]
{f (t1 , . . . , tn )/f (s1 , . . . , sn )} ∪ S
{f (t1 , . . . , tn )/g (s1 , . . . , sm )} ∪ S
{f (t1 , . . . , tn )/x } ∪ S
{x /s1 } ∪ S
P. Di Gianantonio (Udine)
=⇒ {t1 /s1 , . . . , tn /sn } ∪ S
=⇒ fail, if f g
=⇒ fail
=⇒ fail if x /s2 ∈ S ∧ s1
Rewriting Systems
• ≺ non possiede catene strettamente crescenti (catene di termini
sempre piu` generali)
s2
26 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
27 / 111
Ordine di generalita` tra sostituzioni
Unificazione
Definizione
Problema: dati due termini t e s esiste una loro istanza comune (con
identica sostituzione).
La sostituzione τ e` piu` generale di σ:
σ
Definizione
τ
[Unificatore, MGU]
• Se s σ ≡ t σ allora σ e` detto un unificatore di s e t.
se
∃ ρ. σ = τ ρ
• Il piu` generale (il piu` grande rispetto all’ordine
e t, e` detto Most general unifier MGU.
`
Proprieta:
σ
τ ⇒ ∀t . t σ
t τ.
Theorem
Vale la freccia inversa?
Quasi sempre.
Esercizio (molto difficile): costruire un controesempio.
P. Di Gianantonio (Udine)
Rewriting Systems
Se s e t sono unificabile allora ammettono un MGU (unico a meno di
renaming).
28 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
Algoritmo di Unificazione (Martelli,
Montanari)
{f (t1 , . . . , tn ) = f (s1 , . . . , sn )} ∪ E
{f (t1 , . . . , tn ) = g (s1 , . . . , sm )} ∪ E
{x = x } ∪ E
{f (t1 , . . . , tn ) = x } ∪ E
{x = t } ∪ E
{x = t } ∪ E
P. Di Gianantonio (Udine)
tra gli unificatori di s
Considerazioni
• Versione non deterministica dell’algoritmo di Robinson (1965),
algoritmo unificazione WAM
esempio di utilita` del non determinismo
=⇒ {t1 = s1 , . . . , tn = sn } ∪ E
=⇒ fail, se f g
=⇒ E
=⇒ {x = f (t1 , . . . , tn )} ∪ E
=⇒ fail se x ∈ Var (t ) e x t
=⇒ {x = t } ∪ E {x /t }
se x Var (t ), x ∈ Var (E )
Rewriting Systems
29 / 111
• Correttezza: correttezza delle singole regole: nessuna altera
l’insieme degli unificatori
• Terminazione: non completamente ovvia.
• Se nessuna regola e` applicabile allora le equazioni ammettono un
ovvio MGU.
• Posso utilizzare l’algoritmo per una dimostrazione costruttiva
dell’esistenza del MGU
30 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
31 / 111
Regole di riduzione su Σ-termini
Term Rewriting Systems
Un insieme di regole di riduzione su Σ.
Definizione
Definizione
[Regola di riduzione] Una regola di riduzione (su Σ) e data da un coppia di
termini l → r in T (Σ, V ) tali che:
[Term rewriting system]
1) l non e` una variabile;
2) Var (r ) ⊆ Var (l )
• Un TRS induce una relazione di riduzione →R su T (Σ, V ), l’unione
delle riduzioni definite dalle singole regole.
l → r rappresenta uno schema di regole: tutte le regole ottenibili per
istanziazione delle variabili, e inserimento in contesti.
• Se non c’e` ambiguita` si rimuove il pendice →.
• Un TRS e` un istanza di Abstract Reduction System.
• Tutte le definizioni, proposizione per i ARS si applicano ai TRS.
Ossia: sequenza di riduzione, →∗ , =, WCR, CR, normal form, WN,
SN, NF, UN.
• Se le regole hanno nome ρ : l → r, con t →ρ s specificare che t
riduce a s mediante un’applicazione delle regola ρ.
{C [l σ ] → C [r σ ] | σ sostituzione, C [ ] contesto}
• l σ redex
• r σ contractum
P. Di Gianantonio (Udine)
Rewriting Systems
• Un TRS e` una coppia R := Σ, R formato da una signature Σ ed un
insieme di regole su Σ.
32 / 111
Esempi — Aritmetica
P. Di Gianantonio (Udine)
Rewriting Systems
33 / 111
Esempi – Logica Combinatoria (Moses
¨
Schonfinkel,
Haskell Curry)
Logica Combinatoria S , K : 0, app : 2
Scriviamo app con la notazione infissa: app (x , y ) diventa x · y
Aritmetica: 0 : 0, S : 1, add , mult : 2
• add (x , 0) → x
• (K · x ) · y → x
• add (x , S (y )) → S (add (x , y ))
• ((S · x ) · y ) · z → (x · z ) · (y · z ).
• mult (x , 0) → 0
Ridurre ((S · K ) · K ) · x.
• mult (x , S (y )) → add (mult (x , y ), x )
Mostrare che mult (S (S (0)), S (S (0))) e` CR.
Come per la moltiplicazione il simbolo · puo` essere omesso, l’applicazione
e` associativa a sinistra. Si eseguono prima le operazioni a sinistra. Es.
SKK = ((SK )K ).
Problema definire un operazione di sottrazione con le opportune regole.
Posto SKK = I ridurre SII(SII).
Ridurre mult (S (S (0)), S (S (0))).
Posto S (KS )K = B ridurre Bxyz.
Nella logica combinatoria posso codificare ogni funzione calcolabile.
P. Di Gianantonio (Udine)
Rewriting Systems
34 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
35 / 111
Condizioni sulle regole
Condizioni sulle regole
Da proprieta` delle regole derivano proprieta` del TRS.
Da proprieta` delle regole derivano proprieta` del TRS.
`
La regola ρ : l → r e:
`
La regola ρ : l → r e:
• lineare a sinistra se l e` lineare.
• lineare a sinistra se l e` lineare.
La verifica di l’applicabilita` della regola, in un punto, ha costo
costante. L’applicabilita` non dipende troppo strettamente da come il
termine e` scritto.
• non duplicante se non ha variabili con piu` occorrenze in r che in l.
Duplicante altrimenti. Duplica (o triplica . . . ) una parte del redex.
• non eliminante se Var (l ) ⊆ Var (r ).
Eliminante altrimenti. Dal redex vengono eliminate tutte le istanze che
fanno matching con una variabile di l.
• non collassante se r non e` una variabile. Collassante altrimenti.
Un TRS si dice lineare a sinistra (non duplicante, non eliminante, non
collassante) se lo sono tutte le sue regole.
P. Di Gianantonio (Udine)
Rewriting Systems
36 / 111
P. Di Gianantonio (Udine)
Condizioni sulle regole per assicurare la
confluenza, (CR)
Rewriting Systems
36 / 111
Sovrapposizione tra regole
Definizione
Definire delle proprieta` sulle regole per assicurare la confluenza del TRS.
Due regole, ρ0 : l0 → r0 e ρ1 : l1 → r1 si sovrappongono se l0 e un
sottotermine non variabile di l1 hanno un istanza in comune, o viceversa.
Osservazioni: le sovrapposizione possono coinvolgere completamente
l0 , l1
ρ1 : f (g (x ), y ) → x
ρ2 : f (x , b )
→ b
Esempio di TRS non confluente
ρ1 : f (g (x ), y ) → x
ρ2 : g ( a )
→ b
Il termine f (g (a ), b ) non e` confluente.
Considerare il termine f (g (a ), b ).
Le regole ρ1 e ρ2 sono entrambe applicabili ma l’applicazione di una
distrugge l’applicabilita` dell’altra (e la confluenza del termine).
Una regole puo` sovrapporsi a se stessa non banalmente:
ρ : f (f (x )) → a
Un’analisi di quando questo puo` avvenire porta alla prossima definizione.
Considerare il termine f (f (f (b ))).
P. Di Gianantonio (Udine)
Rewriting Systems
37 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
38 / 111
Condizione equivalente
Esempio di non sovrapposizione
Regole che non si sovrappongono possono avere redex innestati, ma in
questo caso uno non distrugge l’altro.
Confrontare:
Due regole, ρ0 : l0 → r0 e ρ1 : l1 → r1 si sovrappongono se, dopo un
renaming delle variabili t.c. Var (l0 ) ∪ Var (l1 ) = ∅, l0 unifica con un
sottotermine non variabile di l1 , o viceversa.
ρ1 : f ( x , y ) → x
ρ2 : g (a )
→ b
con
ρ1 : f (g (x ), y ) → x
ρ2 : g ( a )
→ b
Sul termine f (g (a ), b ).
P. Di Gianantonio (Udine)
Rewriting Systems
39 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
Risultati
40 / 111
Controesempio
Considerare il TRS formato dalle regole:
ρ1 : f (x , x ) → b
ρ2 : g (x )
→ f (x , g (x ))
ρ3 : a
→ g (a )
Theorem
Un TRS privo di sovrapposizioni tra regole e` debolmente confluente, WCR
(weak Church-Rosser).
Questo teorema e` spesso presentato in una forma rafforzata in cui si
ammettono buone sovrapposizione tra regole (convergent critical pairs).
Questo non assicura la confluenza (CR), a meno che il sistema non sia
fortemente normalizzante (WCR ∧ SN ⇒ CR).
Osservare che:
• le regole non si sovrappongono
• il TRS e` WCR
• g (a ) →∗ b e g (a ) →∗ g (b ),
• b e g (b ) non hanno nessun ridotto in comune.
P. Di Gianantonio (Udine)
Rewriting Systems
41 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
42 / 111
Ortogonalita`
Constructor Based TRS
Quasi sempre nel definire una signature Σ, partizione i simboli in
• C, costruttori, i generatori degli elementi di un tipo
Definizione
Un TRS R e` ortogonale se e` lineare a sinistra e non contiene regole che si
• D, definiti, l’insieme di funzioni che voglio definire su di un certo tipo.
Esempi:
• per la signature dei naturali, costruttori sono 0, S, i definiti add , mul
sovrappongono.
• per le liste i costruttori sono nil , cons, la concatenazione e` definita.
Theorem
Ogni TRS ortogonale e` confluente (CR).
Definizione
Un Constructor Based TRS contiene solo regole nella forma:
f (t1 , . . . , tn ) → s con f ∈ D ∧ ∀i . ti ∈ T (C, V )
P. Di Gianantonio (Udine)
Rewriting Systems
43 / 111
P. Di Gianantonio (Udine)
Haskell
Rewriting Systems
Strategie di riduzione
Dato un TRS R ed un termine t, i passi che portano a definire una
riduzione t → t sono:
Haskell e` un Constructor Based TRS, anche se possiede in piu` il
meccanismo delle guardie.
• si selezione una posizione p di t,
Lemma
In CBTRS, due regole, ρ0 : l0 → r0 e ρ1 : l1 → r1 si sovrappongono sse l0
ed l1 hanno un istanza in comune.
Il teorema dell’ortogonalita` si applica, con gli opportuni aggiustamenti, ad
Haskell
• una regola ρ : l → r in R,
• tali che esiste σ = match{l /t |p } (l σ = t |p ),
• in questo caso t = t [r σ ]p e il sottotermine t |p costituisce il redex della
riduzione.
• le regole devono essere lineari a sinistra,
Data t, possono esistere piu` coppie p, ρ tali che ρ e` applicabile in t |p .
• le regole che possono sovrapporsi appartengono ad una stessa
definizione di funzione, l’ordine di applicazione su queste regole,
forza la confluenza.
Possono esistere piu` riduzioni t → t .
P. Di Gianantonio (Udine)
44 / 111
Rewriting Systems
Una strategia di riduzione seleziona, per ogni termine t una tra le tante
riduzioni su t.
45 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
46 / 111
Strategie di riduzione
Strategie di riduzione classiche
Definizione estensionale
Definizione
Una strategia di riduzione ad un passo F per TRS Σ, R e` una funzione
F : T (Σ, V ) → T (Σ, V ) ∪ {∗} tale che
• F(t ) ≡ ∗ se t →
parallel-innermost (a molti passi) riduco tutti i redex piu` interni (con
posizioni massimali in lunghezza). I redex sono disgiunti.
• t → F(t ) altrimenti.
Una strategia di riduzione a molti passi garantisce t →+ F(t ).
leftmost-outtermost (a un passo) scelgo il redex piu` a sinistra tra quelli piu`
esterni.
In una definizione piu` operazionale posso indicare per ogni termine t
quale regola ρ, e quale posizione p vada considerate per la riscrittura.
parallel-outtermost (a molti passi) riduco tutti i redex piu` esterni (con
posizioni minimali in lunghezza). I redex sono disgiunti.
In un TRS ortogonale, in ogni posizione esiste al piu` una regola
applicabile. Posso specificare una strategia dando per ogni termine la
posizione del redex.
P. Di Gianantonio (Udine)
leftmost-innermost (a un passo) scelgo il redex piu` a sinistra tra quelli piu`
interni.
In termini di posizioni: scelgo il redex con posizione p
minima nell’ordine lessicografico tra i redex aventi una
posizione p massimale in lunghezza.
Rewriting Systems
full-substitution (a molti passi) riduco tutti i redex piu` ovunque. I redex non
sono disgiunti ma in un TRS ortogonali una riduzione non
disturba l’applicabilita` di un altra.
47 / 111
P. Di Gianantonio (Udine)
Normalizzazione
Rewriting Systems
48 / 111
Outtermost, innermost
Una strategia di riduzione F e` normalizzante se porta ad una forma
normale ogni qualvolta questa esista:
per ogni t che ha forma normale allora esiste n tale che Fn (t ) = ∗.
• Innermost: strategia di riduzione eager, si valutano gli argomenti
prima di passarli alla funzione, ML.
Con opportune condizione, left-normal orthogonal system la
leftmost-outtermost e` normalizzante.
• Outtermost: strategie di riduzione lazy, valuto un argomento solo se
espressamente richiesto, Haskell .
Controesempio al teorema piu` generale, il termine f (c , a )
Strategie eager non sono normalizzanti: valuto un argomento che diverge
anche se questo non viene usato nella funzione.
• f (x , b ) → d
Strategie lazy, con regole di riduzioni duplicanti, portano a valutare un
argomento piu` volte, a meno che non rappresenti i termini con DAG (Direct
Acyclic Graph), come in Haskell.
• a→b
• c→c
La parallel-outtermost e` normalizzante.
P. Di Gianantonio (Udine)
Rewriting Systems
49 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
50 / 111
Haskell and TRS
Lambda astrazione
Posso costruire le nameless functions
\x -> x + 2
\f -> \x -> f (f x)
In Haskell si possono definire constructor based TRS.
Nelle definizioni di tipo, si definiscono per ogni tipo i costruttori.
Definizioni di funzioni date attraverso il matching danno le regole di
riduzione.
Questo non definisce completamente la computazione in Haskell
Nei TRS espressioni sono di un tipo base, non possono mai essere
funzioni
Haskell possono definire e manipolare funzioni.
In altri formalismi si scrive come: λx .x + 2
Funzioni oggetti manipolabili come gli altri.
Una regola per l’applicazione. La β-regola.
(\x -> x + x ) n
→
n + n
In generale
(\x -> f ) m
P. Di Gianantonio (Udine)
Rewriting Systems
51 / 111
P. Di Gianantonio (Udine)
Operatore di legame
→
f {x/m}
Rewriting Systems
52 / 111
Rinomina delle variabili
Necessaria nel corso di una riduzione.
Con la lambda astrazione introduco un operatore di legame - chiusura.
Senza rinomina delle variabili
\x ->
Fa diventare la x un variabile chiusa, non accessibile al resto termine.
(\f -> \x -> f x) (\y -> x + y)
I termini fanno considerati a meno di α-equivalenza.
Introduco un α-regola.
\x -> (\y -> x + y) x
\x -> x + x
Riduce a
Scorretta, la variabile libera x viene catturata.
\x -> x + 2
La riduzione corretta
perfettamente equivalente a
(\f -> \x
(\f -> \z
\z -> (\y
\z -> x +
\y -> y + 2
P. Di Gianantonio (Udine)
Rewriting Systems
53 / 111
-> f x) (\y -> x + y)
-> f z) (\y -> x + y)
-> x + y) z
z
P. Di Gianantonio (Udine)
Rewriting Systems
54 / 111
Variabili
Indici di de Bruijn
Pensare alle variabili chiuse come puntatori (a λ-astrazioni) e non come
identificatori.
In questo modo
α-regola, necessita` di applicarla nel corso della riduzione,
si complica:
• implementazione dei linguaggi,
\ y -> x + y
• studio formale del linguaggio e del sistema di riscrittura.
viene rappresentata come
Possibile soluzione del problema:
\-> x + p
dove p e` un puntatore a \->.
P. Di Gianantonio (Udine)
Rewriting Systems
55 / 111
P. Di Gianantonio (Udine)
Lambda calcolo, puro non tipato
Posso codificare i numeri naturali
0 → (\f x -> x)
1 → (\f x -> f x)
2 → (\f x -> f (f x))
n → (\f x -> fn x)
Successore: \m -> \f x -> f (m f x)
Somma: \m n -> \f x -> m f ( n f x)
Prodotto: \m n -> \f x -> m ( n f) x
Esponente: \m n -> \f x -> n m f x
Esercizio difficile: definire il predecessore.
• variabili,
• applicazione,
• λ-astrazione
come unica regola di riduzione la β regola.
Sistema non tipato, ogni elemento puo` essere applicato a se stesso.
( x -> x x)( x -> x x)
Rewriting Systems
56 / 111
Numerali di Church
Posso costruire un sistema di calcolo interessante usando solo
P. Di Gianantonio (Udine)
Rewriting Systems
57 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
58 / 111
Untyped λ-calculus in Haskell
λ-calcolo con costanti
Posso definire il tipo di data dei λ-termini non tipati.
data Untyped = Abst [Untyped -> Untyped]
Codificare tutto tramite λ-termini puri non pratico.
L’applicazione non e` immediata, va espressa esplicitamente
t s
Si introducono delle costanti, rappresentati
elementi,
funzioni base.
diventa
Possibili molte scelte diverse.
app t s
Un λ-calcolo tipato con costanti definisce
Core Language di Haskell.
dove
app = \ t -> case t of Abst f | f
P. Di Gianantonio (Udine)
Rewriting Systems
59 / 111
P. Di Gianantonio (Udine)
Core Language
Rewriting Systems
60 / 111
Tipi di dato ricorsivi, Costruttori e
distruttori
Nel definire la semantica di un linguaggio, o la sua implementazione e utile
considerare i core Language:
• linguaggio semplice, insieme ridotto di costruttori primitive,
sottoinsieme ridotto del linguaggio principale,
In Haskell le constanti vengono definite mediante le dichiarazione di tipo.
Ogni dichiarazione di tipo introduce un certo numero di costruttori e una
costante distruttore
data PNat = Z | S PNat
• linguaggio principale puo` essere (facilmente) tradotto nel linguaggio
core,
• approccio modulare all’implementazione, alla semantica
La definizione genera due funzioni costruttori di tipo:
Z :: PNat
S :: PNat -> PNat
Dal punto di vista teorico i linguaggi core risaltano:
• i meccanismi fondamentali della computazione,
e una funzione distruttore:
• similitudini: differenze tra linguaggi.
case_PNat ::
P. Di Gianantonio (Udine)
Rewriting Systems
61 / 111
a -> ( PNat -> a) -> PNat -> a
P. Di Gianantonio (Udine)
Rewriting Systems
62 / 111
Distruttori
Esempio
Con regole di riduzione
La funzione somma viene tradotta nel core language in
case PNat a f Z → a
case PNat a f (S n) → f n
add = \ x y -> case x of O -> y |
S x1 -> S (add x1 y)
case PNat a f m
viene scritto come:
o nel linguaggio puro
case m of Z -> a |
S n -> f n
P. Di Gianantonio (Udine)
add = Y (\ f x y -> case_PNat y (\ x1 -> f x1 y) x)
Rewriting Systems
63 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
Core teorico
Sistemi di tipo
• Si riduce tutto ad applicazione di funzioni.
• Definizioni per pattern matching ridotte a uso di funzioni case (su un
singolo argomento e completi)
P. Di Gianantonio (Udine)
Rewriting Systems
64 / 111
65 / 111
I TRS e λ-calcolo, considerati sino ad ora, non tipati.
Linguaggi non tipati portano sono flessibili ma spingono ad errori.
Tipi pongono dei vincoli portano a programmi piu` strutturati ma portano a
delle rigidita` nella definizione di programmi.
Tipi polimorfi di Haskell permetto un controllo sintattico senza porre troppi
vincoli inutile e con un type-checking semplice.
Esistono altri sistemi di tipi polimorfi.
P. Di Gianantonio (Udine)
Rewriting Systems
66 / 111
Convergenza
Strategie di riduzione.
λ-calcolo sistema di regole non deterministico, in un termine ci sono piu`
redex e piu` possibili riduzioni
(\f -> f ( f a ) ) ((\x -> g x x )b )
Teorema (Church-Rosser)
La riscritture nel λ-calcolo e` confluente (e` Church-Rosser).
P. Di Gianantonio (Udine)
Rewriting Systems
67 / 111
Narrowing
P. Di Gianantonio (Udine)
Rewriting Systems
68 / 111
Da linguaggi funzionali a linguaggi logici
Meccanismo di riscrittura in Curry.
Riscrittura su termini con variabili t ed un insieme di regole {li = ri |i ∈ I}
Data un termine t, con variabili:
Posso codificare Prolog in Haskell?
• seleziono una posizione p rappresentante un sottotermine t |p , non
variabile di t,
Prima differenza tipato – non tipato, superabile:
• seleziono una variante di una regola l = r tale che t |p e l, siano
unificabili,
• posso trasformare Prolog in un linguaggio tipato, perdendo in
`
flessibilita.
• sia σ l’mgu di t |p e l.
• posso far diventare Haskell quasi non tipato definendo un tipo
“calderone” a cui assegnare ogni espressione che non sia una
funzione.
• t viene riscritta in (t [r ]p )σ . Notazione: t
Definisco
∗
come la chiusura transitiva di
t
∗
σ tn
se esiste t
σ1 t1
σ
(t [r ]p )σ
, formalmente:
σ2
...
σn tn
con σ = σ1 σ2 . . . σn (= σn ◦ . . . ◦ σ1 )
P. Di Gianantonio (Udine)
Rewriting Systems
69 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
70 / 111
Codifica (naif) di programmi logici
Esempio
Un programma Prolog P, viene codificato in un programma Haskell P .
Uso due tipi:
• un tipo Term (Termini) con tanti costruttori quanti i costruttori usati in
P.
• un tipo Prop con un unico elemento (costruttore unario) Success.
likes(mary,food).
likes(mary,wine).
likes(john,wine).
likes(john,mary).
likes(john, x) :- likes(mary, x), likes(x, food)
E le funzioni:
• & (and) : Prop → Prop → Prop
Success & Success = Success
• tante funzioni predi : Term → . . . → Term → Prop, quante sono le
relazioni definite in P.
Ogni regola clausola Prolog, viene trasformata in una regola di riscrittura
(matching rule).
P. Di Gianantonio (Udine)
Rewriting Systems
71 / 111
viene tradotto con
likes Mary Food = Success
likes Mary Wine = Success
likes John Wine = Success
likes John Mary = Success
likes John x = (likes Mary x) & (likes x Food)
P. Di Gianantonio (Udine)
Codifica di programmi logici
Rewriting Systems
72 / 111
Codifica di linguaggi logici
Cosa manca in questa codifica:
Cosa posso fare con P ?
• clausole con variabili extra a destra non hanno una traduzione lecita
in Haskell.
Dato un goal ground verificare se e` dimostrabile.
Problema: il programma P tenta solo una strada. Con il meccanismo
delle eccezioni, posso indurlo a provare piu` strade.
La possibilita` di fallimento diventa una caratteristica indispensabile per la
ricerca.
• la possibilita` di verificare la soddisfacibilita` di asserzioni non ground,
con variabili libere. Riscrittura su termini non-ground.
La sostituzione restituita come risultato.
• la ricerca di piu` soluzioni, non-determinismo.
Curry e` l’estensione di Haskell che rende questa codifica completa.
P. Di Gianantonio (Udine)
Rewriting Systems
73 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
74 / 111
E-unificazione
E-unificazione mediante narrowing
Estensione di Prolog a linguaggi funzionali.
• In Prolog posso simulare funzioni con relazioni.
Theorem (Completezza del narrowing)
• Non posso costruire termini con simboli di funzione.
Dato un insieme di regole di riscrittura R confluenti e terminanti.
se s σ =R t σ allora esistono:
• Altrimenti devo considerare il problema dell’E-unificazione,
l’unificazione su termini contenenti simboli di funzione:
• s1 , t1 tali che (s = t )
• un mgu τ per s e t ,
E-unificazione
Dato un insieme di regole di riscritture R, e due termini s , t, definire le
sostituzioni σ tali che
σ(s ) =R σ(t )
tali che τ ◦ τ e` piu` generale di σ (σ
Rewriting Systems
τ ◦ τ)
Mediante narrowing posso rendere uguale tutto cio` che e` eguagliabile.
Puo` essere indecidibile.
Anche restringendo la classe di regole di riscrittura, l’E-unificazione resta
complessa (mancano algoritmi efficienti).
P. Di Gianantonio (Udine)
∗ (s = t ),
1
1
τ
τ
τ
(s1 ≡ t1 )
75 / 111
IL narrowing e` anche corretto: tutto cio` che riesco ad uguagliare mediante
narrowing e` anche E-unificabile.
P. Di Gianantonio (Udine)
Rewriting Systems
Restrizione del full-narrowing
76 / 111
Basic narrowing
Il principale problema del narrowing e` l’esplosione di possibili riscritture
alternative per uno stesso termini (la presenza di variabili aumenta di
molto le possibilita` di riscrittura).
Necessario definire strategie di riduzione, che
• siano efficienti,
Problema: ho la regola rev (rev L ) = L e cerco le sostituzioni σ che
rendono vera
rev x = x,
Posso costruire la seguente catena
rev x = x
x /rev x1 rev x1 = x1
x1 /rev x2 x2 = rev x2
Questo tipo di derivazioni sono eliminate se non applico il narrowing ai
termini introdotti da unificazioni.
Implementazione: in serie di narrowing t σ1 t1 σ2 . . . σn tn marco i
simboli di funzione che appartenevano a t o alla parte destra di una regola
applicata.
• preservino la completezza.
Nel caso di regole confluenti e terminanti, il basic narrowing e` terminante
e completo.
P. Di Gianantonio (Udine)
Rewriting Systems
77 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
78 / 111
Inner narrowing
Inner narrowing
Ci limitiamo a insiemi di regole di riduzione constructor-based.
In ogni regola l = r, l e` un pattern, contiene un unico simbolo di funzione
come radice (Haskell).
• si cercano solo le sostituzioni ground (che portano a termini uguali).
Strategia poco efficiente, porta ad istanziare variabile e ad applicare
regole piu` dello stretto necessario.
Non si batte la riduzione Prolog.
Una motivazione per i linguaggi funzionali logici e` che questi posso indurre
strategie di riduzione piu` efficienti dei linguaggi logici.
• fx=a
• ga=a
∗
{}
a
Non completa con funzioni parziali (come per i TRS).
P. Di Gianantonio (Udine)
Rewriting Systems
• regole confluenti e complete
• solo funzioni totali
Innermost seleziona il redex piu` interno:
Non completa
La riduzione f (g a )
Completa se
79 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
Outtermost Narrowing - Lazy narrowing
Core Language
Outtermost non completa, esclude alcune riduzioni. Con
Nel definire la semantica di un linguaggio, o la sua implementazione e utile
considerare i core Language:
• fOO=O
• linguaggio semplice, insieme ridotto di costruttori primitive,
sottoinsieme ridotto del linguaggio principale,
• f (S O) O = S O
• f x (S y) = S S O
nell’espressione f (fxy )z, la strategia outtermost non cerca di valutare l’f ,
interna.
Lazy: valuta redex interni se utili per ridurre quelli esterni, difficile
caratterizzare i narrowing veramente necessari.
Rewriting Systems
• linguaggio principale puo` essere (facilmente) tradotto nel linguaggio
core,
• approccio modulare all’implementazione, alla semantica
Dal punto di vista teorico i linguaggi core risaltano:
Soluzione: needed narrowing, per regole constructor based porta ad una
applicazione minima dei passi di narrowing.
P. Di Gianantonio (Udine)
80 / 111
81 / 111
• i meccanismi fondamentali della computazione,
• similitudini: differenze tra linguaggi.
P. Di Gianantonio (Udine)
Rewriting Systems
82 / 111
Core Language (teorico) per Haskell
Tipi di dato ricorsivi, Costruttori e
distruttori
data Nat = O | S Nat
La definizione genera due funzioni costruttori di tipo:
Lambda calcolo tipato.
O :: Nat
S :: Nat -> Nat
• un insieme di funzioni basi
• applicazione e λ-astrazione.
e una funzione distruttore di tipo case, la funzione somma viene tradotta
nel core language in
add = \ x y -> case x of O -> y |
S x1 -> S (add x1 y)
o per evitare definizioni ricorsive
add = Y (\ f x y -> case x of O -> y | S x1 -> S (f x1 y) )
Al case per i naturali possiamo assegnare tipo:
P. Di Gianantonio (Udine)
Rewriting Systems
83 / 111
P. Di Gianantonio (Udine)
case
Rewriting Systems
:: a -> (Nat -> a) -> Nat -> a
Core teorico
84 / 111
Pattern matching - case statement
La definizione
and True True
and x
False
and False x
• Si riduce tutto ad applicazione di funzioni.
= True
= False
= False
• Definizioni per pattern matching ridotte a uso di funzioni case (su un
singolo argomento e completi)
diventa
• Analisi della complessita` dei costrutti.
and = \x y -> case x of True -> case y of True -> True
False -> False
False -> False
Una dichiarazione per pattern matching si trasforma in un albero di scelte
con un foglie le parti destre delle equazioni.
Pattern matching porta a definizione piu` compatte leggibili eleganti.
P. Di Gianantonio (Udine)
Rewriting Systems
85 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
86 / 111
Strategie di riduzione
Rewriting e Narrowing
Nel core language, il case statement rende evidente l’ordine di valutazione
degli argomenti,
L’ordine di applicazione delle regole di riscrittura dipende dalla strategia di
riduzione del linguaggio
Il passaggio da regole di riscrittura a narrowing porta alla perdita di buone
`
proprieta:
• confluenza,
• lazy – outtermost,
• terminazione,
• eager – innermost.
• l’applicazione del narrowing ci allontana dal soluzione desiderata,
istanziazione non desiderata.
Pattern matching descrizione piu` dichiarativa, tuttavia:
• esplosione dello spazio di ricerca
• regole ortogonali, garantisco la confluenza,
• e` semplice descrivere la strategia di riduzione in termini di regole di
riscrittura
outtermost – innermost.
P. Di Gianantonio (Udine)
Rewriting Systems
87 / 111
Necessita` di usare strategie di riduzione, ma anche qui le cose si
complicano: molte proposte, quasi tutte le strategie di riduzione hanno dei
difetti.
P. Di Gianantonio (Udine)
Da funzionale a logico funzionale
Rewriting Systems
88 / 111
Needed narrowing
Il passaggio da funzionale - logico funzionale e` piu` semplice a livello di
core language.
Si aggiunge:
• un costrutto di scelta non deterministica (or),
• variabili libere,
• un versione flexible del costrutto case fcase
Descrizione sintetica:
L’espressione
• per ogni funzione f , definita mediante regole, viene data una
traduzione ottimale nel core language. (Definitional tree)
fcase y of True -> exp1
False -> exp2
• le regole vengono applicate valutando le traduzioni ottimali, nel core
language, con strategia lazy.
Con y variabile logica, riduce a:
exp1 {y/True}
ma anche a
exp2 {y/False}
P. Di Gianantonio (Udine)
Rewriting Systems
89 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
90 / 111
Esempi di traduzione
Traduzione ottimale
Le regole:
O
<= x
-> True
S x <= O
-> False
S x <= S y -> x <= y
Nella traduzione non ottimale si istanzia y anche quando il primo
argomento e` zero.
Traduzione ottimale:
x <= y
= fcase x of O -> True
S x1 -> fcase y of O -> False
S y1 -> x1 <= y1
Traduzione non ottimale:
x <= y
=
fcase y of O -> fcase x of O ->
S x1
S y1 -> fcase x of O
S
P. Di Gianantonio (Udine)
True
-> False
-> True
x1 -> x1 <= y1
Rewriting Systems
91 / 111
La terza foglia del case tree corrisponde al caso in cui y = S y1 e x = O,
ossia descrive una regola
0 <= S y1 -> True, non contenuta nell’insieme di regole originario.
La regola e` comunque corretta in quanto istanza di una regola (0 <= y
-> True) dell’insieme originario.
Definizione:
Traduzione e` ottimale se ogni sottocaso finale dell’albero dei fcase
corrisponde ad una regola.
P. Di Gianantonio (Udine)
Rewriting Systems
Esempi di riduzione:
92 / 111
Costrutto or
x <= x + y
• Il narrowing ricondotto a istanziazione variabili, sostituzione variabili
con termini.
• Ogni istanziazione di una variabile, indotta dal flexible case, (es. { x/
S x1 } ) la variabile creata (x1) deve essere nuova ossia non
utilizzata altrove nel termine.
P. Di Gianantonio (Udine)
Rewriting Systems
93 / 111
choice = 0
choice = 1
choice = 0 ’or’ 1
Si forniscono piu` alternative. Tutte devono essere considerate.
P. Di Gianantonio (Udine)
Rewriting Systems
94 / 111
Costrutto Fail
Scrittura sintetica
Indica l’impossibilita` di fornire un risultato.
Per ottenere una scrittura piu` sintetica, e` conveniente omettere in casi che
conducono a Fail.
minux x O = x
minus (S x) (S y) = minus x y
Per esempio al posto di scrivere
minus x y = fcase y of O -> x
S y1 -> fcase x of
O -> Fail
S x1 -> minus x y
viene tradotta in
minus x y = fcase y of O -> x
S y1 -> fcase x of
O -> Fail
S x1 -> minus x y
Si scrive:
minus x y = fcase y of O -> x
S y1 -> fcase x of
S x1 -> minus x y
Tra le varie computazioni alternative, quelle che portano a fail devono
essere annullate.
P. Di Gianantonio (Udine)
Rewriting Systems
95 / 111
P. Di Gianantonio (Udine)
Come ottenere la traduzione ottimale
Rewriting Systems
Come ottenere la traduzione ottimale
`
Una definizione mediante regole dell’and booleano e:
`
Una definizione mediante regole dell’and booleano e:
and True True = True
and x
False = False
and False x
= False
and True True = True
and x
False = False
and False x
= False
che puo` essere tradotta come:
che puo` essere tradotta come:
and x y = fcase x of True -> fcase y of True -> True
False -> False
False -> False
and x y = fcase x of True -> fcase y of True -> True
False -> False
False -> False
ottimale?
ottimale? No.
P. Di Gianantonio (Udine)
Rewriting Systems
96 / 111
97 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
97 / 111
Traduzione ottimale
Definitional tree
Una traduzione ottimale puo` essere ottenuta attraverso la scelta non
deterministica or
L’insieme di equazioni che definiscono un termine, sono tradotte in
• un termine (albero)
x and y = case x of True -> case y of True -> True
• con connettivi (nodi) i costrutti fcase e or,
• e sottotermini finali (foglie) varianti delle parti destre delle regole.
False -> False
’or’
case y of False -> False
La traduzione e` ottimale, corretta e completa se tutte le destre parti
devono essere inserite, nel punto corretto.
Il costrutto or permette traduzioni ottimali, ma va usato con parsimonia,
porta ad computazioni meno efficienti,
Le sottoespressioni di or devono essere case su variabili differenti.
P. Di Gianantonio (Udine)
Rewriting Systems
98 / 111
Il definitional tree e` una rappresentazione sintetica della traduzione
ottimale.
P. Di Gianantonio (Udine)
Da regole a definitional tree
• se esiste, si considera il primo argomento (quello piu` a sinistra) tra
quelli istanziati (demanded) in ogni regola, quindi:
• si applica un costrutto fcase (branch tree) su esso,
• si ripartiscono le regole in piu` sottoinsiemi,
• si ripete la procedura sui sottoinsiemi,
• altrimenti, si considera il primo argomento tra quelli istanziati in
qualche regola,
• si applica un costrutto or (or tree) con due sottotermini, ottenuti
partizionando l’insieme di regole in due sottoinsiemi:
• il primo contiene le regole che istanziano l’argomento
• il secondo tutte le altre regole.
Dato un insieme di regole, esistono, in generale, diversi possibili
definitional tree associati.
equ
equ
equ
equ
equ
T
x
F
T
F
F
T
x
T
F
x
F
T
T
F
=
=
=
=
=
F
F
F
T
T
L’algoritmo di Curry ne seleziona uno.
Definitional tree diversi possono avere comportamenti differenti rispetto
alla divergenza
• applicando ricorsivamente la procedura sui due insiemi,
• altrimenti, se non esiste nessun argomento da istanziare, le regole
sono immediatamente applicabili.
Rewriting Systems
99 / 111
Da regole a definitional tree
Algoritmo usato da Curry (descrizione sintetica e informale):
Dato un insieme di regole per una funzione f con n argomenti (posizioni):
P. Di Gianantonio (Udine)
Rewriting Systems
100 / 111
Le risposte calcolate, quando generate, coincidano.
Differenze dovuta al comportamento del costrutto or
P. Di Gianantonio (Udine)
Rewriting Systems
101 / 111
Costrutto or
Dalla traduzione ottimale alla strategia di
narrowing
Le implementazioni non rispettano il comportamento teorico.
• comportamento teorico: in A or B genera sia le risposte calcolate da
A che quelle calcolate da B.
• implementazioni: in A or B genera le risposte calcolate da B solo se
la valutazione di A non porta alla divergenza.
Date le regole:
f x
f O
bot
=
=
=
O
S O
bot
nelle implementazioni di Curry, l’esecuzione di f bot diverge, anche se in
teoria puo` terminare con O
P. Di Gianantonio (Udine)
Rewriting Systems
102 / 111
La traduzione ottimale, attraverso il core language, indica in che modo
ridurre un termine con passi elementari.
A piu` alto livello, con minor numero di passi, questa riduzione puo` essere
vista come applicazioni di regole di narrowing.
Con una diversa lettura, una traduzione ottimale (definitional tree) indica
una strategia di riduzione (outtermost needed narrowing).
Ricordiamo che, dato un insieme di regole R, ed un termine t,
una strategia di narrowing definisce:
• che regola Ri applicare,
• in che posizione p del termine applicarla (a che sottotermine),
• con quale unificazione σ, (il needed narrowing non necessariamente
usa l’mgu)
P. Di Gianantonio (Udine)
t
t
p ,Ri ,σ
Rewriting Systems
Ottimalita`
Da definitional tree a strategia di
narrowing
Per ridurre un termine t, non in head normal form, con simbolo principale
una funzione f , considero
• il definitional tree T di f ,
• genero tanti rami di narrowing quanti sono i nodi in T con un pattern
p, di profondita` massimale, che unifichi con t,
• nel caso di nodo terminale (regola), applico la regola mediante
narrowing su tutto il termine,
• nel caso di nodo branch, considero la variabile x selezionata nel
pattern, e l’unificazione σ del pattern p con t, se σ(x ) e`
• un sottotermine t con simbolo principale una funzione, allora applico la
σ e passo a fare il narrowing su t ,
• un sottotermine t con simbolo principale un costruttore, alloro questo
ramo di narrowing fallisce.
P. Di Gianantonio (Udine)
Rewriting Systems
103 / 111
104 / 111
Da un punto di vista intuitivo, il needed narrowing, mediante valutazione
nel core language e` ottimale,
ossia porta a ridurre un termine t in head normal form usando le
istanziazioni piu` generali e un insieme minimo di riduzioni
´
perche:
• la traduzione ottimale mi porta ad applicare le regole, valutando o
istanziando al minimo gli argomenti,
• la riduzione lazy nel core language, porta a valutare solo gli
argomenti strettamente necessari.
Inoltre il needed narrowing e` anche completo, se esiste una sequenza di
passi di narrowing che portano un termine t in head normal form, allora
applicato su t il needed narrowing porta ad una head normal form.
P. Di Gianantonio (Udine)
Rewriting Systems
105 / 111
Needed position
Funzioni induttivamente sequenziali
Presentazione teorica, si dimostra che la strategia needed porta solo a
passi di riduzione strettamente necessari:
La definizione strategia needed e` piuttosto forte.
Definizione
Per regole di riscrittura arbitrarie, strategie di neeed possono non esistere.
Controesempio:
[Neeed position]
• in un termine t una posizione p e` needed se
in ogni riduzione, con regole di riscrittura, normalizzante (in head
normal form),
un discendente del sottotermine t |p funge da redex.
and (and True x) (and True y)
Si consideri anche and (and True x) (and False y)
Definizione
• un passo di narrowing t
` needed se
p ,R ,σ t e
per ogni τ, p e` una posizione needed in t στ .
[Regole induttivamente sequeziale] Un insieme di regole per una funzione
f e` induttivamente sequenziale se possiede un definitional tree senza nodi
or.
• una strategia di narrowing e` needed se lo e` ogni suo passo.
Insieme di regole induttivamente sequenziale e` anche ortogonale (le
regole non si sovrappongono), ma non il viceversa.
Esempi: x <= add y z
add 1 x <= add y (add y z)
add 1 x <= mult 2 (add y z)
P. Di Gianantonio (Udine)
Rewriting Systems
106 / 111
P. Di Gianantonio (Udine)
Needed narrowing
Rewriting Systems
107 / 111
Constrained equality =:=
Il costrutto =:= non puo` essere ridotto al solo needed narrowing.
La regola x =:= x = success
Theorem
• non e` lineare sinistra,
La strategia di riduzione needed narrowing su funzioni induttivamente
`
sequenziali e:
• non ha un definitional tree associato.
Il costrutto =:= non puo` essere ridotto ad un termine del core language.
Es x =:= add y 3 deve restituire
success con l’unificazione x / (add y 3)
Nessuna traduzione, nel core language, di =:= puo` portare a questo
risultato.
Infatti le sostituzioni generate dal needed narrowing istanziano usando
sempre nuove variabili.
Ossia il needed narrowing su un termine t genera sostituzioni nella forma
(x1 /t1 , . . . xn /tn ), dove le variabili in t1 , . . . tn sono diverse dalle variabili in t
e diverse tra loro.
• deterministica,
• needed: vengono eseguiti solo passi needed,
• completa: per ogni termine s se (s ∗σ t ) con una qualsiasi
sequenza di passi di narrowing, e t e` in normal form, allora anche
esiste t normal form t.c. s ∗σ t attraverso passi di needed
narrowing e σ σ .
P. Di Gianantonio (Udine)
Rewriting Systems
108 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
109 / 111
Semantica di =:=
Flexible and rigid
Nel valutare in comportamento di un termine e` importante valutare se il
comportamento delle funzioni e` rigido o flessibile.
Il comportamento della constrained equality necessita di una descrizione
ad hoc.
Per valuare
s =:= t
• la si porta in normal form s’ =:= t’, emediante il needed narrowing
• si applica l’algoritmo di unificazione sulle forme normali.
• rigido: non si istanziano le variabili logiche, se un argomento needed
e` una variabile logica, la computazione si sospende. Esempi: le
operazioni su valori numerici, l’uguaglianza booleana ==, il costrutto
case.
• flessibile: se un argomento needed e` una variabile logica la istanzia,
applica il narrowing.
Esempi: funzioni definite per pattern matching.
In una descrizione completa dell’algoritmo di narrowing, si aggiunge
un’etichetta ai nodi branch nei definitional tree.
• flessibile: applico il narrowing,
• rigido: nel caso di variabile logica sospendo la computazione.
Corrispondenti a due versioni del costrutto case.
P. Di Gianantonio (Udine)
Rewriting Systems
110 / 111
P. Di Gianantonio (Udine)
Rewriting Systems
111 / 111

Download Report