linguaggio Fun

È un superlinguaggio del linguaggio Exp. La sua grammatica contiene tutti i suoi elementi e le funzioni unarie.

$$M,N::=5\mid 7\mid \dots \mid N+M\mid \text{let}x=M\text{in}N\mid Fnx⟹M\mid MN$$

$MN$ è l’applicazione.

L’applicazione di funzione è associativa a sinistra: ad esempio $(MN)L$ vuol dire $M$ passato a $N$ applicato a $L$. Cioè se avessimo $\underset{M}{\underbrace{(\text{Fn}x⟹x)}}\underset{N}{\underbrace{(\text{Fn}x⟹x+1)}}\underset{L}{\underbrace{7}}$, dovremmo passare $N$ (la funzione successore) come oggetto a $M$ (la funzione identità). Otteniamo $N$ applicato a $7$, quindi $MNL$ restituisce $8$.

Dobbiamo cambiare il dominio semantico $E$ di $E⊢M⇝v$ rispetto a com’era in Exp.

Il problema di $MN$ è così definito si può applicare un intero a un altro intero, non solo funzioni, ad esempio $57$ (5 applicato a 7, non 57). Oppure $5(\text{Fn}z⟹z+1)$ (funzione applicata a un intero) che è sintatticamente ben costruito ma non ha senso. La semantica operazionale non potrà dargli un valore, perché l’albero di derivazione si bloccherà. Serve la ŧeoria dei tipi per risolvere parzialmente questo problema, ma per ora siamo in un universo non tipato.

Esempi:

$$\underset{M}{\underbrace{(\text{Fn }x⟹(\text{Fn }z⟹xz))}}\underset{N}{\underbrace{(\text{Fn }y⟹y+1)}}\underset{L}{\underbrace{7}}$$ $$⇝\underset{MN}{\underbrace{(\text{Fn }z⟹((\text{Fn }y⟹y+1)z))}}\underset{L}{\underbrace{7}}$$ $$⇝(\text{Fn }y⟹y+1)7$$ $$⇝7+1$$ $$⇝8$$

---

$$(\text{Fn}x⟹(\text{Fn}y⟹x))7⇝\text{Fn}y⟹7$$

---

Possiamo creare funzioni binarie con la curryficazione componendo funzioni unarie.

$$\text{Fn}x⟹\text{Fn}y⟹x+y$$

Il curry di una funzione è da $A\wedge B\to C$ a $A\to (B\to C)$ e la uncurryficazione è il contrario.

---

Bisogna cambiare l’insieme $\text{val}$:

$$\text{val}=\mathbb{N}\cup (\text{Val}\times \text{Fun}\times \text{Exp})$$

I valori funzionali saranno triple $(X,M,E)$ definite chiusure: variabile, elemento del linguaggio (pezzo di sintassi) e ambiente.

Regole di inferenza aumentate: (eager statica)

$$\{\begin{array}{l}E⊢k\to k\\ E⊢x\to v(\text{se}E(x)=v)\\ \frac{E⊢M\to v_{1}E\to N\to v_2}{E⊢M+N\to v}(\text{se}{v}_1+v_2=v)\\ \frac{E⊢M\to vE(x,v)⊢N\to v^{\prime }}{E⊢\text{let}x=M\text{in}N\to v^{\prime }}\end{array}$$ $$E⊢\text{Fn}x⟹M⇝(x,M,E)$$

Call by value

$$\frac{E⊢M\to (x,M^{\prime },E^{\prime })E(x,v)⊢N\to v}{E⊢MN\to }$$

Let non serve più

$$\text{let}x=M\text{in}N\equiv (\text{Fn}x⟹N)M$$

All’estremo, si può fare a meno del + e a meno dei numeri, usando i numeri di Church. Si ottiene il lambda calculus.

---

todo

in eager va in loop infinito (effetto computazionale che introducono le funzioni) e non da un valore, mentre in lazy.

---

let x = M in N è operazionalmente equivalente ($\equiv$) a (fn x -> N)M in un mondo non tipato, dove in let x = M in N possiamo avere il polimorfismo, mentre in (fn x -> N)M no.