Si richiede di scrivere un interprete per un linguaggio (linguaggio oggetto) lambda-calc+ che contiene il lambda calcolo e alcune costanti e funzioni primitive quali i numeri, i valori "vero" e "falso", le operazioni aritmetiche e di confronto sui numeri, e l'if-then-else.
La scelta precisa del linguaggio oggetto e' lasciata libera, a condizione
che contenga il lambda-calcolo e che le funzioni primitive siano
sufficienti a scrivere programmi quali ad es.
il fattoriale con uno stile "tradizionale" (cioe' senza ricorrere
ai complicati encodings dei numeri e funzioni numeriche nel lambda calcolo).
In particolare, e' lasciata libera la scelta di avere o meno il tipo
di dato tupla.
La sintassi
Una possibile grammatica per le espressioni di tale linguaggio
(comprendente le tuple) e':
Un'altra possibile grammatica per le espressioni di tale linguaggio
(senza le tuple) e':
Il passo di riduzione, che indicheremo con -->,
e' specificato dalle seguenti regole (piu', eventualmente, la regola per le
tuple):
Nella regola beta, M[N/x] rappresenta il termine ottenuto da M sostituendo N al posto di tutte le occorrenze libere di x, eventualmente ridenominando tramite alfa-conversione i sottotermini di M della forma (lambda y. M'), con y appartenente a N, per evitare il problema del "capture" (variabili libere di N che diventano legate dopo la sostituzione).
Eval_prim si occupa della valutazione delle espressioni che contengono una funzione primitiva applicata a top-level. Potra' essere definita con una semantica a piccoli passi oppure a grandi passi, a piacere (cioe': in (Eval_prim M N), N puo' essere un'espressione ottenuta da M valutando alcune operazioni, e ulteriormente riducibile, oppure puo' essere la forma normale di M, cioe' una costante numerica o booleana.)
La riduzione in forma normale e' specificata dalla relazione
Per la valutazione del progetto, e' richiesto di presentare
il codice del programma, commentato, ed eventualmente una descrizione
della rappresentazione scelta per il linguaggio oggetto.
Inoltre si dovranno presentare delle prove di sessione, in cui
venga calcolata la forma normale di alcune espressioni, fra cui
almeno una contenente una funzione ricorsiva tipo il fattoriale.
Notare che il linguaggio oggetto non ha il costrutto let, quindi per
descrivere funzioni ricorsive si dovra' fare uso della tecnica vista a
lezione, basata sull'operatore di punto fisso
| X == Y | Ha successo sse X e Y rappresentano sintatticamente lo stesso termine (tenuto conto dei legami creati dalle unificazioni eseguite fino a quel momento) |
| X \==Y | Ha successo sse X e Y non rappresentano sintatticamente lo stesso termine, cioe' sse X == Y fallisce |
Alternativamente, si puo' implementare la creazione di un identificatore
nuovo tramite assert e retract. Assumendo di rappresentare un
identificatore con ide(n),
dove ne' un numero, il predicato newide(ide(n)), che genera ogni volta un
identificatore nuovo, potra' essere definito da:
newide(ide(N)) :- retract(numero(N)), M is N+1,
assert(numero(M)).
numero(0).
La combinazione delle regole nu, mu e csi puo' provocare delle sequenze infinite di riduzioni, anche per espressioni che possono essere ridotte a forma normale applicando le regole in ordine diverso, cioe' applicando sempre la beta-rule e la prim-rule quando queste possono essere applicate. Cio' fa parte della semantica del lambda calcolo, e va quindi considerata una caratteristica "naturale" dell'interprete. E' pero' opportuno scrivere l'interprete in modo che esso segua per primo il cammino che porta alla forma normale (se questa esiste), invece di quelli infiniti. A questo scopo, tenendo presente che il Prolog segue una strategia di ricerca depth-first, bastera' scrivere le clausole per il passo di riduzione in modo che la beta-rule e la prim-rule siano considerate prima della nu e della mu.
Per avere un idea della lunghezza del progetto: La docente ha effettuato un'implementazione in Prolog delle relazioni richieste, con un programma che consiste di 15 clausole, piu' quelle relative alla valutazione delle funzioni primitive.
Per quanto riguarda il problema delle sequenze infinite di riduzioni vale quanto detto sopra per il Prolog (anche il Lambda Prolog segue una strategia depth-first).
Grazie al suo potere espressivo, il Lambda Prolog e' il linguaggio che permette l'implementazione piu' compatta delle relazioni richieste. La docente ha effettuato una tale implementazione con un programma che consiste di sole 7 clausole, piu' quelle relative alla valutazione delle funzioni primitive, piu' le dichiarazioni kind e type.
Per quanto riguarda la riduzione a forma normale:
Se le funzioni primitive sono tutte deterministiche,
allora si pou' sfruttare la proprieta' di confluenza (debole)
del lambda-calcolo che garantisce che tutte le forme normali coincidono.
Quindi bastera' arrestarsi quando si trova una forma normale,
e restituire quella (l'unica cosa a cui occorre fare attenzione e'
l'ordine in cui vengono generati nella lista gli E' detti sopra, per evitare
il problema delle sequenze infinite di riduzioni. Vedi quanto detto a proposito del Prolog).
Se invece si vuole arricchire il linguaggio con primitive
non-deterministiche
(ad es. una primitiva random_bool
che restituisce non-deterministicamente vero o falso)
allora c'e' il problema che le forme normali possono essere
infinite. Una funzione che restituisca tutte le forme normali,
in tal caso, puo' essere implementata
solo in modo lazy. Dovranno quindi essere usate le tecniche viste a
lezione per simulare la valutazione lazy in ML.
Per quanto riguarda la rappresentazione delle lambda-astrazioni, ML offre i tipi di ordine superiore, come il Lambda Prolog, per cui si puo' effettuare la codifica come detto per il Lambda Prolog, e sfruttare esattamente lo stesso meccanismo per l'implementazione della beta-rule. A differenza del Lambda Prolog pero', in ML non e' affatto banale, con questa rappresentazione, implementare la csi-rule (secondo me e' impossibile, a causa della non disponibilita' del pattern-matching sui tipi funzionali). Poiche' lo svolgimento del progetto in ML e' gia' reso abbastanza complicato dal problema del non-determinismo menzionato sopra, si accettano progetti che omettono l'implementazione della csi-rule (l'interprete risultante dovra' essere completo solo rispetto alle riduzioni alla weak-normal form).
Alternativamente, si potra' usare la stessa rappresentazione first-order
che si userebbe in Prolog, con un'analoga implementazione della beta-rule.
C'e' pero' il problema che ML non mette a disposizione un meccanismo
primitivo per generare nuovi identificatori (necessari per l'eventuale
alfa-conversione). Dovremo realizzare allora una funzione
newide che,
ogni volta che viene invocata, restituisce un nuovo identificatore.
Un modo di farlo e' quello di sfruttare la possibilita' di side-effect
offerta dal tipo reference, e rappresentare
i nuovi identificatori come ide(n), dove n e' un numero. La funzione newide
potra' allora essere definita come:
val newide =
let val numero = ref 0
in fn() => (numero := !numero + 1 ; ide(!numero))
end
Con questa definizione, la dichiarazione let x =
newide() ...
assegnera' ad x un nuovo
identificatore ogni volta che viene valutata.
La sintassi dei tipi dovra' contenere i seguenti (piu' eventualmente i tipi
delle tuple e una rappresentazione dell'errore)
Per la valutazione del progetto, e' richiesto di presentare
il codice del programma, commentato, ed eventualmente una descrizione
della rappresentazione scelta per il linguaggio oggetto.
Inoltre si dovranno presentare delle prove di sessione, in cui
venga calcolato il tipo di alcune espressioni, fra cui alcune
con tipo polimorfo di ordine superiore.
Notare che l'operatore di punto fisso
non e' tipabile, quindi ovviamente non e' richiesto calcolare il tipo di
espressioni rappresentanti funzioni ricorsive
L'implementazione della regola app richiede di effettuare l'unificazione del tipo calcolato per N con una parte del tipo calcolato per M (cioe': calcola il tipo T1 di N, calcola il tipo T3 di M, controlla che T3 sia della forma T1'->T2, e unifica T1 con T1'). Sfortunatamente, non si puo' usare direttamente il meccanismo di unificazione fornito dal Prolog perche esso non e' completamente corretto, non essendo implementato l'occur-check (ad esempio il Prolog permetterebbe di unificare i tipi T1 e T1->T2, il che e' ovviamente scorretto). Occorrera' quindi modificare l'algoritmo di unificazione del Prolog per tener conto dell'occur check. In altre parole, occorre definire ed usare un predicato di unificazione esplicita, unify(X,Y), che ha successo sse X e Y rappresentano tipi unificabili tenendo conto dell'occur check. A tale scopo torneranno utili le metaprimitive == e \== (vedi spiegazione del progetto 1).
Se abbiamo lo stesso identificatore in lambda astrazioni diverse (come ad esempio nell'espressione (lambda x.x)(lambda x. (x 1))), occore stare attenti a non associare le due occorrenze bound di x allo stesso tipo (nell'esempio, la seconda x deve avere tipo integer -> A, e la prima (integer -> A) -> A ). Per aggirare il problema, la cosa piu' conveniente e' alfa-convertire l'espressione iniziale in modo che tutti gli identificatori usati nelle lambda astrazioni siano diversi fra loro. Anche in questo caso sara' conveniente rappresentare gli identificatori del linguaggio oggetto con variabili Prolog, cosi' da poter usare il meccanismo del Prolog per generare nuove variabili.
Per avere un'idea della dimensione del progetto: La docente ha effettuato un'implementazione Prolog del type system con un programma contenente 26 clausole, piu' quelle per le primitive. Di queste 26, 11 sono per la ridefinizione dell'algoritmo di unificazione (per le espressioni che rappresentano tipi), e 8 per la alfa-conversione dell'espressione di partenza.
La docente ha effettuato un'implementazione Lambda Prolog del type system con un programma contenente solo 3 clausole, piu' quelle per le primitive, piu' le dichiarazioni kind e type.
Poiche' anche ML consente di manipolare tipi di ordine superiore,
si potrebbe pensare di usare la stessa rappresentazione delle
lambda-espressioni suggerita per Lambda Prolog e di seguire la stessa idea
per l'implementazione di abs.
Purtroppo pero' ML non ha un meccanismo automatico di ragionamento
ipotetico (per trattare l'ipotesi |- y : T1), e quindi dovremo
usare esplicitamente l'ambiente. La regola sara' quindi della forma:
Alternativamente si possono rappresentare le lambda astrazioni con termini del prim'ordine come in Prolog. In questo caso sara' utile effettuare la alfa-conversione dell'espressione iniziale in modo che tutti gli identificatori delle lambda astrazioni siano distinti fra loro (vedi quanto detto per il Prolog).
Poiche' in ML non esiste un meccanismo di unificazione, la dovremo implementare. Si suggerisce quindi di suddividere il problema in due problemi principali:
Lo schema di funzionamento del type system sara' quindi il seguente. Data un'espressione M:
In questa implementazione, sara' necessario sia generare nuovi identificatori (del linguaggio oggetto), sia nuove variabili di tipo (parametri). Per fare questo, si consiglia di usare la newide (vedi spiegazione del progetto 1) e una funzione newpar definita analogamente.
Si prevede che un'implementazione ML del type system richieda 40-50 righe di codice (tutto compreso), usando la prima delle rappresentazioni possibili per le lambda astrazioni, cioe' quella higher-order. Piu' o meno la stessa dimensione dell'implementazione Prolog: In ML dobbiamo implementare esplicitamente la creazione di nuovi identificatori e parametri, e l'applicazione di una sostituzione ad una espressione di tipo (necessaria per applicare theta a T nel passo 4). Inoltre l'implementazione dell'algoritmo di unificazione e' leggermente piu' lunga (in Prolog e' facilitata dal fatto che in certi passi dell'algoritmo possiamo sfruttare l'unificazione del linguaggio stesso). In compenso, con la rappresentazione higher-order delle lambda astrazioni, non e' necessario effettuare l'alfa-conversione dell'espressione iniziale.
Si richiede di definire, in C++, la classe degli "Alberi binari razionali". Si ricorda che un albero razionale e' un albero, possibilmente infinito, i cui sottoalberi possono avere solo un numero finito di forme diverse. Un modo di rappresentare gli alberi razionali e' quello di considerare alberi binari in cui, in un nodo n, il puntatore al sottoalbero sinistro o destro di n puo' anche "tornare indietro" e puntare ad un antenato di n. (In realta' tutti i grafi finiti diretti e connessi e con un nodo selezionato rappresentano alberi razionali, ma e' meglio restringersi alla rappresentazione detta prima per evitare i problemi di sharing quando dobbiamo fare il garbage collection).
Le informazioni della classe devono essere nascoste in modo opportuno, in modo che chi usa oggetti di quella classe non possa creare strutture circolari che rappresentano grafi arbitrari.
Per la valutazione del progetto, e' richiesto di presentare il codice del programma, commentato (e commentato bene, data la poca leggibilita' del C++), ed una descrizione delle operazioni principali. Inoltre si dovranno presentare delle prove di sessione, in cui vengano costruiti e stampati alcuni alberi, fra cui naturalmente almeno alcuni infiniti.
Opzionale: Gli alberi razionali sono strutture disponibili in Prolog II, una versione estesa del Prolog. Chiaramente, la presenza di queste strutture implica una modifica dell'algoritmo di unificazione. Quello che abbiamo visto a lezione e' basato sul concetto di sostituzione come funzione da variabili in termini finiti; Se si considerano anche termini (alberi) razionali infiniti, ovviamente il concetto di unificazione cambia, e si potranno unificare, ad esempio, il termini f(x,a) e f(g(b,x),a). Lo mgu sara' una sostituzione che lega x ad un termine infinito della forma g(b,g(b,g(b,...))))), che e' un albero razionale rappresentabile con l'equazione x=g(b,x).
Sara' considerato opzionale, ma valutato molto positivamente nel caso che venga fatto, l'arricchimento del progetto con l'implementazione (sempre in C++) dell'algoritmo di unificazione del Prolog II.
Per altre informazioni riguardo questo progetto, leggere le "Frequently Asked Questions".