• Contenuto della Tesi di Laurea: "Riscrittura di Lambda-Grafi: Condivisione ed Ottimalità"

Un interprete ottimale secondo Levy' per il Lambda-Calcolo, e la funzione di decondivisione semantica.

Oggetto della Tesi è la dimostrazione di esistenza costruttiva per una funzione di visita semantica per lambda-grafi e la costruzione di un riduttore ottimale per il Lambda Calcolo.

I Lambda termini vengono dotati di una struttura a grafo, detta lambda-grafo, che permette sia una condivisione, o "sharing of computation", sia la gestione di una ottimalita' rispetto al numero di operazioni, o riduzioni, necessarie alla eventuale terminazione del calcolo.

lambda-grafo

Nell'ambito della teoria del Lambda Calcolo , prima, e in quello dei sistemi di riscrittura piu' generali poi, si e' data una caratterizzazione teorica dei requisiti a cui deve soddisfare un generico algoritmo per la minimizzazione del numero di riduzioni.
Esistono algoritmi in cui il numero degli "effettivi" passi di calcolo (riduzioni di famiglie di redessi ) e' minimizzato ma, al contempo,
il numero di applicazioni di regole ausiliarie aumenta in modo considerevole ( a volte in modo super-esponenziale ): tali algoritmi si compongono di un insieme fissato di regole di riscrittura di grafi in cui un sottoinsieme proprio di queste e' ottimale.
La restrizione del sistema di riscrittura al sottoinsieme di regole ottimali ottiene lo scopo prefissato: non esiste alcun processo di
riduzione normalizzante che raggiunge la forma normale in un numero inferiore di beta-riduzioni.

Il calcolo si ferma pero' ad un grafo.
Come recuperare la informazione intrinseca contenuta nel lambda-grafo per ottenere il lambda-termine corrispondente ?
Se si intende per "decondivisione" questa operazione di reinterpretazione allora si puo' riformulare la domanda in questo modo:

Come "decondividere" un lambda-grafo ?

Si puo' procedere in due modi distinti: o considerare il sistema di riscrittura ampliato alle regole che permettono la decondivisione "all'interno" del sistema stesso, oppure cercare una funzione di visita a carattere semantico che scelga quella successione ben definita di vertici sul lambda-grafo che corrisponde in maniera univoca al lambda-termine rappresentato dal grafo stesso.
Questa funzione deve essere ben definita su lambda-grafi ed essere coerente con il sistema di riscrittura stesso: dopo ogni applicazione delle regole la funzione deve fornire il corretto lambda-termine corrispondente.

Il primo risultato della Tesi e' quello della costruzione di un interprete o riduttore ottimale secondo Levy (Graph Optimal Lambda-Reducer) per un linguaggio, che e' una versione ampliata del Lambda Calcolo puro, la sintassi per i programmi e' basata su quella della "CuCh-machine". In questo linguaggio si possono scrivere funzioni e dati in forma di lambda-termini e si puo' procedere al loro calcolo attraverso il sistema di riscrittura di Guerrini.
Alcuni esempi di calcoloi dimostrano comunque che esiste una inefficienza intrinseca del sistema di riscrittura non ottimale.
Se si calcola la forma normale di un termine, senza fermarsi a considerare la forma normale a grafo, si deve effettuare un numero molto grande di regole di riduzione ausiliarie: il che elimina totalmente i benefici derivanti dall'uso di un sottosistema ottimale secondo Levy.
Il comportamento invece cambia drasticamente se si considera solo il raggiungimento delle forme normali a grafo con il sottosistema ottimale: Il numero di riduzioni nel sottosistema ottimale, rimane cosi' "lineare" con la "dimensione" del lambda-termine
(si veda l'articolo di Asperti "P=NP up to sharing").

I risultati ottenuti dalla implementazione del riduttore ottimale confermano i risultati teorici e hanno fornito, precedendola, una spinta verso la costruzione della funzione di decondivisione semantica. Questa funzione e' una funzione definita ricorsiva sui nodi del lambda-grafo ad un parametro : esso simula la semantica dei contesti necessaria alla corretta interpretazione del grafo come lambda-termine.

Si puo', allora, dare un metodo strutturato per il calcolo di forme normali per lambda-termini. Dapprima si trasformano le funzioni (lambda-termini) in grafi (lambda-grafi), poi si procede al calcolo in un sistema di riscrittura ottimale e la funzione di decondivisione semantica permette il recupero, ad ogni passo, del risultato intermedio. Questa funzione, evitando le riscritture necessarie alla decondivisione, fornisce anche un metodo generalmente piu' efficiente per la implementazione di un riduttore per il Lambda Calcolo.

• Il riduttore ottimale:

Il riduttore, che in effetti è un interprete, è stato scritto in linguaggio C (Si è usato un compilatore Gnu-C su piattaforme Sun e PC-Linux-Dos). Le parti di riconoscimento sintattico ed analisi lessicale, sono state realizzate con i generatori Flex (lex) e Bison (yacc).

La fase di riconoscimento sintattico , attraverso l'analizzatore lessicale ed il parser LALR , permette , nella fase di input , di trasformare
i lambda-termini in lambda-alberi. Il processo di valutazione inizia attraverso il comando eval che riceve come argomento
un nodo stack. Questo nodo \e' identificato attraverso la linea di programma, il nome di una variabile o l'ultimo (last) elemento dello
stack stesso.

I comandi principali permettono la valutazione (eval) di un lambda-termine o variabile definita, il calcolo della forma normale a grafo o ad albero e la possibilità di effettuare un "read-back" sintattico o semantico (nella versione rilasciata la funzione di decondivisione semantica non è implementata nella sua generalità ma solo una sua versione semplificata che permette la decondivisione ad esempio di numerali di Church).

Sono presenti inoltre alcuni comandi di Trace, di Log su file, di lettura da file esterni, di settaggio del prompt.

#
# Esempio di programma in GoLRed.
#.
uno := \x y . x y;
due := \x y . x(x y);
tre := \x y . x(x(x y));
#
# Definizioni di combinatori (da CuCH)
#.
A := lmb: x y z w . x z (y z w);
B := lmb: x y z . x (y z);
C := lmb: x y z . x z y;
C* := lmb: x y . y x;
D := lmb: x y z . z x y;
S := lmb: x y z . x z (y z);
W := lmb: x y . x y y;
W* := lmb: x . x x;
I := lmb: x . x;
#
# ...................................................
a1:= due due;
a2:= tre due;
# ................................Program starts here
#
# ................................Echo on file (gral.log)
@set_echo ON;
#
# ................................No direct Read_back (Graph Normal Form)
@treeNF NO;
#
# ................................defines a variable
V_1 := due due;
#
# ................................evaluates it
@eval V_1;
# ................................print the variable structure on terminal and on file
@print V_1;
# ................................executes syntactical read-back
@read_back;
#
@quit;

Download:

Si può avere GoLRed compilato per SunOs4.1, Linux e Dos (Windows), o anche i sorgenti: scrivetemi a maz@dsi.uniroma1.it

• "La CuCh machine"

CuCh machine home page.....