Ottimalità dell'ottimalità — Complessità della riduzione su grafi di condivisione
Abstract
Trent’anni or sono il concetto di ottimalità venne formulato in
senso teorico da Lévy, ma solo un decennio dopo Lamping riesce a
darne elegante implementazione algoritmica. Realizza un sistema
di riduzione su grafi che si scoprirà poi avere interessanti analogie
con la logica lineare presentata nello stesso periodo da Girard.
Ma l’ottimalità è davvero ottimale? In altre parole, l’implementazione
ottimale del λ-calcolo realizzata attraverso i grafi di condivisione,
è davvero la migliore strategia di riduzione, in termini di complessità?
Dopo anni di infondati dubbi e di immeritato oblìo, alla conferenza
LICS del 2007, Baillot, Coppola e Dal Lago, danno una prima risposta
positiva, seppur parziale. Considerano infatti il caso particolare delle
logiche affini elementare e leggera, che possiedono interessanti proprietà
a livello di complessità intrinseca e semplificano l’arduo problema.
La prima parte di questa tesi presenta, in sintesi, la teoria dell’ottimalità
e la sua implementazione condivisa.
La seconda parte affronta il tema della sua complessità, a cominciare da una
panoramica dei più importanti risultati ad essa legati. La successiva
introduzione alle logiche affini, e alle relative caratteristiche, costituisce
la necessaria premessa ai due capitoli successivi, che presentano una
dimostrazione alternativa ed originale degli ultimi risultati basati appunto
su EAL e LAL. Nel primo dei due capitoli viene definito un sistema intermedio
fra le reti di prova delle logiche e la riduzione dei grafi, nel secondo sono
dimostrate correttezza ed ottimalità dell’implementazione condivisa per mezzo
di una simulazione.
Lungo la trattazione sono offerti alcuni spunti di riflessione sulla dinamica
interna della β-riduzione riduzione e sui suoi legami con le reti di prova della
logica lineare.