Paradigmi - funzionale Flashcards
Booleani di church
FALSE
FALSE = fn x => fn y => y
Booleani di church
NOT
NOT = fn x => fn y => yx
Booleani di church
- cosa sono
- come sono fatti
I booleani di church sono una rappresentazione dei valori booleani e dei costrutti logici elementari utilizzando solo i lambda termini, ossia :
M ::= x | fn x => M | MN
Quindi in altre parole sono i booleani scritti sotto forma di funzioni.
Booleani di church
If
IF = fn z a b => z a b;
Booleani di church
And
AND = fn xy => x y false
Booleani di church
Or
OR = fn xy => x true y
Booleani di church
True
TRUE = fn x => fn y => x
Numeri di church
- cosa sono
- come sono fatti
I numeri di Church sono una rappresentazione dei numeri naturali come lambda termini, ossia :
M ::= x | fn x => M | MN
In altre parole sono scritti sotto forma di funzioni.
L’idea è quella di rappresentare il naturale i come i applicazioni di un argomento y a una funziona x:
2 = fn xy => x(xy)
In generale quindi:
n-esimo num di church = fn xy => x^n y
Numeri di church - successore
fn zxy => x(zxy)
La funziona successore riceve un numero z e restituisce quel numero che applica x a y una volta in più
Numeri di church - somma
fn zwxy => z(wxy)
La funziona somma riceve due numeri di church x e w, e restituisce quel numero che applica w volte x a y, e poi viene viene passato a z che applica altre z volte x a y
alternativa: fn zw => z succ w
applico z volte la funzione successore a partire da w
Numeri di church - eval (da num di church a numero normale)
fn z => z succ 0
La funzione eval riceve un numero di church in input e restituisce il risultato della funzione successore applicato x volte a 0
Numeri di church - moltiplicazione
fn uvx => u(vx)
u e v sono numeri di churhc. viene restituita la funzione che applica u volte la funziona v all’argomento x
alternativa: fn zw => z (plus w) c0
La funzione times riceve due numeri di church in input e restituisce la funzione che applica x volte plus a
Numeri di church - lave
fun lave 0 = (fn x => fn y => y)
| lave n = succ( lave(n-1));
(* n=2
succ(succ(0))
0 = fn x => fn y => y
succ(z) = fn x => fn y => x (z x y)
succ(succ(z)) = fn x => fn y => x (succ(z) x y)
succ(succ(z)) = fn x => fn y => x (fn x => fn y => x (z x y) x y
succ(succ(fn x => fn y => y)) = fn x => fn y => x (fn x => fn y => x (fn x => fn y => y (x y)) x y
succ(succ(fn x => fn y => y)) = fn x => fn y => x (x y)
Numeri di church - predecessore
S ≡ fn z ⇒ <succ (P2,1 z), P2,1 zi
pred ≡ fn z ⇒ P2,2 (z S hc0, c0i)
Numeri di church - fattoriale
Numeri di church - zero
val zero = fn x => fn y => y
Qual è il suo tipo
a -> b -> b
Numeri di church - uno
val uno = fn x => fn y => x y;
Qual è il suo tipo
(a -> b) -> a -> b
Numeri di church - due
val due = fn x => fn y => x (x y);
Qual è il suo tipo
(‘a -> ‘a) -> ‘a -> ‘a
Numeri di church - tre
val tre = fn x => fn y => x ( x (x y ));
Qual è il suo tipo
(a -> a) -> a -> a
Costrutti logici - TRUE = fn x => fn y => x
Qual è il suo tipo
a -> b -> a
Costrutti logici - FALSE = fn x => fn y => y
Qual è il suo tipo
a -> b -> b
Costrutti logici - NOT = fn x => fn y => yx
Qual è il suo tipo
b -> (b -> a) -> a
Costrutti logici - IF = fn z => fn a => fn b => z a b;
Qual è il suo tipo
(a -> b -> c) -> a -> b -> c
Costrutti logici - AND = fn x => fn y => x y false
Qual è il suo tipo
(a -> (b -> c -> c) -> d) -> a -> d
o anche (‘a -> bool -> ‘b) -> ‘a -> ‘b
Costrutti logici - OR = fn x => fn y => x true y
Qual è il suo tipo
( (a -> b -> a) -> c -> d) -> c -> d
o anche (bool -> a -> b) -> a -> b
Lambda calcolo
[linguaggio+regole+semantica]
Il lambda calcolo è un sistema formale definito dal matematico Alonzo Church nel 1936, sviluppato per analizzare formalmente le funzioni e il loro calcolo.
Le funzioni sono espresse per mezzo di un linguaggio formale, i lambda termini, che stabilisce quali siano le regole per formare un termine:
M ::= x | fn x => M | MN
Il calcolo delle funzioni è espresso con un sistema di riscrittura, che definisce come i termini possano essere ridotti e semplificati.
Utilizziamo una semantica “call-by-value” basata sugli ambienti, le cui regole sono: [var], [fn] ed [appl].
Il sistema lambda introdotto da Church usa normalmente una semantica call-by-name
Cosa cambia tra lambda calcolo e fun
Il lambda calcolo fa a meno delle costanti k, della somma M+N, del let.
Fun e lambda calcolo sono tuttavia equivalenti in quanto:
- le costanti le possiamo rappresentare come numeri di church, ossia possiamo rappresentare numeri tramite funzioni
- la somma si può scivere tramite funzioni e applicarla ai numeri di church
- [let] E|- let x => M in N –> v lo scriviamo come E |- (fn x => N) M –> v
Quali linguaggi abbiamo studiato
Nell’ambito dei paradigmi funzionali abbiamo studiato exp, fun, lambda calcolo, mentre per il paradigma imperativo abbiamo studiato imp e all.
Exp è il linguaggio minimo per studiare la nozione di variabiledi un linguaggio funzionale, come SML, haskell e LISP.
Fun aggiunge ad exp il ocncetto di funzione, ovvero l’astrazione di un termine rispetto a una variabile.
Questi linguaggi astratti ci consentono di studiare il concetto di scoping statico delle variabili, tipico di lingugagi come SML e haskell, e quello dinamico, che viene implementato in parte da LISP o S.
Ci consentono inoltre di studiare le due tipologia di valutazione eager (usata da SML e LISP) e lazy (usata da haskell e S)
schema
Lambda calcolo è invece un linguaggio funzionale equipotente a fun, ma con una sintassi più ristretta: manca delle costanti, della somma e del let, che riesce a rappresentare però tramite funzioni.
Imp è un linguaggio con if-then-else, while, dichiarazione di variabili e assegnamento di un valore a una variabile già dichiarata. In Imp viene introdotto la nozione di locazione, un’astrazione di un indrizzo di memoria).
All (algol-like-language) arricchisce Imp di procedure ed array.
Exp
breve presentazione
Exp è il linguaggio minimo per studiare la nozione di variabile, ossia l’astrazione di un valore, di un linguaggio funzionale, come SML, haskell e LISP.
In exp non si assegna un valore a una variabile, ma è più un concetto di “segnaposto” per un termine (ossia si sostituisce la variabile con un intero termine, invece di assegnarle un valore).
Exp
Sintassi
k è una generica costante
x è una generica metavariabile
M è un generico termine di exp
Exp è definito induttivamente nel seguente modo:
k ::= 5 | 40 | . . .
M ::= k | x | M + N | let x = M in N
Il let è un operatore di sintassi astratta con segnatura:
let: var x exp x exp –> exp
intuitivamente rappresenta un pezzo di programmma che assegna localmente alla variabile x il valore risultante dal termine M e un corpo N, che può contenere la variabile x.
Semantica operazionale - Exp
la relazione –>
La semantica di exp viene presentata nello stile operazionale, usando la nozione di ambiente.
La semantica operazionale di Exp è una relazione
–> ⊆ Env × Exp × Val.
Un’asserzione di appartenenza (E, M, v) ∈ –> viene chiamata giudizio operazionale e si scrive: E |- M –> v. Questa relazione è definita dal seguente insieme di regole: const, var, plus, let.
Exp
Regole - const
E |- k –> k
Exp
Regole - var
E|- x –> v
(se E(x) = v)
Exp
Regole - plus
Exp
Regole - plus
Quando una variabile si dice libera?
Si dice che una occorrenza di una variabile x è libera in un termine t quando non compare nel corpo N di nessun sottotermine di t della forma let x = M in N.
Ogni occorrenza libera di x in un termine N si dice legata (bound ) alla dichiarazione di x nel termine let x = M in N.
Lo scope di tale dichiarazione è l’insieme delle occorrenze libere di x in N.
Con scope di una variabile si intende la porzione di programma all’interno della quale una variabile può essere riferita.
Cos’è lo scope di una variabile?
Con scope di una variabile si intende la porzione di programma all’interno della quale una variabile può essere riferita.
Per esempio, all’interno di un termine let x=M in N, lo scope della dichiarazione di x è l’insieme delle occorrenze libere di x in N.
due espressioni si dicono alfa-equivalenti?
Due espressioni si dicono alfa-equivalenti se sono identiche a meno di ridenominazione di variabili legate. Ad esempio: l’espressione let x = 1 in x + 1è alfa-equivalente a let y = 1 in y+1
ambiente
Un ambiente è una funzione parziale che associa dei valori a un insieme finito di variabili:
Env = var –fin–> val
L’insieme Val dei “valori”, ovvero l’insieme dei
possibili risultati della valutazione di un termine, coincide con l’insieme delle costanti.
Per esempio, l’ambiente E in cui z vale 3 ed y vale 9 è indicato con {(z,3),(y,9)}.
equivalenza operazionale
Definiamo operazionalmente equivalenti due programmi M ed N tali che, per ogni ambiente E e valore v, E |- M –> v se e solo se E |- N –> v. L’equivalenza operazionale, che indichiamo con
M ∼ N, è chiaramente una relazione di equivalenza tra programmi.
Valutazione Lazy
La valutazione lazy (pigra) è usata in Haskell e in S.
Questa valutazione consiste nel calcolarsi il risultato di un programma solo se quel risultato effettivamente ci serve, e non quindi “a priori”. Ci sono casi in cui effettivamente si risparmia tempo, come ad esempio:
let x = M in 1
M potrebbe essere un espressione molto complicata e potremmo metterci tanto tempo a risolverla, usando un approccio lazy, si risparmierebbe questo tempo dato che x non viene mai utilizzato.
Questa valutazione ci obbliga a cambiare la nozione di ambiente, che ora associa variabili a espressioni e non a valori.
Come cambia l’ambiente (e le regole) con la valutazione lazy
exp
Con la valutazione lazy adattiamo la nozione di ambiente, che ora associa variabili a espressioni e non più a valori.
Env-lazy = Var –fin–> Exp
regole nuove
si risparmia sempre tempo di calcolo con lazy?
No non sempre, perchè lazy ci permette sì di calcolarci un’espressione quando e se ce n’è effettivamente bisogno, ma ci obbliga a ricalcolarla a ogni occorrenza della variabile associata all’espressione.
Per esempio, nella seguente espression con lazy N si calcola 3 volte, con eager 1 sola:
let x = N in (x + x + x)
Esempio termine diverso con scoping statico o dinamico
let x = 2 in (let y = x in (let x = 3 in y + 1))
lazy statico viene 3
lazy dinamico viene 4
Eager e lazy sono equivalenti? (Esempio in cui non lo sono)
No non sono equivalenti, per dare un esempio in cui la valutazione usata cambia il risultato:
let x = 2 in (let y = x in (let x = 3 in y + 1))
Lazy: associamo in Env x a M (che non sappiamo ancora valere 2), poi y a x (importante questo punto, non associamo y al valore di x, ossia 2, ma la generica variabile x), poi associamo x a 3 e eseguiamo il corpo N y+1 nell’ambiente {(x,M),(y,x),(x,M’)} con M–>2 e M’–>3. y è associato a x, andando a cercare nell’ambiente x, troviamo che è associato a M’, che calcolato restituisce il valore 3. y+1 fa quindi 4.
Eager: associamo a x il valore 2, poi alla variabile y il valore di x, ossia 2, poi alla variabile x il valore 3. L’env è {(x,2),(y,2),(x,3)}. il corpo N restituisce il valore 3.
Quindi il risultato cambia quando usiamo variabili non associate a valori costanti, ma associate ad altre variabili, che possono cambiare valore a seconda del punto in cui siamo nel programma (y avrà valore diverso a seconda di quando lo usiamo).
Valutazione Eager
La valutazione Eager (avida) è adottata in SML e LISP. Con eager, al momento della dichiarazione di una variabile x:=M, si associa nell’ambiente x al valore risultante dall’espressione M, che viene valutato subito.
Scoping di un linguaggio
Lo scoping di un linguaggio è quell’insieme di regole che determinano la visibilità di una variabile all’interno di un programma, che consentono cioè di associare una variabile a ciascun riferimento (ovvero uso della variabile mediante un identificatore).
Può essere statico o dinamico.
In modo intuitivo: col dinamico, quando si entra dentro una funzione che utilizza una variabile omonima a una fuori la funzione, le modifiche fatte alla variabile nascono e muiono in quella funzione.
Uno stesso linguaggio può adottare regole di scoping diverse per entità di tipo diverso. In Java, per esempio, il riferimento ad un campo di un oggetto (ovvero la variabile a cui punta il riferimento) viene risolto staticamente, mentre il riferimento ad un metodo viene risolto dinamicamente.
let x = x in x
che risultato produce in sml?
let val x = x in x end;
stdIn:1.14 Error: unbound variable or constructor: x
Scoping statico
Nello scoping statico i riferimenti ad una variabile sono risolti in base alla struttura sintattica del programma.
Può essere effettuata dal compilatore, scegliendo il più recente legame attivo elaborato a tempo di compilazione
Scoping dinamico
Nello scoping dinamico i riferimenti sono risolti in base allo stato di esecuzione del programma, per esempio: una dichiarazione estende il suo effetto fino a che non si incontra un’altra dichiarazione di variabile con lo stesso nome.
Come si modifica l’ambiente con lo scoping statico
exp
L’ambiente con scoping dinamico associa variabili a espressioni M (lazy). Con lo scoping statico associa alla variabile x sia l’espressione M, sia l’ambiente che c’è al momento della dichiarazione di x. Questo rende il valore di M indipendente dal momento in cui si valuta (l’ambiente non cambia, l’abbiamo salvato).
Env-lazy statico = Var –fin–> (Exp × EnvLS).
come si modificano le regole di exp con lazy statico
Fun
breve presentazione
Il linguaggio Fun estende Exp con la nozione di funzione. Dato un termine t con una variabile libera x è possibile costruire, per astrazione su x, la funzione φ che, dato un valore v per x, restituisce il risultato della valutazione di [v/x]t.
In Fun φ si esprime come fn x ⇒ t; in questo termine la variabile x rappresenta il valore d’ingresso della funzione, e prende il nome di parametro
Fun
sintassi
k ::= 5 | 40 | . . .
M ::= k | x | M + N | let x = M in N | fn x ⇒ M | M N
L’operatore di sintassi astratta fn ha segnatura:
fn : Var × Fun → Fun
L’insieme Val dei valori non coincide più con l’insieme delle costanti. è necessario infatti introdurre un nuovo tipo di valore per rappresentare funzioni. Un tale valore, che chiamiamo chiusura, ha la forma (x, M, E), dove x è una variabile, M è un termine ed E è un ambiente, e rappresenta la funzione che mappa un valore v nel risultato della valutazione di M nell’ambiente E {(x, v)}.
Val = {5, 40, . . . } ∪ (Var × Fun × Env)
Fun
regole (eager scoping statico)
fun eager dinamico come cambiano le regole
rispetto a statico
let x = 7 in ((fn y ⇒ (let x = 3 in y 9)) (fn z ⇒ x))
valutarlo con scoping dinamico e statico
Cosa cambia?
La differenza tra i due si vede nell’applicazione della funzione fn=>x (sostituita a y) all’argomento 9. Quindi y9 torna x. A cosa è associato x? nello scoping dinamico a 3, mentre nello statico ci andiamo a salvare l’ambiente di quando abbiamo dichiarato la funzione (fn=>x), in cui x valeva 7.
quindi statico torna 7, dinamico torna 3.
Termine fun che cambia da statico a dinamico
Dare un esempio
let x = 7 in ((fn y ⇒ (let x = 3 in y 9)) (fn z ⇒ x))
Termine fun in cui lazy cambia da eager
dare un esempio
(fn x ⇒ x x) (fn x ⇒ x x)
sml statico o dinamico? lazy o eager? come provarlo?
Sml è eager,statico.
(* sml è statico )
let val x = 3 in ( let val y = x in (let val x = 5 in y end) end) end;
val it = 3 : int
( ricorsione )
fun bomba x = bomba(x-1);
( sml è eager *)
(fn x => 6) (bomba 5);
uncaught exception Overflow [overflow]
C’è differenza tra lazy statico ed eager statico in exp?
No non c’è differenza. La reale differenza tra lazy e eager è una questione di gestione di ambienti:
in lazy si associa a una variabile x un espressione, che si valuterà al momento della valutazione di un termine che contiene x, a differenza di eager che associa a una variabile x un valore, calcolato al momento della dichiarazione di x.
Quindi per rendere lazy equivalente a eager modifichiamo Env: ora associa alla variabile x sia l’espressione M, sia l’ambiente che c’è al momento della dichiarazione di x. Questo rende il valore di M indipendente dal momento in cui si valuta (l’ambiente non cambia, l’abbiamo salvato).
La valutazione Lazy che associa variabili a una coppia espressione-ambiente, si dice che ha scoping statico
Env-lazy statico = Var –fin–> (Exp × EnvLS).
C’è differenza tra lazy statico ed eager statico in fun?
esempio?
Cambia nella derivazione della regola [appl]
E |- MN –> v
con lazy statico non ci calcoliamo subito N, ma lo salviamo nell’ambiente, associandolo all’argomento della funzione.