Probabilistic Lambda-calculus and Quantitative Program Analysis