Az F# nyelv erőforrásanalízise

Az F# nyelv erőforrásanalízise Góbi Attila Eötvös Loránd Tudományegyetem Támogatta a KMOP-1.1.2-08/1-2008-0002 és az Európai Regionális Fejlesztési Alap.

2012. Június 19.

Góbi Attila

(ELTE)

Az F# nyelv erőforrásanalízise

2012. Június 19.

1/1

Áttekintés

Góbi Attila

(ELTE)


2012. Június 19.

2/1

Áttekintés

Outline

Góbi Attila

(ELTE)


2012. Június 19.

3/1

Áttekintés

Áttekintés

Absztrakt és egzakt interpretáció Irreleváns költségek (∼) Intervallum kalkulus Mohó, magasabbrendű nyelven Paraméterezhető Monoton költségek mérése

Góbi Attila

(ELTE)


2012. Június 19.

4/1

Áttekintés

Áttekintés Source code program transformation Core program dependency analysis Function group (component)

driver

abstract interpretation Mathematical equations equations solver Math. formulas

Góbi Attila

(ELTE)


2012. Június 19.

5/1

A Core nyelv

Outline

Góbi Attila

(ELTE)


2012. Június 19.

6/1

A Core nyelv

A Core nyelv Abstract Syntax

program ::= decl∗ decl ::= ident ident∗ ’=’ expr expr ::= expr expr+ literal ident

’let’ ident ’=’ expr ’in’ expr ’case’ expr ’of ’ case+

case ::= pattern ’→’ expr pattern ::= ’_’ ident ident∗ literal

Beágyazott minták nincsenek Csak a legutolsó minta lehet ’_’ A mintaillesztésben az azonosító csak adatkonstruktor lehet Góbi Attila

(ELTE)


2012. Június 19.

7/1

A Core nyelv

Core nyelv Beépített függvények

Egészeken: +int , -int , *int , int , <=int , >=int , ==int , /=int , div, mod Hasonlóan más típusokon Adatkonstruktorok: Nil, Cons, True, False Szintaktikus cukor: Nil ([]) és Cons (:)

Góbi Attila

(ELTE)


2012. Június 19.

8/1

Egzakt kalkulus

Outline

Góbi Attila

(ELTE)


2012. Június 19.

9/1

Egzakt kalkulus

Egzakt kalkulus

R∞= [0, ∞] alaphalmazon [e] az egzakt költség

κ0 , κ1 , κ2 , . . . , π, η, α1 , α2 , ζ 1 , ζ 2 , . . . ∈ [0, ∞[ Irreleváns költség: ∼

Góbi Attila

(ELTE)


2012. Június 19.

10 / 1

Egzakt kalkulus

Szabályok [∼e]=0 [e[v:= ∼e1 ]] = [e[v:= ∼e2 ]] if e1 ∼ e2 [e[v:=f]]=[f]+[e[v:= f]] ha f zárt, és v nem case kifejezésben van Examples [∼42]=0 [1 + ∼(1+1)] = [1 + ∼2] [1 + (2+3)] = [2+3]+[1+ ∼(2+3)] = [1 + ∼5]

Góbi Attila

(ELTE)


2012. Június 19.

11 / 1

Egzakt kalkulus

Adatkonstruktor telített alkalmazása

[C e1 . . . en ] = κn Examples [42] = κ0 [True] = κ0 [[∼1]] = [∼1 : []] = [Cons ∼1 []] = κ2 + κ0

Góbi Attila

(ELTE)


2012. Június 19.

12 / 1

Egzakt kalkulus

Natív függvény hívása

Legyen f függvény, n aritással [f ∼e1 . . . ∼en ] = |f|δ |f| architektúrafüggő |+int | = 1,|==int | = 1,|*int | = 4,|modint | = 16 Example [∼1 + ∼2] = δ [∼1 + ∼2 + ∼3] = 2δ [∼3 * ∼15] = 4δ

Góbi Attila

(ELTE)


2012. Június 19.

13 / 1

Egzakt kalkulus

Case kifejezések Adatkonstruktor [case ∼(C f1 . . . fm ) of p1 → e1 . . . pn → en ] = π + [ei [v1 := ∼f1 , . . . , vm :=∼fm ]] ha pi = C f1 . . . fm az első illeszkedős Wildchar [case ∼e of p1 → e1 . . . pn → en ] = π + [en ] ha pn = _ az első illeszkedés Example [case ∼[] of [] → True; _ → False] = π + [True] = π + κ0

Góbi Attila

(ELTE)


2012. Június 19.

14 / 1

Egzakt kalkulus

Let kifejezések

[let v = ∼e in e‘] = [e’[v:= ∼e]] Example [let x = 1 + 1 in x + x] = [1 + 1] + [let x = ∼(1 + 1) in x + x] = [1 + 1] + [∼(1+1) + ∼(1+1)] = [1 + 1] + [∼2 + ∼2]

Góbi Attila

(ELTE)


2012. Június 19.

15 / 1

Egzakt kalkulus

Telített függvényalkalmazások

[f ∼e1 . . . ∼en ] = αn + [e[v1 := ∼e1 , . . . , vn := ∼en ]] Example [double (1 + 1)] = [1 + 1] + α1 + [∼(1+1) + ∼(1+1)] = 2κ0 + δ + α1 + δ double x = x + x

Góbi Attila

(ELTE)


2012. Június 19.

16 / 1

Egzakt kalkulus

Részleges alkalmazások

n argumentumból closure készítésének költsége: ζn Example [(f ∼1) ∼2] = ζ 1 + α1 , if f has arity 2 [(f ∼1) ∼2] = 2ζ 1 , if f has arity 3 [f ∼1 ∼2] = ζ 2 , if f has arity 3

Góbi Attila

(ELTE)


2012. Június 19.

17 / 1

Kiterjesztett kifejezések

Outline

Góbi Attila

(ELTE)


2012. Június 19.

18 / 1


Tetszőleges kifejezés _τ τ típusú tetszőleges kifejezés |e| = Az e kiterjesztett kifejezéshez tartozó kifejezések halmaza Szemantika |e| = {e} ha e konstruktor, változó vagy függvényszimbólum |_τ | = {∼e | e ∈ az összes τ típusú kifejezés} |∼e| = {∼e’ | e’ ∈ |e|} |case e of p1 → f1 ; . . . ; pn → fn | = {case e’ of p1 → f1 ’; . . . ; pn → fn ’ | e’ ∈ |e|, f1 ’ ∈ |f1 |, . . . , fn ’ ∈ |fn |} |let v = e1 in e2 | = {let v = e1 ’ in e2 ’ | e1 ’ ∈ |e1 |, e2 ’ ∈ |e2 |} |e1 . . . en | = {e1 ’ . . . en ’ | e1 ’ ∈ |e1 |, . . . , en ’ ∈ |en |}

Góbi Attila

(ELTE)


2012. Június 19.

19 / 1


Tetszőleges lista

Listn τ : τ típusú elemekből álló n hosszúságú lista Szemantika |List0 τ | = {∼[]} |Listn+1 τ | = |∼(_τ : Listn τ )|

Góbi Attila

(ELTE)


2012. Június 19.

20 / 1

Költségbecslés

Outline

Góbi Attila

(ELTE)


2012. Június 19.

21 / 1

Költségbecslés

Intervallum aritmetika Nyelvtan kiterjesztését már bemutattuk Most a költség kalkulus kiterjesztése következik Intervallum aritmetika (a, b) = zárt intervallum a és b végpontokkal, ahol a, b ∈ (a, b) + (c, d) = (a+c, b+d)

R∞

n(a, b) = (na, nb) (a, b) ∪ (c, d) = (min a c, max b d) a∈

R∞ beágyazható, mint (a, a)

(a, b) ⊆ (c, d) ⇔ a ≥ c ∧ b ≤ d

Góbi Attila

(ELTE)


2012. Június 19.

22 / 1

Költségbecslés

A költségbecslés szematikája

Kiterjesztett kifejezések [e] = (a, b) ⇔ ∀e’ ∈ |e|: a ≤ [e’] ≤ b és (a, b) a legszűkebb ilyen Nyílt kifejezések [e] = [e[v1 := _τ 1 ] ] ahol v1 az e kifejezés τ 1 típusú szabad változója

Góbi Attila

(ELTE)


2012. Június 19.

23 / 1

Költségbecslés

A költségbecslés szematikája

[e[v:= ∼e1 ]] = [e[v:= ∼e2 ]] if e1 ∼ e2 [case _ of p1 → e1 ; . . . ; pn → en ] = [e1 ] ∪ . . . ∪ [en ] [case ∼List0 of [] → e1 ; v1 :v2 → e2 ] = π + [e1 ] [case ∼Listn+1 of [] → e1 ; v1 :v2 → e2 ] = π + [e2 [v1 := _, v2 := ∼Listn ]] ...

Góbi Attila

(ELTE)


2012. Június 19.

24 / 1

Resource analysis

Góbi Attila

(ELTE)


2012. Június 19.

25 / 1

Az F# nyelv erőforrásanalízise

Recommend Documents