of 48

# POPL 2012 Presentation

Published on: Mar 4, 2016
Published in: Education      Technology

#### Transcripts - POPL 2012 Presentation

• 1. A Type Theory for Probability Density Functions Sooraj Bhat Ashish Agarwal Richard Vuduc Alexander Gray Georgia Institute of Technology New York University POPL 2012 – January 27, 2012Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 1 / 27
• 2. An example probabilistic programvar z ∼ ﬂip (1/2) invar x1 ∼ uniform 1 2 in var x2 ∼ uniform 3 5 in return (if z then x1 else x2)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 2 / 27
• 3. Using a probabilistic programBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 3 / 27
• 4. Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 4 / 27
• 5. Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 5 / 27
• 6. P(A) = 3/4Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 5 / 27
• 7. P(A) = 3/4 how can we compute this?Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 5 / 27
• 8. Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 6 / 27
• 9. P(A) = f (x) dx ABhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 7 / 27
• 10. This is the probability density function (pdf). P(A) = f (x) dx ABhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 7 / 27
• 11. What we want var z ∼ ﬂip (1/2) in var x1 ∼ uniform 1 2 in in: var x2 ∼ uniform 3 5 in return (if z then x1 else x2) f(x) = 1 ≤ x ≤ 2 ∗ (1/2)out: + 3 ≤ x ≤ 5 ∗ (1/4)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 8 / 27
• 12. A pdf may not exist!var z ∼ ﬂip (1/2) invar x1 ∼ uniform 1 2 in var x2 ∼ return 4 in return (if z then x1 else x2)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 9 / 27
• 13. A pdf may not exist!Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 10 / 27
• 14. ContributionsFirst formal syntactic work on pdfs. type system (“P has a pdf”) compiler for calculating pdfsBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 11 / 27
• 15. Abstract syntax base types τ ::= bool | Z | R | τ1 × τ2 expressions ε ::= x | l | op ε1 ...εn | if ε1 then ε2 else ε3Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 12 / 27
• 16. Abstract syntax base types τ ::= bool | Z | R | τ1 × τ2 expressions ε ::= x | l | op ε1 ...εn | if ε1 then ε2 else ε3 types t ::= τ | dist τ distributions e ::= random | return ε | var x ∼ e1 in e2Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 12 / 27
• 17. Abstract syntax base types τ ::= bool | Z | R | τ1 × τ2 expressions ε ::= x | l | op ε1 ...εn | if ε1 then ε2 else ε3 types t ::= τ | dist τ distributions e ::= random | return ε | var x ∼ e1 in e2 programs p ::= pdf eBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 12 / 27
• 18. The power of return+bindThe probability monad [Giry ’82] semantics [Ramsey & Pfeﬀer POPL’03] veriﬁcation [Audebaud & Paulin-Mohring MPC’06] sampling [Park, Pfenning, Thrun POPL’05] EDSLs [Erwig & Kollmansberger JFP’05, Kiselyov & Shan ’09]Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 13 / 27
• 19. The power of return+bind+random ﬂip ε := var u ∼ random in return (u ≤ ε) uniform ε1 ε2 := var u ∼ random in return ((ε2 − ε1) ∗ u + ε1)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 14 / 27
• 20. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 21. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x)“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 22. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x) random λx return (2 ∗ x)“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 23. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” λx return (2 ∗ x) “Has a pdf, for all x?”“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 24. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “Has a pdf, for all x?”“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 25. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “Has a pdf, for all x?” NO“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 26. Type system: the obvious strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “Has a pdf, for all x?” NO“Has a pdf?” NO too conservativeBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 15 / 27
• 27. Type system: reﬁned strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x)“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 16 / 27
• 28. Type system: reﬁned strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “∀N, [[random]]({x | [[return(2∗x)]](N) = 0}) = 0?”“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 16 / 27
• 29. Type system: reﬁned strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “∀N, [[random]]({x | [[return(2∗x)]](N) = 0}) = 0?” YES“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 16 / 27
• 30. Type system: reﬁned strategyvar x ∼ random in return (2 ∗ x) random “Well formed distribution?” YES λx return (2 ∗ x) “∀N, [[random]]({x | [[return(2∗x)]](N) = 0}) = 0?” YES“Has a pdf?” YES too hard to mechanizeBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 16 / 27
• 31. Type system: our strategyAll non-trivial distributions: var x1 ∼ e1 in ... e := var xn ∼ en in return εBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 17 / 27
• 32. Type system: our strategyAll non-trivial distributions: var x1 ∼ e1 in ... e := var xn ∼ en in return εInspect the joint distribution of e1, ..., en the RV transform, λ(x1, ..., xn ) εBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 17 / 27
• 33. Type system: our strategyvar x ∼ random in return (2 ∗ x) random λx 2 ∗ x“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 18 / 27
• 34. Type system: our strategyvar x ∼ random in return (2 ∗ x) random “Has a pdf?” λx 2 ∗ x “Non-nullifying?”“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 18 / 27
• 35. Type system: our strategyvar x ∼ random in return (2 ∗ x) random “Has a pdf?” YES λx 2 ∗ x “Non-nullifying?”“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 18 / 27
• 36. Type system: our strategyvar x ∼ random in return (2 ∗ x) random “Has a pdf?” YES λx 2 ∗ x “Non-nullifying?” YES“Has a pdf?”Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 18 / 27
• 37. Type system: our strategyvar x ∼ random in return (2 ∗ x) random “Has a pdf?” YES λx 2 ∗ x “Non-nullifying?” YES“Has a pdf?” YESBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 18 / 27
• 38. Intuition for nullifying function e := var x ∼ e in return (h x)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 19 / 27
• 39. ContributionsFirst formal syntactic work on pdfs. type system (“P has a pdf”) compiler for calculating pdfsBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 20 / 27
• 40. Compiling pdfs to a usable form 5 usable: λx x + 5, 0 x2 dx not usable: g dP, dP/dLBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 21 / 27
• 41. Compiling pdfs to a usable form 5 usable: λx x + 5, 0 x2 dx not usable: g dP, dP/dL δ ::= ε | λx : τ δ | δ1 δ2 | δBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 21 / 27
• 42. pdf (uniform 3 5)var u ∼ random in return (2∗u+3)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 22 / 27
• 43. pdf (uniform 3 5)var u ∼ random in return (2∗u+3)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 23 / 27
• 44. pdf (uniform 3 5)var u ∼ random in return (2∗u+3)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 24 / 27
• 45. What we get var z ∼ ﬂip (1/2) in var x1 ∼ uniform 1 2 in in: var x2 ∼ uniform 3 5 in return (if z then x1 else x2) f(x) = (1/2) ∗ 1 ≤ x ≤ 2out: + (1/2) ∗ 3 ≤ x ≤ 5 ∗ (1/2)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 25 / 27
• 46. What we get var z ∼ ﬂip (1/2) in var x1 ∼ uniform 1 2 in in: var x2 ∼ uniform 3 5 in return (if z then x1 else x2) f(x) = (1/2) ∗ 1 ≤ x ≤ 2out: + (1/2) ∗ 3 ≤ x ≤ 5 ∗ (1/2)Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 25 / 27
• 47. More in the paper full measure-theoretic details pdfs in spaces besides R multivariate distributions more examplesBhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 26 / 27
• 48. Future workConditional probability. [Borgstram et al. ESOP’11]Implementation in Coq.Bhat et al. (Georgia Tech, NYU) A Type Theory for pdfs POPL 2012 27 / 27