programmazione logica (inferenza di tipo à la type-classes)
Riflessione computazionale
Bello:
nella teoria dei tipi dimostrare 2+3=3+2 è facile,
o meglio, la dimostrazione è molto corta apply: erefl
tale dimostrazione non dipende dalla taglia delle espressioni
coinvolte, ie rimane triviale anche per 2+3+4+5=5+2+3+4
Meno bello:
il calcollo è completo su termini chiusi, se sono presenti
variabili dobbiamo ragionare per induzione o riutilizzare lemmi
dimostrati in precendenza, eg x + 0 = x
la taglia della dimostrazione dipende però dal numero di passi
da fare, eg (x + 0) + 0 = x richiede 2 riscritture
Osservazione:
l'esecuzione di un programma p non richiede una prova
p x = y
e non importa quanti passi di esecuzione p faccia
la prova di p x = y è sempre erefl
Idea: potremmo scrivere un programma che fa la dimostrazione
(quando questa è ripetitiva).
Per empio p potrebbe prendere una expressione in
un monoide e metterla in forma normale, e.g.
x + 0 + (y + 0) ----> x + y
Iniziamo col dare una rappresentazione concreta (un dato
induttivo) alle espressioni nel monoide.
Intepretazione
Il termine x + (0 + y) è di tipo nat ed è
un termine che potremmo trovare in un goal.
La sua rappresentazione sintattica Op (Value x) ..
non ha tipo nat, anche se rappresenta un termine
di tale tipo.
Scriviamo una funziona che interpreta una
espressione sintattica in un monoide
Normalizzazione
Op Identity x --> x
Op x Identity --> x
Op x (Op y z) --> Op (Op x y) z
Correttezza dell'algoritmo di normalizzazione
Reificazione
Non è una funzione delle teoria dei tipi:
la teoria quozienta i termini wrt il calcolo
1 + 1 e 2 sono indistinguibili
ma Op (Value 1) (Value 1) e Value 2 sono
ben diversi!
quello che è preservato è il significato (interpretazione)
Soluzione: la funzione di reificazione la scriviamo un
linguaggio che non è la teoria dei tipi ;-)
Fortuna: non ci interessa dimostrarla corretta, basta
che lo sia in pratica.
Esercizio:
aggiungere un elemento assorbente
al monoide (sintassi, interpretazione, normalizzazione,
prova di correttezza, codice quote e codice monoid)
Inductive Syntax A :=
| Identity
| Annihilator
| Value (a : A)
| Op (m1 : Syntax A) (m2 : Syntax A).
Arguments Value {_} a.
Arguments Op {_} m1 m2.
Arguments Identity {_}.
Arguments Annihilator {_}.
Fixpoint interp {A} op id abs (m : Syntax A) :=
match m with
| Identity => id
| Annihilator => abs
| Value x => x
| Op l r => op (interp op id abs l) (interp op id abs r)
end.
Fixpoint norm {A} (m : Syntax A) :=
match m with
| Identity => Identity
| Annihilator => Annihilator
| Value x => Value x
| Op l r =>
let l := norm l in
let r := norm r in
match l, r with
| Annihilator, _ => Annihilator
| _, Annihilator => Annihilator
| Identity, _ => r
| _, Identity => l
| _, Op a b => Op (Op l a) b
| _, _ => Op l r
end
end.
Lemma norm_ok {A op id abs} :
(forall a b c, op a (op b c) = op (op a b) c) ->
(forall a, op id a = a) ->
(forall a, op a id = a) ->
(forall a, op abs a = abs) ->
(forall a, op a abs = abs) ->
forall (m : Syntax A),
interp op id abs m = interp op id abs (norm m).
Proof.
move=> opA idL idR abdL absR m.
elim: m => //= e1 -> e2 ->.
case: (norm e1); case: (norm e2) => //=.
Qed.
Ltac quote op id abs t :=
match t with
| (op ?a ?b) =>
let x := quote op id abs a in
let y := quote op id abs b in
uconstr:(Op x y)
| id => uconstr:(Identity)
| abs => uconstr:(Annihilator)
| ?x => uconstr:(Value x)
end.
Ltac monoid op id abs opA idL idR absL absR :=
match goal with
|- ?a = ?b =>
let x := quote op id abs a in
let y := quote op id abs b in
change (interp op id abs x = interp op id abs y);
rewrite [interp op id abs x](norm_ok opA idL idR absL absR);
rewrite [interp op id abs y](norm_ok opA idL idR absL absR);
compute -[op]
end.