Linguaggi di programmazione - Semantica Operazionale Strutturata

[Abbath]

Salve a tutti, vorrei chiedervi se potreste aiutarmi a capire come si risolve l'esercizio seguente.

Ringrazio anticipatamente chiunque possa darmi una mano.
Grazie

[onlyReferee]

Bisogna che cerchi di applicare le regole presenti "a ritroso" e vedere, tra i vari branch che ottieni, quale di essi ti permette di non ottenere una contraddizione (ergo ottenere il vero senza lasciare la computazione delle formule incompiuta per mancanza di regole da applicare).

[Abbath]

Ti ringrazio per la risposta. So che non è un esercizio difficile, so che devo usare le regole per riscrivere a ritroso l'espressione e trovarne il tipo finale, ma non riesco a mettere le cose insieme. Sono completamente bloccato e non riesco a trovare esercizi con la soluzione in rete. La spiegazione nel libro o nelle slides di riferimento è un centesimo della complessità di questo esercizio, e non avendo soluzioni di riferimento non riesco a capire il meccanismo.
Se hai la pazienza di mostrarmi la soluzione (o una parte di essa) ti ringrazierei tantissimo, mi sarebbe molto utile per uscire dal buio in cui sto arrancando.

[onlyReferee]

Allora, per applicare correttamente le regole a partire dalla tua espressione bisogna che individui passo per passo quale applicare (ovviamente a ritroso come dicevamo). Per far ciò bisogna vedere l'espressione corrente sempre "a livello quanto più globale possibile", ossia individuando qual è l'operatore più esterno applicato. Suggerimento: la prima regola da applicare è quella con il $rec$. Da lì basta che individui chi è, rispetto alla tua espressione, $y$ e chi è $\lambda x.t$. Poi procedi applicando, ove possibile, le regole opportune a $y$ e $\lambda x.t$.

[Abbath]

Si capisco con che cosa devo iniziare e come si usano le regole, ma non capisco la tecnica con la quale costruire questo albero di derivazione. Non so se devo sostituire i costrutti dell'espressione alle regole, oppure usare solo le regole tali e quali per costruire l'albero analizzando l'espressione. Inoltre non capisco dove utilizzare il let-in..

[onlyReferee]

"Abbath":[...]Non so se devo sostituire i costrutti dell'espressione alle regole, oppure usare solo le regole tali e quali per costruire l'albero analizzando l'espressione. Inoltre non capisco dove utilizzare il let-in..

Prima bisogna che applichi le varie regole e, appena fatto, ti segni a fianco il tipo corrispondente. Ti riporto di seguito ciò che si ottiene applicando la $rec$ (attenzione perché poi ti accorgerai di volta in volta che sviluppi le formule come, una volta ultimato, quando procedi all'indietro bisogna che procedi andando a sostituire i tipi trovati con i relativi valori):
$
\frac{\frac{...}{f: \tau} \qquad \qquad \frac{...}{\lambda : x.if fst(x) \quad then \quad (rec \quad g.(\lambda y.fst(y) + snd(y))x) \quad else (f(fst(x) - 1, fst(x) \times snd(x))) : \tau}}{rec f.(\lambda:x.if fst(x) then (rec \quad g.(\lambda y.fst(y) + snd(y))x) else (f(fst(x) - 1, fst(x) \times snd(x)))):\tau}
$
Chiaramente il nostro obiettivo sarà capire a cosa corrisponde $\tau$ ma per scoprirlo bisogna appunto applicare le regole fino in fondo sostituendo poi i vari tipi corrispondenti. Ad esempio se poi vogliamo applicare la regola corrispondente per il termine $\lambda x.if [...]$ noterai subito che il tipo da sostituire al posto del $\tau$ sarà $\tau_1 \rightarrow \tau_2$.

[Abbath]

Scusa se rispondo così tardi sono stato parecchio impegnato, appena posso riprovo cercando di seguire il tuo suggerimento e posto la mia soluzione! Grazie ancora!

[onlyReferee]

Certo, così confrontiamo i risultati ottenuti, volentieri. Un corso di logica matematica e due sui fondamenti dei linguaggi di programmazione spero mi siano serviti.

[Abbath]

Ciao, scusami se metto la foto della mia risoluzione in allegato (ci metterei sei mesi a farlo in latex).
Ho numerato le righe così magari viene meglio se mi devi indicare qualcosa.
Procedendo all'indietro direi che il tipo è: se la if è true sarà int, se è else sarà di tipo T1 * T2 (ossia una tupla int*int).